Theory Example_First_Order_Logic

(*
  Title:  Example Completeness Proof for a Natural Deduction Calculus for First-Order Logic
  Author: Asta Halkjær From
*)

chapter ‹Example: First-Order Logic›

theory Example_First_Order_Logic imports Derivations 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)
  | Exi ‹('f, 'p) fm› (‹❙∃›)

abbreviation Neg (‹❙¬ _› [70] 70) where ‹❙¬ p ≡ p ❙⟶ ❙⊥›

section ‹Semantics›

type_synonym ('a, 'f, 'p) model = ‹(nat ⇒ 'a) × ('f ⇒ 'a list ⇒ 'a) × ('p ⇒ 'a list ⇒ bool)›

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›
| ‹(E, F, G) ⊨⇩∃ ❙⋅P ts ⟷ G P (map ⦇(E, F)⦈ ts)›
| ‹(E, F, G) ⊨⇩∃ p ❙⟶ q ⟷ (E, F, G) ⊨⇩∃ p ⟶ (E, F, G) ⊨⇩∃ q›
| ‹(E, F, G) ⊨⇩∃ ❙∃p ⟷ (∃x. (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 ‹params S ≡ ⋃p ∈ S. params_fm p›

abbreviation ‹params' l ≡ params (set l)›

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]: ‹f ∉ params_fm p ⟹ (E, F(f := x), G) ⊨⇩∃ p ⟷ (E, F, G)⊨⇩∃ p›
  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]: ‹(E, F, G) ⊨⇩∃ sub_fm s p ⟷ (λ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 sub_tm_Var [simp]: ‹sub_tm ❙# t = t›
  by (induct t) (auto cong: map_cong)

lemma reduce_Var [simp]: ‹(❙# 0 ⨟ λn. ❙# (Suc n)) = ❙#›
proof (rule ext)
  fix n
  show ‹(❙# 0 ⨟ λn. ❙# (Suc n)) n = ❙#n›
    by (induct n) simp_all
qed

lemma sub_fm_Var [simp]:
  fixes p :: ‹('f, 'p) fm›
  shows ‹sub_fm ❙# p = p›
proof (induct p)
  case (Pre P ts)
  then show ?case
    by (auto cong: map_cong)
qed simp_all

lemma semantics_tm_id [simp]: ‹⦇(❙#, ❙∙)⦈ t = t›
  by (induct t) (auto cong: map_cong)

lemma semantics_tm_id_map [simp]: ‹map ⦇(❙#, ❙∙)⦈ ts = ts›
  by (auto cong: map_cong)

text ‹The built-in ‹size› is not invariant under substitution.›

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›

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

section ‹Calculus›

inductive Calculus :: ‹('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›
| ExiI [intro]: ‹A ⊢⇩∃ ⟨t⟩p ⟹ A ⊢⇩∃ ❙∃p›
| ExiE [elim]: ‹A ⊢⇩∃ ❙∃p ⟹ a ∉ params (set (p # q # A)) ⟹ ⟨❙⋆a⟩p # A ⊢⇩∃ q ⟹ A ⊢⇩∃ q›
| Clas: ‹(p ❙⟶ q) # A ⊢⇩∃ p ⟹ A ⊢⇩∃ p›

subsection ‹Weakening›

abbreviation ‹psub f ≡ map_fm f id›

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

lemma map_tm_upd [simp]: ‹a ∉ params_tm t ⟹ map_tm (f(a := b)) t = map_tm f t›
  by (induct t) auto

lemma psub_upd [simp]: ‹a ∉ params_fm p ⟹ psub (f(a := b)) p = psub f p›
  by (induct p) auto

class inf_univ =
  fixes itself :: ‹'a itself›
  assumes infinite_UNIV: ‹infinite (UNIV :: 'a set)›

lemma Calculus_psub:
  fixes f :: ‹'f ⇒ 'g :: inf_univ›
  shows ‹A ⊢⇩∃ p ⟹ map (psub f) A ⊢⇩∃ psub f p›
proof (induct A p arbitrary: f pred: Calculus)
  case (Assm p A)
  then show ?case
    by simp
next
  case (FlsE A p)
  then show ?case
    by force
next
  case (ImpI p A q)
  then show ?case
    by auto
next
  case (ImpE A p q)
  then show ?case
    by auto
next
  case (ExiI A t p)
  then show ?case
    by (metis Calculus.ExiI fm.simps(27) psub_inst_single)
next
  case (ExiE A p a q)
  let ?params = ‹params' (p # q # A)›
  have ‹finite ?params›
    by simp
  then obtain b where b: ‹b ∉ {f a} ∪ f ` ?params›
    using ex_new_if_finite infinite_UNIV
    by (metis finite.emptyI finite.insertI finite_UnI finite_imageI)

  define g where ‹g ≡ f(a := b)›

  have ‹a ∉ params' (p # q # A)›
    using ExiE by simp
  then have b': ‹b ∉ params' (map (psub g) (p # q # A))›
    unfolding g_def using b ExiE(3) by (auto simp: fm.set_map(1))

  have ‹map (psub g) A ⊢⇩∃ psub g (❙∃p)›
    using ExiE by blast
  then have ‹map (psub g) A ⊢⇩∃ ❙∃(psub g p)›
    by simp
  moreover have ‹map (psub g) (⟨❙⋆a⟩p # A) ⊢⇩∃ psub g q›
    using ExiE by blast
  then have ‹⟨❙⋆b⟩(psub g p) # map (psub g) A ⊢⇩∃ psub g q›
    unfolding g_def by simp
  ultimately have ‹map (psub g) A ⊢⇩∃ psub g q›
    using b' by fastforce
  moreover have ‹psub g q = psub f q› ‹map (psub g) A = map (psub f) A›
    unfolding g_def using ExiE.hyps(3) by simp_all
  ultimately show ?case
    by metis
next
  case (Clas p q A)
  then show ?case
    using Calculus.Clas by auto
qed

lemma Weaken:
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  shows ‹A ⊢⇩∃ p ⟹ set A ⊆ set B ⟹ B ⊢⇩∃ p›
proof (induct A p arbitrary: B pred: Calculus)
  case (Assm p A)
  then show ?case
    by auto
next
  case (FlsE A p)
  then show ?case
    using Calculus.FlsE by blast
next
  case (ImpI p A q)
  then show ?case
    by (simp add: Calculus.ImpI subset_code(1))
next
  case (ImpE A p q)
  then show ?case
    by blast
next
  case (ExiI A t p)
  then show ?case
    by blast
next
  case (ExiE A p a q)
  let ?params = ‹params' (p # q # B)›
  have ‹finite ?params›
    by simp
  then obtain b where b: ‹b ∉ ?params›
    using ex_new_if_finite infinite_UNIV by blast
  then have b': ‹b ∉ params' A›
    using ExiE by auto

  define f where ‹f ≡ id(a := b, b := a)›
  let ?B = ‹map (psub f) B›

  have f: ‹∀p ∈ set A. psub f p = p›
    using ExiE(3) b' by (simp add: fm.map_id f_def)
  then have ‹set A ⊆ set ?B›
    using ExiE.prems by force
  then have ‹?B ⊢⇩∃ ❙∃ p›
    using ExiE.hyps by blast

  moreover have ‹⟨❙⋆a⟩p ∈ set (⟨❙⋆a⟩p # ?B)›
    using ExiE(3) b by (auto simp: fm.map_id0)
  then have ‹set (⟨❙⋆ a⟩ p # A) ⊆ set (⟨❙⋆a⟩p # ?B)›
    using ‹set A ⊆ set ?B› by auto
  then have ‹⟨❙⋆a⟩p # ?B ⊢⇩∃ q›
    using ExiE(5) by blast

  moreover have ‹a ∉ params' (p # q # ?B)›
    using ExiE(3) b by (simp add: fm.set_map(1) image_iff f_def)

  ultimately have ‹?B ⊢⇩∃ q›
    by fast
  then have ‹map (psub f) ?B ⊢⇩∃ psub f q›
    using Calculus_psub by blast
  moreover have ‹psub f q = q›
    using ExiE.hyps(3) b fm.map_id unfolding f_def by auto
  moreover have ‹f o f = id›
    unfolding f_def by auto
  then have ‹psub f o psub f = id›
    by (auto simp: fm.map_comp fm.map_id0)
  then have ‹map (psub f) ?B = B›
    unfolding map_map by (metis list.map_id)
  ultimately show ?case
    by simp
next
  case (Clas p q A)
  then show ?case
    using Calculus.Clas
    by (metis insert_mono list.simps(15))
qed

section ‹Soundness›

theorem soundness: ‹A ⊢⇩∃ p ⟹ ∀q ∈ set A. (E, F, G) ⊨⇩∃ q ⟹ (E, F, G) ⊨⇩∃ p›
proof (induct p arbitrary: F pred: Calculus)
  case (ExiE A p a q)
  then obtain x where ‹(x ⨟ E, F, G) ⊨⇩∃ p›
    by fastforce
  then have ‹(E, F(a := λ_. x), G) ⊨⇩∃ ⟨❙⋆a⟩p›
    using ExiE(3) by simp
  moreover have ‹∀q ∈ set A. (E, F(a := λ_. x), G) ⊨⇩∃ q›
    using ExiE(3, 6) by simp
  ultimately have ‹(E, F(a := λ_. x), G) ⊨⇩∃ q›
    using ExiE(5) by simp
  then show ?case
    using ExiE(3) by simp
qed auto

corollary soundness': ‹[] ⊢⇩∃ p ⟹ M ⊨⇩∃ p›
  using soundness by (cases M) fastforce

corollary ‹¬ ([] ⊢⇩∃ ❙⊥)›
  using soundness' by fastforce

section ‹Admissible Rules›

lemma Assm_head: ‹p # A ⊢⇩∃ p›
  by auto

lemma Boole: ‹(❙¬ p) # A ⊢⇩∃ ❙⊥ ⟹ A ⊢⇩∃ p›
  using Clas FlsE by blast

corollary Weak:
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  shows ‹A ⊢⇩∃ p ⟹ q # A ⊢⇩∃ p›
  using Weaken[where B=‹q # A›] by auto

lemma deduct1:
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  shows ‹A ⊢⇩∃ p ❙⟶ q ⟹ p # A ⊢⇩∃ q›
  using Assm_head Weak by blast

lemma Weak':
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  shows ‹A ⊢⇩∃ p ⟹ B @ A ⊢⇩∃ p›
  by (induct B) (simp_all add: Weak)

interpretation Derivations ‹Calculus :: ('f :: inf_univ, 'p) fm list ⇒ _›
proof
  show ‹⋀A p. p ∈ set A ⟹ A ⊢⇩∃ p›
    by simp
next
  show ‹⋀A B. A ⊢⇩∃ r ⟹ set A = set B ⟹ B ⊢⇩∃ r› for r :: ‹('f, 'p) fm›
    using Weaken by blast
qed

section ‹Maximal Consistent Sets›

definition consistent :: ‹('f, 'p) fm set ⇒ bool› where
  ‹consistent S ≡ ∀A. set A ⊆ S ⟶ ¬ A ⊢⇩∃ ❙⊥›

fun witness :: ‹('f, 'p) fm ⇒ ('f, 'p) fm set ⇒ ('f, 'p) fm set› where
  ‹witness (❙∃p) S = (let a = SOME a. a ∉ params ({p} ∪ S) in {⟨❙⋆a⟩p})›
| ‹witness _ _ = {}›

lemma consistent_add_witness:
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  assumes ‹consistent S› ‹❙∃p ∈ S› ‹a ∉ params S›
  shows ‹consistent ({⟨❙⋆a⟩p} ∪ S)›
  unfolding consistent_def
proof safe
  fix A
  assume ‹set A ⊆ {⟨❙⋆a⟩p} ∪ S› ‹A ⊢⇩∃ ❙⊥›
  then obtain A' where ‹set A' ⊆ S› ‹(⟨❙⋆a⟩p) # A' ⊢⇩∃ ❙⊥›
    using assms derive_split1 by (metis consistent_def insert_is_Un subset_insert)
  then have ‹⟨❙⋆a⟩p # A' ⊢⇩∃ ❙⊥›
    using Boole by blast
  then have ‹⟨❙⋆a⟩p # ❙∃p # A' ⊢⇩∃ ❙⊥›
    using Weak deduct1 by blast
  moreover have ‹a ∉ params_fm p› ‹∀p ∈ set (❙∃p # A'). a ∉ params_fm p›
    using ‹set A' ⊆ S› assms(2-3) by auto
  then have ‹a ∉ params ({p} ∪ {❙⊥} ∪ set (❙∃p # A'))›
    using calculation by simp
  moreover have ‹❙∃p # A' ⊢⇩∃ ❙∃p›
    by simp
  ultimately have ‹❙∃p # A' ⊢⇩∃ ❙⊥›
    by fastforce
  moreover have ‹set (❙∃p # A') ⊆ S›
    using ‹set A' ⊆ S› assms(2) by simp
  ultimately show False
    using assms(1) unfolding consistent_def by blast
qed

lemma consistent_witness':
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  assumes ‹consistent ({p} ∪ S)› ‹infinite (UNIV - params S)›
  shows ‹consistent (witness p S ∪ {p} ∪ S)›
  using assms
proof (induct p S rule: witness.induct)
  case (1 p S)
  have ‹infinite (UNIV - params ({p} ∪ S))›
    using 1(2) finite_params_fm by (simp add: infinite_Diff_fin_Un)
  then have ‹∃a. a ∉ params ({p} ∪ S)›
    by (simp add: not_finite_existsD set_diff_eq)
  then have ‹(SOME a. a ∉ params ({p} ∪ S)) ∉ params ({p} ∪ S)›
    by (rule someI_ex)
  then obtain a where a: ‹witness (❙∃p) S = {⟨❙⋆a⟩p}› ‹a ∉ params ({❙∃p} ∪ S)›
    by simp
  then show ?case
    using 1(1-2) a(1) consistent_add_witness[where S=‹{❙∃p} ∪ S›] by auto
qed (auto simp: assms)

interpretation MCS_Witness_UNIV consistent witness ‹params_fm :: ('f :: inf_univ, 'p) fm ⇒ _›
proof
  fix p and S :: ‹('f, 'p) fm set›
  show ‹finite (params (witness p S))›
    by (induct p S rule: witness.induct) simp_all
next
  fix p and S :: ‹('f, 'p) fm set›
  assume ‹consistent ({p} ∪ S)› ‹infinite (UNIV - params S)›
  then show ‹consistent ({p} ∪ S ∪ witness p S)›
    using consistent_witness' by (simp add: sup_commute)
next
  show ‹infinite (UNIV :: ('f, 'p) fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed (auto simp: consistent_def)

interpretation Derivations_Cut_MCS consistent ‹Calculus :: ('f :: inf_univ, 'p) fm list ⇒ _›
proof
  show ‹⋀S. consistent S = (∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢⇩∃ q))›
    unfolding consistent_def using FlsE by blast
next
  show ‹⋀A B p. A ⊢⇩∃ p ⟹ p # B ⊢⇩∃ q ⟹ A @ B ⊢⇩∃ q› for q :: ‹('f, 'p) fm›
    by (metis ImpE ImpI Un_upper1 Weak' Weaken set_append)
qed

interpretation Derivations_Bot consistent Calculus ‹❙⊥ :: ('f :: inf_univ, 'p) fm›
proof
qed fast

interpretation Derivations_Imp consistent Calculus ‹λp q. p ❙⟶ q :: ('f :: inf_univ, 'p) fm›
proof qed fast+

interpretation Derivations_Exi consistent witness params_fm Calculus ‹❙∃› ‹λt p. ⟨t⟩p :: ('f :: inf_univ, 'p) fm›
proof qed auto

section ‹Truth Lemma›

abbreviation canonical :: ‹('f, 'p) fm set ⇒ ('f tm, 'f, 'p) model› (‹ℳ⇩∃›) where
  ‹ℳ⇩∃(S) ≡ (❙#, ❙∙, λP ts. ❙⋅P ts ∈ S)›

fun semics ::
  ‹('a, 'f, 'p) model ⇒ (('a, 'f, 'p) model ⇒ ('f, 'p) fm ⇒ bool) ⇒ ('f, 'p) fm ⇒ bool›
  (‹(_ ⟦_⟧⇩∃ _)› [55, 0, 55] 55) where
  ‹_ ⟦_⟧⇩∃ ❙⊥ ⟷ False›
| ‹(E, F, G) ⟦_⟧⇩∃ ❙⋅P ts ⟷ G P (map ⦇(E, F)⦈ ts)›
| ‹(E, F, G) ⟦ℛ⟧⇩∃ p ❙⟶ q ⟷ ℛ (E, F, G) p ⟶ ℛ (E, F, G) q›
| ‹(E, F, G) ⟦ℛ⟧⇩∃ ❙∃p ⟷ (∃x. ℛ (x ⨟ E, F, G) p)›

fun rel :: ‹('f, 'p) fm set ⇒ ('f tm, 'f, 'p) model ⇒ ('f, 'p) fm ⇒ bool› (‹ℛ⇩∃›) where
  ‹ℛ⇩∃(S) (E, _, _) p ⟷ sub_fm E p ∈ S›

theorem saturated_model:
  assumes ‹⋀p. ∀M ∈ {ℳ⇩∃(S)}. M ⟦ℛ⇩∃(S)⟧⇩∃ p ⟷ ℛ⇩∃(S) M p› ‹M ∈ {ℳ⇩∃(S)}›
  shows ‹ℛ⇩∃(S) M p ⟷ M ⊨⇩∃ p›
proof (induct p rule: wf_induct[where r=‹measure size_fm›])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms(1)[of x] assms(2) by (cases x) simp_all
qed

theorem saturated_MCS:
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  assumes ‹MCS S›
  shows ‹ℛ⇩∃(S) (ℳ⇩∃(S)) p ⟷ ℳ⇩∃(S) ⟦ℛ⇩∃(S)⟧⇩∃ p›
  using assms by (cases p) (auto cong: map_cong)

interpretation Truth_Witness semics semantics_fm ‹λS. {ℳ⇩∃(S)}› rel consistent witness
  ‹params_fm :: ('f :: inf_univ, 'p) fm ⇒ _›
proof
  fix p and M :: ‹('f tm, 'f, 'p) model›
  show ‹M ⊨⇩∃ p ⟷ M ⟦(⊨⇩∃)⟧⇩∃ p›
    by (cases M, induct p) auto
qed (use saturated_model saturated_MCS in blast)+

section ‹Cardinalities›

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

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 (FlsM, n)›
abbreviation ‹EXI ≡ Inr (ExiM, 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 ❙⊥ = [FLS]›
| ‹encode_fm (❙⋅P ts) = PRE (length ts) # PRES P # encode_tms ts›
| ‹encode_fm (p ❙⟶ q) = IMP (length (encode_fm p)) # encode_fm p @ encode_fm q›
| ‹encode_fm (❙∃p) = EXI # 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 Fls
  then show ?case
    by (cases q) auto
next
  case (Pre P ts)
  then show ?case
    by (cases q) (auto simp: inj_encode_tm')
next
  case (Imp p1 p2)
  then show ?case
    by (cases q) auto
next
  case (Exi p)
  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, ExiM}› for p
    by (cases p) auto
  then show ?thesis
    by (meson ex_new_if_finite finite.emptyI finite_insert)
qed

lemma card_of_fm:
  ‹|UNIV :: ('f :: inf_univ, 'p) fm set| ≤o |UNIV :: 'f set| +c |UNIV :: 'p set|›
proof -
  have ‹|UNIV :: marker set| ≤o |UNIV :: nat set|›
    using finite_marker by (simp add: ordLess_imp_ordLeq)
  moreover have ‹infinite (UNIV :: ('f + 'p) set)›
    by (simp add: inf_univ_class.infinite_UNIV)
  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

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M :: ('f tm, 'f :: inf_univ, 'p) model. (∀q ∈ X. M ⊨⇩∃ q) ⟶ M ⊨⇩∃ p›
    ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - params X|›
  shows ‹∃A. set A ⊆ X ∧ A ⊢⇩∃ p›
proof (rule ccontr)
  assume ‹∄A. set A ⊆ X ∧ A ⊢⇩∃ p›
  then have *: ‹∀A. set A ⊆ {❙¬ p} ∪ X ⟶ ¬ A ⊢⇩∃ ❙⊥›
    using Boole FlsE by (metis derive_split1 insert_is_Un subset_insert)

  let ?X = ‹{❙¬ p} ∪ X›
  let ?S = ‹Extend ?X›

  have ‹consistent ?X›
    unfolding consistent_def using * by blast
  moreover have ‹infinite (UNIV - params X)›
    using assms(2) inf_univ_class.infinite_UNIV
    by (metis Cinfinite_csum Cnotzero_UNIV Field_card_of cinfinite_def cinfinite_mono)
  then have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - params X - params_fm (❙¬ p)|›
    using assms(2) finite_params_fm card_of_infinite_diff_finite
    by (metis ordIso_iff_ordLeq ordLeq_transitive)
  then have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - (params X ∪ params_fm (❙¬ p))|›
    by (metis Set_Diff_Un)
  then have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV - params ?X|›
    by (metis UN_insert insert_is_Un sup_commute)
  then have ‹|UNIV :: ('f, 'p) fm set| ≤o |UNIV - params ?X|›
    using assms card_of_fm ordLeq_transitive by blast
  ultimately have ‹MCS ?S›
    using MCS_Extend by fast
  then have ‹p ∈ ?S ⟷ ℳ⇩∃(?S) ⊨⇩∃ p› for p
    using truth_lemma by fastforce
  then have ‹p ∈ ?X ⟶ ℳ⇩∃(?S) ⊨⇩∃ p› for p
    using Extend_subset by blast
  then have ‹ℳ⇩∃(?S) ⊨⇩∃ ❙¬ p› ‹∀q ∈ X. ℳ⇩∃(?S) ⊨⇩∃ q›
    by blast+
  moreover from this have ‹ℳ⇩∃(?S) ⊨⇩∃ p›
    using assms(1) by blast
  ultimately show False
    by simp
qed

abbreviation valid :: ‹('f, 'p) fm ⇒ bool› where
  ‹valid p ≡ ∀M :: ('f tm, _, _) model. M ⊨⇩∃ p›

theorem completeness:
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  assumes ‹valid p› ‹|UNIV :: 'p set| ≤o |UNIV :: 'f set|›
  shows ‹[] ⊢⇩∃ p›
proof -
  have ‹|UNIV :: 'f set| +c |UNIV :: 'p set| ≤o |UNIV :: 'f set|›
    using assms(2)
    by (simp add: inf_univ_class.infinite_UNIV cinfinite_def csum_absorb1 ordIso_imp_ordLeq)
  then show ?thesis
    using assms strong_completeness[where X=‹{}›] infinite_UNIV_listI by auto
qed

corollary completeness':
  fixes p :: ‹('f :: inf_univ, 'f) fm›
  assumes ‹valid p›
  shows ‹[] ⊢⇩∃ p›
  using assms completeness[of p] by simp

theorem main:
  fixes p :: ‹('f :: inf_univ, 'p) fm›
  assumes ‹|UNIV :: 'p set| ≤o |UNIV :: 'f set|›
  shows ‹valid p ⟷ [] ⊢⇩∃ p›
  using assms completeness soundness' by blast

corollary main':
  fixes p :: ‹('f :: inf_univ, 'f) fm›
  shows ‹valid p ⟷ [] ⊢⇩∃ p›
  using completeness' soundness' by blast

end