Theory MaximalSet

(* 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 MaximalSet
imports FinitenessClosedCharProp 
begin
(*>*)

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


primrec sucP :: "'b formula set ⇒ 'b formula set set ⇒ (nat ⇒ 'b formula) ⇒ nat ⇒ 'b formula set"
where
  "sucP S 𝒞 f 0 = S"
| "sucP S 𝒞 f (Suc n) =
    (if sucP S 𝒞 f n ∪ {f n} ∈ 𝒞    
     then sucP S 𝒞 f n ∪ {f n}
     else sucP S 𝒞 f n)" 


definition MsucP :: "'b formula set ⇒ 'b formula set set ⇒ (nat ⇒ 'b formula) ⇒ 'b formula set" 
where 
"MsucP S 𝒞 f = (⋃n. sucP S 𝒞 f n)"



(*<*)

(*>*)


theorem Max_subsetuntoP: "S ⊆ MsucP S 𝒞 f"
(*<*)
proof (rule subsetI)
  fix x
  assume "x ∈ S"
  hence "x ∈ sucP S 𝒞 f 0" by simp
  hence  "∃n. x ∈ sucP S 𝒞 f n" by (rule exI)
  thus "x ∈ MsucP S 𝒞 f" by (simp add: MsucP_def)
qed 
(*>*)


definition chain :: "(nat ⇒ 'a set) ⇒ bool" where
  "chain S = (∀n. S n ⊆ S (Suc n))"


(*<*)

(*>*)

(*<*) 
lemma chainD:
  assumes "chain S" and "x ∈ S m"
  shows "x ∈ S (m + n)"
proof -
  show ?thesis using assms by (induct n)(auto simp add: chain_def)  
qed

lemma chainD':
  assumes hip1: "chain S" and hip2: "x ∈ S m" and hip3: "m ≤ k"
  shows "x ∈ S k"
proof -
  have "∃n. k = m + n" using hip3 by arith
  then obtain n where n: "k = m + n" by (rule exE) 
  moreover
  have "x ∈ S (m + n)" using hip1 hip2 by (rule chainD)  
  thus ?thesis using n by simp
qed

lemma chain_index:
  assumes ch: "chain S" and fin: "finite F"
  shows "F ⊆ (⋃n. S n) ⟹ ∃n. F ⊆ S n" using fin
proof (induct rule: finite_induct)
  assume "{} ⊆ (⋃n. S n)"
  show "∃n.{} ⊆ S n"  by simp
  next
    fix x F
    assume 
      h1: "finite F" 
      and h2: "x ∉ F" 
      and h3: "F ⊆ (⋃n. S n)⟹ ∃n. F ⊆ S n" 
      and h4: "insert x F ⊆ (⋃n. S n)"
  show "∃n. insert x F ⊆ S n"
  proof -
    have "∃m. x ∈ S m" using h4 by simp
    then obtain m where m: "x ∈ S m" by (rule exE)
    have "F ⊆ (⋃n. S n)" using h4 by simp
    hence  "∃n. F ⊆ S n" using h3 by simp
    then obtain n where n: "F ⊆ S n" by (rule exE)
    have "m ≤ (max m n)"  by (simp add: max_def)      
    with ch m  have 1: "x ∈ S (max m n)" by (rule chainD')   
    have 2:  "F ⊆ S (max m n)" 
    proof (rule subsetI)
      fix y
      assume "y ∈ F"
      hence "y ∈ S n" using n by blast
      moreover
      have "n ≤ (max m n)" by simp
      ultimately
      show "y ∈ S (max m n)"  by (rule chainD'[OF ch _ _])
    qed 
    have "insert x F  ⊆ S (max m n)" using 1 2 by simp
    thus ?thesis by (rule exI)
  qed
qed
(*>*)


theorem chain_union_closed:
  assumes hip1: "finite_character 𝒞" 
  and hip2:"chain S" 
  and hip3: "∀n. S n ∈ 𝒞"
  shows "(⋃n. S n) ∈ 𝒞"
(*<*)
proof -
  have "∀S. (S ∈ 𝒞) = (∀T. finite T ⟶ T ⊆ S ⟶ T ∈ 𝒞)" 
  using hip1 by (unfold finite_character_def)
  hence 1: "(⋃n. S n) ∈ 𝒞 = (∀T. finite T ⟶ T ⊆ (⋃n. S n) ⟶ T ∈ 𝒞)" 
  by (rule allE)
  thus "(⋃n. S n) ∈ 𝒞"
  proof -
    have "(∀T. finite T ⟶ T ⊆ (⋃n. S n) ⟶ T ∈ 𝒞)"
    proof (rule allI impI)+
      fix T
      assume h1: "finite T" and h2: "T ⊆ (⋃n. S n)"
      have "∃n. T ⊆ S n" using hip2 h1 h2 by (rule chain_index)
      moreover  
      have "subset_closed 𝒞" using hip1 by (rule finite_character_closed)
      hence "∀S∈𝒞. ∀S'⊆S. S' ∈ 𝒞"  by (unfold subset_closed_def)
      ultimately
      show "T ∈ 𝒞" using hip3 by auto   
    qed         
    thus "(⋃n. S n) ∈ 𝒞" using 1 by simp
  qed
qed    
(*>*)


(*>*)

lemma chain_suc: "chain (sucP S 𝒞 f)"
by (simp add: chain_def) blast


theorem MaxP_in_C:
  assumes hip1: "finite_character 𝒞" and hip2: "S ∈ 𝒞" 
  shows  "MsucP S 𝒞 f ∈ 𝒞"
proof (unfold MsucP_def) 
  have "chain (sucP S 𝒞 f)" by (rule chain_suc)
  moreover
  have "∀n. sucP S 𝒞 f n ∈ 𝒞"
  proof (rule allI)
    fix n
    show "sucP S 𝒞 f n ∈ 𝒞" using hip2 
      by (induct n)(auto simp add: sucP_def)
  qed   
  ultimately  
  show "(⋃ n. sucP S 𝒞 f n) ∈ 𝒞" by (rule chain_union_closed[OF hip1]) 
qed 


definition enumeration :: "(nat ⇒'b) ⇒ bool" where
  "enumeration f = (∀y.∃n. y = (f n))"


lemma enum_nat: "∃g. enumeration (g:: nat ⇒ nat)"
proof -
  have "∀y. ∃ n. y = (λn. n) n" by simp
  hence "enumeration (λn. n)" by (unfold enumeration_def)
  thus ?thesis by auto
qed


theorem suc_maximalP: 
  assumes hip1: "enumeration f" and hip2: "subset_closed 𝒞"  
  shows "maximal (MsucP S 𝒞 f) 𝒞"
proof -  (* (simp add: maximal_def MsucP_def) *)
  have "∀S'∈𝒞. (⋃x. sucP S 𝒞 f x) ⊆ S' ⟶ (⋃x. sucP S 𝒞 f x) = S'"
  proof (rule ballI impI)+
    fix S'
    assume h1: "S' ∈ 𝒞" and h2: "(⋃x. sucP S 𝒞 f x) ⊆ S'"
    show "(⋃x. sucP S 𝒞 f x) = S'"    
    proof (rule ccontr)
      assume "(⋃x. sucP S 𝒞 f x) ≠ S'"
      hence  "∃z. z ∈ S' ∧ z ∉ (⋃x. sucP S 𝒞 f x)" using h2 by blast
      then obtain z where z: "z ∈ S' ∧ z ∉ (⋃x. sucP S 𝒞 f x)" by (rule exE)
      have "∃n. z = f n" using hip1 h1 by (unfold enumeration_def) simp 
      then obtain n where n: "z = f n" by (rule exE) 
      have "sucP S 𝒞 f n ∪ {f n} ⊆ S'"
      proof - 
        have "f n ∈ S'" using z n  by simp
        moreover        
        have "sucP S 𝒞 f n ⊆ (⋃x. sucP S 𝒞 f x)" by auto 
        ultimately 
        show ?thesis using h2 by simp
      qed      
      hence "sucP S 𝒞 f n ∪ {f n} ∈ 𝒞" 
        using h1 hip2 by (unfold subset_closed_def) simp
      hence "f n ∈ sucP S 𝒞 f (Suc n)" by simp      
      moreover
      have "∀x. f n ∉ sucP S 𝒞 f x" using z n by simp
      ultimately show False
        by blast
    qed
  qed
  thus ?thesis
    by  (simp add: maximal_def MsucP_def) 
qed

corollary ConsistentExtensionP:
  assumes hip1: "finite_character 𝒞" 
  and hip2: "S ∈ 𝒞" 
  and hip3:  "enumeration f" 
  shows "S ⊆ MsucP S 𝒞 f" 
  and "MsucP S 𝒞 f ∈ 𝒞" 
  and "maximal (MsucP S 𝒞 f) 𝒞"
proof -
  show "S ⊆ MsucP S 𝒞 f" using Max_subsetuntoP by auto
next
  show "MsucP S 𝒞 f ∈ 𝒞" using  MaxP_in_C[OF hip1 hip2] by simp
next
  show "maximal (MsucP S 𝒞 f) 𝒞" 
    using finite_character_closed[OF hip1] and hip3 suc_maximalP
    by auto
qed

(*<*)
end
(*>*)