Theory Example_Hybrid_Logic

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

chapter ‹Example: Hybrid Logic›

theory Example_Hybrid_Logic imports Derivations begin

section ‹Syntax›

datatype (nominals_fm: 'i, 'p) fm
  = Fls (‹❙⊥›)
  | Pro 'p (‹❙‡›)
  | Nom 'i (‹❙⋅›)
  | Imp ‹('i, 'p) fm› ‹('i, 'p) fm› (infixr ‹❙⟶› 55)
  | Dia ‹('i, 'p) fm› (‹❙◇›)
  | Sat 'i ‹('i, 'p) fm› (‹❙@›)

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

type_synonym ('i, 'p) lbd = ‹'i × ('i, 'p) fm›

primrec nominals_lbd :: ‹('i, 'p) lbd ⇒ 'i set› where
  ‹nominals_lbd (i, p) = {i} ∪ nominals_fm p›

abbreviation nominals :: ‹('i, 'p) lbd set ⇒ 'i set› where
  ‹nominals S ≡ ⋃ip ∈ S. nominals_lbd ip›

lemma finite_nominals_fm: ‹finite (nominals_fm p)›
  by (induct p) simp_all

lemma finite_nominals_lbd: ‹finite (nominals_lbd p)›
  by (cases p) (simp add: finite_nominals_fm)

section ‹Semantics›

datatype ('w, 'p) model =
  Model (R: ‹'w ⇒ 'w set›) (V: ‹'w ⇒ 'p ⇒ bool›)

type_synonym ('i, 'p, 'w) ctx = ‹('w, 'p) model × ('i ⇒ 'w) × 'w›

fun semantics :: ‹('i, 'p, 'w) ctx ⇒ ('i, 'p) fm ⇒ bool› (‹_ ⊨ _› [50, 50] 50) where
  ‹(M, g, w) ⊨ ❙⊥ ⟷ False›
| ‹(M, _, w) ⊨ ❙‡P ⟷ V M w P›
| ‹(_, g, w) ⊨ ❙⋅i ⟷ w = g i›
| ‹(M, g, w) ⊨ (p ❙⟶ q) ⟷ (M, g, w) ⊨ p ⟶ (M, g, w) ⊨ q›
| ‹(M, g, w) ⊨ ❙◇ p ⟷ (∃v ∈ R M w. (M, g, v) ⊨ p)›
| ‹(M, g, _) ⊨ ❙@i p ⟷ (M, g, g i) ⊨ p›

lemma semantics_fresh: ‹i ∉ nominals_fm p ⟹ ((M, g, w) ⊨ p) = ((M, g(i := v), w) ⊨ p)›
  by (induct p arbitrary: w) auto

lemma semantics_fresh_lbd:
  ‹k ∉ nominals_lbd (i, p) ⟹ ((M, g, w) ⊨ p) = ((M, g(k := v), w) ⊨ p)›
  by (induct p arbitrary: w) auto

section ‹Calculus›

inductive Calculus :: ‹('i, 'p) lbd list ⇒ ('i, 'p) lbd ⇒ bool› (‹_ ⊢⇩@ _› [50, 50] 50) where
  Assm [intro]: ‹(i, p) ∈ set A ⟹ A ⊢⇩@ (i, p)›
| Ref [intro]: ‹A ⊢⇩@ (i, ❙⋅i)›
| Nom [intro]: ‹A ⊢⇩@ (i, ❙⋅k) ⟹ A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (k, p)›
| FlsE [elim]: ‹A ⊢⇩@ (i, ❙⊥) ⟹ A ⊢⇩@ (k, p)›
| ImpI [intro]: ‹(i, p) # A ⊢⇩@ (i, q) ⟹ A ⊢⇩@ (i, p ❙⟶ q)›
| ImpE [elim]: ‹A ⊢⇩@ (i, p ❙⟶ q) ⟹ A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (i, q)›
| SatI [intro]: ‹A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (k, ❙@i p)›
| SatE [elim]: ‹A ⊢⇩@ (i, ❙@k p) ⟹ A ⊢⇩@ (k, p)›
| DiaI [intro]: ‹A ⊢⇩@ (i, ❙◇ (❙⋅k)) ⟹ A ⊢⇩@ (k, p) ⟹ A ⊢⇩@ (i, ❙◇ p)›
| DiaE [elim]: ‹A ⊢⇩@ (i, ❙◇ p) ⟹ k ∉ nominals ({(i, p), (j, q)} ∪ set A) ⟹
    (k, p) # (i, ❙◇ (❙⋅k)) # A ⊢⇩@ (j, q) ⟹ A ⊢⇩@ (j, q)›
| Clas: ‹(i, p ❙⟶ q) # A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (i, p)›
| Weak: ‹A ⊢⇩@ (i, p) ⟹ (k, q) # A ⊢⇩@ (i, p)›

section ‹Soundness›

theorem soundness: ‹A ⊢⇩@ (i, p) ⟹ list_all (λ(i, p). (M, g, g i) ⊨ p) A ⟹ (M, g, g i) ⊨ p›
proof (induct ‹(i, p)› arbitrary: i p g rule: Calculus.induct)
  case (Nom A i k p)
  then show ?case
    by fastforce
next
  case (DiaE A i p k j q)
  then have ‹(M, g, g i) ⊨ ❙◇ p›
    by blast
  then obtain v where v: ‹v ∈ R M (g i)› ‹(M, g, v) ⊨ p›
    by auto
  let ?g = ‹g(k := v)›
  have ‹(M, ?g, ?g k) ⊨ p› ‹(M, ?g, ?g i) ⊨ ❙◇ (❙⋅k)›
    using v fun_upd_same DiaE(3) semantics_fresh_lbd by fastforce+
  moreover have ‹list_all (λ(i, p). (M, ?g, ?g i) ⊨ p) A›
    using DiaE.prems DiaE.hyps(3) semantics_fresh_lbd by (induct A) fastforce+
  ultimately have ‹list_all (λ(i, p). (M, ?g, ?g i) ⊨ p) ((k, p) # (i, ❙◇ (❙⋅k)) # A)›
    by simp
  then have ‹(M, ?g, ?g j) ⊨ q›
    using DiaE.hyps by fast
  then show ?case
    using DiaE.hyps(3) semantics_fresh_lbd by fastforce
qed (auto simp: list_all_iff)

corollary soundness': ‹[] ⊢⇩@ (i, p) ⟹ i ∉ nominals_fm p ⟹ (M, g, w) ⊨ p›
  using soundness semantics_fresh by (metis fun_upd_same list.pred_inject(1))

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

section ‹Admissible Rules›

lemma Assm_head: ‹(p, i) # A ⊢⇩@ (p, i)›
  by auto

lemma deduct1: ‹A ⊢⇩@ (i, p ❙⟶ q) ⟹ (i, p) # A ⊢⇩@ (i, q)›
  by (meson ImpE Weak Assm_head)

lemma Boole: ‹(i, ❙¬ p) # A ⊢⇩@ (i, ❙⊥) ⟹ A ⊢⇩@ (i, p)›
  using Clas FlsE by meson

lemma Weak': ‹A ⊢⇩@ (i, p) ⟹ B @ A ⊢⇩@ (i, p)›
proof (induct B)
  case (Cons b B)
  then show ?case
    by (cases b) (metis Cons Weak append_Cons)
qed simp

lemma ImpI':
  assumes ‹(k, q) # A ⊢⇩@ (i, p)›
  shows ‹A ⊢⇩@ (i, (❙@k q) ❙⟶ p)›
  using assms
proof -
  have ‹(k, q) # A ⊢⇩@ (k, ❙@i p)›
    using assms by fast
  then show ?thesis
    by (meson Assm_head ImpE ImpI SatE Weak)
qed

lemma Weaken: ‹A ⊢⇩@ (i, p) ⟹ set A ⊆ set B ⟹ B ⊢⇩@ (i, p)›
proof (induct A arbitrary: i p)
  case Nil
  then show ?case
    using Weak' by fastforce
next
  case (Cons kq A)
  then show ?case
  proof (cases kq)
    case (Pair k q)
    then show ?thesis
      using Cons by (meson Assm ImpI' ImpE SatI list.set_intros(1) set_subset_Cons subset_eq)
  qed
qed

interpretation Derivations Calculus
proof
  fix A B and p :: ‹('i, 'p) lbd›
  assume ‹A ⊢⇩@ p› ‹set A ⊆ set B›
  then show ‹B ⊢⇩@ p›
    by (cases p) (metis Weaken)
qed

section ‹Maximal Consistent Sets›

definition consistent :: ‹('i, 'p) lbd set ⇒ bool› where
  ‹consistent S ≡ ∄S' a. set S' ⊆ S ∧ S' ⊢⇩@ (a, ❙⊥)›

lemma consistent_add_witness:
  assumes ‹consistent S› ‹(i, ❙◇ p) ∈ S› ‹k ∉ nominals S›
  shows ‹consistent ({(k, p), (i, ❙◇ (❙⋅k))} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S' a. set S' ⊆ {(k, p), (i, ❙◇ (❙⋅k))} ∪ S ∧ S' ⊢⇩@ (a, ❙⊥)›
  then obtain S' a where ‹set S' ⊆ S› ‹(k, p) # (i, ❙◇ (❙⋅k)) # S' ⊢⇩@ (a, ❙⊥)›
    using assms derive_split[where X=S and B=‹[(k, p), (i, ❙◇ (❙⋅k))]›]
    by (metis append_Cons append_Nil list.simps(15) set_empty)
  then have ‹(k, p) # (i, ❙◇ (❙⋅k)) # S' ⊢⇩@ (i, ❙⊥)›
    by fast
  then have ‹(k, p) # (i, ❙◇ (❙⋅k)) # (i, ❙◇ p) # S' ⊢⇩@ (i, ❙⊥)›
    by (fastforce intro: Weaken)
  moreover have ‹k ∉ nominals ({(i, p), (i, ❙⊥)} ∪ set ((i, ❙◇ p) # S'))›
    using ‹set S' ⊆ S› assms(2-3) by auto
  moreover have ‹(i, ❙◇ p) # S' ⊢⇩@ (i, ❙◇ p)›
    by auto
  ultimately have ‹(i, ❙◇ p) # S' ⊢⇩@ (i, ❙⊥)›
    by fastforce
  moreover have ‹set ((i, ❙◇ p) # S') ⊆ S›
    using ‹set S' ⊆ S› assms(2) by simp
  ultimately show False
    using assms(1) unfolding consistent_def by blast
qed

fun witness :: ‹('i, 'p) lbd ⇒ ('i, 'p) lbd set ⇒ ('i, 'p) lbd set› where
  ‹witness (i, ❙◇ p) S = (let k = (SOME k. k ∉ nominals ({(i, p)} ∪ S)) in {(k, p), (i, ❙◇ (❙⋅k))})›
| ‹witness (_, _) _ = {}›

lemma consistent_witness':
  assumes ‹consistent ({(i, p)} ∪ S)› ‹infinite (UNIV - nominals S)›
  shows ‹consistent (witness (i, p) S ∪ {(i, p)} ∪ S)›
  using assms
proof (induct ‹(i, p)› S arbitrary: i p rule: witness.induct)
  case (1 i p S)
  have ‹infinite (UNIV - nominals ({(i, p)} ∪ S))›
    using 1(2) finite_nominals_lbd
    by (metis UN_Un finite.emptyI finite.insertI finite_UN_I infinite_Diff_fin_Un)
  then have ‹∃k. k ∉ nominals ({(i, p)} ∪ S)›
    by (simp add: not_finite_existsD set_diff_eq)
  then have ‹(SOME k. k ∉ nominals ({(i, p)} ∪ S)) ∉ nominals ({(i, p)} ∪ S)›
    by (rule someI_ex)
  then obtain k where ‹witness (i, ❙◇ p) S = {(k, p), (i, ❙◇ (❙⋅k))}›
    ‹k ∉ nominals ({(i, ❙◇ p)} ∪ S)›
    by (simp add: Let_def)
  then show ?case
    using 1(1-2) consistent_add_witness[where S=‹{(i, ❙◇ p)} ∪ S›] by simp
qed (auto simp: assms)

interpretation MCS_Saturation consistent nominals_lbd witness
proof
  fix S S' :: ‹('i, 'p) lbd set›
  assume ‹consistent S› ‹S' ⊆ S›
  then show ‹consistent S'›
    unfolding consistent_def by fast
next
  fix S :: ‹('i, 'p) lbd set›
  assume ‹¬ consistent S›
  then show ‹∃S'⊆S. finite S' ∧ ¬ consistent S'›
    unfolding consistent_def by blast
next
  fix ip :: ‹('i, 'p) lbd›
  show ‹finite (nominals_lbd ip)›
    using finite_nominals_fm by (cases ip) simp
next
  fix ip :: ‹('i, 'p) lbd› and S :: ‹('i, 'p) lbd set›
  show ‹finite (nominals (witness ip S))›
    by (induct ip S rule: witness.induct) (auto simp: finite_nominals_fm Let_def)
next
  fix ip and S :: ‹('i, 'p) lbd set›
  assume ‹consistent ({ip} ∪ S)› ‹infinite (UNIV - nominals S)›
  then show ‹consistent (witness ip S ∪ {ip} ∪ S)›
    using consistent_witness' by (cases ip) simp
next
  have ‹infinite (UNIV :: ('i, 'p) fm set)›
    using infinite_UNIV_size[of ‹❙◇›] by simp
  then show ‹infinite (UNIV :: ('i, 'p) lbd set)›
    using finite_prod by blast
qed

interpretation Derivations_MCS_Cut Calculus consistent ‹(undefined, ❙⊥)›
proof
  fix S :: ‹('i, 'p) lbd set›
  show ‹consistent S = (∄S'. set S' ⊆ S ∧ S' ⊢⇩@ (undefined, ❙⊥))›
    unfolding consistent_def by fast
next
  fix A and p :: ‹('i, 'p) lbd›
  assume ‹p ∈ set A›
  then show ‹A ⊢⇩@ p›
    by (metis Assm surj_pair)
next
  fix A B and p q :: ‹('i, 'p) lbd›
  assume ‹A ⊢⇩@ p› ‹p # B ⊢⇩@ q›
  then have ‹A @ B ⊢⇩@ p› ‹p # A @ B ⊢⇩@ q›
    by (simp_all add: derive_struct subsetI)
  then show ‹A @ B ⊢⇩@ q›
    by (cases p, cases q) (meson ImpE ImpI' SatI)
qed

lemma saturated: ‹saturated H ⟹ (i, ❙◇p) ∈ H ⟹ ∃k. (i, ❙◇ (❙⋅k)) ∈ H ∧ (k, p) ∈ H›
  unfolding saturated_def by (metis insert_subset witness.simps(1))

section ‹Nominals›

lemma MCS_Nom_refl:
  assumes ‹consistent S› ‹maximal S›
  shows ‹(i, ❙⋅i) ∈ S›
  using assms Ref by (metis MCS_derive MCS_derive_fls)

lemma MCS_Nom_sym:
  assumes ‹consistent S› ‹maximal S› ‹(i, ❙⋅k) ∈ S›
  shows ‹(k, ❙⋅i) ∈ S›
  using assms Nom Ref by (metis MCS_derive)

lemma MCS_Nom_trans:
  assumes ‹consistent S› ‹maximal S› ‹(i, ❙⋅j) ∈ S› ‹(j, ❙⋅k) ∈ S›
  shows ‹(i, ❙⋅k) ∈ S›
proof -
  have ‹∃S'. set S' ⊆ S ∧ S' ⊢⇩@ (i, ❙⋅j)›
    using assms MCS_derive by blast
  then have ‹∃S'. set S' ⊆ S ∧ S' ⊢⇩@ (i, ❙⋅j) ∧ S' ⊢⇩@ (j, ❙⋅k)›
    by (metis Assm_head Calculus.intros(12) assms(4) insert_subset list.set(2))
  then have ‹∃S'. set S' ⊆ S ∧ S' ⊢⇩@ (i, ❙⋅k)›
    using Nom Ref by metis
  then show ?thesis
    using assms MCS_derive by blast
qed

section ‹Truth Lemma›

fun semics :: ‹('i, 'p, 'w) ctx ⇒ (('i, 'p, 'w) ctx ⇒ ('i, 'p) fm ⇒ bool) ⇒ ('i, 'p) fm ⇒ bool›
  where
    ‹semics _ _ ❙⊥ ⟷ False›
  | ‹semics (M, _, w) _ (❙‡P) ⟷ V M w P›
  | ‹semics (_, g, w) _ (❙⋅i) ⟷ w = g i›
  | ‹semics (M, g, w) rel (p ❙⟶ q) ⟷ rel (M, g, w) p ⟶ rel (M, g, w) q›
  | ‹semics (M, g, w) rel (❙◇ p) ⟷ (∃v ∈ R M w. rel (M, g, v) p)›
  | ‹semics (M, g, _) rel (❙@ i p) ⟷ rel (M, g, g i) p›

fun rel :: ‹('i, 'p) lbd set ⇒ ('i, 'p, 'i) ctx ⇒ ('i, 'p) fm ⇒ bool› where
  ‹rel H (_, _, i) p = ((i, p) ∈ H)›

definition val :: ‹('i, 'p) lbd set ⇒ 'i ⇒ 'p ⇒ bool› where
  ‹val H i P ≡ (i, ❙‡P) ∈ H›

definition hequiv :: ‹('i, 'p) lbd set ⇒ 'i ⇒ 'i ⇒ bool› where
  ‹hequiv H i k ≡ (i, ❙⋅k) ∈ H›

lemma hequiv_reflp:
  assumes ‹consistent H› ‹maximal H›
  shows ‹reflp (hequiv H)›
  unfolding hequiv_def reflp_def using assms MCS_Nom_refl by fast

lemma hequiv_symp:
  assumes ‹consistent H› ‹maximal H›
  shows ‹symp (hequiv H)›
  unfolding hequiv_def symp_def using assms MCS_Nom_sym by fast

lemma hequiv_transp:
  assumes ‹consistent H› ‹maximal H›
  shows ‹transp (hequiv H)›
  unfolding hequiv_def transp_def using assms MCS_Nom_trans by fast

lemma hequiv_equivp:
  assumes ‹consistent H› ‹maximal H›
  shows ‹equivp (hequiv H)›
  using assms by (simp add: equivpI hequiv_reflp hequiv_symp hequiv_transp)

definition assign :: ‹('i, 'p) lbd set ⇒ 'i ⇒ 'i› where
  ‹assign H i ≡ minim ( |UNIV| ) {k. hequiv H i k}›

lemma hequiv_ne:
  assumes ‹consistent H› ‹maximal H›
  shows ‹{k. hequiv H i k} ≠ {}›
  unfolding hequiv_def using assms MCS_Nom_refl by fast

lemma hequiv_assign:
  assumes ‹consistent H› ‹maximal H›
  shows ‹hequiv H i (assign H i)›
  unfolding assign_def using assms hequiv_ne wo_rel.minim_in
  by (metis Field_card_of card_of_well_order_on mem_Collect_eq top.extremum wo_rel_def)

lemma hequiv_Nom:
  assumes ‹consistent H› ‹maximal H› ‹hequiv H i k› ‹(i, p) ∈ H›
  shows ‹(k, p) ∈ H›
proof -
  have ‹∃A. set A ⊆ H ∧ A ⊢⇩@ (i, p)›
    using assms MCS_derive by fast
  then have ‹∃A. set A ⊆ H ∧ A ⊢⇩@ (i, p) ∧ A ⊢⇩@ (i, ❙⋅k)›
    using assms(3) unfolding hequiv_def by (metis Assm_head Weak insert_subset list.simps(15))
  then have ‹∃A. set A ⊆ H ∧ A ⊢⇩@ (k, p)›
    using Nom by fast
  then show ?thesis
    using assms MCS_derive by fast
qed

definition reach :: ‹('i, 'p) lbd set ⇒ 'i ⇒ 'i set› where
  ‹reach H i ≡ {assign H k |k. (i, ❙◇ (❙⋅k)) ∈ H}›

abbreviation canonical :: ‹('i × ('i, 'p) fm) set ⇒ 'i ⇒ ('i, 'p, 'i) ctx› where
  ‹canonical H i ≡ (Model (reach H) (val H), assign H, assign H i)›

lemma Hintikka_model':
  assumes ‹⋀i p. semics (canonical H i) (rel H) p ⟷ rel H (canonical H i) p›
  shows ‹(canonical H i ⊨ p) ⟷ rel H (canonical H i) p›
proof (induct p arbitrary: i rule: wf_induct[where r=‹measure size›])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms[of i x] by (cases x) (auto simp: reach_def)
qed

lemma Hintikka_Extend':
  assumes ‹consistent H› ‹maximal H› ‹saturated H›
  shows ‹semics (canonical H i) (rel H) p ⟷ rel H (canonical H i) p›
proof (cases p)
  case Fls
  have ‹(assign H i, ❙⊥) ∉ H›
    using assms(1-2) MCS_derive unfolding consistent_def by fast
  then show ?thesis
    using Fls by simp
next
  case (Pro P)
  have ‹val H (assign H i) P ⟷ (assign H i, ❙‡P) ∈ H›
    unfolding val_def ..
  then show ?thesis
    using Pro by simp
next
  case (Nom k)
  have ‹assign H i = assign H k ⟷ (assign H i, ❙⋅k) ∈ H›
    using assms(1-2) hequiv_equivp hequiv_assign by (metis assign_def equivp_def hequiv_def)
  then show ?thesis
    using Nom by simp
next
  case (Imp p q)
  have ‹(i, p) # A ⊢⇩@ (a, ❙⊥) ⟹ A ⊢⇩@ (i, p ❙⟶ q)› ‹A ⊢⇩@ (i, q) ⟹ A ⊢⇩@ (i, p ❙⟶ q)› for A a i
    by (auto simp: Weak)
  moreover have ‹A ⊢⇩@ (i, p ❙⟶ q) ⟹ (i, p) # A ⊢⇩@ (i, q)› for A i
    using deduct1 .
  ultimately have ‹((assign H i, p) ∈ H ⟶ (assign H i, q) ∈ H) ⟷ (assign H i, p ❙⟶ q) ∈ H›
    using assms(1-2) MCS_derive MCS_derive_fls by (metis insert_subset list.simps(15))
  then show ?thesis
    using Imp by simp
next
  case (Dia p)
  have ‹(∃k ∈ reach H (assign H i). (k, p) ∈ H) ⟷ (assign H i, ❙◇ p) ∈ H›
  proof
    assume ‹∃k ∈ reach H (assign H i). (k, p) ∈ H›
    then have ‹∃k. (assign H i, ❙◇ (❙⋅k)) ∈ H ∧ (assign H k, p) ∈ H›
      unfolding reach_def by fast
    then have ‹∃k. (assign H i, ❙◇ (❙⋅k)) ∈ H ∧ (k, p) ∈ H›
      by (metis assms(1-2) hequiv_Nom hequiv_assign hequiv_symp sympD)
    then have ‹∃k. ∃A. set A ⊆ H ∧ A ⊢⇩@ (assign H i, ❙◇ (❙⋅k)) ∧ A ⊢⇩@ (k, p)›
      by (metis Assm_head Weak assms(1-2) MCS_derive insert_subset list.simps(15))
    then have ‹∃A. set A ⊆ H ∧ A ⊢⇩@ (assign H i, ❙◇ p)›
      by fast
    then show ‹(assign H i, ❙◇ p) ∈ H›
      by (simp add: assms(1-2) MCS_derive)
  next
    assume ‹(assign H i, ❙◇ p) ∈ H›
    then have ‹∃k. (assign H i, ❙◇ (❙⋅k)) ∈ H ∧ (k, p) ∈ H›
      using assms(3) saturated by fast
    then have ‹∃k. (assign H i, ❙◇ (❙⋅k)) ∈ H ∧ (assign H k, p) ∈ H›
      by (meson assms(1-2) hequiv_Nom hequiv_assign)
    then show ‹∃k ∈ reach H (assign H i). (k, p) ∈ H›
      unfolding reach_def by fast
  qed
  then show ?thesis
    using Dia by simp
next
  case (Sat k p)
  have ‹(assign H k, p) ∈ H ⟷ (assign H i, ❙@k p) ∈ H›
    by (metis SatE SatI assms(1-2) MCS_derive hequiv_Nom hequiv_assign hequiv_symp sympD)
  then show ?thesis
    using Sat by simp
qed

interpretation Truth_Saturation
  consistent nominals_lbd witness semics semantics ‹λH. {canonical H i |i. True}› rel
proof unfold_locales
  fix p and M :: ‹('i, 'p, 'w) ctx›
  show ‹(M ⊨ p) = semics M semantics p›
    by (cases M, induct p) auto
next
  fix p H and M :: ‹('i, 'p, 'i) ctx›
  assume ‹∀M ∈ {canonical H i |i. True}. ∀p. semics M (rel H) p = rel H M p›
    ‹M ∈ {canonical H i |i. True}›
  then show ‹(M ⊨ p) = rel H M p›
    using Hintikka_model' by fast
next
  fix H :: ‹('i, 'p) lbd set›
  assume ‹consistent H› ‹maximal H› ‹saturated H›
  then show ‹∀M∈{canonical H i |i. True}. ∀p. semics M (rel H) p = rel H M p›
    using Hintikka_Extend' by fast
qed

lemma Truth_lemma:
  assumes ‹consistent H› ‹maximal H› ‹saturated H›
  shows ‹(canonical H i ⊨ p) ⟷ (i, p) ∈ H›
proof -
  have ‹(canonical H i ⊨ p) ⟷ (assign H i, p) ∈ H›
    using truth_lemma_saturation assms by fastforce
  then show ?thesis
    using assms by (meson MCS_Nom_sym hequiv_Nom hequiv_assign hequiv_def)
qed

section ‹Cardinalities›

datatype marker = FlsM | ImpM | DiaM | SatM

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

abbreviation ‹NOM i ≡ Inl (Inl i)›
abbreviation ‹PRO x ≡ Inl (Inr x)›
abbreviation ‹FLS ≡ Inr (FlsM, 0)›
abbreviation ‹IMP n ≡ Inr (FlsM, n)›
abbreviation ‹DIA ≡ Inr (DiaM, 0)›
abbreviation ‹SAT ≡ Inr (SatM, 0)›

primrec encode :: ‹('i, 'p) fm ⇒ ('i, 'p) enc list› where
  ‹encode ❙⊥ = [FLS]›
| ‹encode (❙‡P) = [PRO P]›
| ‹encode (❙⋅i) = [NOM i]›
| ‹encode (p ❙⟶ q) = IMP (length (encode p)) # encode p @ encode q›
| ‹encode (❙◇ p) = DIA # encode p›
| ‹encode (❙@ i p) = SAT # NOM i # encode p›

lemma encode_ne [simp]: ‹encode p ≠ []›
  by (induct p) auto

lemma inj_encode': ‹encode p = encode q ⟹ p = q›
proof (induct p arbitrary: q)
  case Fls
  then show ?case 
    by (cases q) auto
next
  case (Pro P)
  then show ?case 
    by (cases q) auto
next
  case (Nom i)
  then show ?case 
    by (cases q) auto
next
  case (Imp p1 p2)
  then show ?case 
    by (cases q) auto
next
  case (Dia p)
  then show ?case 
    by (cases q) auto
next
  case (Sat x1a p)
  then show ?case 
    by (cases q) auto
qed

lemma inj_encode: ‹inj encode›
  unfolding inj_def using inj_encode' by blast

primrec encode_lbd :: ‹('i, 'p) lbd ⇒ ('i, 'p) enc list› where
  ‹encode_lbd (i, p) = NOM i # encode p›

lemma inj_encode_lbd': ‹encode_lbd (i, p) = encode_lbd (k, q) ⟹ i = k ∧ p = q›
  using inj_encode' by auto

lemma inj_encode_lbd: ‹inj encode_lbd›
  unfolding inj_def using inj_encode_lbd' by auto

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

lemma card_of_lbd:
  assumes ‹infinite (UNIV :: 'i set)›
  shows ‹|UNIV :: ('i, 'p) lbd set| ≤o |UNIV :: 'i 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 :: ('i + 'p) set)›
    using assms by simp
  ultimately have ‹|UNIV :: ('i, 'p) enc list set| ≤o |UNIV :: ('i + 'p) set|›
    using card_of_params_marker_lists by blast
  moreover have ‹|UNIV :: ('i, 'p) lbd set| ≤o |UNIV :: ('i, 'p) enc list set|›
    using card_of_ordLeq inj_encode_lbd by blast
  ultimately have ‹|UNIV :: ('i, 'p) lbd set| ≤o |UNIV :: ('i + 'p) set|›
    using ordLeq_transitive by blast
  then show ?thesis
    unfolding csum_def by simp
qed

section ‹Completeness›

theorem strong_completeness:
  fixes p :: ‹('i, 'p) fm›
  assumes ‹∀M :: ('i, 'p) model. ∀g w.
      (∀(k, q) ∈ X. (M, g, g k) ⊨ q) ⟶ (M, g, w) ⊨ p›
    ‹infinite (UNIV :: 'i set)›
    ‹|UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - nominals X|›
  shows ‹∃A. set A ⊆ X ∧ A ⊢⇩@ (i, p)›
proof (rule ccontr)
  assume ‹∄A. set A ⊆ X ∧ A ⊢⇩@ (i, p)›
  then have *: ‹∄A. ∃a. set A ⊆ X ∧ ((i, ❙¬ p) # A ⊢⇩@ (a, ❙⊥))›
    using Boole FlsE by metis

  let ?S = ‹{(i, ❙¬ p)} ∪ X›
  let ?H = ‹Extend ?S›

  have ‹consistent ?S›
    unfolding consistent_def using * derive_split1 by metis
  moreover have ‹infinite (UNIV - nominals X)›
    using assms(2-3)
    by (metis Cinfinite_csum Cnotzero_UNIV Field_card_of cinfinite_def cinfinite_mono)
  then have ‹|UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - nominals X - nominals_lbd (i, ❙¬ p)|›
    using assms(3) finite_nominals_lbd card_of_infinite_diff_finite
    by (metis ordIso_iff_ordLeq ordLeq_transitive)
  then have ‹|UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - (nominals X ∪ nominals_lbd (i, ❙¬ p))|›
    by (metis Set_Diff_Un)
  then have ‹|UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - nominals ?S|›
    by (metis UN_insert insert_is_Un sup_commute)
  then have ‹|UNIV :: ('i, 'p) lbd set| ≤o |UNIV - nominals ?S|›
    using assms card_of_lbd ordLeq_transitive by blast
  ultimately have ‹consistent ?H› ‹maximal ?H› ‹saturated ?H›
    using MCS_Extend by fast+
  then have ‹canonical ?H i ⊨ p ⟷ (i, p) ∈ ?H› for i p
    using Truth_lemma by fast
  then have ‹(i, p) ∈ ?S ⟹ canonical ?H i ⊨ p› for i p
    using Extend_subset by blast
  then have ‹canonical ?H i ⊨ ❙¬ p› ‹∀(k, q) ∈ X. canonical ?H k ⊨ q›
    by blast+
  moreover from this have ‹canonical ?H i ⊨ p›
    using assms(1) by blast
  ultimately show False
    by simp
qed

abbreviation valid :: ‹('i, 'p) fm ⇒ bool› where
  ‹valid p ≡ ∀(M :: ('i, 'p) model) g w. (M, g, w) ⊨ p›

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

corollary completeness':
  fixes p :: ‹('i, 'i) fm›
  assumes ‹valid p› ‹infinite (UNIV :: 'i set)›
  shows ‹[] ⊢⇩@ (i, p)›
  using assms completeness[of p] by simp

theorem main:
  fixes p :: ‹('i, 'p) fm›
  assumes ‹i ∉ nominals_fm p› ‹infinite (UNIV :: 'i set)› ‹|UNIV :: 'p set| ≤o |UNIV :: 'i set|›
  shows ‹valid p ⟷ [] ⊢⇩@ (i, p)›
  using assms completeness soundness' by metis

corollary main':
  fixes p :: ‹('i, 'i) fm›
  assumes ‹i ∉ nominals_fm p› ‹infinite (UNIV :: 'i set)›
  shows ‹valid p ⟷ [] ⊢⇩@ (i, p)›
  using assms completeness' soundness' by metis

end