Theory Example_Bounded_FOL

(*
  File: Example_Bounded_FOL.thy
  Title: Completeness and Compactness Proofs for a First-Order Logic Calculus with a Restriction
         on Universal Quantifier Elimination.
  Author: Asta Halkjær Boserup, 2025-2026.
*)

chapter ‹Example: First-Order Logic with Restricted Instantiation›

theory Example_Bounded_FOL imports
  Abstract_Consistency_Property
begin

section ‹Syntax›

datatype (params_tm: 'f) tm
  = Var nat (‹❙#›)
  | Fun 'f ‹'f tm list› (‹❙○›)

abbreviation Const (‹❙⋆›) where ‹❙⋆a ≡ ❙○a []›

datatype (params_fm: 'f, 'p) fm
  = Fls (‹❙⊥›)
  | Pre 'p ‹'f tm list› (‹❙⋅›)
  | Imp ‹('f, 'p) fm› ‹('f, 'p) fm› (infixr ‹❙⟶› 55)
  | Uni ‹('f, 'p) fm› (‹❙∀›)

abbreviation Neg :: ‹('f, 'p) fm ⇒ ('f, 'p) fm› (‹❙¬ _› [70] 70) where
  ‹❙¬ p ≡ p ❙⟶ ❙⊥›

abbreviation has_subterm :: ‹('f, 'p) fm› where
  ‹has_subterm ≡ ❙⋅undefined [❙#0] ❙⟶ ❙⋅undefined [❙#0]›

abbreviation with_subterm :: ‹('f, 'p) fm ⇒ ('f, 'p) fm› where
  ‹with_subterm p ≡ has_subterm ❙⟶ p›

section ‹Semantics›

datatype ('a, 'f, 'p) model = Model ‹'a set› ‹nat ⇒ 'a› ‹'f ⇒ 'a list ⇒ 'a› ‹'p ⇒ 'a list ⇒ bool›

primrec wf_model :: ‹('a, 'f, 'p) model ⇒ bool› where
  ‹wf_model (Model U E F G) ⟷ (∀n. E n ∈ U) ∧ (∀f ts. F f ts ∈ U)›

fun semantics_tm :: ‹(nat ⇒ 'a) × ('f ⇒ 'a list ⇒ 'a) ⇒ 'f tm ⇒ 'a› (‹⦉_⦊›) where
  ‹⦉(E, _)⦊ (❙#n) = E n›
| ‹⦉(E, F)⦊ (❙○f ts) = F f (map ⦉(E, F)⦊ ts)›

primrec add_env :: ‹'a ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'a› (infix ‹⪢› 0) where
  ‹(t ⪢ s) 0 = t›
| ‹(t ⪢ s) (Suc n) = s n›

fun semantics_fm :: ‹('a, 'f, 'p) model ⇒ ('f, 'p) fm ⇒ bool› (infix ‹⊨› 50) where
  ‹(_ ⊨ ❙⊥) = False›
| ‹(Model _ E F G ⊨ ❙⋅P ts) = G P (map ⦉(E, F)⦊ ts)›
| ‹(Model U E F G ⊨ p ❙⟶ q) = (Model U E F G ⊨ p ⟶ Model U E F G ⊨ q)›
| ‹(Model U E F G ⊨ ❙∀p) = (∀x ∈ U. Model U (x ⪢ E) F G ⊨ p)›

section ‹Operations›

primrec lift_tm :: ‹'f tm ⇒ 'f tm› where
  ‹lift_tm (❙#n) = ❙#(n+1)›
| ‹lift_tm (❙○f ts) = ❙○f (map lift_tm ts)›

primrec sub_tm :: ‹(nat ⇒ 'f tm) ⇒ 'f tm ⇒ 'f tm› where
  ‹sub_tm s (❙#n) = s n›
| ‹sub_tm s (❙○f ts) = ❙○f (map (sub_tm s) ts)›

primrec sub_fm :: ‹(nat ⇒ 'f tm) ⇒ ('f, 'p) fm ⇒ ('f, 'p) fm› where
  ‹sub_fm _ ❙⊥ = ❙⊥›
| ‹sub_fm s (❙⋅P ts) = ❙⋅P (map (sub_tm s) ts)›
| ‹sub_fm s (p ❙⟶ q) = sub_fm s p ❙⟶ sub_fm s q›
| ‹sub_fm s (❙∀p) = ❙∀(sub_fm (❙#0 ⪢ λn. lift_tm (s n)) p)›

abbreviation inst_single :: ‹'f tm ⇒ ('f, 'p) fm ⇒ ('f, 'p) fm› (‹⟨_⟩›) where
  ‹⟨t⟩ ≡ sub_fm (t ⪢ ❙#)›

abbreviation psub :: ‹('f ⇒ 'g) ⇒ ('f, 'p) fm ⇒ ('g, 'p) fm› where
  ‹psub f ≡ map_fm f id›

primrec size_fm :: ‹('f, 'p) fm ⇒ nat› where
  ‹size_fm ❙⊥ = 1›
| ‹size_fm (❙⋅_ _) = 1›
| ‹size_fm (p ❙⟶ q) = 1 + size_fm p + size_fm q›
| ‹size_fm (❙∀p) = 1 + size_fm p›

subsection ‹Lemmas›

lemma wf_model_tm [simp]: ‹wf_model (Model U E F G) ⟹ ⦉(E, F)⦊ t ∈ U›
  by (induct t) simp_all

lemma size_sub_fm [simp]: ‹size_fm (sub_fm s p) = size_fm p›
  by (induct p arbitrary: s) simp_all

lemma upd_params_tm [simp]: ‹f ∉ params_tm t ⟹ ⦉(E, F(f := x))⦊ t = ⦉(E, F)⦊ t›
  by (induct t) (auto cong: map_cong)

lemma upd_params_fm [simp]:
  assumes ‹f ∉ params_fm p›
  shows ‹Model U E (F(f := x)) G ⊨ p ⟷ Model U E F G ⊨ p›
  using assms by (induct p arbitrary: E) (auto cong: map_cong)

lemma finite_params_tm [simp]: ‹finite (params_tm t)›
  by (induct t) simp_all

lemma finite_params_fm' [simp]: ‹finite (params_fm p)›
  by (induct p) simp_all

lemma env [simp]: ‹P ((x ⪢ E) n) = (P x ⪢ λn. P (E n)) n›
  by (induct n) simp_all

lemma lift_lemma: ‹⦉(x ⪢ E, F)⦊ (lift_tm t) = ⦉(E, F)⦊ t›
  by (induct t) (auto cong: map_cong)

lemma sub_tm_semantics: ‹⦉(E, F)⦊ (sub_tm s t) = ⦉(λn. ⦉(E, F)⦊ (s n), F)⦊ t›
  by (induct t) (auto cong: map_cong)

lemma sub_fm_semantics [simp]:
  ‹Model U E F G ⊨ sub_fm s p ⟷ Model U (λn. ⦉(E, F)⦊ (s n)) F G ⊨ p›
  by (induct p arbitrary: E s) (auto cong: map_cong simp: sub_tm_semantics lift_lemma)

lemma map_tm_sub_tm [simp]: ‹map_tm f (sub_tm g t) = sub_tm (map_tm f o g) (map_tm f t)›
  by (induct t) simp_all

lemma map_tm_lift_tm [simp]: ‹map_tm f (lift_tm t) = lift_tm (map_tm f t)›
  by (induct t) simp_all

lemma psub_sub_fm: ‹psub f (sub_fm g p) = sub_fm (map_tm f o g) (psub f p)›
  by (induct p arbitrary: g) (simp_all add: comp_def)

lemma map_tm_inst_single: ‹(map_tm f o (u ⪢ ❙#)) t = (map_tm f u ⪢ ❙#) t›
  by (induct t) auto

lemma psub_inst_single [simp]: ‹psub f (⟨t⟩p) = ⟨map_tm f t⟩(psub f p)›
  unfolding psub_sub_fm map_tm_inst_single ..

section ‹Terms›

primrec terms_tm :: ‹'f tm ⇒ 'f tm set› where
  ‹terms_tm (❙#n) = {❙#n}›
| ‹terms_tm (❙○f ts) = {❙○f ts} ∪ ⋃(set (map terms_tm ts))›

primrec terms_fm :: ‹('f, 'p) fm ⇒ 'f tm set› where
  ‹terms_fm ❙⊥ = {}›
| ‹terms_fm (❙⋅_ ts) = ⋃(set (map terms_tm ts))›
| ‹terms_fm (p ❙⟶ q) = terms_fm p ∪ terms_fm q›
| ‹terms_fm (❙∀p) = terms_fm p›

definition terms :: ‹('f, 'p) fm set ⇒ 'f tm set› where
  ‹terms S ≡ ⋃p ∈ S. terms_fm p›

subsection ‹Lemmas›

lemma terms_mono: ‹S ⊆ S' ⟹ terms S ⊆ terms S'›
  unfolding terms_def by blast

lemma terms_tm_refl [intro]: ‹t ∈ terms_tm t›
  by (induct t) simp_all

lemma terms_tm_trans [trans]: ‹s ∈ terms_tm t ⟹ r ∈ terms_tm s ⟹ r ∈ terms_tm t›
  by (induct t) auto

lemma map_terms_tm [simp]: ‹terms_tm (map_tm f t) = map_tm f ` terms_tm t›
  by (induct t) auto

lemma map_terms_fm [simp]: ‹terms_fm (map_fm f g p) = map_tm f ` terms_fm p›
  by (induct p) auto

lemma terms_tm_closed [dest]: ‹t ∈ terms_tm s ⟹ terms_tm t ⊆ terms_tm s›
  using terms_tm_trans by blast

lemma terms_fm_closed: ‹t ∈ terms_fm p ⟹ terms_tm t ⊆ terms_fm p›
  by (induct p) auto

lemma terms_source: ‹t ∈ terms S ⟹ ∃S' ⊆ S. finite S' ∧ t ∈ terms S'›
  unfolding terms_def using insert_subset by blast

lemma terms_tm_Fun: ‹❙○f ts ∈ terms_tm s ⟹ t ∈ set ts ⟹ t ∈ terms_tm s›
  using terms_tm_refl terms_tm_trans
  by (metis UN_I UnI2 list.set_map terms_tm.simps(2))

lemma terms_Fun: ‹❙○f ts ∈ terms S ⟹ set ts ⊆ terms S›
  using terms_tm_Fun terms_tm_refl terms_fm_closed
  unfolding terms_def by fast

section ‹Guard›

definition guard :: ‹'a ⇒ 'a set ⇒ 'a› (infix ‹∈?› 50) where
  ‹x ∈? S ≡ if x ∈ S then x else SOME y. y ∈ S›

lemma guard_in: ‹S ≠ {} ⟹ (x ∈? S) ∈ S›
  unfolding guard_def using some_in_eq by auto

lemma guard_refl [simp]: ‹t ∈ S ⟹ t ∈? S = t›
  unfolding guard_def by simp

section ‹Model Existence›

inductive
  confl_class :: ‹('f, 'p) fm list ⇒ ('f, 'p) fm list ⇒ bool› (infix ‹↝⇩✗› 50) and
  alpha_class :: ‹('f, 'p) fm list ⇒ ('f, 'p) fm list ⇒ bool› (infix ‹↝⇩α› 50) and
  beta_class :: ‹('f, 'p) fm list ⇒ ('f, 'p) fm list ⇒ bool› (infix ‹↝⇩β› 50) and
  gamma_class :: ‹('f, 'p) fm list ⇒ (('f, 'p) fm set ⇒ _) × ('f tm ⇒ _) ⇒ bool› (infix ‹↝⇩γ› 50)
  where
    CFls [intro]: ‹[ ❙⊥ ] ↝⇩✗ [ ❙⊥ ]›
  | CNeg [intro]: ‹[ ❙¬ (❙⋅P ts) ] ↝⇩✗ [ ❙⋅P ts ]›
  | CImpN [intro]: ‹[ ❙¬ (p ❙⟶ q) ] ↝⇩α [ p, ❙¬ q ]›
  | CImpP [intro]: ‹[ p ❙⟶ q ] ↝⇩β [ ❙¬ p, q ]›
  | CAllP [intro]: ‹[ ❙∀p ] ↝⇩γ (terms, λt. [ ⟨t⟩p ])›

fun δ :: ‹('f, 'p) fm ⇒ 'f ⇒ ('f, 'p) fm list› where
  ‹δ (❙¬ ❙∀p) x = [ ❙¬ ⟨❙⋆x⟩p ]›
| ‹δ _ _ = []›

interpretation P: Params psub params_fm ‹λ_. True›
  by unfold_locales (auto simp: fm.map_id0 cong: fm.map_cong0)

interpretation C: Confl psub params_fm ‹λ_. True› confl_class
  by unfold_locales (auto elim!: confl_class.cases)

interpretation A: Alpha psub params_fm ‹λ_. True› alpha_class
  by unfold_locales (auto elim!: alpha_class.cases)

interpretation B: Beta psub params_fm ‹λ_. True› beta_class
  by unfold_locales (auto elim!: beta_class.cases)

interpretation G: Gamma map_tm psub params_fm ‹λ_. True› gamma_class
proof
  show ‹⋀ps F qs t A. ps ↝⇩γ (F, qs) ⟹ t ∈ F A ⟹ ∃B ⊆ A. finite B ∧ t ∈ F B›
    by (elim gamma_class.cases) (auto simp: terms_source)  
qed (fastforce simp: terms_def elim: gamma_class.cases)+

interpretation D: Delta psub params_fm ‹λ_. True› δ
proof
  show ‹⋀f. δ (psub f p) (f x) = map (psub f) (δ p x)› for p :: ‹('f, 'p) fm› and x
    by (induct p x rule: δ.induct) simp_all
qed

abbreviation Kinds :: ‹('f, ('f, 'p) fm) kind list› where
  ‹Kinds ≡ [C.kind, A.kind, B.kind, G.kind, D.kind]›

lemma prop⇩E_Kinds [intro]:
  assumes ‹P.sat⇩E C.kind C› ‹P.sat⇩E A.kind C› ‹P.sat⇩E B.kind C› ‹P.sat⇩E G.kind C› ‹P.sat⇩E D.kind C›
  shows ‹P.prop⇩E Kinds C›
  unfolding P.prop⇩E_def using assms by simp

interpretation Consistency_Kinds psub params_fm ‹λ_. True› Kinds
  using P.Params_axioms C.Consistency_Kind_axioms A.Consistency_Kind_axioms
    B.Consistency_Kind_axioms G.Consistency_Kind_axioms D.Consistency_Kind_axioms
  by (auto intro: Consistency_Kinds.intro simp: Consistency_Kinds_axioms_def)

interpretation Maximal_Consistency psub params_fm ‹λ_. True› Kinds
proof
  show ‹infinite (UNIV :: ('f, 'p) fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed simp

abbreviation canonical :: ‹('f, 'p) fm set ⇒ ('f tm, 'f, 'p) model› where
  ‹canonical H ≡
  Model (terms H) (λn. ❙#n ∈? terms H) (λf ts. ❙○f ts ∈? terms H) (λP ts. ❙⋅P ts ∈ H)›

lemma wf_canonical:
  assumes ‹terms H ≠ {}›
  shows ‹wf_model (canonical H)›
  using assms guard_in by (metis (no_types, lifting) wf_model.simps)

lemma canonical_tm_id [simp]:
  ‹t ∈ terms H ⟹ ⦉(λn. ❙#n ∈? terms H, λP ts. ❙○P ts ∈? terms H)⦊ t = t›
proof (induct t)
  case (Fun f ts)
  moreover from this have ‹t ∈ set ts ⟹ t ∈ terms H› for t
    by (meson in_mono terms_Fun)
  ultimately show ?case
    by (simp add: list.map_ident_strong)
qed simp

lemma canonical_tm_id_map [simp]:
  ‹set ts ⊆ terms H ⟹ map ⦉(λn. ❙#n ∈? terms H, λP ts. ❙○P ts ∈? terms H)⦊ ts = ts›
  by (induct ts) simp_all

locale MyHintikka = Hintikka psub params_fm ‹λ_. True› Kinds H
  for H :: ‹('f, 'p) fm set› +
  assumes terms_ne: ‹terms H ≠ {}›
begin

lemmas
  confl = sat⇩H[of C.kind] and
  alpha = sat⇩H[of A.kind] and
  beta = sat⇩H[of B.kind] and
  gamma = sat⇩H[of G.kind] and
  delta = sat⇩H[of D.kind]

theorem model: ‹(p ∈ H ⟶ canonical H ⊨ p) ∧ (❙¬ p ∈ H ⟶ ¬ canonical H ⊨ p)›
proof (induct p rule: wf_induct[where r=‹measure size_fm›])
  case 1
  then show ?case
    by simp
next
  case (2 x)
  then show ?case
  proof (cases x)
    case Fls
    then show ?thesis
      using confl by fastforce
  next
    case (Pre P ts)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙⋅P ts› ‹❙⋅P ts ∈ H›
      moreover from this have ‹set ts ⊆ terms H›
        using terms_tm_refl terms_def by fastforce
      ultimately show ‹canonical H ⊨ ❙⋅P ts›
        by simp
    next
      assume ‹x = ❙⋅P ts› ‹❙¬ ❙⋅P ts ∈ H›
      then have ‹❙⋅P ts ∉ H›
        using confl by force
      moreover have ‹set ts ⊆ terms H›
        using ‹❙¬ ❙⋅P ts ∈ H› terms_def terms_tm_refl by fastforce
      ultimately show ‹¬ canonical H ⊨ ❙⋅P ts›
        by simp
    qed
  next
    case (Imp p q)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = p ❙⟶ q› ‹p ❙⟶ q ∈ H›
      then have ‹❙¬ p ∈ H ∨ q ∈ H›
        using beta by force
      then show ‹canonical H ⊨ p ❙⟶ q›
        using 2 Imp by auto
    next
      assume ‹x = p ❙⟶ q› ‹❙¬ (p ❙⟶ q) ∈ H›
      then have ‹p ∈ H ∧ ❙¬ q ∈ H›
        using alpha by force
      then show ‹¬ canonical H ⊨ p ❙⟶ q›
        using 2 Imp by auto
    qed
  next
    case (Uni p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙∀p› ‹❙∀p ∈ H›
      then have ‹∀t ∈ terms H. ⟨t⟩p ∈ H›
        using gamma by fastforce
      moreover have ‹∀t. (⟨t⟩p, ❙∀p) ∈ measure size_fm›
        by simp
      ultimately have ‹∀t ∈ terms H. canonical H ⊨ ⟨t⟩p›
        using 2 ‹x = ❙∀p› by blast
      then show ‹canonical H ⊨ ❙∀p›
        by simp
    next
      assume ‹x = ❙∀p› ‹❙¬ ❙∀p ∈ H›
      then obtain a where ‹❙¬ ⟨❙⋆a⟩p ∈ H›
        using delta by fastforce
      moreover have ‹(⟨❙⋆a⟩p, ❙∀p) ∈ measure size_fm›
        by simp
      ultimately have ‹¬ canonical H ⊨ ⟨❙⋆a⟩p›
        using 2 ‹x = ❙∀p› by blast
      then show ‹¬ canonical H ⊨ ❙∀p›
        using wf_canonical[OF terms_ne] by auto
    qed
  qed
qed

end

theorem model_existence:
  fixes S :: ‹('f, 'p) fm set›
  assumes ‹P.prop⇩E Kinds C›
    and ‹S ∈ C›
    and ‹P.enough_new S›
    and ‹terms S ≠ {}›
    and ‹p ∈ S›
  shows ‹canonical (mk_mcs C S) ⊨ p›
proof -
  have *: ‹MyHintikka (mk_mcs C S)›
  proof
    show ‹terms (mk_mcs C S) ≠ {}›
      using assms(4) terms_mono Extend_subset by blast
  next
    show ‹P.prop⇩H Kinds (mk_mcs C S)›
      using mk_mcs_Hintikka[OF assms(1-3)] Hintikka.hintikka by blast
  qed
  moreover have ‹p ∈ mk_mcs C S›
    using assms(5) Extend_subset by blast
  ultimately show ?thesis
    using MyHintikka.model by blast
qed

section ‹Compactness›

abbreviation semantics_set :: ‹('a, 'f, 'p) model ⇒ ('f, 'p) fm set ⇒ bool› (infix ‹⊫› 50) where
  ‹M ⊫ S ≡ ∀p ∈ S. M ⊨ p›

lemma compact_C: ‹P.sat⇩E C.kind {S :: ('f, 'p) fm set. P.enough_new S ∧
    (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
proof safe
  fix S ps qs and q :: ‹('f, 'p) fm›
  assume ‹ps ↝⇩✗ qs› and *: ‹set ps ⊆ S›
    ‹∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
    ‹q ∈ set qs› ‹q ∈ S›
  then show ‹q ∈ {}›
  proof cases
    case CFls
    then show ?thesis
      using *(1-2) by (meson List.finite_set list.set_intros(1) semantics_fm.simps(1))
  next
    case (CNeg P ts)
    then have ‹{❙⋅P ts, ❙¬ ❙⋅P ts} ⊆ S› ‹finite {❙⋅P ts, ❙¬ ❙⋅P ts}›
      using * by simp_all
    then have ‹∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊨ ❙⋅P ts ∧ Model U E F G ⊨ ❙¬ ❙⋅P ts›
      using * by (meson insertCI)
    then show ?thesis
      by simp
  qed
qed

lemma compact_A: ‹P.sat⇩E A.kind {S :: ('f, 'p) fm set. P.enough_new S ∧
    (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
proof safe
  fix qs and S :: ‹('f, 'p) fm set›
  assume ‹P.enough_new S›
  then show ‹P.enough_new (set qs ∪ S)›
    using params_left by blast
next
  fix ps qs and S S' :: ‹('f, 'p) fm set›
  assume ‹ps ↝⇩α qs› and *: ‹set ps ⊆ S›
    ‹∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
    ‹S' ⊆ set qs ∪ S› ‹finite S'›
  then show ‹∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'›
  proof cases
    case (CImpN p q)
    let ?S = ‹{❙¬ (p ❙⟶ q)} ∪ (S' - {p, ❙¬ q})›
    have ‹?S ⊆ S› ‹finite ?S›
      using CImpN * by fastforce+
    then obtain U :: ‹'a set› and E F G where
      M: ‹wf_model (Model U E F G)› ‹Model U E F G ⊫ ?S›
      using * by meson
    then have ‹Model U E F G ⊫ {p, ❙¬ q} ∪ ?S›
      by auto
    then show ?thesis
      using M(1) by blast
  qed
qed

lemma compact_B: ‹P.sat⇩E B.kind {S :: ('f, 'p) fm set. P.enough_new S ∧
    (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
proof safe
  fix ps qs and S S' :: ‹('f, 'p) fm set›
  assume ‹ps ↝⇩β qs› and *: ‹set ps ⊆ S› ‹P.enough_new S›
    ‹∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
  then show ‹∃q∈set qs. insert q S ∈ {S. P.enough_new S ∧ (∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
  proof cases
    case (CImpP p q)
    then have P: ‹∀q∈set qs. {q} ∪ S ∈ {S. P.enough_new S}›
      using * params_left by (metis List.set_insert insert_is_Un list.set(1) mem_Collect_eq)

    show ?thesis
    proof (rule ccontr)
      assume ‹¬ (∃q∈set qs. insert q S ∈ {S. P.enough_new S ∧ (∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))})›
      then have ‹∀q∈set qs. ∃S' ⊆ {q} ∪ S. finite S' ∧ ¬(∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
        using P by simp
      then have ‹∀q∈set qs. ∃S' ⊆ {q} ∪ S. finite S' ∧ (∀(U :: 'a set) E F G. wf_model (Model U E F G) ⟶ ¬ Model U E F G ⊫ S')›
        by meson
      then obtain Sp Sq where
        Sp: ‹Sp ⊆ {❙¬ p} ∪ S› ‹finite Sp› ‹∀(U :: 'a set) E F G. wf_model (Model U E F G) ⟶ ¬ Model U E F G ⊫ Sp› and
        Sq: ‹Sq ⊆ {q} ∪ S› ‹finite Sq› ‹∀(U :: 'a set) E F G. wf_model (Model U E F G) ⟶ ¬ Model U E F G ⊫ Sq›
        using CImpP by auto

      let ?S = ‹{p ❙⟶ q} ∪ (Sp - {❙¬ p}) ∪ (Sq - {q})›
      have ‹finite ?S›
        using Sp(2) Sq(2) by blast
      moreover have ‹?S ⊆ S›
        using *(1) CImpP(1) Sp(1) Sq(1) by auto
      ultimately obtain U :: ‹'a set› and E F G where
        M: ‹wf_model (Model U E F G)› ‹Model U E F G ⊫ ?S›
        using * by meson
      then have ‹Model U E F G ⊫ Sp ∨ Model U E F G ⊫ Sq›
        by auto
      then show False
        using M(1) Sp(3) Sq(3) by blast
    qed
  qed
qed

lemma compact_G: ‹P.sat⇩E G.kind {S :: ('f, 'p) fm set. P.enough_new S ∧
    (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
proof safe
  fix qs :: ‹'f tm ⇒ ('f, 'p) fm list› and t and S :: ‹('f, 'p) fm set›
  assume ‹P.enough_new S›
  then show ‹P.enough_new (set (qs t) ∪ S)›
    using params_left by fast
next
  fix ps qs F t and S S' :: ‹('f, 'p) fm set›
  assume ‹ps ↝⇩γ (F, qs)› and *: ‹set ps ⊆ S› ‹P.enough_new S›
    ‹∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
    ‹t ∈ F S› ‹S' ⊆ set (qs t) ∪ S› ‹finite S'›
  then show ‹∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'›
  proof cases
  case (CAllP p)
    let ?S = ‹{❙∀p} ∪ (S' - set (qs t))›
    have ‹?S ⊆ S› ‹finite ?S›
      using CAllP * by fastforce+
    then obtain U :: ‹'a set› and E F G where
      M: ‹wf_model (Model U E F G)› ‹Model U E F G ⊫ ?S›
      using * by meson
    then have ‹Model U E F G ⊫ set (qs t) ∪ ?S›
      using CAllP by auto
    then show ?thesis
      using M(1) by blast
  qed
qed

lemma compact_D: ‹P.sat⇩E D.kind {S :: ('f, 'p) fm set. P.enough_new S ∧
    (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
proof safe
  fix p and S :: ‹('f, 'p) fm set›
  assume *: ‹p ∈ S› ‹P.enough_new S›
    ‹∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
  then show ‹∃x. True ∧ set (δ p x) ∪ S ∈ {S. P.enough_new S ∧
    (∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
  proof (induct p _ rule: δ.induct)
    case (1 p _)
    then have P: ‹∀x. set (δ (❙¬ ❙∀ p) x) ∪ S ∈ {S. P.enough_new S}›
      using * params_left by fast

    show ?case
    proof (rule ccontr)
      assume ‹∄x. True ∧ set (δ (❙¬ ❙∀ p) x) ∪ S ∈ {S. P.enough_new S ∧ (∀S'⊆S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
      then have ‹∀x. ∃S' ⊆ {❙¬ ⟨❙⋆x⟩p} ∪ S. finite S' ∧ ¬(∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
        using P by simp
     moreover obtain x where x: ‹x ∉ P.params S›
       using ‹P.enough_new S› unfolding P.enough_new_def
       by (metis Diff_eq_empty_iff card_of_ordLeq_finite finite.emptyI inf_univ subsetI)
     ultimately obtain S' where
        S': ‹S' ⊆ {❙¬ ⟨❙⋆x⟩p} ∪ S› ‹finite S'› ‹∀(U :: 'a set) E F G. wf_model (Model U E F G) ⟶ ¬ Model U E F G ⊫ S'›
        using 1 by meson

      let ?S = ‹{❙¬ ❙∀p} ∪ (S' - {❙¬ ⟨❙⋆x⟩p})›
      have ‹finite ?S›
        using S'(2) by blast
      moreover have **: ‹?S ⊆ S›
        using *(1) 1(1) S'(1) by auto
      ultimately obtain U :: ‹'a set› and E F G where
        M: ‹wf_model (Model U E F G)› ‹Model U E F G ⊫ ?S›
        using * by meson
      then obtain z where z: ‹z ∈ U› ‹¬ Model U (z ⪢ E) F G ⊨ p›
        by auto
 
      let ?F = ‹F(x := λ_. z)›
      have ‹¬ Model U (?F x [] ⪢ E) ?F G ⊨ p›
        using M x z ** by auto
      moreover have ‹Model U E ?F G ⊫ ?S›
        using M x ** by (metis (no_types, lifting) UN_iff in_mono upd_params_fm)
      ultimately have ‹∃F. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'›
        using M(1) z by (auto intro!: exI[of _ ?F])
      then show False
        using S'(3) by blast
    qed
  qed simp_all
qed

lemma compact_prop: ‹P.prop⇩E Kinds {S :: ('f, 'p) fm set. P.enough_new S ∧
    (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'a set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
  using compact_C compact_A compact_B compact_G compact_D ..

theorem compactness:
  fixes S :: ‹('f, 'p) fm set›
  assumes ‹P.enough_new S›
  shows ‹(∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S) ⟷ (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))›
proof safe
  fix U :: ‹'f tm set› and E F G and S' :: ‹('f, 'p) fm set›
  assume ‹wf_model (Model U E F G)› ‹Model U E F G ⊫ S› ‹S' ⊆ S›
  then show ‹∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'›
    by blast
next
  let ?S = ‹{has_subterm} ∪ S›
  assume *: ‹∀S' ⊆ S. finite S' ⟶ (∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
  have ‹∀S' ⊆ ?S. finite S' ⟶ (∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S')›
  proof safe
    fix S'
    assume ‹S' ⊆ {has_subterm} ∪ S› ‹finite S'›
    then obtain U :: ‹'f tm set› and E F G where M: ‹wf_model (Model U E F G)› ‹Model U E F G ⊫ S' - {has_subterm}›
      using * by (meson Diff_subset_conv finite_Diff)
    then have ‹Model U E F G ⊫ S'›
      by auto
    then show ‹∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'›
      using M(1) by blast
  qed
  moreover have P: ‹P.enough_new ?S›
    using assms by (metis List.set_insert empty_set params_left)
  ultimately have *: ‹?S ∈ {S :: ('f, 'p) fm set. P.enough_new S ∧
    (∀S' ⊆ S. finite S' ⟶ (∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S'))}›
    by fast

  have **: ‹terms ?S ≠ {}›
    unfolding terms_def by simp
  have ‹∃C. canonical (mk_mcs C ?S) ⊫ ?S›
    using model_existence[OF compact_prop * P **] by blast
  moreover have ‹terms (mk_mcs C ?S) ≠ {}› for C
    using ** by (metis Extend_subset empty_subsetI subset_antisym terms_mono)
  ultimately show ‹∃(U :: 'f tm set) E F G. wf_model (Model U E F G) ∧ Model U E F G ⊫ S›
    using wf_canonical by fast
qed

section ‹Natural Deduction›

locale Natural_Deduction
begin

inductive ND_Set :: ‹('f, 'p) fm set ⇒ ('f, 'p) fm ⇒ bool› (infix ‹⊩› 50) where
  Assm [dest]: ‹p ∈ A ⟹ A ⊩ p›
| FlsE [elim]: ‹A ⊩ ❙⊥ ⟹ A ⊩ p›
| ImpI [intro]: ‹{p} ∪ A ⊩ q ⟹ A ⊩ (p ❙⟶ q)›
| ImpE [dest]: ‹A ⊩ (p ❙⟶ q) ⟹ A ⊩ p ⟹ A ⊩ q›
| UniI [intro]: ‹A ⊩ ⟨❙⋆a⟩p ⟹ a ∉ P.params ({p} ∪ A) ⟹ A ⊩ ❙∀p›
| UniE [dest]: ‹A ⊩ ❙∀p ⟹ t ∈ terms ({p} ∪ A) ⟹ A ⊩ ⟨t⟩p›
| Clas: ‹{p ❙⟶ q} ∪ A ⊩ p ⟹ A ⊩ p›

subsection ‹Soundness›

theorem soundness_set:
  assumes ‹A ⊩ p› ‹wf_model (Model U E F G)›
  shows ‹∀q ∈ A. Model U E F G ⊨ q ⟹ Model U E F G ⊨ p›
  using assms
proof (induct A p arbitrary: F pred: ND_Set)
  case (UniI A a p)
  have ‹∀x ∈ U. ∀q ∈ A. Model U E (F(a := λ_. x)) G ⊨ q›
    using UniI(3-) by simp
  moreover have ‹∀x ∈ U. wf_model (Model U E (F(a := λ_. x)) G)›
    using UniI(5) by simp
  ultimately have ‹∀x ∈ U. Model U E (F(a := λ_. x)) G ⊨ ⟨❙⋆a⟩p›
    using UniI by meson
  then show ?case
    using UniI by simp
qed auto

subsection ‹Derivational Consistency›

lemma Boole: ‹{❙¬ p} ∪ A ⊩ ❙⊥ ⟹ A ⊩ p›
  unfolding Neg_def using Clas FlsE by fast

sublocale DC: Derivational_Confl psub params_fm ‹λ_. True› confl_class ‹λA. ¬ A ⊩ ❙⊥›
proof
  fix A ps qs and q :: ‹('f, 'p) fm›
  assume ‹ps ↝⇩✗ qs› ‹set ps ⊆ A› ‹q ∈ set qs› ‹q ∈ A›
  then show ‹¬ ¬ A ⊩ ❙⊥›
    by cases auto
qed

sublocale DA: Derivational_Alpha psub params_fm ‹λ_. True› alpha_class ‹λA. ¬ A ⊩ ❙⊥›
proof (standard; safe)
  fix A and ps qs :: ‹('f, 'p) fm list›
  assume ‹ps ↝⇩α qs› and *: ‹set ps ⊆ A› ‹¬ A ⊩ ❙⊥› ‹set qs ∪ A ⊩ ❙⊥›
  then show False
  proof cases
    case (CImpN p q)
    then have ‹A ⊩ ❙¬ (p ❙⟶ q)›
      using *(1) by auto
    moreover have ‹A ⊩ p ❙⟶ q›
      using CImpN(2) * Boole[of q ‹{p} ∪ A›] by auto
    ultimately show ?thesis
      using * by blast
  qed
qed

sublocale DB: Derivational_Beta psub params_fm ‹λ_. True› beta_class ‹λA. ¬ A ⊩ ❙⊥›
proof
  fix A and ps qs :: ‹('f, 'p) fm list›
  assume ‹ps ↝⇩β qs› and *: ‹set ps ⊆ A› ‹¬ A ⊩ ❙⊥›
  then show ‹∃q ∈ set qs. ¬ {q} ∪ A ⊩ ❙⊥›
  proof cases
    case (CImpP p q)
    then show ?thesis
      using * Boole[of p A]
      by (metis Assm ImpE ImpI list.set_intros(1) set_subset_Cons subset_iff)
  qed
qed

sublocale DG: Derivational_Gamma map_tm psub params_fm ‹λ_. True› gamma_class ‹λA. ¬ A ⊩ ❙⊥›
proof
  fix A F qs t and ps :: ‹('f, 'p) fm list›
  assume ‹ps ↝⇩γ (F, qs)› and *: ‹set ps ⊆ A› ‹t ∈ F A› ‹¬ A ⊩ ❙⊥›
  then show ‹¬ set (qs t) ∪ A ⊩ ❙⊥›
  proof cases
    case (CAllP p)
    then have ‹t ∈ terms ({p} ∪ A)›
      using * terms_mono by blast
    then show ?thesis
      using CAllP * UniE[of A p t] ImpI by auto
  qed
qed

sublocale DD: Derivational_Delta psub params_fm ‹λ_. True› δ ‹λA. ¬ A ⊩ ❙⊥›
proof (standard; safe)
  fix A a and p :: ‹('f, 'p) fm›
  assume ‹p ∈ A› ‹a ∉ P.params A› ‹¬ A ⊩ ❙⊥› ‹set (δ p a) ∪ A ⊩ ❙⊥›
  then show False
  proof (induct p a rule: δ.induct)
    case (1 p x)
    then have ‹x ∉ P.params ({p} ∪ A)›
      by auto
    moreover have ‹A ⊩ ⟨❙⋆ x⟩ p›
      using 1(4) Boole by auto
    ultimately show ?case
      using 1 UniI by blast
  qed simp_all
qed

sublocale Derivational_Consistency psub params_fm ‹λ_. True› Kinds ‹λA. ¬ A ⊩ ❙⊥›
  using prop⇩E_Kinds[OF DC.kind DA.kind DB.kind DG.kind DD.kind] by unfold_locales

subsection ‹Strong Completeness›

lemma with_subterm_elim: ‹A ⊩ with_subterm p ⟹ A ⊩ p›
  using Assm ImpE by blast

theorem strong_completeness:
  fixes p :: ‹('f, 'p) fm›
  assumes mod: ‹⋀(U :: 'f tm set) E F G. wf_model (Model U E F G) ⟹
    (∀q ∈ A. Model U E F G ⊨ q) ⟹ Model U E F G ⊨ p›
    and ‹P.enough_new A›
  shows ‹A ⊩ p›
proof (rule ccontr)
  assume ‹¬ A ⊩ p›
  then have ‹¬ A ⊩ with_subterm p›
    using with_subterm_elim by blast
  then have *: ‹¬ {❙¬ with_subterm p} ∪ A ⊩ ❙⊥›
    using Boole by (metis insert_is_Un)

  let ?S = ‹set [❙¬ with_subterm p] ∪ A›
  let ?C = ‹{A. P.enough_new A ∧ ¬ A ⊩ ❙⊥}›
  let ?M = ‹canonical (mk_mcs ?C ?S)›

  have ne: ‹terms ?S ≠ {}›
    unfolding terms_def by simp
  then have ‹terms (mk_mcs ?C ?S) ≠ {}›
    by (metis (no_types, lifting) ext Extend_subset subset_empty terms_mono)
  then have wf: ‹wf_model ?M›
    using wf_canonical by fast

  have ‹P.prop⇩E Kinds ?C›
    using Consistency by blast
  moreover have ‹P.enough_new ?S›
    using assms(2) params_left by blast
  moreover from this have ‹?S ∈ ?C›
    using * by simp
  ultimately have *: ‹∀p ∈ ?S. ?M ⊨ p›
    using model_existence ne by blast
  then have ‹?M ⊨ p›
    using mod[OF wf] by fast 
  then show False
    using * by simp
qed

subsection ‹Natural Deduction with Lists›

inductive ND_List :: ‹('f, 'p) fm list ⇒ ('f, 'p) fm ⇒ bool› (infix ‹⊢› 50) where
  Assm [simp]: ‹p ∈ set A ⟹ A ⊢ p›
| FlsE [elim]: ‹A ⊢ ❙⊥ ⟹ A ⊢ p›
| ImpI [intro]: ‹p # A ⊢ q ⟹ A ⊢ p ❙⟶ q›
| ImpE [dest]: ‹A ⊢ p ❙⟶ q ⟹ A ⊢ p ⟹ A ⊢ q›
| UniI [intro]: ‹A ⊢ ⟨❙⋆a⟩p ⟹ a ∉ P.params ({p} ∪ set A) ⟹ A ⊢ ❙∀p›
| UniE [dest]: ‹A ⊢ ❙∀p ⟹ t ∈ terms ({p} ∪ set A) ⟹ A ⊢ ⟨t⟩p›
| Clas: ‹(p ❙⟶ q) # A ⊢ p ⟹ A ⊢ p›

definition bounded :: ‹'a list ⇒ 'a set ⇒ ('a list ⇒ bool) ⇒ bool› where
  ‹bounded K A P ≡ set K ⊆ A ∧ (∀B. set K ⊆ set B ⟶ set B ⊆ A ⟶ P B)›

lemma bounded_one [elim]:
  assumes ‹bounded K A P› ‹⋀A. P A ⟹ Q A›
  shows ‹bounded K A Q›
  using assms unfolding bounded_def by simp

lemma bounded_two [elim]:
  assumes ‹bounded K A P› ‹bounded K' A Q› ‹⋀A. P A ⟹ Q A ⟹ R A›
  shows ‹bounded (K @ K') A R›
  using assms unfolding bounded_def by simp

lemma bounded_removeAll [dest]:
  assumes ‹bounded K ({p} ∪ A) P›
  shows ‹bounded (removeAll p K) A (λB. P (p # B))›
  using assms unfolding bounded_def
  by (metis Diff_subset_conv insert_is_Un insert_mono list.simps(15) set_removeAll)

lemma bounded_terms:
  assumes ‹t ∈ terms ({p} ∪ A)›
  shows ‹t ∈ terms_fm p ∧ bounded [] A (λB. t ∈ terms (set (p # B))) ∨
    (∃q ∈ A. t ∈ terms_fm q ∧ bounded [q] A (λB. t ∈ terms (set (p # B))))›
  using assms unfolding terms_def bounded_def by auto

lemma bounded_params:
  assumes ‹a ∉ P.params ({p} ∪ A)› ‹bounded K A P›
  shows ‹bounded K A (λB. a ∉ P.params (set (p # B)))›
  using assms unfolding bounded_def by auto

lemma finite_kernel: ‹A ⊩ p ⟹ ∃K. bounded K A (λB. B ⊢ p)›
proof (induct A p pred: ND_Set)
  case (Assm p A)
  then show ?case
    unfolding bounded_def by (auto intro!: exI[of _ ‹[p]›])
next
  case (UniI A a p)
  then show ?case
    using bounded_params by fastforce
next
  case (UniE A p t)
  then show ?case
    using bounded_terms by fastforce
next
  case (Clas p q A)
  then have ‹∃K. bounded K A (λB. (p ❙⟶ q) # B ⊢ p)›
    by fast
  then show ?case
    using ND_List.Clas unfolding bounded_def by meson
qed fast+

corollary finite_assumptions: ‹A ⊩ p ⟹ ∃B. set B ⊆ A ∧ B ⊢ p›
  using finite_kernel unfolding bounded_def by blast

lemma to_set: ‹A ⊢ p ⟹ set A ⊩ p›
  by (induct A p pred: ND_List) (auto intro: ND_Set.Clas)

corollary soundness_list:
  assumes ‹A ⊢ p› ‹wf_model (Model U E F G)› ‹∀q ∈ set A. Model U E F G ⊨ q›
  shows ‹Model U E F G ⊨ p›
  using assms soundness_set to_set by fast

corollary soundness_nil: ‹[] ⊢ p ⟹ wf_model (Model U E F G) ⟹ Model U E F G ⊨ p›
  using soundness_list by (metis empty_iff list.set(1))

corollary ‹¬ ([] ⊢ ❙⊥)›
  using soundness_nil by fastforce

corollary strong_completeness_list:
  fixes p :: ‹('f, 'p) fm›
  assumes mod: ‹⋀(U :: 'f tm set) E F G. wf_model (Model U E F G) ⟹ (∀q ∈ A. Model U E F G ⊨ q) ⟹ Model U E F G ⊨ p›
    and ‹P.enough_new A›
  shows ‹∃B. set B ⊆ A ∧ B ⊢ p›
  using assms strong_completeness finite_assumptions by blast

theorem main:
  fixes p :: ‹('f, 'p) fm›
  assumes ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV :: 'f set|›
  shows ‹[] ⊢ p ⟷ (∀(U :: 'f tm set) E F G. wf_model (Model U E F G) ⟶ Model U E F G ⊨ p)›
  using assms strong_completeness_list[of ‹{}› p] soundness_nil[of p] unfolding P.enough_new_def
  by simp blast

end

section ‹Tableau›

locale Tableau
begin

inductive TC :: ‹('f, 'p) fm set ⇒ bool› (‹⊢ _› [51] 50) where
  Axiom [simp]: ‹❙¬ ❙⋅P ts ∈ A ⟹ ❙⋅P ts ∈ A ⟹ ⊢ A›
| FlsP [simp]: ‹❙⊥ ∈ A ⟹ ⊢ A›
| FlsN [intro]: ‹⊢ A ⟹ ⊢ {❙¬ ❙⊥} ∪ A›
| ImpP [intro]: ‹⊢ {❙¬ p} ∪ A ⟹ ⊢ {q} ∪ A ⟹ ⊢ {p ❙⟶ q} ∪ A›
| ImpN [intro]: ‹⊢ {p, ❙¬ q} ∪ A ⟹ ⊢ {❙¬ (p ❙⟶ q)} ∪ A›
| UniP [intro]: ‹⊢ {⟨t⟩p} ∪ A ⟹ t ∈ terms ({p} ∪ A) ⟹ ⊢ {❙∀p} ∪ A›
| UniN [intro]: ‹⊢ {❙¬ ⟨❙⋆a⟩p} ∪ A ⟹ a ∉ P.params ({p} ∪ A) ⟹ ⊢ {❙¬ ❙∀p} ∪ A›

subsection ‹Soundness›

theorem soundness:
  assumes ‹⊢ A› ‹wf_model (Model U E F G)›
  shows ‹∃q ∈ A. ¬ Model U E F G ⊨ q›
  using assms
proof (induct A arbitrary: F pred: TC)
  case (Axiom P ts A)
  then show ?case
    by (meson semantics_fm.simps(1) semantics_fm.simps(3))
next
  case (FlsP A)
  then show ?case
    by force
next
  case (UniP t p A)
  then have ‹∃q ∈ {⟨t⟩ p} ∪ A. ¬ Model U E F G ⊨ q›
    by blast
  moreover have ‹⦉(E, F)⦊ t ∈ U›
    using UniP.prems by auto
  then have ‹¬ Model U E F G ⊨ ⟨t⟩ p ⟹ ¬ Model U E F G ⊨ ❙∀p›
    by auto
  ultimately show ?case
    by blast
next
  case (UniN a p A)
  then have ‹∀x ∈ U. wf_model (Model U E (F(a := λ_. x)) G)›
    by simp
  then have ‹∀x ∈ U. ∃q ∈ {❙¬ ⟨❙⋆ a⟩ p} ∪ A. ¬ Model U E (F(a := λ_. x)) G ⊨ q›
    using UniN(2) by fast
  then show ?case
    using UniN by simp
qed auto

subsection ‹Derivational Consistency›

sublocale DC: Derivational_Confl psub params_fm ‹λ_. True› confl_class ‹λA. ¬ ⊢ A›
proof
  fix A ps qs and q :: ‹('f, 'p) fm›
  assume ‹ps ↝⇩✗ qs› ‹set ps ⊆ A› ‹q ∈ set qs› ‹q ∈ A›
  then show ‹¬ ¬ ⊢ A›
    by cases auto
qed

sublocale DA: Derivational_Alpha psub params_fm ‹λ_. True› alpha_class ‹λA. ¬ ⊢ A›
proof
  fix A and ps qs :: ‹('f, 'p) fm list›
  assume ‹ps ↝⇩α qs› and *: ‹set ps ⊆ A› ‹¬ ⊢ A›
  then show ‹¬ ⊢ set qs ∪ A›
  proof cases
    case (CImpN p q)
    then show ?thesis
      using * ImpN[of p q A]
      by (auto simp: sup.order_iff)
  qed
qed

sublocale DB: Derivational_Beta psub params_fm ‹λ_. True› beta_class ‹λA. ¬ ⊢ A›
proof
  fix A and ps qs :: ‹('f, 'p) fm list›
  assume ‹ps ↝⇩β qs› and *: ‹set ps ⊆ A› ‹¬ ⊢ A› 
  then show ‹∃q ∈ set qs. ¬ ⊢ {q} ∪ A›
  proof cases
    case (CImpP p q)
    then show ?thesis
      using * ImpP[of p A q]
      by (auto simp: sup.order_iff)
  qed
qed

sublocale DG: Derivational_Gamma map_tm psub params_fm ‹λ_. True› gamma_class ‹λA. ¬ ⊢ A›
proof
  fix A F qs t and ps :: ‹('f, 'p) fm list›
  assume ‹ps ↝⇩γ (F, qs)› and *: ‹set ps ⊆ A› ‹t ∈ F A› ‹¬ ⊢ A›
  then show ‹¬ ⊢ set (qs t) ∪ A›
  proof cases
    case (CAllP p)
    then have ‹t ∈ terms ({p} ∪ A)›
      using * terms_mono by blast
    then show ?thesis
      using CAllP * UniP[of t p A]
      by (auto simp: sup.order_iff)
  qed
qed

sublocale DD: Derivational_Delta psub params_fm ‹λ_. True› δ ‹λA. ¬ ⊢ A›
proof
  fix A a and p :: ‹('f, 'p) fm›
  assume ‹p ∈ A› ‹a ∉ P.params A› ‹¬ ⊢ A›
  then show ‹¬ ⊢ set (δ p a) ∪ A›
  proof (induct p a rule: δ.induct)
    case (1 p x)
    then have ‹x ∉ P.params ({p} ∪ A)›
      by auto
    then show ?case
      using 1 UniN[of x p A] by (auto simp: sup.order_iff insert_absorb)
  qed simp_all
qed

sublocale Derivational_Consistency psub params_fm ‹λ_. True› Kinds ‹λA. ¬ ⊢ A›
  using prop⇩E_Kinds[OF DC.kind DA.kind DB.kind DG.kind DD.kind] by unfold_locales

subsection ‹Strong Completeness›

theorem strong_completeness:
  fixes p :: ‹('f, 'p) fm›
  assumes mod: ‹⋀(U :: 'f tm set) E F G. wf_model (Model U E F G) ⟹ (∀q ∈ A. Model U E F G ⊨ q) ⟹ Model U E F G ⊨ p›
    and ‹P.enough_new A›
  shows ‹⊢ {❙¬ with_subterm p} ∪ A›
proof (rule ccontr)
  assume *: ‹¬ ⊢ {❙¬ with_subterm p} ∪ A›
  
  let ?S = ‹set [❙¬ with_subterm p] ∪ A›
  let ?C = ‹{A. P.enough_new A ∧ ¬ ⊢ A}›
  let ?M = ‹canonical (mk_mcs ?C ?S)›

  have ne: ‹terms ?S ≠ {}›
    unfolding terms_def by simp
  then have ‹terms (mk_mcs ?C ?S) ≠ {}›
    by (metis (no_types, lifting) ext Extend_subset subset_empty terms_mono)
  then have wf: ‹wf_model ?M›
    using wf_canonical by fast

  have ‹P.prop⇩E Kinds ?C›
    using Consistency by blast
  moreover have ‹P.enough_new ?S›
    using assms(2) params_left by blast
  moreover from this have ‹?S ∈ ?C›
    using * by simp
  ultimately have *: ‹∀p ∈ ?S. ?M ⊨ p›
    using model_existence ne by blast
  then have ‹?M ⊨ p›
    using mod[OF wf] by fast 
  then show False
    using * by simp
qed

end

end