Theory Maximal_Consistent_Sets

(*
  File:      Maximal_Consistent_Sets.thy
  Author:    Asta Halkjær From

  Maximal Consistent Sets based on the transfinite Lindenbaum construction in the textbook
  "Model Theory" by Chang and Keisler (Elsevier Science Publishers 1990)
*)

theory Maximal_Consistent_Sets imports "HOL-Cardinals.Cardinal_Order_Relation" begin

context wo_rel begin

lemma underS_bound: ‹a ∈ underS n ⟹ b ∈ underS n ⟹ a ∈ under b ∨ b ∈ under a›
  by (meson BNF_Least_Fixpoint.underS_Field REFL Refl_under_in in_mono under_ofilter ofilter_linord)

lemma finite_underS_bound:
  assumes ‹finite X› ‹X ⊆ underS n› ‹X ≠ {}›
  shows ‹∃a ∈ X. ∀b ∈ X. b ∈ under a›
  using assms
proof (induct X rule: finite_induct)
  case (insert x F)
  then show ?case
  proof (cases ‹F = {}›)
    case True
    then show ?thesis
      using insert underS_bound by fast
  next
    case False
    then show ?thesis
    using insert underS_bound by (metis TRANS insert_absorb insert_iff insert_subset under_trans)
  qed
qed simp

lemma finite_bound_under:
  assumes ‹finite p› ‹p ⊆ (⋃n ∈ Field r. f n)›
  shows ‹∃m. p ⊆ (⋃n ∈ under m. f n)›
    using assms
proof (induct rule: finite_induct)
  case (insert x p)
  then obtain m where ‹p ⊆ (⋃n ∈ under m. f n)›
    by fast
  moreover obtain m' where ‹x ∈ f m'› ‹m' ∈ Field r›
    using insert(4) by blast
  then have ‹x ∈ (⋃n ∈ under m'. f n)›
    using REFL Refl_under_in by fast
  ultimately have ‹{x} ∪ p ⊆ (⋃n ∈ under m. f n) ∪ (⋃n ∈ under m'. f n)›
    by fast
  then show ?case
    by (metis SUP_union Un_commute insert_is_Un sup.absorb_iff2 ofilter_linord under_ofilter)
qed simp

end

locale MCS_Lim_Ord =
  fixes r :: ‹'a rel›
  assumes WELL: ‹Well_order r›
    and isLimOrd_r: ‹isLimOrd r›
  fixes consistent :: ‹'a set ⇒ bool›
  assumes consistent_hereditary: ‹consistent S ⟹ S' ⊆ S ⟹ consistent S'›
    and inconsistent_finite: ‹⋀S. ¬ consistent S ⟹ ∃S' ⊆ S. finite S' ∧ ¬ consistent S'›
begin

definition extendS :: ‹'a set ⇒ 'a ⇒ 'a set ⇒ 'a set› where
  ‹extendS S n prev ≡ if consistent ({n} ∪ prev) then {n} ∪ prev else prev›

definition extendL :: ‹('a ⇒ 'a set) ⇒ 'a ⇒ 'a set› where
  ‹extendL rec n ≡ ⋃m ∈ underS r n. rec m›

definition extend :: ‹'a set ⇒ 'a ⇒ 'a set› where
  ‹extend S n ≡ worecZSL r S (extendS S) extendL n›

lemma wo_rel_r: ‹wo_rel r›
  by (simp add: WELL wo_rel.intro)

lemma adm_woL_extendL: ‹adm_woL r extendL›
  unfolding extendL_def wo_rel.adm_woL_def[OF wo_rel_r] by blast

definition Extend :: ‹'a set ⇒ 'a set› where
  ‹Extend S ≡ ⋃n ∈ Field r. extend S n›


lemma extend_subset: ‹n ∈ Field r ⟹ S ⊆ extend S n›
proof (induct n rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
  case 1
  then show ?case
    unfolding extend_def wo_rel.worecZSL_zero[OF wo_rel_r adm_woL_extendL]
    by simp
next
  case (2 i)
  moreover from this have ‹i ∈ Field r›
    by (meson FieldI1 wo_rel.succ_in wo_rel_r)
  ultimately show ?case
    unfolding extend_def extendS_def
      wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)] by auto
next
  case (3 i)
  then show ?case
    unfolding extend_def extendL_def
      wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
    using wo_rel_r by (metis SUP_upper2 emptyE underS_I wo_rel.zero_in_Field wo_rel.zero_smallest)
qed

lemma Extend_subset': ‹Field r ≠ {} ⟹ S ⊆ Extend S›
  unfolding Extend_def using extend_subset by fast

lemma extend_underS: ‹m ∈ underS r n ⟹ extend S m ⊆ extend S n›
proof (induct n rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
  case 1
  then show ?case
    unfolding extend_def using wo_rel_r by (simp add: wo_rel.underS_zero)
next
  case (2 i)
  moreover from this have ‹m = i ∨ m ∈ underS r i›
    by (metis wo_rel.less_succ underS_E underS_I wo_rel_r)
  ultimately show ?case
    unfolding extend_def extendS_def
      wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)]
    by auto
next
  case (3 i)
  then show ?case
    unfolding extend_def extendL_def
      wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
    by blast
qed

lemma extend_under: ‹m ∈ under r n ⟹ extend S m ⊆ extend S n›
  using extend_underS wo_rel_r
  by (metis empty_iff in_Above_under set_eq_subset wo_rel.supr_greater wo_rel.supr_under underS_I
      under_Field under_empty)

lemma consistent_extend:
  assumes ‹consistent S›
  shows ‹consistent (extend S n)›
  using assms
proof (induct n rule: wo_rel.well_order_inductZSL[OF wo_rel_r])
  case 1
  then show ?case
    unfolding extend_def wo_rel.worecZSL_zero[OF wo_rel_r adm_woL_extendL] .
next
  case (2 i)
  then show ?case
    unfolding extend_def extendS_def
      wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)]
    by auto
next
  case (3 i)
  show ?case
  proof (rule ccontr)
    assume ‹¬ consistent (extend S i)›
    then obtain S' where S': ‹finite S'› ‹S' ⊆ (⋃n ∈ underS r i. extend S n)› ‹¬ consistent S'›
      unfolding extend_def extendL_def
        wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
      using inconsistent_finite by auto
    then obtain ns where ns: ‹S' ⊆ (⋃n ∈ ns. extend S n)› ‹ns ⊆ underS r i› ‹finite ns›
      by (metis finite_subset_Union finite_subset_image)
    moreover have ‹ns ≠ {}›
      using S'(3) assms calculation(1) consistent_hereditary by auto
    ultimately obtain j where ‹∀n ∈ ns. n ∈ under r j› ‹j ∈ underS r i›
      using wo_rel.finite_underS_bound wo_rel_r ns by (meson subset_iff)
    then have ‹∀n ∈ ns. extend S n ⊆ extend S j›
      using extend_under by fast
    then have ‹S' ⊆ extend S j›
      using S' ns(1) by blast
    then show False
      using 3(3) ‹¬ consistent S'› assms consistent_hereditary ‹j ∈ underS r i› by blast
  qed
qed

lemma consistent_Extend:
  assumes ‹consistent S›
  shows ‹consistent (Extend S)›
  unfolding Extend_def
proof (rule ccontr)
  assume ‹¬ consistent (⋃n ∈ Field r. extend S n)›
  then obtain S' where ‹finite S'› ‹S' ⊆ (⋃n ∈ Field r. extend S n)› ‹¬ consistent S'›
    using inconsistent_finite by metis
  then obtain m where ‹S' ⊆ (⋃n ∈ under r m. extend S n)› ‹m ∈ Field r›
    using wo_rel.finite_bound_under wo_rel_r
    by (metis SUP_le_iff assms consistent_hereditary emptyE under_empty)
  then have ‹S' ⊆ extend S m›
    using extend_under by fast
  moreover have ‹consistent (extend S m)›
    using assms consistent_extend by blast
  ultimately show False
    using ‹¬ consistent S'› consistent_hereditary by blast
qed

definition maximal' :: ‹'a set ⇒ bool› where
  ‹maximal' S ≡ ∀p ∈ Field r. consistent ({p} ∪ S) ⟶ p ∈ S›

lemma Extend_bound: ‹n ∈ Field r ⟹ extend S n ⊆ Extend S›
  unfolding Extend_def by blast

lemma maximal'_Extend: ‹maximal' (Extend S)›
  unfolding maximal'_def
proof safe
  fix p
  assume *: ‹p ∈ Field r› ‹consistent ({p} ∪ Extend S)›
  then have ‹{p} ∪ extend S p ⊆ {p} ∪ Extend S›
    unfolding Extend_def by blast
  then have **: ‹consistent ({p} ∪ extend S p)›
    using * consistent_hereditary by blast
  moreover have succ: ‹aboveS r p ≠ {}›
    using * isLimOrd_r wo_rel.isLimOrd_aboveS wo_rel_r by fast
  then have ‹succ r p ∈ Field r›
    using wo_rel_r by (simp add: wo_rel.succ_in_Field)
  moreover have ‹p ∈ extend S (succ r p)›
    using ** unfolding extend_def extendS_def
      wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL succ]
    by simp
  ultimately show ‹p ∈ Extend S›
    using Extend_bound by fast
qed

end

locale MCS =
  fixes consistent :: ‹'a set ⇒ bool›
  assumes infinite_UNIV: ‹infinite (UNIV :: 'a set)›
    and ‹consistent S ⟹ S' ⊆ S ⟹ consistent S'›
    and ‹⋀S. ¬ consistent S ⟹ ∃S' ⊆ S. finite S' ∧ ¬ consistent S'›

sublocale MCS ⊆ MCS_Lim_Ord ‹|UNIV|›
proof
  show ‹Well_order |UNIV|›
    by simp
next
  have ‹infinite ( Field |UNIV :: 'a set| )›
    using infinite_UNIV by simp
  with card_order_infinite_isLimOrd card_of_Card_order
  show ‹isLimOrd |UNIV :: 'a set|› .
next
  fix S S'
  show ‹consistent S ⟹ S' ⊆ S ⟹ consistent S'›
    using MCS_axioms unfolding MCS_def by blast
next
  fix S S'
  show ‹¬ consistent S ⟹ ∃S' ⊆ S. finite S' ∧ ¬ consistent S'›
    using MCS_axioms unfolding MCS_def by blast
qed

context MCS begin

lemma Extend_subset: ‹S ⊆ Extend S›
  by (simp add: Extend_subset')

definition maximal :: ‹'a set ⇒ bool› where
  ‹maximal S ≡ ∀p. consistent ({p} ∪ S) ⟶ p ∈ S›

lemma maximal_maximal': ‹maximal S ⟷ maximal' S›
  unfolding maximal_def maximal'_def by simp

lemma maximal_Extend: ‹maximal (Extend S)›
  using maximal'_Extend maximal_maximal' by fast

end

end