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 by (simp add: guard_in)

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

section ‹Cardinalities›

datatype marker = VarM | FunM | TmM | PreM | FlsM | ImpM | UniM

type_synonym ('f, 'p) enc = ‹('f + 'p) + marker × nat›

abbreviation ‹FUNS f ≡ Inl (Inl f)›
abbreviation ‹PRES p ≡ Inl (Inr p)›

abbreviation ‹VAR n ≡ Inr (VarM, n)›
abbreviation ‹FUN n ≡ Inr (FunM, n)›
abbreviation ‹TM n ≡ Inr (TmM, n)›

abbreviation ‹PRE n ≡ Inr (PreM, n)›
abbreviation ‹FLS ≡ Inr (FlsM, 0)›
abbreviation ‹IMP n ≡ Inr (ImpM, n)›
abbreviation ‹UNI ≡ Inr (UniM, 0)›

primrec
  encode_tm :: ‹'f tm ⇒ ('f, 'p) enc list› and
  encode_tms :: ‹'f tm list ⇒ ('f, 'p) enc list› where
  ‹encode_tm (❙#n) = [VAR n]› |
  ‹encode_tm (❙○f ts) = FUN (length ts) # FUNS f # encode_tms ts› |
  ‹encode_tms [] = []› |
  ‹encode_tms (t # ts) = TM (length (encode_tm t)) # encode_tm t @ encode_tms ts›

lemma encode_tm_ne [simp]: ‹encode_tm t ≠ []›
  by (induct t) auto

lemma inj_encode_tm':
  ‹(encode_tm t :: ('f, 'p) enc list) = encode_tm s ⟹ t = s›
  ‹(encode_tms ts :: ('f, 'p) enc list) = encode_tms ss ⟹ ts = ss›
proof (induct t and ts arbitrary: s and ss rule: encode_tm.induct encode_tms.induct)
  case (Var n)
  then show ?case
    by (cases s) auto
next
  case (Fun f fts)
  then show ?case
    by (cases s) auto
next
  case Nil_tm
  then show ?case
    by (cases ss) auto
next
  case (Cons_tm t ts)
  then show ?case
    by (cases ss) auto
qed

lemma inj_encode_tm: ‹inj encode_tm›
  unfolding inj_def using inj_encode_tm' by blast

primrec encode_fm :: ‹('f, 'p) fm ⇒ ('f, 'p) enc list› where
  ‹encode_fm (❙⋅P ts) = PRE (length ts) # PRES P # encode_tms ts› |
  ‹encode_fm ❙⊥ = [FLS]› |
  ‹encode_fm (p ❙⟶ q) =
    IMP (length (encode_fm p)) # encode_fm p @ encode_fm q› |
  ‹encode_fm (❙∀p) = UNI # encode_fm p›

lemma encode_fm_ne [simp]: ‹encode_fm p ≠ []›
  by (induct p) auto

lemma inj_encode_fm': ‹encode_fm p = encode_fm q ⟹ p = q›
proof (induct p arbitrary: q)
  case Pre
  then show ?case
    by (cases q) (auto simp: inj_encode_tm')
next
  case Fls
  then show ?case
    by (cases q) auto
next
  case Imp
  then show ?case
    by (cases q) auto
next
  case Uni
  then show ?case
    by (cases q) auto
qed

lemma inj_encode_fm: ‹inj encode_fm›
  unfolding inj_def using inj_encode_fm' by blast

lemma finite_marker: ‹finite (UNIV :: marker set)›
proof -
  have ‹p ∈ {VarM, FunM, TmM, FlsM, PreM, ImpM, UniM}› for p
    by (cases p) auto
  then show ?thesis
    by (meson ex_new_if_finite finite.emptyI finite_insert)
qed

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

lemma card_of_fm:
  assumes ‹infinite (UNIV :: 'f set)›
  shows ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV :: 'f set| +c |UNIV :: 'p set|›
proof -
  have ‹|UNIV :: marker set| ≤o |UNIV :: nat set|›
    using finite_marker finite_iff_ordLess_natLeq infinite_UNIV_nat
      infinite_iff_natLeq_ordLeq ordLess_imp_ordLeq ordLess_ordLeq_trans by meson
  moreover have ‹infinite (UNIV :: ('f + 'p) set)›
    using assms by simp
  ultimately have ‹|UNIV :: ('f, 'p) enc list set| ≤o |UNIV :: ('f + 'p) set|›
    using card_of_params_marker_lists by blast
  moreover have ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV :: ('f, 'p) enc list set|›
    using card_of_ordLeq inj_encode_fm by blast
  ultimately have ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV :: ('f + 'p) set|›
    using ordLeq_transitive by blast
  then show ?thesis
    unfolding csum_def by simp
qed

lemma card_of_fm_pair:
  assumes ‹infinite (UNIV :: 'a set)›
  shows ‹|UNIV :: ('a, 'a) fm set| ≤o |UNIV :: 'a set|›
  using assms Cnotzero_UNIV Field_card_of card_of_fm card_of_least card_of_well_order_on
    csum_absorb1 ordLeq_ordIso_trans unfolding cinfinite_def by metis

lemma star[iff]: ‹(case t of Fun a l ⇒ (case l of [] ⇒ T a| _ # _ ⇒ False) | Var _ ⇒ False) =
    (∃a. t = ❙⋆a ∧ T a)›
proof (induct t)
  case (Fun _ A)
  then show ?case
    by (induct A) simp_all
qed simp

lemma triv[iff]: ‹a ∉ P.params (set (p # A)) ⟷ (a ∉ params_fm p ∧ (∀p∈set A. a ∉ params_fm p))›
  by simp

primrec member where
  ‹member p [] = False› |
  ‹member p (q # A) = (if p = q then True else member p A)›

lemma member [iff]: ‹member p A ⟷ p ∈ set A›
  by (induct A) simp_all

abbreviation ‹fresh t A ≡ (case t of Fun a [] ⇒ a ∉ P.params (set A) | _ ⇒ False)›

abbreviation ‹known t A ≡ t ∈ terms (set A)›

abbreviation ‹valid U p ≡ ∀E F G. (∀n. E n ∈ U) ∧ (∀f ts. F f ts ∈ U) ⟶ Model U E F G ⊨ p›

proposition ‹valid {} p›
  by simp

inductive ND :: ‹('f, 'p) fm list ⇒ ('f, 'p) fm ⇒ bool› (infix ‹↝› 50) where
  Assm: ‹A ↝ p› if ‹member p A› |
  FlsE: ‹A ↝ ❙⊥ ⟹ A ↝ p› |
  ImpI: ‹p # A ↝ q ⟹ A ↝ p ❙⟶ q› |
  ImpE: ‹A ↝ p ❙⟶ q ⟹ A ↝ p ⟹ A ↝ q› |
  UniI: ‹A ↝ ⟨t⟩p ⟹ A ↝ ❙∀p› if ‹fresh t (p # A)› |
  UniE: ‹A ↝ ❙∀p ⟹ A ↝ ⟨t⟩p› if ‹known t (p # A)› |
  ImpC: ‹(p ❙⟶ q) # A ↝ p ⟹ A ↝ p›

lemma (in Natural_Deduction) reduction[iff]: ‹A ⊢ p ⟷ A ↝ p›
proof
  show ‹A ⊢ p ⟹ A ↝ p›
    by (induct rule: ND_List.induct)
      (auto simp: ND.Assm ND.UniE elim: ND.FlsE ND.ImpE ND.ImpC ND.UniE intro: ND.ImpI ND.UniI)
next
  show ‹A ↝ p ⟹ A ⊢ p›
    by (induct rule: ND.induct) (auto elim: ND_List.Clas)
qed

theorem (in Natural_Deduction)
  assumes ‹[] ↝ p›
  shows ‹∀U. valid U p›
  using assms by (simp add: soundness_nil)

theorem (in Natural_Deduction)
  fixes p :: ‹(string, string) fm›
  shows ‹[] ↝ p ⟷ (∀(U :: string tm set). valid U p)›
  using main card_of_fm_pair infinite_UNIV_listI by auto

end