# 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›

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
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
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
by auto
next
case (3 i)
then show ?case
unfolding extend_def extendL_def
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
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
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
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›

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
```