section "Formula"

theory Formula
  imports Base 
begin

subsection "Variables"

datatype vbl = X nat
  ― ‹FIXME there's a lot of stuff about this datatype that is
 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 (metis Suc_inject nextX.simps vbl.exhaust vbl.inject)

lemma inj_nextX: "inj nextX"
  by(auto simp add: inj_on_def)

lemma ind: 
  assumes "P zeroX" "∧ v. P v ==> P (nextX v)"
  shows "P v'"
proof -
  have "P (X n)" for n
    by (induction n) (use assms zeroX_def nextX_def in force)+
  then show ?thesis
    by (metis X_deX)
qed

lemma zeroX_nextX[iff]: "zeroX ≠ nextX a"
  by (metis nat.discI nextX.simps vbl.exhaust vbl.inject zeroX_def)

lemmas nextX_zeroX[iff] = not_sym[OF zeroX_nextX]

lemma nextX: "nextX (X n) = X (Suc n)"
  by simp

lemma vblcase_zeroX[simp]: "vblcase a b zeroX = a" 
  by(simp add: vblcase_def)

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

lemma vbl_cases: "x = zeroX ∨ (∃y. x = nextX y)"
  by (metis X_deX nextX old.nat.exhaust zeroX_def)

lemma vbl_casesE: "[ x = zeroX ==> P; ∧ y. x = nextX y ==> P ] ==> P"
  using vbl_cases by blast

lemma comp_vblcase: "f ∘ vblcase a b = vblcase (f a) (f ∘ b)"
proof
  fix x
  show "(f ∘ vblcase a b) x = (case x of zeroX → f a | nextX x → (f ∘ b) x)"
    using vbl_cases [of x] by auto
qed

lemma equalOn_vblcaseI': "equalOn (preImage nextX A) f g ==> equalOn A (vblcase x f) (vblcase x g)"
  unfolding equalOn_def
  by (metis vbl_casesE vblcase_nextX vblcase_zeroX vimageI2) 
    
lemma equalOn_vblcaseI: "(zeroX ∈ A ==> x=y) ==> equalOn (preImage nextX A) f g ==> equalOn A (vblcase x f) (vblcase y g)"
  by (smt (verit) equalOnD equalOnI equalOn_vblcaseI' vbl_casesE vblcase_nextX)

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

lemma finiteFreshVar: "finite A ==> freshVar A ∉ A"
  unfolding freshVar_def
  by (metis (no_types, lifting) LeastI_ex X_deX finite_imageI
      finite_nat_set_iff_bounded image_eqI order_less_imp_triv
      vbl.inject)

lemma freshVarI: "[finite A; B ⊆ A] ==> freshVar A ∉ B"
  using finiteFreshVar in_mono by blast

lemma freshVarI2: "[finite A; ∧x . x ∉ A ==> P x] ==> P (freshVar A)"
  using finiteFreshVar by presburger

lemmas vblsimps = vblcase_zeroX vblcase_nextX zeroX_nextX
  nextX_zeroX nextX_nextX comp_vblcase


subsection "Predicates"

datatype predicate = Predicate nat

datatype signs = Pos | Neg

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

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 [case_names FAtomP FAtomN FConjP FConjN FAllP FAllN, cases type: formula]: 
  "[∧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"
  by (induct A; rule signs.induct; force)

    ― ‹induction using nat induction, not wellfounded induction›

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

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 ∘ dual P Q R = dual (p ∘ P) (q ∘ Q) (r ∘ R)"
proof
  fix x
  show "(dual p q r ∘ dual P Q R) x = dual (p ∘ P) (q ∘ Q) (r ∘ R) x"
    by (induct x) auto
qed

lemma dualFNot': "dual invSign invSign invSign = FNot"
proof
  fix x
  show "dual invSign invSign invSign x = FNot x"
    by (induct x) auto
qed

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) ∪ (freeVarsF A1)"    
  | freeVarsFAll:  "freeVarsF (FAll z body) = preImage nextX (freeVarsF body)"

definition
  freeVarsFL :: "formula list → vbl set" where
  "freeVarsFL Γ = Union (freeVarsF ` (set Γ))"

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) 

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

lemma freeVarsFL_cons: "freeVarsFL (A#Γ) = freeVarsF A ∪ freeVarsFL Γ"
  by(simp add: freeVarsFL_def)

lemma finite_freeVarsFL[simp]: "finite (freeVarsFL Γ)"
  by(induct Γ) (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: "size (subF theta A) = size (A::formula)"
  by(induct A arbitrary: theta) auto

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

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

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

lemma size_instance: "size (instanceF v A) = size A"
  by (simp add: 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 objectsNonEmpty: "objects M ≠ {}"
  using Rep_model[of M]
  by(simp add: objects_def model_def)

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 φ (FAtom z P vs) = sign z (evalP M P (map φ vs))"
  | evalFConj: "evalF M φ (FConj z A0 A1) = sign z (sign z (evalF M φ A0) ∧ sign z (evalF M φ A1))"
  | evalFAll:  "evalF M φ (FAll z body) =
      sign z (∀x∈objects M. sign z (evalF M (λv . (case v of zeroX → x | nextX v → φ v)) body))"

definition
  valid :: "formula → bool" where
  "valid F ≡ (∀M φ. evalF M φ F = True)"


lemma evalF_FAll: "evalF M φ (FAll Pos A) = (∀x∈objects M. (evalF M (vblcase x φ) A))"
  by simp
  
lemma evalF_FEx: "evalF M φ (FAll Neg A) = (∃x∈objects M. (evalF M (vblcase x φ) A))"
  by simp

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

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

lemma evalF_equiv:  "equalOn (freeVarsF A) f g ==> evalF M f A = evalF M g A"
proof(induction A arbitrary: f g)
  case (FAtom x1 x2 x3)
  then show ?case
    unfolding equalOn_def
    by (metis (mono_tags, lifting) evalFAtom freeVarsFAtom map_eq_conv)
next
  case (FConj x1 A1 A2)
  then show ?case
    by (smt (verit, ccfv_SIG) FConj equalOn_UnD evalFConj freeVarsFConj)
next
  case (FAll x1 A)
  then show ?case
    by (metis (full_types) equalOn_vblcaseI' evalF_FAll evalF_FEx freeVarsFAll
        signs.exhaust)
qed

    ― ‹composition of substitutions›
lemma evalF_subF_eq: "evalF M φ (subF theta A) = evalF M (φ ∘ theta) A"
proof (induction A arbitrary: φ theta)
  case (FAtom x1 x2 x3)
  then show ?case
    by (metis evalFAtom list.map_comp subFAtom)
next
  case (FConj x1 A1 A2)
  then show ?case
    by auto
next
  case (FAll x1 A)
  then have "(vblcase x φ ∘ vblcase zeroX (λv. nextX (theta v))) = (vblcase x (φ ∘ theta))"
    if "x ∈ objects M" for x
    using that 
    apply (clarsimp simp add: o_def fun_eq_iff split: vbl.splits)
    by (metis vbl_cases vblcase_nextX vblcase_zeroX)
  with FAll show ?case
    by (simp add: comp_def)
qed

lemma evalF_instance: "evalF M φ (instanceF u A) = evalF M (vblcase (φ u) φ) A"
  by (metis comp_id comp_vblcase evalF_subF_eq fun.map_ident instanceF_def)

lemma instanceF_E: "instanceF g formula ≠ FAll signs formula"
  by (metis less_irrefl_nat size_instance sizelemmas(3))

end