Theory ND_Compl_Truthtable

theory ND_Compl_Truthtable
imports ND_Sound
begin

textβ€ΉThis proof is inspired by Huth and Ryan~citeβ€Ή"huth2004logic"β€Ί.β€Ί
  
definition "turn_true π’œ F ≑ if π’œ ⊨ F then F else (Not F)"
lemma lemma0[simp,intro!]: "π’œ ⊨ turn_true π’œ F" unfolding turn_true_def by simp

lemma turn_true_simps[simp]: 
  "π’œ ⊨ F ⟹ turn_true π’œ F = F"
  "Β¬ π’œ ⊨ F ⟹ turn_true π’œ F = Β¬ F"
unfolding turn_true_def by simp_all
(* often more sensible than to unfold everything *)

definition line_assm :: "'a valuation β‡’ 'a set β‡’ 'a formula set" where
"line_assm π’œ ≑ (`) (Ξ»k. turn_true π’œ (Atom k))"
definition line_suitable :: "'a set β‡’ 'a formula β‡’ bool" where
"line_suitable Z F ≑ (atoms F βŠ† Z)"
lemma line_suitable_junctors[simp]:
  "line_suitable π’œ (Not F) = line_suitable π’œ F"
  "line_suitable π’œ (And F G) = (line_suitable π’œ F ∧ line_suitable π’œ G)"
  "line_suitable π’œ (Or F G) = (line_suitable π’œ F ∧ line_suitable π’œ G)"
  "line_suitable π’œ (Imp F G) = (line_suitable π’œ F ∧ line_suitable π’œ G)"
unfolding line_suitable_def by(clarsimp; linarith)+

lemma line_assm_Cons[simp]: "line_assm π’œ (kβ–Ήks) = (if π’œ k then Atom k else Not (Atom k)) β–Ή line_assm π’œ ks"
unfolding line_assm_def by simp

lemma NotD: "Ξ“ ⊒ Β¬ F ⟹ Fβ–ΉΞ“ ⊒ βŠ₯" by (meson Not2I NotE Weaken subset_insertI)

lemma truthline_ND_proof:
  fixes F :: "'a formula"
  assumes "line_suitable Z F"
  shows "line_assm π’œ Z ⊒ turn_true π’œ F"
using assms proof(induction F)
  case (Atom k) thus ?case using Ax[where 'a='a] by (simp add: line_suitable_def line_assm_def)
next
  case Bot
  have "turn_true π’œ βŠ₯ = Not Bot" unfolding turn_true_def by simp
  thus ?case by (simp add: Ax NotI) (* the theorems from ND/BigFormulas would be useful here. but… nah. *)
next
  have [simp]: "Ξ“ ⊒ Β¬ (Β¬ F) ⟷ Ξ“ ⊒ F" for F :: "'a formula" and Ξ“ by (metis NDtrans Not2E Not2I)
  case (Not F)
  hence "line_assm π’œ Z ⊒ turn_true π’œ F" by simp
  thus ?case by(cases "π’œ ⊨ F"; simp)
next
  have [simp]: "⟦line_assm π’œ Z ⊒ Β¬ F; Β¬ π’œ ⊨ F⟧ ⟹ F ∧ Gβ–Ή line_assm π’œ Z ⊒ βŠ₯" for F G by(blast intro!: NotE[where F=F] intro: AndE1[OF Ax] Weaken[OF _ subset_insertI])
  have [simp]: "⟦line_assm π’œ Z ⊒ Β¬ G; Β¬ π’œ ⊨ G⟧ ⟹ F ∧ Gβ–Ή line_assm π’œ Z ⊒ βŠ₯" for F G by(blast intro!: NotE[where F=G] intro: AndE2[OF Ax] Weaken[OF _ subset_insertI]) 
    (* (meson AndL_sim Not2I NotE Weaken subset_insertI) *)
  case (And F G)
  thus ?case by(cases "π’œ ⊨ F"; cases "π’œ ⊨ G"; simp; intro ND.NotI AndI; simp) 
next
  case (Or F G)
  thus ?case by(cases "π’œ ⊨ F"; cases "π’œ ⊨ G"; simp; (elim ND.OrI1 ND.OrI2)?) (force intro!: NotI dest!: NotD dest: OrL_sim)
next
  case (Imp F G)
  hence mIH: "line_assm π’œ Z ⊒ turn_true π’œ F" "line_assm π’œ Z ⊒ turn_true π’œ G" by simp+
  thus ?case by(cases "π’œ ⊨ F"; cases "π’œ ⊨ G"; simp; intro ImpI NotI ImpL_sim; simp add: Weaken[OF _ subset_insertI] NotSwap NotD NotD[THEN BotE])
qed
thm NotD[THEN BotE]

lemma deconstruct_assm_set:
  assumes IH: "β‹€π’œ. line_assm π’œ (kβ–ΉZ) ⊒ F"
  shows "β‹€π’œ. line_assm π’œ Z ⊒ F"
proof cases
  assume "k ∈ Z" with IH show "?thesis π’œ" for π’œ by (simp add: insert_absorb)
next
  assume "k βˆ‰ Z"
  fix π’œ
  textβ€ΉSince we require the IH for arbitrary @{term π’œ}, we use a modified @{term π’œ} from the conclusion like this:β€Ί
  from IH have av: "line_assm (π’œ(k := v)) (kβ–ΉZ) ⊒ F" for v by blast
  textβ€ΉHowever, that modification is only relevant for @{term "kβ–ΉZ"}, nothing from @{term Z} gets touched.β€Ί
  from β€Ήk βˆ‰ Zβ€Ί have "line_assm (π’œ(k := v)) Z = line_assm π’œ Z" for v unfolding line_assm_def turn_true_def by force
  textβ€ΉThat means we can rewrite the modified @{const line_assm} like this:β€Ί
  hence "line_assm (π’œ(k := v)) (kβ–ΉZ) = 
      (if v then Atom k else Not (Atom k)) β–Ή line_assm π’œ Z" for v by simp
  textβ€ΉInserting @{const True} and @{const False} for β€Ήvβ€Ί yields the two alternatives.β€Ί
  with av have "Atom k β–Ή line_assm π’œ Z ⊒ F" "Not (Atom k) β–Ή line_assm π’œ Z ⊒ F"
    by(metis (full_types))+
  with ND_caseDistinction show "line_assm π’œ Z ⊒ F" .
qed

theorem ND_complete:
  assumes taut: "⊨ F"
  shows "{} ⊒ F"
proof -
  have [simp]: "turn_true Z F = F" for Z using taut by simp
  (* ↑ too fast for you? read ↓ *)
  have "line_assm π’œ {} ⊒ F" for π’œ
  proof(induction arbitrary: π’œ rule: finite_empty_induct)
    show fat: "finite (atoms F)" by (fact atoms_finite)
  next
    have su: "line_suitable (atoms F) F" unfolding line_suitable_def by simp
    with truthline_ND_proof[OF su] show base: "line_assm π’œ (atoms F) ⊒ F" for π’œ by simp
  next
    case (3 k Z)
    from β€Ήk ∈ Zβ€Ί have *: β€Ήk β–Ή Z - {k} = Zβ€Ί by blast
    from β€Ήβ‹€π’œ. line_assm π’œ Z ⊒ Fβ€Ί
    show β€Ήline_assm π’œ (Z - {k}) ⊒ Fβ€Ί
      using deconstruct_assm_set[of k "Z - {k}" F π’œ]
      unfolding * by argo
  qed
  (* could have done that more efficiently…
  have "line_assm π’œ {} ⊒ F" for π’œ
    using deconstruct_assm_set[OF spec[where P="Ξ»π’œ. line_assm π’œ (_ β–Ή _) ⊒ F"]]
    using finite_empty_induct[OF fat, where P="Ξ»Z. βˆ€π’œ. line_assm π’œ Z ⊒ F",
        OF base[THEN allI[where P="Ξ»π’œ. line_assm π’œ (atoms F) ⊒ F"]]]
    by (metis (full_types) insert_Diff_single insert_absorb)*)
  thus ?thesis unfolding line_assm_def by simp
qed

corollary ND_sound_complete: "{} ⊒ F ⟷ ⊨ F"
  using ND_sound[of "{}" F] ND_complete[of F] unfolding entailment_def by blast

end