Theory Abstract_Consistency_Property

(*
  Author: Asta Halkjær Boserup, 2026.

  Inspiration:
  - "A Unifying Principal in Quantification Theory", 1963, Raymond M. Smullyan.
  - "First-Order Logic", 1968, Raymond M. Smullyan.
  - "First-Order Logic and Automated Theorem Proving", 1996, Melvin Fitting.
  - "FOL-Fitting", Stefan Berghofer.
*)

chapter ‹Abstract Consistency Properties›

theory Abstract_Consistency_Property imports
  "HOL-Cardinals.Cardinal_Order_Relation"
begin

section ‹Utility›

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

lemma infinite_diff_finite: ‹finite A ⟹ infinite (- B) ⟹ infinite (- (A ∪ B))›
  by (metis Compl_Diff_eq double_complement finite_Diff2 sup_commute)

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 infinite_left: ‹finite C ⟹ infinite A ⟹ |A| ≤o |- B| ⟹ |A| ≤o |- (C ∪ B)|›
  by (metis (no_types, opaque_lifting) Compl_Diff_eq card_of_infinite_diff_finite card_of_ordLeq_finite
      double_complement ordIso_iff_ordLeq ordLeq_transitive sup_commute)

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)

context wo_rel
begin

lemma underS_bound: ‹a ∈ underS c ⟹ b ∈ underS c ⟹ 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 a› ‹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 ⊆ (⋃a ∈ Field r. f a)›
  shows ‹∃b. p ⊆ (⋃a ∈ under b. f a)›
  using assms
proof (induct rule: finite_induct)
  case (insert x p)
  then obtain b where ‹p ⊆ (⋃a ∈ under b. f a)›
    by fast
  moreover obtain b' where ‹x ∈ f b'› ‹b' ∈ Field r›
    using insert(4) by blast
  then have ‹x ∈ (⋃a ∈ under b'. f a)›
    using REFL Refl_under_in by fast
  ultimately have ‹{x} ∪ p ⊆ (⋃a ∈ under b. f a) ∪ (⋃a ∈ under b'. f a)›
    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)

definition is_chain :: ‹('a ⇒ 'a set) ⇒ bool› where
  ‹is_chain f ≡ ∀a ∈ Field r. ∀b ∈ Field r. b ∈ under a ⟶ f b ⊆ f a›

lemma is_chainD: ‹is_chain f ⟹ b ∈ under a ⟹ x ∈ f b ⟹ x ∈ f a›
  unfolding is_chain_def by (metis equals0D subsetD under_Field under_empty)

lemma chain_index:
  assumes ch: ‹is_chain f› and fin: ‹finite F› and ne: ‹Field r ≠ {}›
  shows ‹F ⊆ (⋃a ∈ Field r. f a) ⟹ ∃a ∈ Field r. F ⊆ f a›
  using fin
proof (induct rule: finite_induct)
  case empty
  then show ?case
    using ne by blast
next
  case (insert x F)
  then have ‹∃a ∈ Field r. F ⊆ f a› ‹∃b ∈ Field r. x ∈ f b› ‹F ⊆ (⋃x ∈ Field r. f x)›
    using ch by simp_all
  then obtain a and b where f: ‹F ⊆ f a› ‹x ∈ f b› and nm: ‹a ∈ Field r› ‹b ∈ Field r›
    by blast
  have ‹b ∈ under (max2 a b)› ‹a ∈ under (max2 a b)›
    using nm  by (meson REFL Refl_under_in TRANS max2_greater_among subset_iff under_incl_iff)+
  have ‹x ∈ f (max2 a b)›
    using is_chainD ch ‹b ∈ under (max2 a b)› f(2) by blast
  moreover have ‹F ⊆ f (max2 a b)›
    using is_chainD ch ‹a ∈ local.under (max2 a b)› f(1) by blast
  ultimately show ?case
    using nm unfolding max2_def by auto
qed

end

section ‹Finite Character›

definition close :: ‹'a set set ⇒ 'a set set› where
  ‹close C ≡ {S. (∃S' ∈ C. S ⊆ S')}›

definition subset_closed :: ‹'a set set ⇒ bool› where
  ‹subset_closed C ≡ ∀S' ∈ C. ∀S ⊆ S'. S ∈ C›

lemma subset_in_close: ‹S ⊆ S' ⟹ x ∪ S' ∈ C ⟹ x ∪ S ∈ close C›
  unfolding close_def by blast

lemma close_closed: ‹subset_closed (close C)›
  unfolding close_def subset_closed_def by blast

lemma close_subset: ‹C ⊆ close C›
  unfolding close_def by blast

definition finite_char :: ‹'a set set ⇒ bool› where
  ‹finite_char C ≡ ∀S. S ∈ C ⟷ (∀S' ⊆ S. finite S' ⟶ S' ∈ C)›

definition mk_finite_char :: ‹'a set set ⇒ 'a set set› where
  ‹mk_finite_char C ≡ {S. (∀S' ⊆ S. finite S' ⟶ S' ∈ C)}›

lemma finite_char: ‹finite_char (mk_finite_char C)›
  unfolding finite_char_def mk_finite_char_def by blast

lemma finite_char_closed: ‹finite_char C ⟹ subset_closed C›
  unfolding finite_char_def subset_closed_def by (meson order_trans)

lemma finite_char_subset: ‹subset_closed C ⟹ C ⊆ mk_finite_char C›
  unfolding mk_finite_char_def subset_closed_def by blast

lemma (in wo_rel) chain_union_closed:
  assumes ‹finite_char C› ‹is_chain f› ‹∀a ∈ Field r. f a ∈ C› ‹Field r ≠ {}›
  shows ‹(⋃a ∈ Field r. f a) ∈ C›
  using assms chain_index unfolding finite_char_def by metis

definition maximal :: ‹'a set set ⇒ 'a set ⇒ bool› where
  ‹maximal C S ⟷ (∀S' ∈ C. S ⊆ S' ⟶ S = S')›

section ‹Consistency Properties›

locale Params =
  fixes map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm›
    and params_fm :: ‹'fm ⇒ 'x set›
    and is_param :: ‹'x ⇒ bool›
  assumes map_fm_id: ‹map_fm id = id›
    and finite_params_fm [simp]: ‹⋀p. finite (params_fm p)›
    and map_params_fm: ‹⋀f g p. (∀x ∈ params_fm p. f x = g x) ⟹ map_fm f p = map_fm g p›
begin

definition is_subst :: ‹('x ⇒ 'x) ⇒ bool› where
  ‹is_subst f ≡ ∀x. is_param x ⟷ is_param (f x)›

lemma is_subst_id [intro]: ‹is_subst id›
  unfolding is_subst_def by simp

definition mk_alt_consistency :: ‹'fm set set ⇒ 'fm set set› where
  ‹mk_alt_consistency C ≡ {S. (∃f. is_subst f ∧ map_fm f ` S ∈ C)}›

lemma mk_alt_consistency_subset: ‹C ⊆ mk_alt_consistency C›
  unfolding mk_alt_consistency_def
proof
  fix x
  assume ‹x ∈ C›
  then have ‹map_fm id ` x ∈ C›
    using map_fm_id by simp
  then have ‹∃f. is_subst f ∧ map_fm f ` x ∈ C›
    by blast
  then show ‹x ∈ {S. ∃f. is_subst f ∧ map_fm f ` S ∈ C}›
    by blast
qed

lemma mk_alt_consistency_closed:
  assumes ‹subset_closed C›
  shows ‹subset_closed (mk_alt_consistency C)›
  unfolding subset_closed_def mk_alt_consistency_def
proof safe
  fix S S' f
  assume ‹is_subst f› ‹map_fm f ` S' ∈ C› ‹S ⊆ S'›
  moreover have ‹map_fm f ` S ⊆ map_fm f ` S'›
    using ‹S ⊆ S'› by blast
  moreover have ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
    using ‹subset_closed C› unfolding subset_closed_def by blast
  ultimately show ‹∃f. is_subst f ∧ map_fm f ` S ∈ C›
    by blast
qed

abbreviation params :: ‹'fm set ⇒ 'x set› where
  ‹params S ≡ ⋃p ∈ S. params_fm p›

lemma infinite_params: ‹infinite (U - params B) ⟹ infinite (U - params (set ps ∪ B))›
  using finite_params_fm by (metis List.finite_set UN_Un finite_UN_I infinite_Diff_fin_Un)

lemma infinite_params_left: 
  assumes ‹infinite A› ‹|A| ≤o |U - params S|›
  shows ‹|A| ≤o |U - params (set ps ∪ S)|›
proof -
  have ‹infinite (U - params S)›
    using assms card_of_ordLeq_infinite by blast
  then have ‹|U - params S| =o |U - params (set ps ∪ S)|›
    by (simp add: Set_Diff_Un Un_commute card_of_infinite_diff_finite ordIso_symmetric)
  then show ?thesis
    using assms(2) ordLeq_ordIso_trans by blast
qed

definition enough_new :: ‹'fm set ⇒ bool› where
  ‹enough_new S ≡ |UNIV :: 'fm set| ≤o |Collect is_param - params S|›

lemma enough_new_countable:
  assumes ‹∃to_nat :: 'fm ⇒ nat. inj to_nat› ‹infinite (Collect is_param - params S)›
  shows ‹enough_new S›
  unfolding enough_new_def using assms
  by (meson UNIV_I card_of_ordLeqI infinite_iff_card_of_nat ordLeq_transitive)

lemma enough_new_all_param:
  assumes ‹|UNIV :: 'fm set| ≤o |UNIV - params S|› ‹⋀x. is_param x›
  shows ‹enough_new S›
  unfolding enough_new_def using assms by (simp add: Collect_cong)

end

datatype ('x, 'fm) kind
  = Cond ‹'fm list ⇒ ('fm set set ⇒ 'fm set ⇒ bool) ⇒ bool› ‹'fm set ⇒ bool›
  | Wits ‹'fm ⇒ 'x ⇒ 'fm list›

inductive (in Params) sat⇩E :: ‹('x, 'fm) kind ⇒ 'fm set set ⇒ bool› where
  sat⇩E_Cond [intro!]: ‹(⋀S ps Q. S ∈ C ⟹ set ps ⊆ S ⟹ P ps Q ⟹ Q C S) ⟹ sat⇩E (Cond P H) C›
| sat⇩E_Wits [intro!]: ‹(⋀S p. S ∈ C ⟹ p ∈ S ⟹ (∃x. is_param x ∧ set (W p x) ∪ S ∈ C)) ⟹ sat⇩E (Wits W) C›

inductive_cases (in Params) sat⇩E_CondE[elim!]: ‹sat⇩E (Cond P H) C›
inductive_cases (in Params) sat⇩E_WitsE[elim!]: ‹sat⇩E (Wits W) C›

inductive (in Params) sat⇩A :: ‹('x, 'fm) kind ⇒ 'fm set set ⇒ bool› where
  sat⇩A_Cond [intro!]: ‹(⋀S ps Q. S ∈ C ⟹ set ps ⊆ S ⟹ P ps Q ⟹ Q C S) ⟹ sat⇩A (Cond P H) C›
| sat⇩A_Wits [intro!]: ‹(⋀S p x. S ∈ C ⟹ p ∈ S ⟹ x ∉ params S ⟹ is_param x ⟹ set (W p x) ∪ S ∈ C) ⟹ sat⇩A (Wits W) C›

inductive_cases (in Params) sat⇩A_CondE[elim!]: ‹sat⇩A (Cond P H) C›
inductive_cases (in Params) sat⇩A_WitsE[elim!]: ‹sat⇩A (Wits W) C›

definition (in Params) prop⇩E :: ‹('x, 'fm) kind list ⇒ 'fm set set ⇒ bool› where
  ‹prop⇩E Ks C ≡ ∀K ∈ set Ks. sat⇩E K C›

definition (in Params) prop⇩A :: ‹('x, 'fm) kind list ⇒ 'fm set set ⇒ bool› where
  ‹prop⇩A Ks C ≡ ∀K ∈ set Ks. sat⇩A K C›

inductive (in Params) sat⇩H :: ‹('x, 'fm) kind ⇒ 'fm set ⇒ bool› where
  sat⇩H_Cond [intro!]: ‹H S ⟹ sat⇩H (Cond P H) S›
| sat⇩H_Wits [intro!]: ‹(⋀p. p ∈ S ⟹ (∃x. is_param x ∧ set (W p x) ⊆ S)) ⟹ sat⇩H (Wits W) S›

inductive_cases (in Params) sat⇩H_CondE[elim!]: ‹sat⇩H (Cond P H) C›
inductive_cases (in Params) sat⇩H_WitsE[elim!]: ‹sat⇩H (Wits W) C›

definition (in Params) prop⇩H :: ‹('x, 'fm) kind list ⇒ 'fm set ⇒ bool› where
  ‹prop⇩H Ks S ≡ ∀K ∈ set Ks. sat⇩H K S›

theorem (in Params) sat⇩H_Wits: ‹sat⇩E (Wits W) C ⟹ S ∈ C ⟹ maximal C S ⟹ sat⇩H (Wits W) S›
  unfolding maximal_def by fast

subsection ‹Consistency Kinds›

locale Consistency_Kind = Params map_fm params_fm is_param
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes K :: ‹('x, 'fm) kind›
  assumes respects_close: ‹⋀C. sat⇩E K C ⟹ sat⇩E K (close C)›
    and respects_alt: ‹⋀C. sat⇩E K C ⟹ subset_closed C ⟹ sat⇩A K (mk_alt_consistency C)›
    and respects_fin: ‹⋀C. subset_closed C ⟹ sat⇩A K C ⟹ sat⇩A K (mk_finite_char C)›
    and hintikka: ‹⋀C S. sat⇩E K C ⟹ S ∈ C ⟹ maximal C S ⟹ sat⇩H K S›

locale Consistency_Kinds = Params map_fm params_fm is_param
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes Ks :: ‹('x, 'fm) kind list›
  assumes all_kinds: ‹⋀K. K ∈ set Ks ⟹ Consistency_Kind map_fm params_fm is_param K›
begin

lemma sat⇩E: ‹K ∈ set Ks ⟹ prop⇩E Ks C ⟹ sat⇩E K C›
  unfolding prop⇩E_def by blast

lemma prop⇩E_close: ‹prop⇩E Ks C ⟹ prop⇩E Ks (close C)›
  unfolding prop⇩E_def using all_kinds Consistency_Kind.respects_close by fast

lemma prop⇩E_alt: ‹prop⇩E Ks C ⟹ subset_closed C ⟹ prop⇩A Ks (mk_alt_consistency C)›
  unfolding prop⇩E_def prop⇩A_def using all_kinds Consistency_Kind.respects_alt by fast

lemma prop⇩E_fin: ‹subset_closed C ⟹ prop⇩A Ks C ⟹ prop⇩A Ks (mk_finite_char C)›
  unfolding prop⇩A_def using all_kinds Consistency_Kind.respects_fin by fast

definition mk_alt_fin :: ‹'fm set set ⇒ 'fm set set› where
  ‹mk_alt_fin C ≡ mk_finite_char (mk_alt_consistency (close C))›

lemma mk_alt_fin_subset_closed: ‹subset_closed (mk_alt_fin C)›
  unfolding mk_alt_fin_def using finite_char finite_char_closed by blast

lemma mk_alt_fin_finite_char: ‹finite_char (mk_alt_fin C)›
  unfolding mk_alt_fin_def using finite_char by blast

lemma mk_alt_fin_in: ‹S ∈ C ⟹ S ∈ mk_alt_fin C›
  unfolding mk_alt_fin_def
  by (meson close_closed close_subset finite_char_subset in_mono mk_alt_consistency_closed mk_alt_consistency_subset)

theorem prop⇩E: ‹prop⇩E Ks C ⟹ prop⇩A Ks (mk_alt_fin C)›
  unfolding mk_alt_fin_def
  by (simp add: prop⇩E_alt prop⇩E_close prop⇩E_fin close_closed mk_alt_consistency_closed)

end

fun (in Params) witness_kinds :: ‹('x, 'fm) kind list ⇒ 'fm ⇒ 'fm set ⇒ 'fm set› where
  ‹witness_kinds [] p S = {}›
| ‹witness_kinds (Cond _ _ # Ks) p S = witness_kinds Ks p S›
| ‹witness_kinds (Wits W # Ks) p S =
  (let
    rest = witness_kinds Ks p S;
    a = SOME x. x ∈ Collect is_param - params (rest ∪ {p} ∪ S)
   in set (W p a) ∪ rest)›

lemma (in Params) witness_kinds_new:
  assumes ‹infinite (UNIV :: 'fm set)› ‹infinite (Collect is_param - params S)›
  shows ‹infinite (Collect is_param - params (witness_kinds Ks p S ∪ {p} ∪ S))›
  using assms
proof (induct Ks p S rule: witness_kinds.induct)
  case (1 p S)
  then show ?case
    by (simp add: infinite_Diff_fin_Un)
next
  case (3 W Ks p S)
  then show ?case
    by (metis (no_types, lifting) infinite_params sup_assoc witness_kinds.simps(3))
qed simp_all

lemma (in Params) witness_kinds:
  assumes inf: ‹infinite (UNIV :: 'fm set)› and ‹infinite (Collect is_param - params S)› ‹Wits W ∈ set Ks›
  shows ‹∃x. is_param x ∧ set (W p x) ⊆ witness_kinds Ks p S›
  using assms(2-)
proof (induct Ks p S rule: witness_kinds.induct)
  case (3 W' Ks p S)
  moreover have ‹infinite (Collect is_param - params (witness_kinds Ks p S ∪ {p} ∪ S))›
    using inf 3 witness_kinds_new by blast
  then have ‹∃x. x ∈ Collect is_param - params (witness_kinds Ks p S ∪ {p} ∪ S)›
    by (metis equals0I finite.emptyI)
  then obtain x where x:
    ‹(SOME x. x ∈ Collect is_param - params (witness_kinds Ks p S ∪ {p} ∪ S)) = x›
    ‹is_param x›
    by (metis (mono_tags, lifting) DiffE mem_Collect_eq someI_ex)
  ultimately show ?case
    by (auto simp: Let_def)
qed simp_all

locale Maximal_Consistency = wo_rel ‹|UNIV| :: 'fm rel› + Consistency_Kinds map_fm params_fm is_param Ks
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    Ks :: ‹('x, 'fm) kind list› +
  assumes inf_univ: ‹infinite (UNIV :: 'fm set)›
begin

lemma Cinfinite_r: ‹Cinfinite |UNIV :: 'fm set|›
  by (simp add: cinfinite_def inf_univ)

lemma isLimOrd: isLimOrd
  using Cinfinite_r card_order_infinite_isLimOrd cinfinite_def by blast

lemma aboveS_ne: ‹aboveS a ≠ {}›
  by (simp add: isLimOrd isLimOrd_aboveS)

lemma params_left: ‹enough_new S ⟹ enough_new (set ps ∪ S)›
  unfolding enough_new_def using infinite_params_left inf_univ by blast

definition witness :: ‹'fm ⇒ 'fm set ⇒ 'fm set› where
  ‹witness ≡ witness_kinds Ks›

definition extendS :: ‹'fm set set ⇒ 'fm ⇒ 'fm set ⇒ 'fm set› where
  ‹extendS C a prev ≡ if ({a} ∪ prev ∈ C) then (witness a prev ∪ {a} ∪ prev) else prev›

definition extendL :: ‹'fm set set ⇒ ('fm ⇒ 'fm set) ⇒ 'fm ⇒ 'fm set› where
  ‹extendL C rec a ≡ ⋃b ∈ underS a. rec b›

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

lemma adm_woL_extendL: ‹adm_woL (extendL C)›
  unfolding extendL_def adm_woL_def by blast

definition Extend :: ‹'fm set set ⇒ 'fm set ⇒ 'fm set› where
  ‹Extend C S ≡ ⋃a. extend C S a›

lemma finite_witness_kinds: ‹finite (witness_kinds Qs p S)›
  unfolding witness_def by (induct Qs p S rule: witness_kinds.induct) (simp_all add: Let_def)

lemma finite_witness: ‹finite (witness p S)›
  unfolding witness_def using finite_witness_kinds .

lemma finite_witness_kinds_params: ‹finite (params (witness_kinds Qs p S))›
  using finite_witness_kinds by simp

lemma finite_witness_params: ‹finite (params (witness p S))›
  using finite_witness by simp

lemma extend_zero [simp]: ‹extend C S zero = S›
  unfolding extend_def worecZSL_zero[OF adm_woL_extendL] ..

lemma extend_succ [simp]: ‹extend C S (succ a) =
    (if {a} ∪ extend C S a ∈ C then witness a (extend C S a) ∪ {a} ∪ extend C S a else extend C S a)›
  unfolding extend_def extendS_def worecZSL_succ[OF adm_woL_extendL aboveS_ne] ..

lemma extend_isLim [simp]:
  assumes ‹isLim a› ‹a ≠ zero›
  shows ‹extend C S a = (⋃b ∈ underS a. extend C S b)›
  unfolding extend_def extendL_def worecZSL_isLim[OF adm_woL_extendL assms] ..

lemma extend_subset: ‹S ⊆ extend C S a›
proof (induct a rule: well_order_inductZSL)
  case (Lim i)
  then show ?case
    using zero_smallest by (metis Field_card_of SUP_upper2 UNIV_I extend_isLim underS_I)
qed auto

lemma Extend_subset: ‹S ⊆ Extend C S›
  unfolding Extend_def using extend_subset by fast

lemma extend_underS: ‹b ∈ underS a ⟹ extend C S b ⊆ extend C S a›
proof (induct a rule: well_order_inductZSL)
  case Zero
  then show ?case
    using underS_zero by blast
next
  case (Suc i)
  moreover from this have ‹b = i ∨ b ∈ underS i›
    using less_succ by (metis underS_E underS_I)
  ultimately show ?case
    by auto
next
  case (Lim i)
  then show ?case
    by auto
qed

lemma extend_under: ‹b ∈ under a ⟹ extend C S b ⊆ extend C S a›
  using extend_underS supr_greater supr_under
  by (metis emptyE in_Above_under set_eq_subset underS_I under_empty)

lemma params_origin:
  assumes ‹x ∈ params (extend C S a)›
  shows ‹x ∈ params S ∨ (∃b ∈ underS a. x ∈ params (witness b (extend C S b) ∪ {b}))›
  using assms
proof (induct a rule: well_order_inductZSL)
  case Zero
  then show ?case
    by simp
next
  case (Suc i)
  then consider
    (here) ‹x ∈ params ({i} ∪ witness i (extend C S i))› |
    (there) ‹x ∈ params (extend C S i)›
    using Suc(3) by (fastforce split: if_splits)
  then show ?case
  proof cases
    case here
    then show ?thesis
      using Suc(1) succ_diff succ_in by (metis sup_commute underS_I )
  next
    case there
    then show ?thesis
      using Suc by (metis in_mono underS_subset_under underS_succ)
  next
  qed
next
  case (Lim i)
  then obtain j where ‹j ∈ underS i› ‹x ∈ params (extend C S j)›
    unfolding extend_def extendL_def worecZSL_isLim[OF adm_woL_extendL Lim(1-2)]
    by blast
  then show ?case
    using Lim underS_trans[of _ j i] by meson
qed

lemma is_chain_extend: ‹is_chain (extend C S)›
  by (simp add: extend_under is_chain_def)

lemma extend_in_C_step:
  assumes ‹prop⇩A Ks C› ‹{a} ∪ extend C S a ∈ C›
    and inf: ‹infinite (Collect is_param - params ({a} ∪ extend C S a))›
  shows ‹extend C S (succ a) ∈ C›
proof -
  have ‹set Qs ⊆ set Ks ⟹ witness_kinds Qs a (extend C S a) ∪ {a} ∪ extend C S a ∈ C› for Qs
  proof (induct Qs)
    case Nil
    then show ?case
      using assms(2) by simp
  next
    case (Cons Q Qs)
    let ?S = ‹extend C S a›
    let ?rest = ‹witness_kinds Qs a ?S›

    have Q: ‹Q ∈ set Ks›
      using Cons.prems by simp

    have *: ‹?rest ∪ {a} ∪ ?S ∈ C›
      using Cons by simp

    show ?case
    proof (cases Q)
      case (Wits W)

      have ‹infinite (Collect is_param - params (?rest ∪ {a} ∪ ?S))›
        using finite_witness_kinds_params inf by (metis UN_Un Un_assoc infinite_Diff_fin_Un)
      then have **: ‹∃x. x ∈ Collect is_param - params (?rest ∪ {a} ∪ ?S)›
        by (metis ex_in_conv finite.emptyI)
      then obtain x where x:
        ‹(SOME x. x ∈ Collect is_param - params (?rest ∪ {a} ∪ ?S)) = x›
        ‹x ∉ params (?rest ∪ {a} ∪ ?S)›
        ‹is_param x›
        by (metis (mono_tags, lifting) DiffE mem_Collect_eq someI_ex)

      have ‹a ∈ ?rest ∪ {a} ∪ ?S›
        by simp
      then have ‹∀x. x ∉ params (?rest ∪ {a} ∪ ?S) ⟶ is_param x ⟶ set (W a x) ∪ ?rest ∪ {a} ∪ ?S ∈ C›
        using assms(1) * Q Wits unfolding prop⇩A_def Un_assoc by fast
      then have ‹set (W a x) ∪ ?rest ∪ {a} ∪ ?S ∈ C›
        using x by fast

      moreover have ‹witness_kinds (Q # Qs) a ?S = set (W a x) ∪ ?rest›
        using Cons Wits x by (simp add: Let_def)
      ultimately show ?thesis
        by simp
    next
      case (Cond P)
      then show ?thesis
        using * by simp
    qed
  qed
  then have ‹witness a (extend C S a) ∪ {a} ∪ extend C S a ∈ C›
    unfolding witness_def by blast
  then show ?thesis
    unfolding extend_succ using assms(2) by simp
qed

lemma extend_in_C_stop:
  assumes ‹extend C S a ∈ C›
    and ‹{a} ∪ extend C S a ∉ C›
  shows ‹extend C S (succ a) ∈ C›
  using assms extend_succ by auto


lemma infinite_succ_extend:
  assumes ‹S ∈ C› ‹enough_new S› ‹isSucc p›
  shows ‹infinite (Collect is_param - params (extend C S p))›
  using assms
proof (induct p rule: well_order_inductZSL)
  case Zero
  then show ?case
    using not_isSucc_zero by blast
next
  case (Suc i)
  then have *: ‹|underS i| <o |UNIV :: 'fm set|›
    using card_of_underS by (simp add: Cinfinite_r)

  let ?params = ‹λk. params ({k} ∪ witness k (extend C S k))›
  let ?X = ‹⋃k ∈ underS i. ?params k›
  have ‹|?X| <o |UNIV :: 'fm set|›
  proof (cases ‹finite (underS i)›)
    case True
    then have ‹finite ?X›
      using finite_witness_params by simp
    then show ?thesis
      using Cinfinite_r unfolding cinfinite_def by (simp add: finite_ordLess_infinite)
  next
    case False
    moreover have ‹∀k. finite (?params k)›
      using finite_witness_params by simp
    then have ‹∀k. |?params k| <o |underS i|›
      using False by simp
    ultimately have ‹|?X| ≤o |underS i|›
      using card_of_infinite_smaller_Union by fast
    then show ?thesis
      using * ordLeq_ordLess_trans by blast
  qed
  then have ‹|?X| <o |Collect is_param - params S|›
    using Suc(4) ordLess_ordLeq_trans unfolding enough_new_def by blast
  moreover have ‹infinite (Collect is_param - params S)›
    using Suc(4) Cinfinite_r unfolding cinfinite_def enough_new_def
    by (metis Field_card_of ordLeq_finite_Field)
  ultimately have ‹|Collect is_param - params S - ?X| =o |Collect is_param - params S|›
    using card_of_Un_diff_infinite by blast
  moreover from this have ‹infinite (Collect is_param - params S - ?X)›
    using ‹infinite (Collect is_param - params S)› card_of_ordIso_finite by blast
  moreover have ‹⋀a. a ∈ params (extend C S i) ⟹ a ∈ params S ∨ a ∈ ?X›
    using params_origin by simp
  then have ‹params (extend C S i) ⊆ params S ∪ ?X›
    by fast
  ultimately have ‹infinite (Collect is_param - params (extend C S i))›
    using infinite_Diff_subset by (metis (no_types, lifting) Set_Diff_Un)
  then show ?case
    using Suc extend_succ inf_univ witness_def witness_kinds_new by presburger
next
  case (Lim i)
  then show ?case
    using isLim_def by blast
qed

lemma extend_in_C:
  assumes ‹prop⇩A Ks C› ‹finite_char C› ‹S ∈ C› ‹enough_new S›
  shows ‹extend C S a ∈ C›
  using assms
proof (induct a rule: well_order_inductZSL)
  case Zero
  then show ?case
    by (simp add: adm_woL_extendL extend_def worecZSL_zero)
next
  case (Suc i)
  have ‹infinite (Collect is_param - params (extend C S (succ i)))›
    using infinite_succ_extend aboveS_ne assms(3,4) isSucc_succ by blast
  then have ‹infinite (Collect is_param - params (extend C S i))›
    using extend_succ[of C S i]  by (metis UN_Un Un_upper2 infinite_Diff_subset)
  then have ‹infinite (Collect is_param - params ({i} ∪ extend C S i))›
    using finite_params_fm  by (simp add: Compl_eq_Diff_UNIV infinite_Diff_fin_Un)
  then show ?case
    using Suc extend_in_C_step extend_in_C_stop succ_in[of i] by blast
next
  case (Lim i)
  show ?case
  proof (rule ccontr)
    assume ‹extend C S i ∉ C›
    then obtain S' where S': ‹S' ⊆ (⋃a ∈ underS i. extend C S a)› ‹S' ∉ C› ‹finite S'›
      using Lim(5) unfolding finite_char_def extend_def extendL_def worecZSL_isLim[OF adm_woL_extendL Lim(1-2)]
      by blast
    then obtain as where as: ‹S' ⊆ (⋃a ∈ as. extend C S a)› ‹as ⊆ underS i› ‹finite as›
      by (metis finite_subset_Union finite_subset_image)
    moreover from this(1) have ‹as ≠ {}›
      using S' Lim unfolding finite_char_def
      by (metis Union_empty bot.extremum_uniqueI empty_subsetI image_empty)
    ultimately obtain j where ‹∀a ∈ as. a ∈ under j› ‹j ∈ underS i›
      using finite_underS_bound by (metis in_mono)
    then have ‹∀a ∈ as. extend C S a ⊆ extend C S j›
      using extend_under by fast
    then have ‹S' ⊆ extend C S j›
      using S' as(1) by blast
    then show False
      using Lim(3-) S'(2) as(2-3) ‹∀a∈as. a ∈ under j› ‹as ≠ {}› ‹j ∈ underS i›
      by (meson Order_Relation.underS_Field finite_char_closed subsetD subset_closed_def)
  qed
qed

lemma Extend_in_C:
  assumes ‹prop⇩A Ks C› ‹finite_char C› ‹S ∈ C› ‹enough_new S›
  shows ‹Extend C S ∈ C›
  unfolding Extend_def using assms chain_union_closed is_chain_extend extend_in_C by simp

theorem Extend_maximal:
  assumes ‹subset_closed C›
  shows ‹maximal C (Extend C S)›
  unfolding maximal_def Extend_def
proof (intro ballI impI)
  fix S'
  assume *: ‹S' ∈ C› ‹(⋃x. extend C S x) ⊆ S'›
  moreover have ‹S' ⊆ (⋃x. extend C S x)›
  proof (rule ccontr)
    assume ‹¬ S' ⊆ (⋃x. extend C S x)›
    then have ‹∃z. z ∈ S' ∧ z ∉ (⋃x. extend C S x)›
      by blast
    then obtain a where a: ‹a ∈ S'› ‹a ∉ (⋃x. extend C S x)›
      using *(1) by blast
    then have ‹{a} ∪ extend C S a ⊆ S'›
      using * by blast
    moreover have ‹∀S ⊆ S'. S ∈ C›
      using assms ‹S' ∈ C› unfolding subset_closed_def by blast
    ultimately have ‹{a} ∪ extend C S a ∈ C›
      by blast
    then have ‹a ∈ extend C S (succ a)›
      using a by simp
    then show False
      using * a by blast
  qed
  ultimately show ‹(⋃x. extend C S x) = S'›
    by simp
qed

definition witnessed :: ‹'fm set ⇒ bool› where
  ‹witnessed S ≡ ∀p ∈ S. ∃S'. infinite (Collect is_param - params S') ∧ witness p S' ⊆ S›

theorem Extend_witnessed:
  assumes ‹prop⇩A Ks C› ‹finite_char C› ‹S ∈ C› ‹enough_new S›
  shows ‹witnessed (Extend C S)›
  unfolding witnessed_def
proof safe
  fix p
  assume ‹p ∈ Extend C S›
  then have ‹{p} ∪ extend C S p ⊆ Extend C S›
    unfolding Extend_def by blast
  moreover have ‹Extend C S ∈ C›
    using Extend_in_C assms by blast
  ultimately have ‹{p} ∪ extend C S p ∈ C›
    using ‹finite_char C› finite_char_closed unfolding subset_closed_def by blast
  moreover have ‹extend C S (succ p) ∈ C›
    using assms extend_in_C by blast
  ultimately have ‹witness p (extend C S p) ∪ {p} ∪ extend C S p ∈ C›
    unfolding extend_succ by simp
  then have ‹witness p (extend C S p) ∪ {p} ∪ extend C S p ⊆ Extend C S›
    unfolding Extend_def using extend_succ ‹{p} ∪ extend C S p ∈ C› by fastforce
  moreover have ‹infinite (Collect is_param - params (extend C S (succ p)))›
    using infinite_succ_extend by (meson aboveS_ne assms(3,4) isSucc_def)
  then have ‹infinite (Collect is_param - params (extend C S p))›
    using extend_succ by (metis SUP_union Un_upper2 infinite_Diff_subset)
  ultimately show ‹∃S'. infinite (Collect is_param - params S') ∧ witness p S' ⊆ Extend C S›
    by fast
qed

abbreviation mk_mcs :: ‹'fm set set ⇒ 'fm set ⇒ 'fm set› where
  ‹mk_mcs C S ≡ Extend (mk_alt_fin C) S›

theorem mk_mcs_rmaximal: ‹maximal C (mk_mcs C S)›
  using Extend_maximal maximal_def mk_alt_fin_in mk_alt_fin_subset_closed by meson

theorem mk_mcs_witnessed:
  assumes ‹prop⇩E Ks C› ‹S ∈ C› ‹enough_new S›
  shows ‹witnessed (mk_mcs C S)›
  using assms Extend_witnessed prop⇩E mk_alt_fin_finite_char mk_alt_fin_in by blast

section ‹Hintikka Sets›

lemma mk_mcs_hintikka:
  assumes ‹prop⇩E Ks C› ‹S ∈ C› ‹enough_new S›
  shows ‹prop⇩H Ks (mk_mcs C S)›
  unfolding prop⇩H_def
proof
  fix K
  assume K: ‹K ∈ set Ks›
  show ‹sat⇩H K (mk_mcs C S)›
  proof (cases K)
    case (Cond P H)
    moreover have ‹maximal (mk_alt_fin C) (mk_mcs C S)›
      using Extend_maximal mk_alt_fin_subset_closed by blast
    moreover have ‹prop⇩A Ks (mk_alt_fin C)›
      using assms(1) prop⇩E by blast
    then have ‹mk_mcs C S ∈ mk_alt_fin C›
      using assms(2-3) Extend_in_C mk_alt_fin_finite_char mk_alt_fin_in by blast
    moreover have ‹sat⇩E (Cond P H) (mk_alt_fin C)›
      using ‹prop⇩A Ks (mk_alt_fin C)› Cond K unfolding prop⇩A_def by fast 
    ultimately show ?thesis
      using K all_kinds Consistency_Kind.hintikka by meson
  next
    case (Wits W)
    have ‹witnessed (mk_mcs C S)›
      using mk_mcs_witnessed[OF assms(1-3)] .
    then have ‹∀p ∈ mk_mcs C S. ∃x. is_param x ∧ set (W p x) ⊆ mk_mcs C S ›
      unfolding witnessed_def witness_def using inf_univ Wits witness_kinds K by fast
    then show ?thesis
      using Wits by fast
  qed
qed

end

locale Hintikka = Maximal_Consistency map_fm params_fm is_param Ks
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    Ks :: ‹('x, 'fm) kind list› +
  fixes H :: ‹'fm set›
  assumes hintikka: ‹prop⇩H Ks H›
begin

lemma sat⇩H: ‹K ∈ set Ks ⟹ sat⇩H K H›
  using hintikka unfolding prop⇩H_def by blast

end

context Maximal_Consistency
begin

theorem mk_mcs_Hintikka:
  assumes ‹prop⇩E Ks C› ‹S ∈ C› ‹enough_new S›
  shows ‹Hintikka map_fm params_fm is_param Ks (mk_mcs C S)›
  using assms mk_mcs_hintikka by unfold_locales

end

section ‹Derivational Consistency›

locale Derivational_Kind = Consistency_Kind map_fm params_fm is_param K
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    K :: ‹('x, 'fm) kind› +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes kind: ‹infinite (UNIV :: 'fm set) ⟹ sat⇩E K {A. enough_new A ∧ ⊢ A}›

locale Derivational_Consistency = Maximal_Consistency map_fm params_fm is_param Ks
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    Ks :: ‹('x, 'fm) kind list› +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes all_consistent: ‹infinite (UNIV :: 'fm set) ⟹ prop⇩E Ks {A. enough_new A ∧ ⊢ A}›
begin

theorem Consistency: ‹prop⇩E Ks {A. enough_new A ∧ ⊢ A}›
  using all_consistent inf_univ unfolding prop⇩E_def by fast

end

section ‹Weak Derivational Consistency›

locale Weak_Derivational_Kind = Consistency_Kind map_fm params_fm is_param K
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    K :: ‹('x, 'fm) kind› +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes kind: ‹infinite (Collect is_param) ⟹ sat⇩E K {S. ∃A. set A = S ∧ ⊢ A}›

locale Weak_Derivational_Consistency = Maximal_Consistency map_fm params_fm is_param Ks
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    Ks :: ‹('x, 'fm) kind list› +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes Consistency: ‹infinite (UNIV :: 'x set) ⟹ prop⇩E Ks {S. ∃A. set A = S ∧ ⊢ A}›


section ‹Conflicts›

locale Confl = Params map_fm params_fm is_param
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩✗› 50)
  assumes confl_map: ‹⋀ps qs f. ps ↝⇩✗ qs ⟹ map (map_fm f) ps ↝⇩✗ map (map_fm f) qs›
begin

inductive cond where
  cond [intro!]: ‹ps ↝⇩✗ qs ⟹ cond ps (λ_ S. set qs ∩ S = {})›

inductive_cases condE[elim!]: ‹cond ps Q›

inductive hint where
  hint [intro!]: ‹(⋀ps qs q. ps ↝⇩✗ qs ⟹ set ps ⊆ H ⟹ q ∈ set qs ⟹ q ∉ H) ⟹ hint H›

declare hint.simps[simp]

abbreviation kind :: ‹('x, 'fm) kind› where
  ‹kind ≡ Cond cond hint›

end

sublocale Confl ⊆ Consistency_Kind map_fm params_fm is_param kind
proof
  fix C
  assume conflC: ‹sat⇩E kind C›
  then show ‹sat⇩E kind (close C)›
  proof safe
    fix S ps qs q
    assume ‹S ∈ close C›
    then obtain S' where S': ‹S' ∈ C› and ‹S ⊆ S'›
      unfolding close_def by blast

    assume ‹set ps ⊆ S›
    then have *: ‹set ps ⊆ S'›
      using ‹S ⊆ S'› by blast

    assume **: ‹ps ↝⇩✗ qs›
    then have ‹∀q ∈ set qs. q ∉ S'›
      using conflC S' * by blast
    then have ‹∀q ∈ set qs. q ∉ S›
      using ‹S ⊆ S'› by blast
    moreover assume ‹q ∈ set qs› ‹q ∈ S›
    ultimately show ‹q ∈ {}›
      using ** by auto
  qed
next
  fix C
  assume conflC: ‹sat⇩E kind C›
  then show ‹sat⇩A kind (mk_alt_consistency C)›
  proof safe
    fix S ps qs q

    assume ‹S ∈ mk_alt_consistency C›
    then obtain f where f: ‹map_fm f ` S ∈ C›
      unfolding mk_alt_consistency_def by blast

    let ?C = ‹mk_alt_consistency C›
    let ?S = ‹map_fm f ` S›

    assume ‹set ps ⊆ S›
    then have *: ‹set (map (map_fm f) ps) ⊆ ?S›
      by auto

    assume ‹ps ↝⇩✗ qs›
    then have ‹map (map_fm f) ps ↝⇩✗ (map (map_fm f) qs)›
      using confl_map by blast
    then have ‹∀q ∈ set  (map (map_fm f) qs). q ∉ ?S›
      using conflC f * by blast
    then have ‹∀q ∈ set qs. map_fm f q ∉ ?S›
      by simp
    then have ‹∀q ∈ set qs. q ∉ S›
      by blast
    moreover assume ‹q ∈ set qs› ‹q ∈ S›
    ultimately show ‹q ∈ {}›
      by auto
  qed
next
  fix C
  assume conflAC: ‹sat⇩A kind C› and closedC: ‹subset_closed C›
  then show ‹sat⇩A kind (mk_finite_char C)›
  proof safe
    fix S ps qs q
    assume ‹S ∈ mk_finite_char C›
    then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
      unfolding mk_finite_char_def by blast

    have sc: ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
      using closedC unfolding subset_closed_def by blast
    then have sc': ‹⋀S' x. x ∪ S' ∈ C ⟹ ∀S ⊆ x ∪ S'. S ∈ C›
      by blast

    assume *: ‹set ps ⊆ S› ‹ps ↝⇩✗ qs› ‹q ∈ set qs› ‹q ∈ S›
    then have ‹{q} ∪ set ps ∈ C›
      using ‹set ps ⊆ S› finc by simp
    then have ‹q ∈ {}›
      using * conflAC by blast
    then show ‹q ∈ {}›
      by auto
  qed
next
  fix C S
  assume *: ‹sat⇩E kind C› ‹S ∈ C› ‹maximal C S› 
  show ‹sat⇩H kind S›
  proof safe
    fix ps qs q
    assume **: ‹set ps ⊆ S› ‹ps ↝⇩✗ qs› ‹q ∈ set qs› ‹q ∈ S›
    then show False
      using * by blast
  qed
qed

locale Derivational_Confl = Confl map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩✗› 50) +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀S ps qs x. set ps ⊆ S ⟹ ps ↝⇩✗ qs ⟹ x ∈ set qs ⟹ x ∈ S ⟹ ¬ ⊢ S›

sublocale Derivational_Confl ⊆ Derivational_Kind map_fm params_fm is_param kind consistent
  using infinite_params_left consistent by unfold_locales blast+


locale Weak_Derivational_Confl = Confl map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩✗› 50) +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀A ps qs x. set ps ⊆ set A ⟹ ps ↝⇩✗ qs ⟹ x ∈ set qs ⟹ x ∈ set A ⟹ ¬ ⊢ A›

sublocale Weak_Derivational_Confl ⊆ Weak_Derivational_Kind map_fm params_fm is_param kind consistent
  using infinite_params_left consistent by unfold_locales blast+

section ‹Alpha›

locale Alpha = Params map_fm params_fm is_param
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩α› 50)
  assumes alpha_map: ‹⋀ps qs f. ps ↝⇩α qs ⟶ map (map_fm f) ps ↝⇩α map (map_fm f) qs›
begin

inductive cond where
  cond [intro!]: ‹ps ↝⇩α qs ⟹ cond ps (λC S. set qs ∪ S ∈ C)›

inductive_cases condE[elim!]: ‹cond ps Q›

inductive hint where
  hint [intro!]: ‹(⋀ps qs q. ps ↝⇩α qs ⟹ set ps ⊆ H ⟹ q ∈ set qs ⟹ q ∈ H) ⟹ hint H›

declare hint.simps[simp]

abbreviation kind :: ‹('x, 'fm) kind› where
  ‹kind ≡ Cond cond hint›

end

sublocale Alpha ⊆ Consistency_Kind map_fm params_fm is_param kind
proof
  fix C
  assume alphaC: ‹sat⇩E kind C›
  then show ‹sat⇩E kind (close C)›
  proof safe
    fix S ps qs q
    assume ‹S ∈ close C›
    then obtain S' where S': ‹S' ∈ C› and ‹S ⊆ S'›
      unfolding close_def by blast

    assume ‹set ps ⊆ S› ‹ps ↝⇩α qs›
    then have *: ‹set ps ⊆ S'›
      using ‹S ⊆ S'› by blast

    assume **: ‹ps ↝⇩α qs›
    then have ‹set qs ∪ S' ∈ C›
      using alphaC S' * by blast
    then show  ‹set qs ∪ S ∈ close C›
      using ‹S ⊆ S'› subset_in_close by blast
  qed
next
  fix C
  assume alphaC: ‹sat⇩E kind C›
  then show ‹sat⇩A kind (mk_alt_consistency C)›
  proof safe
    fix S ps qs

    assume ‹S ∈ mk_alt_consistency C›
    then obtain f where f: ‹is_subst f› ‹map_fm f ` S ∈ C›
      unfolding mk_alt_consistency_def by blast

    let ?C = ‹mk_alt_consistency C›
    let ?S = ‹map_fm f ` S›

    assume ‹set ps ⊆ S›
    then have *: ‹set (map (map_fm f) ps) ⊆ ?S›
      by auto

    assume ‹ps ↝⇩α qs›
    then have ‹map (map_fm f) ps ↝⇩α (map (map_fm f) qs)›
      using alpha_map by blast
    then have ‹set (map (map_fm f) qs) ∪ ?S ∈ C›
      using alphaC * f by blast
    then show ‹set qs ∪ S ∈ ?C›
      unfolding mk_alt_consistency_def using f by (auto simp: image_Un)
  qed
next
  fix C
  assume alphaAC: ‹sat⇩A kind C› and closedC: ‹subset_closed C›
  then show ‹sat⇩A kind (mk_finite_char C)›
  proof safe
    fix S ps qs q
    assume ‹S ∈ mk_finite_char C›
    then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
      unfolding mk_finite_char_def by blast

    have sc: ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
      using closedC unfolding subset_closed_def by blast
    then have sc': ‹⋀S' x. x ∪ S' ∈ C ⟹ ∀S ⊆ x ∪ S'. S ∈ C›
      by blast

    assume *: ‹set ps ⊆ S› and **: ‹ps ↝⇩α qs›

    show ‹set qs ∪ S ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof safe
      fix S'
      let ?S' = ‹set ps ∪ (S' - set qs)›

      assume ‹S' ⊆ set qs ∪ S› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by blast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹set qs ∪ ?S' ∈ C›
        using ** alphaAC by fast
      then show ‹S' ∈ C›
        using sc by fast
    qed
  qed
next
  fix C S
  assume *: ‹sat⇩E kind C› ‹S ∈ C› ‹maximal C S› 
  show ‹sat⇩H kind S›
  proof safe
    fix ps qs q
    assume **: ‹set ps ⊆ S› ‹ps ↝⇩α qs›
    then have ‹set qs ∪ S ∈ C›
      using * by blast
    moreover assume ‹q ∈ set qs›
    ultimately show ‹q ∈ S›
      using ‹maximal C S› unfolding maximal_def by fast
  qed
qed

locale Derivational_Alpha = Alpha map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩α› 50) +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀S ps qs. set ps ⊆ S ⟹ ps ↝⇩α qs ⟹ ⊢ S ⟹ ⊢ set qs ∪ S›

sublocale Derivational_Alpha ⊆ Derivational_Kind map_fm params_fm is_param kind consistent
  using infinite_params_left consistent enough_new_def by unfold_locales blast+


locale Weak_Derivational_Alpha = Alpha map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩α› 50) +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀A ps qs. set ps ⊆ set A ⟹ ps ↝⇩α qs ⟹ ⊢ A ⟹ ⊢ qs @ A›

sublocale Weak_Derivational_Alpha ⊆ Weak_Derivational_Kind map_fm params_fm is_param kind consistent
proof
  show ‹sat⇩E kind {S. ∃A. set A = S ∧ ⊢ A}›
  proof safe
    fix ps qs A
    assume ‹set ps ⊆ set A› ‹ps ↝⇩α qs› ‹⊢ A›
    then show ‹∃B. set B = set qs ∪ set A ∧ ⊢ B›
      using consistent[of ps A qs] by (meson set_append)
  qed
qed

section ‹Beta›

locale Beta = Params map_fm params_fm is_param
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩β› 50)
  assumes beta_map: ‹⋀ps qs f. ps ↝⇩β qs ⟶ map (map_fm f) ps ↝⇩β map (map_fm f) qs›
begin

inductive cond where
  cond [intro!]: ‹ps ↝⇩β qs ⟹ cond ps (λC S. ∃q ∈ set qs. {q} ∪ S ∈ C)›

inductive_cases condE[elim!]: ‹cond ps Q›

inductive hint where
  hint [intro!]: ‹(⋀ps qs. ps ↝⇩β qs ⟹ set ps ⊆ H ⟹ ∃q ∈ set qs. q ∈ H) ⟹ hint H›

declare hint.simps[simp]

abbreviation kind :: ‹('x, 'fm) kind› where
  ‹kind ≡ Cond cond hint›

end

sublocale Beta ⊆ Consistency_Kind map_fm params_fm is_param kind
proof
  fix C
  assume betaC: ‹sat⇩E kind C›
  then show ‹sat⇩E kind (close C)›
  proof safe
    fix S ps qs q
    assume ‹S ∈ close C›
    then obtain S' where S': ‹S' ∈ C› and ‹S ⊆ S'›
      unfolding close_def by blast

    assume ‹set ps ⊆ S› ‹ps ↝⇩β qs›
    then have *: ‹set ps ⊆ S'›
      using ‹S ⊆ S'› by blast

    assume **: ‹ps ↝⇩β qs›
    then have ‹∃q ∈ set qs. {q} ∪ S' ∈ C›
      using betaC S' * by blast
    then show ‹∃q ∈ set qs. insert q S ∈ close C›
      using ‹S ⊆ S'› subset_in_close by (metis insert_is_Un)
  qed
next
  fix C
  assume betaC: ‹sat⇩E kind C›
  then show ‹sat⇩A kind (mk_alt_consistency C)›
  proof safe
    fix S ps qs

    assume ‹S ∈ mk_alt_consistency C›
    then obtain f where f: ‹is_subst f› ‹map_fm f ` S ∈ C›
      unfolding mk_alt_consistency_def by blast

    let ?C = ‹mk_alt_consistency C›
    let ?S = ‹map_fm f ` S›

    assume ‹set ps ⊆ S›
    then have *: ‹set (map (map_fm f) ps) ⊆ ?S›
      by auto

    assume ‹ps ↝⇩β qs›
    then have ‹map (map_fm f) ps ↝⇩β (map (map_fm f) qs)›
      using beta_map by blast
    then have ‹∃q ∈ set (map (map_fm f) qs). {q} ∪ ?S ∈ C›
      using betaC * f by blast
    then show ‹∃q ∈ set qs. insert q S ∈ ?C›
      unfolding mk_alt_consistency_def using f by (auto simp: image_Un)
  qed
next
  fix C
  assume betaAC: ‹sat⇩A kind C› and closedC: ‹subset_closed C›
  then show ‹sat⇩A kind (mk_finite_char C)›
  proof safe
    fix S ps qs q
    assume ‹S ∈ mk_finite_char C›
    then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
      unfolding mk_finite_char_def by blast

    have sc: ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
      using closedC unfolding subset_closed_def by blast
    then have sc': ‹⋀S' x. x ∪ S' ∈ C ⟹ ∀S ⊆ x ∪ S'. S ∈ C›
      by blast

    assume *: ‹set ps ⊆ S› and **: ‹ps ↝⇩β qs›

    show ‹∃q ∈ set qs. insert q S ∈ mk_finite_char C›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then have ‹∀q ∈ set qs. ∃Sq. Sq ⊆ insert q S ∧ finite Sq ∧ Sq ∉ C›
        unfolding mk_finite_char_def by blast
      then obtain f where f: ‹∀q ∈ set qs. f q ⊆ insert q S ∧ finite (f q) ∧ f q ∉ C›
        by metis

      let ?S' = ‹set ps ∪ ⋃{f q - {q} |q. q ∈ set qs}›

      have ‹?S' ⊆ S›
        using * f by fast
      moreover have ‹finite ?S'›
        using f by auto
      ultimately have ‹?S' ∈ C›
        using finc by blast
      then have ‹∃q ∈ set qs. {q} ∪ ?S' ∈ C›
        using ** betaAC by fast
      then have ‹∃q ∈ set qs. f q ∈ C›
        using sc' by blast
      then show False
        using f by blast
    qed
  qed
next
  fix C S
  assume *: ‹sat⇩E kind C› ‹S ∈ C› ‹maximal C S› 
  show ‹sat⇩H kind S›
  proof safe
    fix ps qs
    assume **: ‹set ps ⊆ S› ‹ps ↝⇩β qs›
    then have ‹∃q ∈ set qs. {q} ∪ S ∈ C›
      using * by blast
    then show ‹∃q ∈ set qs. q ∈ S›
      using ‹maximal C S› unfolding maximal_def by fast
  qed
qed

locale Derivational_Beta = Beta map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩β› 50) +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀S ps qs. set ps ⊆ S ⟹ ps ↝⇩β qs ⟹ ⊢ S ⟹ ∃q ∈ set qs. ⊢ {q} ∪ S›

sublocale Derivational_Beta ⊆ Derivational_Kind map_fm params_fm is_param kind consistent
proof
  assume inf: ‹infinite (UNIV :: 'fm set)›
  then show ‹sat⇩E kind {A. enough_new A ∧ ⊢ A}›
  proof safe
    fix S ps qs
    assume *: ‹set ps ⊆ S› ‹ps ↝⇩β qs› ‹⊢ S›
    then have ‹∃q ∈ set qs. ⊢ {q} ∪ S›
      using consistent by blast
    moreover assume ‹enough_new S› 
    ultimately show ‹∃q∈set qs. insert q S ∈ {A. enough_new A ∧ ⊢ A}›
      using infinite_params_left[OF inf] unfolding enough_new_def
      by (metis (no_types, lifting) empty_set insert_code(1) insert_is_Un mem_Collect_eq)
  qed
qed

locale Weak_Derivational_Beta = Beta map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ 'fm list ⇒ bool› (infix ‹↝⇩β› 50) +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀A ps qs. set ps ⊆ set A ⟹ ps ↝⇩β qs ⟹ ⊢ A ⟹ ∃q ∈ set qs. ⊢ q # A›

sublocale Weak_Derivational_Beta ⊆ Weak_Derivational_Kind map_fm params_fm is_param kind consistent
proof
  show ‹sat⇩E kind {S. ∃A. set A = S ∧ ⊢ A}›
  proof safe
    fix ps qs A
    assume *: ‹set ps ⊆ set A› ‹ps ↝⇩β qs› ‹⊢ A›
    then have ‹∃q ∈ set qs. ⊢ q # A›
      using consistent by blast
    then show ‹∃q∈set qs. insert q (set A) ∈ {S. ∃A. set A = S ∧ ⊢ A}›
      by (metis (mono_tags, lifting) CollectI list.simps(15))
  qed
qed

section ‹Gamma›

locale Gamma = Params map_fm params_fm is_param
  for
    map_tm :: ‹('x ⇒ 'x) ⇒ 'tm ⇒ 'tm› and
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes classify :: ‹'fm list ⇒ ('fm set ⇒ 'tm set) × ('tm ⇒ 'fm list) ⇒ bool› (infix ‹↝⇩γ› 50)
  assumes gamma_map: ‹⋀ps F qs f. ps ↝⇩γ (F, qs) ⟹ (∃G rs. map (map_fm f) ps ↝⇩γ (G, rs) ∧
      (∀S. map_tm f ` F S ⊆ G (map_fm f ` S)) ∧
      (∀t. map (map_fm f) (qs t) = rs (map_tm f t)))›
    and gamma_mono: ‹⋀ps F qs S S'. ps ↝⇩γ (F, qs) ⟹ S ⊆ S' ⟹ F S ⊆ F S'›
    and gamma_fin: ‹⋀ps F qs t A. ps ↝⇩γ (F, qs) ⟹ t ∈ F A ⟹ ∃B ⊆ A. finite B ∧ t ∈ F B›
begin

inductive cond where
  cond [intro!]: ‹ps ↝⇩γ (F, qs) ⟹ cond ps (λC S. ∀t ∈ F S. set (qs t) ∪ S ∈ C)›

inductive_cases condE[elim!]: ‹cond ps Q›

inductive hint where
  hint [intro!]: ‹(⋀ps F qs. ps ↝⇩γ (F, qs) ⟹ set ps ⊆ H ⟹ (∀t ∈ F H. set (qs t) ⊆ H)) ⟹ hint H›

declare hint.simps[simp]

abbreviation kind :: ‹('x, 'fm) kind› where
  ‹kind ≡ Cond cond hint›

end

sublocale Gamma ⊆ Consistency_Kind map_fm params_fm is_param kind
proof
  fix C
  assume gammaC: ‹sat⇩E kind C›
  then show ‹sat⇩E kind (close C)›
  proof safe
    fix S ps qs F t
    assume ‹S ∈ close C›
    then obtain S' where S': ‹S' ∈ C› and ‹S ⊆ S'›
      unfolding close_def by blast

    assume ‹set ps ⊆ S›
    then have *: ‹set ps ⊆ S'›
      using ‹S ⊆ S'› by blast

    assume **: ‹ps ↝⇩γ (F, qs)› ‹t ∈ F S›
    then have ‹t ∈ F S'›
      using ** gamma_mono ‹S ⊆ S'› by blast
    then have ‹set (qs t) ∪ S' ∈ C›
      using gammaC S' * ** by blast
    then have ‹set (qs t) ∪ S ∈ close C›
      using ‹S ⊆ S'› subset_in_close by blast
    then show ‹set (qs t) ∪ S ∈ close C›
      by (meson close_closed equalityE subset_closed_def sup.mono)
  qed
next
  fix C
  assume gammaC: ‹sat⇩E kind C›
  then show ‹sat⇩A kind (mk_alt_consistency C)›
  proof safe
    fix S ps F qs t

    assume ‹S ∈ mk_alt_consistency C›
    then obtain f where f: ‹is_subst f› ‹map_fm f ` S ∈ C›
      unfolding mk_alt_consistency_def by blast

    let ?C = ‹mk_alt_consistency C›
    let ?S = ‹map_fm f ` S›

    assume ‹set ps ⊆ S›
    then have *: ‹set (map (map_fm f) ps) ⊆ ?S›
      by auto

    assume **: ‹ps ↝⇩γ (F, qs)› and t: ‹t ∈ F S›
    obtain rs G where rs:
      ‹map (map_fm f) ps ↝⇩γ (G, rs)›
      ‹∀S. map_tm f ` F S ⊆ G (map_fm f ` S)›
      ‹∀t. map (map_fm f) (qs t) = rs (map_tm f t)›
      using gamma_map ** by meson
    then have ‹set (rs (map_tm f t)) ∪ ?S ∈ C›
      using gammaC f * t by blast
    then have ‹set (map (map_fm f) (qs t)) ∪ ?S ∈ C›
      using rs by simp
    then show ‹set (qs t) ∪ S ∈ ?C›
      unfolding mk_alt_consistency_def using f by (auto simp: image_Un)
  qed
next
  fix C
  assume gammaAC: ‹sat⇩A kind C› and closedC: ‹subset_closed C›
  then show ‹sat⇩A kind (mk_finite_char C)›
  proof safe
    fix S ps F qs t
    assume ‹S ∈ mk_finite_char C›
    then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
      unfolding mk_finite_char_def by blast

    have sc: ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
      using closedC unfolding subset_closed_def by blast
    then have sc': ‹⋀S' x. x ∪ S' ∈ C ⟹ ∀S ⊆ x ∪ S'. S ∈ C›
      by blast

    assume *: ‹set ps ⊆ S› and **: ‹ps ↝⇩γ (F, qs)› and t: ‹t ∈ F S›

    show ‹set (qs t) ∪ S ∈ mk_finite_char C›
      unfolding mk_finite_char_def 
    proof safe
      fix S'
      assume 1: ‹S' ⊆ set (qs t) ∪ S› and 2: ‹finite S'›

      obtain A where A: ‹A ⊆ S› ‹finite A› ‹S' ⊆ set (qs t) ∪ A› 
        using 1 2 by (meson Diff_subset_conv equalityD2 finite_Diff)

      obtain B where B: ‹B ⊆ S› ‹finite B› ‹t ∈ F B›
        using ** t gamma_fin by meson

      let ?S = ‹set ps ∪ A ∪ B›

      have ‹finite ?S›
        using A(2) B(2) by blast
      moreover have ‹?S ⊆ S›
        using * A(1) B(1) by simp
      ultimately have ‹?S ∈ C›
        using finc by simp

      moreover have ‹set ps ⊆ ?S›
        by blast
      moreover have ‹t ∈ F ?S›
        using ** B(3) gamma_mono by blast
      ultimately have ‹set (qs t) ∪ ?S ∈ C›
        using ** gammaAC by blast

      moreover have ‹S' ⊆ set (qs t) ∪ ?S›
        using A(3) by blast
      ultimately show ‹S' ∈ C›
        using sc by blast
    qed
  qed
next
  fix C S
  assume *: ‹sat⇩E kind C› ‹S ∈ C› ‹maximal C S› 
  show ‹sat⇩H kind S›
  proof safe
    fix ps F qs t
    assume **: ‹set ps ⊆ S› ‹ps ↝⇩γ (F, qs)›
    then have ‹∀t ∈ F S. set (qs t) ∪ S ∈ C›
      using * by blast
    then have ‹∀t ∈ F S. set (qs t) ⊆ S›
      using ‹maximal C S› unfolding maximal_def by fast
    then show ‹t ∈ F S ⟹ x ∈ set (qs t) ⟹ x ∈ S› for x
      by blast
  qed
qed

locale Derivational_Gamma = Gamma map_tm map_fm params_fm is_param classify
  for
    map_tm :: ‹('x ⇒ 'x) ⇒ 'tm ⇒ 'tm› and
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ ('fm set ⇒ 'tm set) × ('tm ⇒ 'fm list) ⇒ bool› (infix ‹↝⇩γ› 50) +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀S ps F qs t. set ps ⊆ S ⟹ ps ↝⇩γ (F, qs) ⟹ t ∈ F S ⟹ ⊢ S ⟹ ⊢ set (qs t) ∪ S›

sublocale Derivational_Gamma ⊆ Derivational_Kind map_fm params_fm is_param kind consistent
  using infinite_params_left consistent enough_new_def by unfold_locales blast+

locale Weak_Derivational_Gamma = Gamma map_tm map_fm params_fm is_param classify
  for
    map_tm :: ‹('x ⇒ 'x) ⇒ 'tm ⇒ 'tm› and
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ ('fm set ⇒ 'tm set) × ('tm ⇒ 'fm list) ⇒ bool› (infix ‹↝⇩γ› 50) +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀A ps F qs t. set ps ⊆ set A ⟹ ps ↝⇩γ (F, qs) ⟹ t ∈ F (set A) ⟹ ⊢ A ⟹ ⊢ qs t @ A›

sublocale Weak_Derivational_Gamma ⊆ Weak_Derivational_Kind map_fm params_fm is_param kind consistent
proof
  show ‹sat⇩E kind {S. ∃A. set A = S ∧ ⊢ A}›
  proof safe
    fix ps qs A F t
    assume *: ‹set ps ⊆ set A› ‹ps ↝⇩γ (F, qs)› ‹⊢ A› ‹t ∈ F (set A)›
    then show ‹∃B. set B = set (qs t) ∪ set A ∧ ⊢ B›
      using consistent[of ps A F qs t] by (meson set_append)
  qed
qed

locale Gamma_UNIV = Params map_fm params_fm is_param
  for
    map_tm :: ‹('x ⇒ 'x) ⇒ 'tm ⇒ 'tm› and
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes classify :: ‹'fm list ⇒ ('tm ⇒ 'fm list) ⇒ bool› (infix ‹↝⇩γ''› 50)
  assumes gamma_map_UNIV: ‹⋀ps qs f. ps ↝⇩γ' qs ⟹ ∃rs. map (map_fm f) ps ↝⇩γ' rs ∧
      (∀t. map (map_fm f) (qs t) = rs (map_tm f t))›
begin

abbreviation (input) classify_UNIV where
  ‹classify_UNIV ≡ λps (F, qs). (F = (λ_. UNIV)) ∧ ps ↝⇩γ' qs›

end

sublocale Gamma_UNIV ⊆ Gamma map_tm map_fm params_fm is_param classify_UNIV
proof
  show ‹⋀ps F qs f.
       (case (F, qs) of (F, qs) ⇒ F = (λ_. UNIV) ∧ ps ↝⇩γ' qs) ⟹
       ∃G rs.
          (case (G, rs) of (F, qs) ⇒ F = (λ_. UNIV) ∧ map (map_fm f) ps ↝⇩γ' qs) ∧
          (∀S. map_tm f ` F S ⊆ G (map_fm f ` S)) ∧ (∀t. map (map_fm f) (qs t) = rs (map_tm f t))›
    using gamma_map_UNIV image_subset_iff by fastforce
  show ‹⋀ps F qs S S'. (case (F, qs) of (F, qs) ⇒ F = (λ_. UNIV) ∧ ps ↝⇩γ' qs) ⟹ S ⊆ S' ⟹ F S ⊆ F S'›
    by simp
  show ‹⋀ps F qs t A. (case (F, qs) of (F, qs) ⇒ F = (λ_. UNIV) ∧ ps ↝⇩γ' qs) ⟹ t ∈ F A ⟹ ∃B⊆A. finite B ∧ t ∈ F B›
    by blast
qed

section ‹Delta›

locale Delta = Params map_fm params_fm is_param
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes δ :: ‹'fm ⇒ 'x ⇒ 'fm list›
  assumes delta_map: ‹⋀p f x. is_param x ⟹ is_subst f ⟹ δ (map_fm f p) (f x) = map (map_fm f) (δ p x)›
begin

abbreviation ‹kind ≡ Wits δ›
end

sublocale Delta ⊆ Consistency_Kind map_fm params_fm is_param kind
proof
  fix C
  assume deltaC: ‹sat⇩E kind C›
  then show ‹sat⇩E kind (close C)›
  proof safe
    fix S p qs q
    assume ‹S ∈ close C›
    then obtain S' where S': ‹S' ∈ C› and ‹S ⊆ S'›
      unfolding close_def by blast

    assume ‹p ∈ S›
    then have *: ‹p ∈ S'›
      using ‹S ⊆ S'› by blast

    have ‹∃x. is_param x ∧ set (δ p x) ∪ S' ∈ C›
      using deltaC S' * by blast
    then show ‹∃x. is_param x ∧ set (δ p x) ∪ S ∈ close C›
      using ‹S ⊆ S'› by (metis subset_in_close)

  qed
next
  fix C
  assume deltaC: ‹sat⇩E kind C›
  then show ‹sat⇩A kind (mk_alt_consistency C)›
  proof safe
    fix S p qs x

    assume ‹S ∈ mk_alt_consistency C›
    then obtain f where f: ‹is_subst f› ‹map_fm f ` S ∈ C›
      unfolding mk_alt_consistency_def by blast

    let ?C = ‹mk_alt_consistency C›
    let ?S = ‹map_fm f ` S›

    assume ‹p ∈ S›
    then have *: ‹map_fm f p ∈ ?S›
      by auto

    assume x: ‹x ∉ params S› ‹is_param x›
    obtain y where y: ‹is_param y› ‹set (δ (map_fm f p) y) ∪ ?S ∈ C›
      using deltaC f * by blast

    let ?g = ‹f(x := y)›

    have g: ‹is_subst ?g›
      using f x y unfolding is_subst_def by simp

    have ‹∀x ∈ params S. f x = ?g x›
      using x by simp
    then have S: ‹∀q ∈ S. map_fm ?g q = map_fm f q›
      using map_params_fm by simp
    then have ‹map_fm ?g p = map_fm f p›
      using ‹p ∈ S› by auto

    moreover have ‹set (δ (map_fm f p) (?g x)) ∪ ?S ∈ C›
      using y by simp
    ultimately have ‹set (map (map_fm ?g) (δ p x)) ∪ ?S ∈ C›
      using delta_map x g by metis
    then have ‹∃f. is_subst f ∧ set (map (map_fm f) (δ p x)) ∪ map_fm f ` S ∈ C›
      using S g by (metis image_cong)
    then show ‹set (δ p x) ∪ S ∈ ?C›
      unfolding mk_alt_consistency_def
      by (metis (mono_tags, lifting) image_Un image_set mem_Collect_eq)
  qed
next
  fix C
  assume deltaAC: ‹sat⇩A kind C› and closedC: ‹subset_closed C›
  then show ‹sat⇩A kind (mk_finite_char C)›
  proof safe
    fix S p qs x
    assume ‹S ∈ mk_finite_char C›
    then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
      unfolding mk_finite_char_def by blast

    have sc: ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
      using closedC unfolding subset_closed_def by blast
    then have sc': ‹⋀S' x. x ∪ S' ∈ C ⟹ ∀S ⊆ x ∪ S'. S ∈ C›
      by blast

    assume *: ‹p ∈ S› and x: ‹x ∉ params S› ‹is_param x›
    show ‹set (δ p x) ∪ S ∈ mk_finite_char C›
      unfolding mk_finite_char_def
    proof safe
      fix S'
      let ?S' = ‹{p} ∪ (S' - set (δ p x))›

      assume ‹S' ⊆ set (δ p x) ∪ S› and ‹finite S'›
      then have ‹?S' ⊆ S›
        using * by fast
      moreover have ‹finite ?S'›
        using ‹finite S'› by blast
      ultimately have ‹?S' ∈ C›
        using finc by blast
      moreover have ‹∀a ∈ ?S'. x ∉ params_fm a›
        using x ‹?S' ⊆ S› by blast
      ultimately have ‹set (δ p x) ∪ ?S' ∈ C›
        using x deltaAC by blast
      then show ‹S' ∈ C›
        using sc by fast
    qed
  qed
next
  show ‹⋀C S. sat⇩E kind C ⟹ S ∈ C ⟹ maximal C S ⟹ sat⇩H kind S›
    using sat⇩H_Wits .
qed

locale Derivational_Delta = Delta map_fm params_fm is_param δ
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    δ :: ‹'fm ⇒ 'x ⇒ 'fm list› +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀S p x. p ∈ S ⟹ is_param x ⟹ x ∉ params S ⟹ ⊢ S ⟹ ⊢ set (δ p x) ∪ S›

sublocale Derivational_Delta ⊆ Derivational_Kind map_fm params_fm is_param kind consistent
proof
  assume inf: ‹infinite (UNIV :: 'fm set)›
  show ‹sat⇩E kind {A. enough_new A ∧ ⊢ A}›
  proof safe
    fix S p
    assume *: ‹p ∈ S› ‹enough_new S› ‹⊢ S›
    then have ‹infinite (Collect is_param - (params ({p} ∪ S)))›
      unfolding enough_new_def using card_of_ordLeq_finite inf by auto
    then obtain x where ‹is_param x› ‹x ∉ params ({p} ∪ S)›
      using infinite_imp_nonempty by blast
    then have ‹∃x. is_param x ∧ ⊢ set (δ p x) ∪ S›
      using *(1,3) consistent ‹⊢ S› by fast
    then show ‹∃x. is_param x ∧ set (δ p x) ∪ S ∈ {A. enough_new A ∧ ⊢ A}›
      using * inf infinite_params_left unfolding enough_new_def by blast
  qed
qed

locale Weak_Derivational_Delta = Delta map_fm params_fm is_param δ
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    δ :: ‹'fm ⇒ 'x ⇒ 'fm list› +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀A p x. p ∈ set A ⟹ is_param x ⟹ x ∉ params (set A) ⟹ ⊢ A ⟹ ⊢ δ p x @ A›

sublocale Weak_Derivational_Delta ⊆ Weak_Derivational_Kind map_fm params_fm is_param kind consistent
proof
  assume inf: ‹infinite (Collect is_param :: 'x set)›
  show ‹sat⇩E kind {S. ∃A. set A = S ∧ ⊢ A}›
  proof safe
    fix p A
    assume *: ‹p ∈ set A› ‹⊢ A›
    then have ‹infinite (Collect is_param - (params (set (p # A))))›
      using inf finite_compl by fastforce
    then obtain x where ‹is_param x› ‹x ∉ params (set (p # A))›
      using infinite_imp_nonempty by blast
    then have ‹∃x. is_param x ∧ ⊢ δ p x @ A›
      using * consistent[of p A x] by auto
    then show ‹∃x. is_param x ∧ set (δ p x) ∪ set A ∈ {S. ∃A. set A = S ∧ ⊢ A}›
      by (metis (mono_tags, lifting) CollectI set_append)
  qed
qed

section ‹Modal›

text ‹
  The Hintikka property you want depends on the concrete logic.
  See Term-Modal Logics by Fitting, Thalmann and Voronkov, p. 156 bottom.
›

locale Modal = Params map_fm params_fm is_param
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› +
  fixes classify :: ‹'fm list ⇒ ('fm set ⇒ 'fm set) × 'fm list ⇒ bool› (infix ‹↝⇩□› 50)
    and hint :: ‹'fm set ⇒ bool›
  assumes modal_map: ‹⋀ps F qs f. ps ↝⇩□ (F, qs) ⟹ ∃G. map (map_fm f) ps ↝⇩□ (G, map (map_fm f) qs) ∧
      (∀S. map_fm f ` F S ⊆ G (map_fm f ` S))›
    and modal_mono: ‹⋀ps F qs S S'. ps ↝⇩□ (F, qs) ⟹ S ⊆ S' ⟹ F S ⊆ F S'›
    and modal_fin: ‹⋀ps F qs S A. ps ↝⇩□ (F, qs) ⟹ finite A ⟹ A ⊆ F S ⟹ ∃S' ⊆ S. finite S' ∧ A ⊆ F S'›
begin

inductive cond where
  cond [intro!]: ‹ps ↝⇩□ (F, qs) ⟹ cond ps (λC S. set qs ∪ F S ∈ C)›

inductive_cases condE[elim!]: ‹cond ps Q›

abbreviation kind :: ‹('x, 'fm) kind› where
  ‹kind ≡ Cond cond hint›

end

locale ModalH = Modal map_fm params_fm is_param classify hint
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ ('fm set ⇒ 'fm set) × 'fm list ⇒ bool› (infix ‹↝⇩□› 50) and
    hint :: ‹'fm set ⇒ bool› +
  assumes modal_hintikka: ‹⋀C S. sat⇩E kind C ⟹ S ∈ C ⟹ maximal C S ⟹ sat⇩H kind S›

sublocale ModalH ⊆ Consistency_Kind map_fm params_fm is_param kind
proof
  fix C
  assume modalC: ‹sat⇩E kind C›
  then show ‹sat⇩E kind (close C)›
  proof safe
    fix S ps F qs
    assume ‹S ∈ close C›
    then obtain S' where S': ‹S' ∈ C› and ‹S ⊆ S'›
      unfolding close_def by blast

    assume ‹set ps ⊆ S›
    then have *: ‹set ps ⊆ S'›
      using ‹S ⊆ S'› by blast

    assume **: ‹ps ↝⇩□ (F, qs)›
    then have ‹set qs ∪ F S' ∈ C›
      using modalC S' * ** by blast
    then show ‹set qs ∪ F S ∈ close C›
      using ‹S ⊆ S'› subset_in_close ** modal_mono by metis
  qed
next
  fix C
  assume modalC: ‹sat⇩E kind C› and closedC: ‹subset_closed C›
  then show ‹sat⇩A kind (mk_alt_consistency C)›
  proof safe
    fix S ps F qs

    assume ‹S ∈ mk_alt_consistency C›
    then obtain f where f: ‹is_subst f› ‹map_fm f ` S ∈ C›
      unfolding mk_alt_consistency_def by blast

    let ?C = ‹mk_alt_consistency C›
    let ?S = ‹map_fm f ` S›

    assume ‹set ps ⊆ S›
    then have *: ‹set (map (map_fm f) ps) ⊆ ?S›
      by auto

    assume **: ‹ps ↝⇩□ (F, qs)›
    obtain G where G:
      ‹map (map_fm f) ps ↝⇩□ (G, map (map_fm f) qs)›
      ‹∀S. map_fm f ` F S ⊆ G (map_fm f ` S)›
      using modal_map ** by meson
    then have ‹set (map (map_fm f) qs) ∪ G ?S ∈ C›
      using modalC f * by blast
    then have ‹set (map (map_fm f) qs) ∪ map_fm f ` F S ∈ C›
      using G closedC unfolding subset_closed_def by (meson Un_mono order_refl)
    then show ‹set qs ∪ F S ∈ ?C›
      unfolding mk_alt_consistency_def using f
      by (auto split: option.splits simp: image_Un)
  qed
next
  fix C
  assume modalAC: ‹sat⇩A kind C› and closedC: ‹subset_closed C›
  then show ‹sat⇩A kind (mk_finite_char C)›
  proof safe
    fix S ps F qs t
    assume S: ‹S ∈ mk_finite_char C›
    then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
      unfolding mk_finite_char_def by blast

    have sc: ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
      using closedC unfolding subset_closed_def by blast
    then have sc': ‹⋀S' x. x ∪ S' ∈ C ⟹ ∀S ⊆ x ∪ S'. S ∈ C›
      by blast

    assume *: ‹set ps ⊆ S› and **: ‹ps ↝⇩□ (F, qs)›

    show ‹set qs ∪ F S ∈ mk_finite_char C›
      unfolding mk_finite_char_def 
    proof safe
      fix S'
      assume 1: ‹S' ⊆ set qs ∪ F S› and 2: ‹finite S'›

      obtain A where A: ‹A ⊆ S› ‹finite A› ‹S' ⊆ set qs ∪ F A› 
        using 1 2 ** modal_fin by (meson Diff_subset_conv finite_Diff)

      let ?S = ‹set ps ∪ A›

      have ‹finite ?S›
        using A(2) by blast
      moreover have ‹?S ⊆ S›
        using * A(1) by simp
      ultimately have ‹?S ∈ C›
        using finc by simp

      moreover have ‹set ps ⊆ ?S›
        by blast
      ultimately have ‹set qs ∪ F ?S ∈ C›
        using ** modalAC by blast

      moreover have ‹S' ⊆ set qs ∪ F ?S›
        using A(3) ** modal_mono by (meson Diff_subset_conv inf_sup_ord(4) subset_trans)
      ultimately show ‹S' ∈ C›
        using sc by blast
    qed
  qed
next
  fix C S
  assume *: ‹sat⇩E kind C› ‹S ∈ C› ‹maximal C S› 
  then show ‹sat⇩H kind S›
    using modal_hintikka by simp
qed

locale Derivational_Modal = ModalH map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ ('fm set ⇒ 'fm set) × 'fm list ⇒ bool› (infix ‹↝⇩□› 50) +
  fixes consistent :: ‹'fm set ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀S ps F qs. set ps ⊆ S ⟹ ps ↝⇩□ (F, qs) ⟹ ⊢ S ⟹ ⊢ set qs ∪ F S›
    and params_subset: ‹⋀ps F qs S. ps ↝⇩□ (F, qs) ⟹ params (F S) ⊆ params S›

sublocale Derivational_Modal ⊆ Derivational_Kind map_fm params_fm is_param kind consistent
proof
  assume inf: ‹infinite (UNIV :: 'fm set)›
  then show ‹sat⇩E kind {A. enough_new A ∧ ⊢ A}›
  proof safe
    fix S ps F qs
    assume ‹ps ↝⇩□ (F, qs)› ‹enough_new S›
    then have ‹enough_new (F S)›
      unfolding enough_new_def using params_subset[of ps F qs S] ordLeq_transitive
        card_of_mono1[of "Collect is_param - params S" "Collect is_param - params (F S)"]
      by blast
    then show ‹enough_new (set qs ∪ F S)›
      using infinite_params_left[OF inf] unfolding enough_new_def by blast
  qed (use consistent in blast)
qed

locale Weak_Derivational_Modal = ModalH map_fm params_fm is_param classify
  for
    map_fm :: ‹('x ⇒ 'x) ⇒ 'fm ⇒ 'fm› and
    params_fm :: ‹'fm ⇒ 'x set› and
    is_param :: ‹'x ⇒ bool› and
    classify :: ‹'fm list ⇒ ('fm set ⇒ 'fm set) × 'fm list ⇒ bool› (infix ‹↝⇩□› 50) +
  fixes consistent :: ‹'fm list ⇒ bool› (‹⊢ _› [51] 50)
  assumes consistent: ‹⋀S ps F qs S'. set ps ⊆ set S ⟹ ps ↝⇩□ (F, qs) ⟹ ⊢ S ⟹ set S' = F (set S) ⟹ ⊢ qs @ S'›
    and params_subset: ‹⋀ps F qs S. ps ↝⇩□ (F, qs) ⟹ params (F S) ⊆ params S›
    and F_size: ‹⋀ps F qs S. ps ↝⇩□ (F, qs) ⟹ |F S| ≤o |S|›

sublocale Weak_Derivational_Modal ⊆ Weak_Derivational_Kind map_fm params_fm is_param kind consistent
proof
  assume inf: ‹infinite (Collect is_param :: 'x set)›
  show ‹sat⇩E kind {S. ∃A. set A = S ∧ ⊢ A}›
  proof safe
    fix ps qs A F
    assume ‹set ps ⊆ set A› ‹ps ↝⇩□ (F, qs)› ‹⊢ A›
    then show ‹∃B. set B = set qs ∪ F (set A) ∧ ⊢ B›
      using consistent[of ps A F qs] F_size
      by (metis card_of_ordLeq_infinite finite_list list.set_finite set_append)
  qed
qed

end