Theory Compactness_Consistency

theory Compactness_Consistency
imports Consistency
begin
  
theorem "sat S ⟷ fin_sat (S :: 'a :: countable formula set)" (is "?l = ?r")
proof
  assume 0: ?r
  let ?C = "{W :: 'a formula set. fin_sat W}"
  have 1: "S ∈ ?C" using 0 unfolding mem_Collect_eq .
  have 2: "pcp ?C" proof -
    { fix S :: "'a formula set"
      assume "S ∈ ?C"
      hence a: "∀s⊆S. finite s ⟶ (∃𝒜. ∀F∈s. 𝒜 ⊨ F)" by (simp add: fin_sat_def sat_def)
      have conj: "⟦h F G ∈ S; s ⊆ f F ▹ g G ▹ S; finite s;
        ⋀A. A ⊨ h F G ⟹ A ⊨ f F ∧ A ⊨ g G⟧ ⟹ ∃𝒜. ∀F∈s. 𝒜 ⊨ F" 
        for F G s and f g :: "'a formula ⇒ 'a formula" and h :: "'a formula ⇒ 'a formula ⇒ 'a formula"
      proof goal_cases
        case 1
        have "h F G ▹ s - {f F,g G}⊆S" "finite (h F G ▹ s-{f F,g G})" using 1 by auto
        then obtain A where 2: "∀H∈h F G ▹ s-{f F,g G}. A ⊨ H" using a by presburger
        hence "A ⊨ f F" "A ⊨ g G" using 1(4) by simp_all
        with 2 have "∀H∈h F G ▹ s. A ⊨ H" by blast
        thus ?case by blast
      qed
      have disj: "⟦h F G ∈ S; s1 ⊆ f F ▹ S; s2 ⊆ g G ▹ S; finite s1; ∀𝒜. ∃x∈s1. ¬ 𝒜 ⊨ x; finite s2; ∀𝒜. ∃x∈s2. ¬ 𝒜 ⊨ x;
        ⋀A. A ⊨ h F G ⟹ A ⊨ f F ∨ A ⊨ g G⟧ ⟹ False"
        for F G s1 s2 and f g :: "'a formula ⇒ 'a formula" and h :: "'a formula ⇒ 'a formula ⇒ 'a formula" 
      proof goal_cases
        case 1
        let ?U = "h F G ▹ (s1 - {f F}) ∪ (s2 - {g G})"
        have "?U ⊆ S" "finite ?U" using 1 by auto
        with a obtain A where 2: "H ∈ ?U ⟹ A ⊨ H" for H by meson
        with 1(1) 1(8)  have "A ⊨ f F ∨ A ⊨ g G" by force
        hence "(∀H ∈ s1. A ⊨ H) ∨ (∀H ∈ s1. A ⊨ H)" using 1(7) 2
          by (metis DiffI Diff_empty Diff_iff UnCI insert_iff)
        thus ?case using 1 by fast
      qed
      have 1: "⊥ ∉ S" using a by (meson empty_subsetI finite.emptyI finite.insertI formula_semantics.simps(2) insertI1 insert_subset)
      have 2: "Atom k ∈ S ⟶ ❙¬ (Atom k) ∈ S ⟶ False" for k using a[THEN spec[of _ "{Atom k, ❙¬(Atom k)}"]] by auto
      have 3: "F ❙∧ G ∈ S ⟶ F ▹ G ▹ S ∈ Collect fin_sat" for F G unfolding fin_sat_def sat_def mem_Collect_eq using conj[] by fastforce
      have 4: "F ❙∨ G ∈ S ⟶ F ▹ S ∈ Collect fin_sat ∨ G ▹ S ∈ Collect fin_sat" for F G
        unfolding fin_sat_def sat_def mem_Collect_eq using disj[of Or F G _ "λk. k" _ "λk. k"] by (metis formula_semantics.simps(5))
      have 5: "F ❙→ G ∈ S ⟶ ❙¬ F ▹ S ∈ Collect fin_sat ∨ G ▹ S ∈ Collect fin_sat" for F G
        unfolding fin_sat_def sat_def mem_Collect_eq using disj[of Imp F G _ Not _ "λk. k"] by (metis formula_semantics.simps(3,6))
      have 6: "❙¬ (❙¬ F) ∈ S ⟶ F ▹ S ∈ Collect fin_sat" for F unfolding fin_sat_def sat_def mem_Collect_eq using conj[of "λF G. Not (Not F)" F F _ "λk. k" "λk. k"] by simp
      have 7: "❙¬ (F ❙∧ G) ∈ S ⟶ ❙¬ F ▹ S ∈ Collect fin_sat ∨ ❙¬ G ▹ S ∈ Collect fin_sat" for F G
        unfolding fin_sat_def sat_def mem_Collect_eq using disj[of "λF G. Not (And F G)" F G _ Not _ Not] by (metis formula_semantics.simps(3,4))
      have 8: "∀F G. ❙¬ (F ❙∨ G) ∈ S ⟶ ❙¬ F ▹ ❙¬ G ▹ S ∈ Collect fin_sat" unfolding fin_sat_def sat_def mem_Collect_eq using conj[] by fastforce
      have 9: "∀F G. ❙¬ (F ❙→ G) ∈ S ⟶ F ▹ ❙¬ G ▹ S ∈ Collect fin_sat" unfolding fin_sat_def sat_def mem_Collect_eq using conj[] by fastforce
      note 1 2 3 4 5 6 7 8 9
    }
    thus "pcp ?C" unfolding pcp_def by auto
  qed
  from pcp_sat 2 1 show ?l .
next
  assume ?l thus ?r unfolding sat_def fin_sat_def by blast
qed

end