Theory Closedness

(* Model Existence Theorem *)

(* Formalization adapted from: 
   Fabián Fernando Serrano Suárez, "Formalización en Isar de la
   Meta-Lógica de Primer Orden." PhD thesis, 
   Departamento de Ciencias de la Computación e Inteligencia Artificial,
   Universidad de Sevilla, Spain, 2012.
   https://idus.us.es/handle/11441/57780.  In Spanish  *)

(*<*)
theory Closedness
imports SyntaxAndSemantics UniformNotation
begin
(*>*)


definition consistenceP :: "'b formula set set ⇒ bool" where
  "consistenceP 𝒞 = 
     (∀S. S ∈ 𝒞 ⟶ (∀P. ¬ (atom P ∈ S ∧ (¬.atom P) ∈ S)) ∧
     FF ∉ S ∧ (¬.TT) ∉ S ∧
     (∀F. (¬.¬.F) ∈ S ⟶ S ∪ {F} ∈  𝒞) ∧
     (∀F. ((FormulaAlfa F) ∧ F∈S) ⟶ (S∪{Comp1 F, Comp2 F}) ∈ 𝒞) ∧
     (∀F. ((FormulaBeta F) ∧ F∈S) ⟶ (S∪{Comp1 F}∈𝒞) ∨ (S∪{Comp2 F}∈𝒞)))"     


definition subset_closed :: "'a set set ⇒ bool" where
  "subset_closed 𝒞 = (∀S ∈ 𝒞. ∀S'. S' ⊆ S ⟶ S' ∈ 𝒞)"


definition closure_subset :: "'a set set ⇒ 'a set set" ("_⁺"[1000] 1000) where
  "𝒞⁺ = {S. ∃S' ∈ 𝒞. S ⊆ S'}"


lemma closed_subset: "𝒞 ⊆ 𝒞⁺"
proof -
  { fix S
    assume "S ∈ 𝒞" 
    moreover 
    have "S ⊆ S" by simp
    ultimately
    have "S ∈ 𝒞⁺"
      by (unfold closure_subset_def, auto) }
  thus ?thesis by auto
qed 


lemma closed_closed: "subset_closed (𝒞⁺)"
proof -
 { fix S T
   assume "S ∈ 𝒞⁺" and "T ⊆ S"
   obtain S1 where "S1 ∈ 𝒞" and "S ⊆ S1" using `S ∈ 𝒞⁺` 
     by (unfold closure_subset_def, auto)
   have "T ⊆ S1" using `T ⊆ S` and `S ⊆ S1`  by simp
   hence "T ∈ 𝒞⁺" using `S1 ∈ 𝒞` 
     by (unfold closure_subset_def, auto)}
 thus ?thesis by (unfold subset_closed_def, auto) 
qed 

lemma cond_consistP1:
  assumes "consistenceP 𝒞" and "T ∈ 𝒞" and "S ⊆ T"  
  shows "(∀P. ¬(atom P ∈ S ∧ (¬.atom P) ∈ S))"
(*<*) 
proof (rule allI)+  
  fix P 
  show "¬(atom P  ∈ S ∧ (¬.atom P) ∈ S)"
  proof -
    have "¬(atom P ∈ T ∧ (¬.atom P) ∈ T)" 
      using `consistenceP 𝒞` and `T ∈ 𝒞`
      by(simp add: consistenceP_def)
    thus "¬(atom P ∈ S ∧ (¬.atom P) ∈ S)" using `S ⊆ T` by auto
  qed
qed 
(*>*)

lemma cond_consistP2:
  assumes "consistenceP 𝒞" and "T ∈ 𝒞" and "S ⊆ T"   
  shows "FF ∉ S ∧ (¬.TT)∉ S"
(*<*)
proof -
  have "FF ∉ T ∧ (¬.TT)∉ T" 
    using `consistenceP 𝒞` and `T ∈ 𝒞` 
    by(simp add: consistenceP_def)
  thus "FF ∉ S ∧ (¬.TT)∉ S" using `S ⊆ T` by auto
qed
(*>*)

lemma cond_consistP3:
  assumes "consistenceP 𝒞" and "T ∈ 𝒞" and "S ⊆ T"   
  shows "∀F. (¬.¬.F) ∈ S ⟶ S ∪ {F} ∈ 𝒞⁺"
proof(rule allI) 
(*<*)       
  fix F
  show "(¬.¬.F) ∈ S ⟶  S ∪ {F} ∈ 𝒞⁺"
  proof (rule impI)
    assume "(¬.¬.F) ∈ S"
    hence "(¬.¬.F) ∈ T" using `S ⊆ T` by auto   
    hence "T ∪ {F} ∈ 𝒞" using `consistenceP 𝒞` and `T ∈ 𝒞` 
      by(simp add: consistenceP_def)
    moreover 
    have "S ∪ {F} ⊆  T ∪ {F}" using `S ⊆ T` by auto
    ultimately   
    show "S ∪ {F} ∈ 𝒞⁺"
      by (auto simp add: closure_subset_def)
  qed
qed
(*>*)

lemma cond_consistP4:
  assumes "consistenceP 𝒞" and "T ∈ 𝒞" and "S ⊆ T" 
  shows "∀F. ((FormulaAlfa F) ∧ F ∈ S) ⟶ (S ∪ {Comp1 F, Comp2 F}) ∈ 𝒞⁺"
(*<*)
proof (rule allI) 
  fix F 
  show "((FormulaAlfa F) ∧ F ∈ S) ⟶ S ∪ {Comp1 F, Comp2 F} ∈ 𝒞⁺"
  proof (rule impI)
    assume "((FormulaAlfa F) ∧ F ∈ S)"
    hence "FormulaAlfa F" and  "F ∈ T" using `S ⊆ T` by auto 
    hence  "T ∪ {Comp1 F, Comp2 F} ∈ 𝒞" 
      using `consistenceP 𝒞` and `FormulaAlfa F` and `T ∈ 𝒞` 
      by (auto simp add: consistenceP_def)
    moreover
    have "S ∪ {Comp1 F, Comp2 F} ⊆ T ∪ {Comp1 F, Comp2 F}" 
      using `S ⊆ T` by auto
    ultimately
    show  "S ∪ {Comp1 F, Comp2 F} ∈ 𝒞⁺" 
      by (auto simp add: closure_subset_def)
  qed
qed
(*>*)
text‹ ›
lemma cond_consistP5:
  assumes "consistenceP 𝒞" and "T ∈ 𝒞" and "S ⊆ T" 
  shows "(∀F. ((FormulaBeta F) ∧ F ∈ S) ⟶ 
              (S ∪ {Comp1 F} ∈ 𝒞⁺) ∨ (S ∪ {Comp2 F} ∈ 𝒞⁺))" 
(*<*)
proof (rule allI) 
  fix F 
  show "((FormulaBeta F) ∧ F ∈ S) ⟶ S ∪ {Comp1 F} ∈ 𝒞⁺ ∨ S ∪ {Comp2 F} ∈ 𝒞⁺" 
  proof (rule impI)
    assume "(FormulaBeta F) ∧ F ∈ S"
    hence "FormulaBeta F" and "F ∈ T" using `S ⊆ T` by auto 
    hence "T ∪ {Comp1 F} ∈ 𝒞 ∨ T ∪ {Comp2 F} ∈ 𝒞" 
      using `consistenceP 𝒞` and `FormulaBeta F` and `T ∈ 𝒞` 
      by(simp add: consistenceP_def)
    moreover
    have "S ∪ {Comp1 F} ⊆ T ∪ {Comp1 F}" and "S ∪ {Comp2 F} ⊆ T ∪ {Comp2 F}" 
      using `S ⊆ T` by auto
    ultimately
    show "S ∪ {Comp1 F} ∈ 𝒞⁺ ∨ S ∪ {Comp2 F} ∈ 𝒞⁺"
      by(auto simp add: closure_subset_def)
  qed
qed
(*>*)

theorem closed_consistenceP:
  assumes hip1: "consistenceP 𝒞"
  shows "consistenceP (𝒞⁺)"
proof -
  { fix S
    assume "S ∈ 𝒞⁺" 
    hence "∃T∈𝒞. S ⊆ T" by(simp add: closure_subset_def)
    then obtain T where hip2: "T ∈ 𝒞" and hip3: "S ⊆ T" by auto
    have "(∀P. ¬ (atom P ∈ S ∧ (¬.atom P) ∈ S)) ∧
               FF ∉ S ∧ (¬.TT) ∉ S ∧
               (∀F. (¬.¬.F) ∈ S ⟶ S ∪ {F} ∈ 𝒞⁺) ∧
               (∀F. ((FormulaAlfa F) ∧ F ∈ S) ⟶ 
                    (S ∪ {Comp1 F, Comp2 F}) ∈ 𝒞⁺) ∧
               (∀F. ((FormulaBeta F) ∧ F ∈ S) ⟶ 
                    (S ∪ {Comp1 F} ∈ 𝒞⁺) ∨ (S ∪ {Comp2 F} ∈ 𝒞⁺))"
      using 
        cond_consistP1[OF hip1 hip2 hip3]  cond_consistP2[OF hip1 hip2 hip3]
        cond_consistP3[OF hip1 hip2 hip3]  cond_consistP4[OF hip1 hip2 hip3]
        cond_consistP5[OF hip1 hip2 hip3] 
      by blast}
  thus ?thesis by (simp add: consistenceP_def)
qed

(*<*)
end
(*>*)