# Theory Formula

```section "Formula"

theory Formula
imports Base
begin

subsection "Variables"

datatype vbl = X nat
really just a lifting from nat (what else could it be). Makes me
wonder whether things wouldn't be clearer is we just identified vbls
with nats›

primrec deX :: "vbl => nat" where "deX (X n) = n"

lemma X_deX[simp]: "X (deX a) = a"
by(cases a) simp

definition "zeroX = X 0"

primrec
nextX :: "vbl => vbl" where
"nextX (X n) = X (Suc n)"

definition
vblcase :: "['a,vbl => 'a,vbl] => 'a" where
"vblcase a f n = (@z. (n=zeroX ⟶ z=a) ∧ (!x. n=nextX x ⟶ z=f(x)))"

declare [[case_translation vblcase zeroX nextX]]

definition
freshVar :: "vbl set => vbl" where
"freshVar vs = X (LEAST n. n ∉ deX ` vs)"

lemma nextX_nextX[iff]: "nextX x = nextX y = (x =  y)"
by(cases x, cases y) auto

lemma inj_nextX: "inj nextX"

lemma ind': "P zeroX ==> (! v . P v --> P (nextX v)) ==> P v'"
apply (case_tac v', simp)
apply(rename_tac nat)
apply(induct_tac nat)
apply(rename_tac n)
apply (drule_tac x="X n" in spec, simp)
done

lemma ind: "⟦ P zeroX; ⋀ v. P v ⟹ P (nextX v) ⟧ ⟹ P v'"
apply(rule ind') by auto

lemma zeroX_nextX[iff]: "zeroX ~= nextX a" ― ‹FIXME iff?›
apply(case_tac a)
done

lemmas nextX_zeroX[iff] = not_sym[OF zeroX_nextX]

lemma nextX: "nextX (X n) = X (Suc n)"
apply simp done

lemma vblcase_zeroX[simp]: "vblcase a b zeroX = a"

lemma vblcase_nextX[simp]: "vblcase a b (nextX n) = b n"

lemma vbl_cases: "x = zeroX | (? y . x = nextX y)"
apply(case_tac x, rename_tac m)
apply(case_tac m)
apply(rule disjI2)
apply (rule_tac x="X nat" in exI, simp)
done

lemma vbl_casesE: "⟦ x = zeroX ⟹ P; ⋀ y. x = nextX y ⟹ P ⟧ ⟹ P"
apply(auto intro: vbl_cases[elim_format]) done

lemma comp_vblcase: "f o vblcase a b = vblcase (f a) (f o b)"
apply(rule ext)
apply(rule_tac x = x in vbl_casesE)
done

lemma equalOn_vblcaseI': "equalOn (preImage nextX A) f g ==> equalOn A (vblcase x f) (vblcase x g)"
apply(rule+)
apply (case_tac xa rule: vbl_casesE, simp, simp)
apply(drule_tac x=y in bspec)
by assumption

lemma equalOn_vblcaseI: "(zeroX : A --> x=y) ==> equalOn (preImage nextX A) f g ==> equalOn A (vblcase x f) (vblcase y g)"
apply (rule equalOnI, rule)
apply (case_tac xa rule: vbl_casesE, simp, simp)
done

lemma X_deX_connection: "X n : A = (n : (deX ` A))"
by force

lemma finiteFreshVar: "finite A ==> freshVar A ~: A"
apply(rule_tac LeastI_ex)
apply(rule_tac x="(Suc (Max (deX ` A)))" in exI)
apply(rule natset_finite_max)
by force

lemma freshVarI: "[| finite A; B <= A |] ==> freshVar A ~: B"
apply(auto dest!: finiteFreshVar) done

lemma freshVarI2: "finite A ==> !x . x ~: A --> P x ==> P (freshVar A)"
apply(auto dest!: finiteFreshVar) done

lemmas vblsimps = vblcase_zeroX vblcase_nextX zeroX_nextX
nextX_zeroX nextX_nextX comp_vblcase

subsection "Predicates"

datatype predicate = Predicate nat

datatype signs = Pos | Neg

lemma signsE: "⟦ signs = Neg ⟹ P; signs = Pos ⟹ P ⟧ ⟹ P"
apply(cases signs, auto) done

lemma expand_case_signs: "Q(case_signs vpos vneg F) = (
(F = Pos --> Q (vpos)) &
(F = Neg --> Q (vneg))
)"
by(induct F) simp_all

primrec sign :: "signs ⇒ bool ⇒ bool"
where
"sign Pos x = x"
| "sign Neg x = (¬ x)"

lemma sign_arg_cong: "x = y ==> sign z x = sign z y" by simp

primrec invSign :: "signs ⇒ signs"
where
"invSign Pos = Neg"
| "invSign Neg = Pos"

subsection "Formulas"

datatype formula =
FAtom signs predicate "(vbl list)"
| FConj signs formula formula
| FAll  signs formula

subsection "formula signs induct, formula signs cases"

lemma formula_signs_induct: "[|
! p vs. P (FAtom Pos p vs);
! p vs. P (FAtom Neg p vs);
!! A B  . [| P A; P B |] ==> P (FConj Pos A B);
!! A B  . [| P A; P B |] ==> P (FConj Neg A B);
!! A    . [| P A |] ==> P (FAll  Pos A);
!! A    . [| P A |] ==> P (FAll  Neg A)
|]
==> P A"
apply(induct_tac A)
apply(rule signs.induct, force, force)+
done

lemma formula_signs_cases: "!!P.
[| !! p vs . P (FAtom Pos p vs);
!! p vs . P (FAtom Neg p vs);
!! f1 f2  . P (FConj Pos f1 f2);
!! f1 f2  . P (FConj Neg f1 f2);
!! f1    . P (FAll  Pos f1);
!! f1    . P (FAll  Neg f1) |]
==> P A"
apply(induct_tac A)
apply(rule signs.induct, force, force)+
done

― ‹induction using nat induction, not wellfounded induction›
lemma strong_formula_induct': "!A. (! B. size B < size A --> P B) --> P A ==> ! A. size A = n --> P (A::formula)"
by (induct_tac n rule: nat_less_induct, blast)

lemma strong_formula_induct: "(! A. (! B. size B < size A --> P B) --> P A) ==> P (A::formula)"
by (rule strong_formula_induct'[rule_format], blast+)

lemma sizelemmas: "size A < size (FConj z A B)"
"size B < size (FConj z A B)"
"size A < size (FAll  z A)"
by auto

lemma expand_case_formula:
"Q(case_formula fatom fconj fall F) = (
(! z P vs  . F = FAtom z P vs  --> Q (fatom z P vs)) &
(! z A0 A1 . F = FConj z A0 A1 --> Q (fconj z A0 A1)) &
(! z A     . F = FAll  z A     --> Q (fall  z A))
)"
apply(cases F) apply simp_all done

primrec FNot :: "formula => formula"
where
FNot_FAtom: "FNot (FAtom z P vs)  = FAtom (invSign z) P vs"
| FNot_FConj: "FNot (FConj z A0 A1) = FConj (invSign z) (FNot A0) (FNot A1)"
| FNot_FAll:  "FNot (FAll  z body)  = FAll  (invSign z) (FNot body)"

primrec neg  :: "signs => signs"
where
"neg Pos = Neg"
| "neg Neg = Pos"

primrec
dual :: "[(signs => signs),(signs => signs),(signs => signs)] => formula => formula"
where
dual_FAtom: "dual p q r (FAtom z P vs)  = FAtom (p z) P vs"
| dual_FConj: "dual p q r (FConj z A0 A1) = FConj (q z) (dual p q r A0) (dual p q r A1)"
| dual_FAll:  "dual p q r (FAll  z body)  = FAll  (r z) (dual p q r body)"

lemma dualCompose: "dual p q r o dual P Q R = dual (p o P) (q o Q) (r o R)"
apply(rule ext)
apply (induct_tac x, auto)
done

apply(rule ext)
apply(induct_tac x)
apply auto
done

lemma dualFNot: "dual invSign id id (FNot A) = FNot (dual invSign id id A)"
by(induct A) (auto simp: id_def)

lemma dualId: "dual id id id A = A"
by(induct A) (auto simp: id_def)

subsection "Frees"

primrec freeVarsF  :: "formula => vbl set"
where
freeVarsFAtom: "freeVarsF (FAtom z P vs)  = set vs"
| freeVarsFConj: "freeVarsF (FConj z A0 A1) = (freeVarsF A0) Un (freeVarsF A1)"
| freeVarsFAll:  "freeVarsF (FAll  z body)  = preImage nextX (freeVarsF body)"

definition
freeVarsFL :: "formula list => vbl set" where
"freeVarsFL gamma = Union (freeVarsF ` (set gamma))"

lemma freeVarsF_FNot[simp]: "freeVarsF (FNot A) = freeVarsF A"
by(induct A) auto

lemma finite_freeVarsF[simp]: "finite (freeVarsF A)"
by(induct A) (auto simp add: inj_nextX finite_preImage)

lemma freeVarsFL_nil[simp]: "freeVarsFL ([]) = {}"

lemma freeVarsFL_cons: "freeVarsFL (A#Gamma) = freeVarsF A ∪ freeVarsFL Gamma"
― ‹FIXME not simp, since simp stops some later lemmas because the simpset isn't confluent›

lemma finite_freeVarsFL[simp]: "finite (freeVarsFL gamma)"
by(induct gamma) (auto simp: freeVarsFL_cons)

lemma freeVarsDual: "freeVarsF (dual p q r A) = freeVarsF A"
by(induct A) auto

subsection "Substitutions"

primrec subF :: "[vbl => vbl,formula] => formula"
where
subFAtom: "subF theta (FAtom z P vs)  = FAtom z P (map theta vs)"
| subFConj: "subF theta (FConj z A0 A1) = FConj z (subF theta A0) (subF theta A1)"
| subFAll: "subF theta (FAll z body)  =
FAll  z (subF (% v . (case v of zeroX => zeroX | nextX v => nextX (theta v))) body)"

lemma size_subF: "!!theta. size (subF theta A) = size (A::formula)"
by(induct A) auto

lemma subFNot: "!!theta. subF theta (FNot A) = FNot (subF theta A)"
by(induct A) auto

lemma subFDual: "!!theta. subF theta (dual p q r A) = dual p q r (subF theta A)"
by(induct A) auto

definition
instanceF :: "[vbl,formula] => formula" where
"instanceF w body = subF (%v. case v of zeroX => w | nextX v => v) body"

lemma size_instance: "!!v. size (instanceF v A) = size (A::formula)"
by(induct A) (auto simp: instanceF_def size_subF)

lemma instanceFDual: "instanceF u (dual p q r A) = dual p q r (instanceF u A)"
by(induct A) (simp_all add: instanceF_def subFDual)

subsection "Models"

typedecl
object

axiomatization obj :: "nat => object"
where inj_obj: "inj obj"

subsection "model, non empty set and positive atom valuation"

definition "model = {z :: (object set * ([predicate,object list] => bool)). (fst z ~= {})}"

typedef model = model
unfolding model_def by auto

definition
objects :: "model => object set" where
"objects M = fst (Rep_model M)"

definition
evalP :: "model => predicate => object list => bool" where
"evalP M = snd (Rep_model M)"

lemma evalP_arg2_cong: "x = y ==> evalP M p x = evalP M p y" by simp

lemma objectsNonEmpty: "objects M ≠ {}"
using Rep_model[of M]

lemma modelsNonEmptyI: "fst (Rep_model M) ≠ {}"
using Rep_model[of M] by(simp add: objects_def model_def)

subsection "Validity"

primrec evalF :: "[model,vbl => object,formula] => bool"
where
evalFAtom: "evalF M phi (FAtom z P vs)  = sign z (evalP M P (map phi vs))"
| evalFConj: "evalF M phi (FConj z A0 A1) = sign z (sign z (evalF M phi A0) & sign z (evalF M phi A1))"
| evalFAll:  "evalF M phi (FAll  z body)  = sign z (!x: (objects M).
sign z
(evalF M (%v . (case v of
zeroX   => x
| nextX v => phi v)) body))"

definition
valid :: "formula => bool" where
"valid F ⟷ (∀M phi. evalF M phi F = True)"

lemma evalF_FAll: "evalF M phi (FAll Pos A) = (!x: (objects M). (evalF M (vblcase x (%v .phi v)) A))"
by simp

lemma evalF_FEx: "evalF M phi (FAll Neg A) = ( ? x:(objects M). (evalF M (vblcase x (%v. phi v)) A))"
by simp

lemma evalF_arg2_cong: "x = y ==> evalF M p x = evalF M p y" by simp

lemma evalF_FNot: "!!phi. evalF M phi (FNot A) = (¬ evalF M phi A)"
by(induct A rule: formula_signs_induct) simp_all

lemma evalF_equiv[rule_format]: "! f g. (equalOn (freeVarsF A) f g) ⟶ (evalF M f A = evalF M g A)"
apply(induct A)
apply (force simp:equalOn_def cong: map_cong, clarify) apply simp apply(drule_tac equalOn_UnD) apply force
apply clarify apply simp apply(rename_tac signs A f g) apply(rule_tac f = "sign signs" in arg_cong) apply(rule ball_cong) apply rule
apply(rule_tac f = "sign signs" in arg_cong) apply(force intro: equalOn_vblcaseI')
done
― ‹FIXME tricky to automate cong args convincingly?›

― ‹composition of substitutions›
lemma evalF_subF_eq: "!phi theta. evalF M phi (subF theta A) = evalF M (phi o theta) A"
apply(induct_tac A)
apply(simp del: o_apply)
apply(simp del: o_apply)
apply(intro allI)
apply(simp del: o_apply)
apply(rename_tac signs phi0 phi theta)
apply(rule_tac f="sign signs" in arg_cong)
apply(rule ball_cong) apply rule
apply(rule_tac f="sign signs" in arg_cong)
apply(subgoal_tac "(vblcase x phi ∘ vblcase zeroX (λv. nextX (theta v))) = (vblcase x (phi ∘ theta))")
apply(simp del: o_apply)
apply(rule ext)
apply (case_tac xa rule: vbl_casesE, simp, simp)
done

lemma o_id'[simp]: "f o (% x. x) = f"
by (fold id_def, simp)

lemma evalF_instance: "evalF M phi (instanceF u A) = evalF M (vblcase (phi u) phi) A"
done

― ‹FIXME move›

lemma s[simp]:" FConj signs formula1 formula2 ≠ formula1"
apply(induct_tac formula1, auto) done

lemma s'[simp]:" FConj signs formula1 formula2 ≠ formula2"
apply(induct formula2, auto) done

lemma instanceF_E: "instanceF g formula ≠ FAll signs formula"
apply clarify
apply(subgoal_tac "Suc (size (instanceF g formula)) = (size (FAll signs formula))")
apply force
apply(simp (no_asm) only: size_instance[rule_format])
apply simp done

end
```