# 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

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

lemma deduct1: ‹A ⊢⇩@ (i, p ❙⟶ q) ⟹ (i, p) # A ⊢⇩@ (i, q)›

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, ❙⊥)›

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)›
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)›
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›
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›
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
```