Theory Maximal_Consistent_Sets

(*
  Title:  Maximal Consistent Sets
  Author: Asta Halkjær From
*)

chapter ‹Maximal Consistent Sets›

theory Maximal_Consistent_Sets imports "HOL-Cardinals.Cardinal_Order_Relation" begin

section ‹Utility›

lemma Set_Diff_Un: ‹X - (Y ∪ Z) = X - Y - Z›
  by blast

lemma infinite_Diff_fin_Un: ‹infinite (X - Y) ⟹ finite Z ⟹ infinite (X - (Z ∪ Y))›
  by (simp add: Set_Diff_Un Un_commute)

lemma infinite_Diff_subset: ‹infinite (X - A) ⟹ B ⊆ A ⟹ infinite (X - B)›
  by (meson Diff_cancel Diff_eq_empty_iff Diff_mono infinite_super)

lemma finite_bound:
  fixes X :: ‹('a :: size) set›
  assumes ‹finite X› ‹X ≠ {}›
  shows ‹∃x ∈ X. ∀y ∈ X. size y ≤ size x›
  using assms by (induct X rule: finite_induct) force+

lemma infinite_UNIV_size:
  fixes f :: ‹('a :: size) ⇒ 'a›
  assumes ‹⋀x. size x < size (f x)›
  shows ‹infinite (UNIV :: 'a set)›
proof
  assume ‹finite (UNIV :: 'a set)›
  then obtain x :: 'a where ‹∀y :: 'a. size y ≤ size x›
    using finite_bound by fastforce
  moreover have ‹size x < size (f x)›
    using assms .
  ultimately show False
    using leD by blast
qed

lemma split_finite_sets:
  assumes ‹finite A› ‹finite B›
  assumes ‹A ⊆ B ∪ S›
  shows ‹∃B' C. finite C ∧ (B' ∪ C = A) ∧ B' ⊆ B ∧ C ⊆ S›
  using assms subset_UnE by fastforce

lemma split_list:
  assumes ‹set A ⊆ set B ∪ S›
  shows ‹∃B' C. set (B' @ C) = set A ∧ set B' ⊆ set B ∧ set C ⊆ S›
  using assms split_finite_sets[where A=‹set A› and B=‹set B› and S=S]
  by (metis List.finite_set finite_Un finite_list set_append)

lemma struct_split:
  assumes ‹⋀A B. P A ⟹ set A ⊆ set B ⟹ P B› ‹P A› ‹set A ⊆ set B ∪ X›
  shows ‹∃C. set C ⊆ X ∧ P (B @ C)›
proof -
  obtain B' C where C: ‹set (B' @ C) = set A› ‹set B' ⊆ set B› ‹set C ⊆ X›
    using assms(3) split_list by meson
  then have ‹P (B @ C)›
    using assms(1)[where B=‹B @ C›] assms(2) by fastforce
  then show ?thesis
    using C by blast
qed

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

lemma underS_trans: ‹a ∈ underS b ⟹ b ∈ underS c ⟹ a ∈ underS c›
  by (meson ANTISYM TRANS underS_underS_trans)

end

lemma card_of_infinite_smaller_Union:
  assumes ‹∀x. |f x| <o |X|› ‹infinite X›
  shows ‹|⋃x ∈ X. f x| ≤o |X|›
  using assms by (metis (full_types) Field_card_of card_of_UNION_ordLeq_infinite
      card_of_well_order_on ordLeq_iff_ordLess_or_ordIso ordLess_or_ordLeq)

lemma card_of_params_marker_lists:
  assumes ‹infinite (UNIV :: 'i set)› ‹|UNIV :: 'm set| ≤o |UNIV :: nat set|›
  shows ‹|UNIV :: ('i + 'm × nat) list set| ≤o |UNIV :: 'i set|›
proof -
  have ‹(UNIV :: 'm set) ≠ {}›
    by simp
  then have ‹|UNIV :: 'm set| *c |UNIV :: nat set| ≤o |UNIV :: nat set|›
    using assms(2) by (simp add: cinfinite_def cprod_cinfinite_bound ordLess_imp_ordLeq)
  then have ‹|UNIV :: ('m × nat) set| ≤o |UNIV :: nat set|›
    unfolding cprod_def by simp
  moreover have ‹|UNIV :: nat set| ≤o |UNIV :: 'i set|›
    using assms infinite_iff_card_of_nat by blast
  ultimately have ‹|UNIV :: ('m × nat) set| ≤o |UNIV :: 'i set|›
    using ordLeq_transitive by blast
  moreover have ‹Cinfinite |UNIV :: 'i set|›
    using assms by (simp add: cinfinite_def)
  ultimately have ‹|UNIV :: 'i set| +c |UNIV :: ('m × nat) set| =o |UNIV :: 'i set|›
    using csum_absorb1 by blast
  then have ‹|UNIV :: ('i + 'm × nat) set| =o |UNIV :: 'i set|›
    unfolding csum_def by simp
  then have ‹|UNIV :: ('i + 'm × nat) set| ≤o |UNIV :: 'i set|›
    using ordIso_iff_ordLeq by blast
  moreover have ‹infinite (UNIV :: ('i + 'm × nat) set)›
    using assms by simp
  then have ‹|UNIV :: ('i + 'm × nat) list set| =o |UNIV :: ('i + 'm × nat) set|›
    by (metis card_of_lists_infinite lists_UNIV)
  ultimately have ‹|UNIV :: ('i + 'm × nat) list set| ≤o |UNIV :: 'i set|›
    using ordIso_ordLeq_trans by blast
  then show ?thesis
    using ordLeq_transitive by blast
qed

section ‹Base Locale›

locale MCS_Base =
  fixes consistent :: ‹'a set ⇒ bool›
  assumes consistent_hereditary: ‹⋀S S'. consistent S ⟹ S' ⊆ S ⟹ consistent S'›
    and inconsistent_finite: ‹⋀S. ¬ consistent S ⟹ ∃S' ⊆ S. finite S' ∧ ¬ consistent S'›
begin

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

end

section ‹Ordinal Locale›

locale MCS_Lim_Ord = MCS_Base +
  fixes r :: ‹'a rel›
  assumes WELL: ‹Well_order r›
    and Cinfinite_r: ‹Cinfinite r›
  fixes params :: ‹'a ⇒ 'i set›
    and witness :: ‹'a ⇒ 'a set ⇒ 'a set›
  assumes finite_params: ‹⋀p. finite (params p)›
    and finite_witness_params: ‹⋀p S. finite (⋃q ∈ witness p S. params q)›
    and consistent_witness: ‹⋀p S. consistent ({p} ∪ S)
      ⟹ infinite (UNIV - (⋃q ∈ S. params q))
      ⟹ consistent (witness p S ∪ {p} ∪ S)›
begin

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

lemma isLimOrd_r: ‹isLimOrd r›
  using Cinfinite_r card_order_infinite_isLimOrd cinfinite_def by blast

subsection ‹Lindenbaum Extension›

abbreviation paramss :: ‹'a set ⇒ 'i set› where
  ‹paramss S ≡ ⋃p ∈ S. params p›

definition extendS :: ‹'a ⇒ 'a set ⇒ 'a set› where
  ‹extendS n prev ≡ if consistent ({n} ∪ prev) then witness n prev ∪ {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 extendL n›

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.zero_in_Field[OF wo_rel_r] wo_rel.zero_smallest[OF wo_rel_r]
    by (metis SUP_upper2 emptyE underS_I)
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.underS_zero[OF wo_rel_r] by fast
next
  case (2 i)
  moreover from this have ‹m = i ∨ m ∈ underS r i›
    by (metis wo_rel.less_succ[OF wo_rel_r] underS_E underS_I)
  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.supr_greater[OF wo_rel_r] wo_rel.supr_under[OF wo_rel_r]
  by (metis emptyE in_Above_under set_eq_subset underS_I under_Field under_empty)

subsection ‹Consistency›

lemma params_origin:
  assumes ‹a ∈ paramss (extend S n)›
  shows ‹a ∈ paramss S ∨ (∃m ∈ underS r n. a ∈ paramss (witness m (extend S m) ∪ {m}))›
  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]
    by blast
next
  case (2 i)
  then consider (here) ‹a ∈ paramss (witness i (extend S i) ∪ {i})› | (there) ‹a ∈ paramss (extend S i)›
    using wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)] extendS_def extend_def
    by (metis (no_types, lifting) UN_Un UnE)
  then show ?case
  proof cases
    case here
    moreover have ‹i ∈ Field r›
      by (meson WELL 2(1) well_order_on_domain wo_rel.succ_in_diff[OF wo_rel_r])
    ultimately show ?thesis
      using 2(1) by (metis Refl_under_in wo_rel.underS_succ[OF wo_rel_r] wo_rel.REFL[OF wo_rel_r])
  next
    case there
    then show ?thesis
      using 2 by (metis in_mono underS_subset_under wo_rel.underS_succ[OF wo_rel_r])
  next
  qed
next
  case (3 i)
  then obtain j where ‹j ∈ underS r i› ‹a ∈ paramss (extend S j)›
    unfolding extend_def extendL_def wo_rel.worecZSL_isLim[OF wo_rel_r adm_woL_extendL 3(1-2)]
    by blast
  then show ?case
    using 3 wo_rel.underS_trans[OF wo_rel_r, of _ j i] by meson
qed

lemma consistent_extend:
  assumes ‹consistent S› ‹r ≤o |UNIV - paramss S|›
  shows ‹consistent (extend S n)›
  using assms(1)
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 blast
next
  case (2 i)
  then have ‹i ∈ Field r›
    by (meson WELL  well_order_on_domain wo_rel.succ_in_diff[OF wo_rel_r])
  then have *: ‹|underS r i| <o r›
    using card_of_underS by (simp add: Cinfinite_r)
  let ?paramss = ‹λk. paramss (witness k (extend S k) ∪ {k})›
  let ?X = ‹⋃k ∈ underS r i. ?paramss k›
  have ‹|?X| <o r›
  proof (cases ‹finite (underS r i)›)
    case True
    then have ‹finite ?X›
      by (simp add: finite_params finite_witness_params)
    then show ?thesis
      using Cinfinite_r assms(2) unfolding cinfinite_def by (simp add: finite_ordLess_infinite)
  next
    case False
    moreover have ‹∀k. finite (?paramss k)›
      by (simp add: finite_params finite_witness_params)
    then have ‹∀k. |?paramss k| <o |underS r i|›
      using False by simp
    ultimately have ‹|?X| ≤o |underS r i|›
      using card_of_infinite_smaller_Union by fast
    then show ?thesis
      using * ordLeq_ordLess_trans by blast
  qed
  then have ‹|?X| <o |UNIV - paramss S|›
    using assms(2) ordLess_ordLeq_trans by blast
  moreover have ‹infinite (UNIV - paramss S)›
    using assms(2) Cinfinite_r unfolding cinfinite_def by (metis Field_card_of ordLeq_finite_Field)
  ultimately have ‹|UNIV - paramss S - ?X| =o |UNIV - paramss S|›
    using card_of_Un_diff_infinite by blast
  moreover from this have ‹infinite (UNIV - paramss S - ?X)›
    using ‹infinite (UNIV - paramss S)› card_of_ordIso_finite by blast
  moreover have ‹⋀a. a ∈ paramss (extend S i) ⟹ a ∈ paramss S ∨ a ∈ ?X›
    using params_origin by simp
  then have ‹paramss (extend S i) ⊆ paramss S ∪ ?X›
    by fast
  ultimately have ‹infinite (UNIV - paramss (extend S i))›
    using infinite_Diff_subset by (metis (no_types, lifting) Set_Diff_Un)
  with 2 show ?case
    unfolding extend_def extendS_def wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL 2(1)]
    using consistent_witness 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'› consistent_hereditary ‹j ∈ underS r i›
      by (meson BNF_Least_Fixpoint.underS_Field)
  qed
qed

lemma consistent_Extend:
  assumes ‹consistent S› ‹r ≤o |UNIV - paramss 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[OF wo_rel_r] assms consistent_hereditary
    by (metis Sup_empty emptyE image_empty subsetI under_empty)
  then have ‹S' ⊆ extend S m›
    using extend_under by fast
  moreover have ‹consistent (extend S m)›
    using assms consistent_extend ‹m ∈ Field r› by blast
  ultimately show False
    using ‹¬ consistent S'› consistent_hereditary by blast
qed

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

subsection ‹Maximality›

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

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[OF wo_rel_r] by blast
  then have ‹succ r p ∈ Field r›
    using wo_rel.succ_in_Field[OF wo_rel_r] by blast
  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

subsection ‹Saturation›

definition saturated' :: ‹'a set ⇒ bool› where
  ‹saturated' S ≡ ∀p ∈ S. p ∈ Field r ⟶ (∃S'. witness p S' ⊆ S)›

lemma saturated'_Extend:
  assumes ‹consistent (Extend S)›
  shows ‹saturated' (Extend S)›
  unfolding saturated'_def
proof safe
  fix p
  assume *: ‹p ∈ Extend S› ‹p ∈ Field r›
  then have ‹extend S p ⊆ Extend S›
    unfolding Extend_def by blast
  then have ‹consistent ({p} ∪ extend S p)›
    using assms(1) * consistent_hereditary by auto
  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)
  ultimately have ‹extend S (succ r p) = witness p (extend S p) ∪ {p} ∪ extend S p›
    unfolding extend_def extendS_def wo_rel.worecZSL_succ[OF wo_rel_r adm_woL_extendL succ]
    by simp
  moreover have ‹extend S (succ r p) ⊆ Extend S›
    unfolding Extend_def using ‹succ r p ∈ Field r› by blast
  ultimately show ‹∃a. witness p a ⊆ Extend S›
    by fast
qed

end

section ‹Locale with Saturation›

locale MCS_Saturation = MCS_Base +
  assumes infinite_UNIV: ‹infinite (UNIV :: 'a set)›
  fixes params :: ‹'a ⇒ 'i set›
    and witness :: ‹'a ⇒ 'a set ⇒ 'a set›
  assumes ‹⋀p. finite (params p)›
    and ‹⋀p S. finite (⋃q ∈ witness p S. params q)›
    and ‹⋀p S. consistent ({p} ∪ S) ⟹ infinite (UNIV - (⋃q ∈ S. params q))
      ⟹ consistent (witness p S ∪ {p} ∪ S)›

sublocale MCS_Saturation ⊆ MCS_Lim_Ord _ ‹|UNIV|›
proof
  show ‹Well_order |UNIV|›
    by simp
next
  show ‹Cinfinite |UNIV :: 'a set|›
    unfolding cinfinite_def using infinite_UNIV by simp
next
  fix p
  show ‹finite (params p)›
    by (metis MCS_Saturation_axioms MCS_Saturation_axioms_def MCS_Saturation_def)
next
  fix p S
  show ‹finite (⋃q ∈ witness p S. params q)›
    by (metis MCS_Saturation_axioms MCS_Saturation_axioms_def MCS_Saturation_def)
next
  fix p S
  show ‹consistent ({p} ∪ S) ⟹
           infinite (UNIV - (⋃q ∈ S. params q)) ⟹
           consistent (witness p S ∪ {p} ∪ S)›
    by (metis MCS_Saturation_axioms MCS_Saturation_axioms_def MCS_Saturation_def)
qed

context MCS_Saturation begin

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

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

definition saturated :: ‹'a set ⇒ bool› where
  ‹saturated S ≡ ∀p ∈ S. ∃S'. witness p S' ⊆ S›

lemma saturated_saturated': ‹saturated S ⟷ saturated' S›
  unfolding saturated_def saturated'_def by simp

lemma saturated_Extend:
  assumes ‹consistent (Extend S)›
  shows ‹saturated (Extend S)›
  using assms saturated'_Extend saturated_saturated' by blast

theorem MCS_Extend:
  assumes ‹consistent S› ‹|UNIV :: 'a set| ≤o |UNIV - paramss S|›
  shows ‹consistent (Extend S)› ‹maximal (Extend S)› ‹saturated (Extend S)›
  using assms consistent_Extend maximal_Extend saturated_Extend by blast+

end

section ‹Locale without Saturation›

locale MCS_No_Saturation = MCS_Base +
  assumes ‹infinite (UNIV :: 'a set)›

sublocale MCS_No_Saturation ⊆ MCS_Saturation consistent ‹λ_. {} :: 'a set› ‹λ_ _. {}›
proof
  show ‹infinite (UNIV :: 'a set)›
    using MCS_No_Saturation_axioms MCS_No_Saturation_axioms_def MCS_No_Saturation_def by blast
next
  show ‹finite {}› ..
next
  show ‹finite (⋃_∈{}. {})›
    by fast
next
  fix p S
  show ‹consistent ({p} ∪ S) ⟹ consistent ({} ∪ {p} ∪ S)›
    by simp
qed

context MCS_No_Saturation begin

lemma always_saturated [simp]: ‹saturated H›
  unfolding saturated_def by simp

theorem MCS_Extend':
  assumes ‹consistent S›
  shows ‹consistent (Extend S)› ‹maximal (Extend S)›
  using assms consistent_Extend maximal_Extend by simp_all

end

section ‹Truth Lemma›

locale Truth_Base =
  fixes semics :: ‹'model ⇒ ('model ⇒ 'fm ⇒ bool) ⇒ 'fm ⇒ bool›
    and semantics :: ‹'model ⇒ 'fm ⇒ bool›
    and models_from :: ‹'a set ⇒ 'model set›
    and rel :: ‹'a set ⇒ 'model ⇒ 'fm ⇒ bool›
  assumes semics_semantics: ‹semantics M p ⟷ semics M semantics p›
    and Hintikka_model: ‹⋀H M p. ∀M ∈ models_from H. ∀p. semics M (rel H) p ⟷ rel H M p ⟹
      M ∈ models_from H ⟹ semantics M p ⟷ rel H M p›

locale Truth_Saturation = MCS_Saturation + Truth_Base +
  assumes MCS_Hintikka: ‹⋀H. consistent H ⟹ maximal H ⟹ saturated H ⟹
      ∀M ∈ models_from H. ∀p. semics M (rel H) p ⟷ rel H M p›
begin

theorem truth_lemma_saturation:
  assumes ‹consistent H› ‹maximal H› ‹saturated H› ‹M ∈ models_from H›
  shows ‹semantics M p ⟷ rel H M p›
  using Hintikka_model MCS_Hintikka assms .

end

locale Truth_No_Saturation = MCS_No_Saturation + Truth_Base +
  assumes MCS_Hintikka: ‹⋀H. consistent H ⟹ maximal H ⟹
      ∀M ∈ models_from H. ∀p. semics M (rel H) p ⟷ rel H M p›
begin

theorem truth_lemma_no_saturation:
  assumes ‹consistent H› ‹maximal H› ‹M ∈ models_from H›
  shows ‹semantics M p ⟷ rel H M p›
  using Hintikka_model MCS_Hintikka assms .

end

end