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› (‹❙@›)
  | All ‹('i, 'p) fm› (‹❙A›)

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

abbreviation Con (infixr ‹❙∧› 35) where ‹p ❙∧ q ≡ ❙¬ (p ❙⟶ ❙¬ q)›

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 [simp]: ‹finite (nominals_fm p)›
  by (induct p) simp_all

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

section ‹Semantics›

datatype ('w, 'p) model =
  Model (W: ‹'w set›) (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› (infix ‹⊨⇩@› 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 ∈ W M ∩ R M w. (M, g, v) ⊨⇩@ p)›
| ‹(M, g, _) ⊨⇩@ ❙@i p ⟷ (M, g, g i) ⊨⇩@ p›
| ‹(M, g, _) ⊨⇩@ ❙A p ⟷ (∀v ∈ W M. (M, g, v) ⊨⇩@ 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› (infix ‹⊢⇩@› 50) where
  Assm [simp]: ‹(i, p) ∈ set A ⟹ A ⊢⇩@ (i, p)›
| Ref [simp]: ‹A ⊢⇩@ (i, ❙∙i)›
| Nom [dest]: ‹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 [dest]: ‹A ⊢⇩@ (i, p ❙⟶ q) ⟹ A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (i, q)›
| SatI [intro]: ‹A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (k, ❙@i p)›
| SatE [dest]: ‹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)›
| AllI [intro]: ‹A ⊢⇩@ (k, p) ⟹ k ∉ nominals ({(i, p)} ∪ set A) ⟹ A ⊢⇩@ (i, ❙A p)›
| AllE [dest]: ‹A ⊢⇩@ (i, ❙A p) ⟹ A ⊢⇩@ (k, p)›
| Clas: ‹(i, p ❙⟶ q) # A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (i, p)›
| Cut: ‹A ⊢⇩@ (k, q) ⟹ (k, q) # B ⊢⇩@ (i, p) ⟹ A @ B ⊢⇩@ (i, p)›

section ‹Soundness›

theorem soundness: ‹A ⊢⇩@ (i, p) ⟹ list_all (λ(i, p). (M, g, g i) ⊨⇩@ p) A ⟹ range g ⊆ W M ⟹ (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 (metis semantics.simps(3))
next
  case (DiaE A i p k j q)
  then have ‹(M, g, g i) ⊨⇩@ ❙◇ p›
    by blast
  then obtain v where v: ‹v ∈ W M ∩ 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(1) DiaE.hyps(3) semantics_fresh_lbd by (fastforce simp: list_all_iff)
  ultimately have ‹list_all (λ(i, p). (M, ?g, ?g i) ⊨⇩@ p) ((k, p) # (i, ❙◇ (❙∙k)) # A)›
    by simp
  moreover have ‹range ?g ⊆ W M›
    using DiaE.prems v by auto
  ultimately have ‹(M, ?g, ?g j) ⊨⇩@ q›
    using DiaE.hyps by blast
  then show ?case
    using DiaE.hyps(3) semantics_fresh_lbd by fastforce
next
  case (AllI A k p i)
  {
    fix v
    assume ‹v ∈ W M›
    let ?g = ‹g(k := v)›
    have ‹∀v. list_all (λ(i, p). (M, ?g, ?g i) ⊨⇩@ p) A›
      using AllI.prems(1) AllI.hyps(3) semantics_fresh_lbd by (fastforce simp: list_all_iff)
    moreover have ‹range ?g ⊆ W M›
      using AllI.prems ‹v ∈ W M› by auto
    ultimately have ‹(M, ?g, ?g k) ⊨⇩@ p›
      using AllI.hyps by fast
  }
  then have ‹∀v ∈ W M. (M, g(k := v), v) ⊨⇩@ p›
    by simp
  then have ‹∀v ∈ W M. (M, g, v) ⊨⇩@ p›
    using AllI.hyps(3) semantics_fresh_lbd by fast
  then show ?case
    by simp
next
  case (AllE A i p k)
  then show ?case
    by fastforce
qed (auto simp: list_all_iff)

corollary soundness':
  assumes ‹[] ⊢⇩@ (i, p)› ‹i ∉ nominals_fm p›
    and ‹range g ⊆ W M› ‹w ∈ W M›
  shows ‹(M, g, w) ⊨⇩@ p›
proof -
  let ?g = ‹g(i := w)›
  from assms(1) have ‹(M, ?g, ?g i) ⊨⇩@ p›
    by (rule soundness) (use assms(3-4) in auto)
  then have ‹(M, ?g, w) ⊨⇩@ p›
    by simp
  then show ?thesis
    using assms(2) semantics_fresh by fast
qed

corollary ‹¬ ([] ⊢⇩@ (i, ❙⊥))›
  by (metis list.pred_inject(1) model.sel(1) semantics.simps(1) soundness subset_refl)

section ‹Admissible Rules›

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

lemma SatE':
  assumes ‹(k, q) # A ⊢⇩@ (i, p)›
  shows ‹(j, ❙@k q) # A ⊢⇩@ (i, p)›
proof -
  have ‹[(j, ❙@k q)] ⊢⇩@ (k, q)›
    by (meson Assm_head SatE)
  then show ?thesis
    using assms by (auto dest: Cut)
qed

lemma ImpI':
  assumes ‹(k, q) # A ⊢⇩@ (i, p)›
  shows ‹A ⊢⇩@ (i, (❙@k q) ❙⟶ p)›
  using assms SatE' by fast

lemma Weak': ‹A ⊢⇩@ (i, p) ⟹ A @ B ⊢⇩@ (i, p)›
  by (simp add: Cut)

lemma Weaken: ‹A ⊢⇩@ (i, p) ⟹ set A ⊆ set B ⟹ B ⊢⇩@ (i, p)›
proof (induct A arbitrary: p)
  case Nil
  then show ?case
    by (metis Weak' append_Nil)
next
  case (Cons kq A)
  then show ?case
  proof (cases kq)
    case (Pair k q)
    then have ‹B ⊢⇩@ (i, ❙@k q ❙⟶ p)›
      using Cons by (simp add: ImpI')
    then show ?thesis
      using Pair Cons(3) by fastforce
  qed
qed

lemma Weak: ‹A ⊢⇩@ (i, p) ⟹ (k, q) # A ⊢⇩@ (i, p)›
  using Weaken[where A=A and B=‹(k, q) # A›] 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

interpretation Derivations Calculus
proof
  fix A and p :: ‹('i, 'p) lbd›
  show ‹p ∈ set A ⟹ A ⊢⇩@(p)›
    by (cases p) simp
next
  fix A B and p :: ‹('i, 'p) lbd›
  assume ‹A ⊢⇩@(p)› ‹set A = set B›
  then show ‹B ⊢⇩@(p)›
    by (cases p) (simp add: Weaken)
qed

section ‹Maximal Consistent Sets›

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

lemma consistent_add_diamond_witness:
  assumes ‹consistent S› ‹(i, ❙◇ p) ∈ S› ‹k ∉ nominals S›
  shows ‹consistent ({(k, p), (i, ❙◇ (❙∙k))} ∪ S)›
  unfolding consistent_def
proof safe
  fix A a
  assume A: ‹set A ⊆ {(k, p), (i, ❙◇ (❙∙k))} ∪ S› ‹A ⊢⇩@ (a, ❙⊥)›
  then obtain A' a B where ‹set A' ⊆ S› ‹B @ A' ⊢⇩@ (a, ❙⊥)› ‹set B = {(k, p), (i, ❙◇ (❙∙k))} ∩ set A›
    using assms derive_split[where p=‹(a, ❙⊥)› and X=S and B=‹[(k, p), (i, ❙◇ (❙∙k))]›]
    by (metis Int_commute empty_set list.simps(15))
  then have ‹(k, p) # (i, ❙◇ (❙∙k)) # A' ⊢⇩@ (a, ❙⊥)›
    by (auto intro: Weaken)
  then have ‹(k, p) # (i, ❙◇ (❙∙k)) # A' ⊢⇩@ (i, ❙⊥)›
    by fast
  then have ‹(k, p) # (i, ❙◇ (❙∙k)) # (i, ❙◇ p) # A' ⊢⇩@ (i, ❙⊥)›
    by (fastforce intro: Weaken)
  moreover have ‹k ∉ nominals ({(i, p), (i, ❙⊥)} ∪ set ((i, ❙◇ p) # A'))›
    using ‹set A' ⊆ S› assms(2-3) by auto
  moreover have ‹(i, ❙◇ p) # A' ⊢⇩@ (i, ❙◇ p)›
    by auto
  ultimately have ‹(i, ❙◇ p) # A' ⊢⇩@ (i, ❙⊥)›
    by fast
  moreover have ‹set ((i, ❙◇ 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_add_global_witness:
  assumes ‹consistent S› ‹(i, ❙¬ ❙A p) ∈ S› ‹k ∉ nominals S›
  shows ‹consistent ({(k, ❙¬ p)} ∪ S)›
  unfolding consistent_def
proof safe
  fix A a
  assume ‹set A ⊆ {(k, ❙¬ p)} ∪ S › ‹A ⊢⇩@ (a, ❙⊥)›
  then obtain A' where ‹set A' ⊆ S› ‹(k, ❙¬ p) # A' ⊢⇩@ (a, ❙⊥)›
    using assms derive_split1 by (metis consistent_def insert_is_Un subset_insert)
  then have ‹(k, ❙¬ p) # A' ⊢⇩@ (k, ❙⊥)›
    by fast
  then have ‹A' ⊢⇩@ (k, p)›
    by (meson Boole)
  moreover have ‹k ∉ nominals ({(i, p), (i, ❙⊥)} ∪ set ((i, ❙A p) # A'))›
    using ‹set A' ⊆ S› assms(2-3) by auto
  ultimately have ‹A' ⊢⇩@ (i, ❙A p)›
    by fastforce
  then have ‹(i, ❙¬ ❙A p) # A' ⊢⇩@ (i, ❙⊥)›
    by (meson Assm_head ImpE Weak)
  moreover have ‹set ((i, ❙¬ ❙A p) # A') ⊆ S›
    using ‹set A' ⊆ 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 (i, ❙¬ ❙A p) S = (let k = SOME k. k ∉ nominals ({(i, p)} ∪ S) in {(k, ❙¬ p)})›
| ‹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) consistent_add_diamond_witness[where S=‹{(i, ❙◇ p)} ∪ S›] by simp
next
  case (2 i p S)
  have ‹infinite (UNIV - nominals ({(i, p)} ∪ S))›
    using 2(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, ❙¬ ❙A p) S = {(k, ❙¬ p)}› ‹k ∉ nominals ({(i, ❙¬ ❙A p)} ∪ S)›
    by (simp add: Let_def)
  then show ?case
    using 2(1) consistent_add_global_witness[where S=‹{(i, ❙¬ ❙A p)} ∪ S›] by auto
qed (auto simp: assms)

interpretation MCS_Witness_UNIV consistent witness nominals_lbd
proof
  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: Let_def)
next
  fix ip and S :: ‹('i, 'p) lbd set›
  assume ‹consistent ({ip} ∪ S)› ‹infinite (UNIV - nominals S)›
  then show ‹consistent ({ip} ∪ S ∪ witness ip S)›
    using consistent_witness' by (cases ip) (simp add: sup_commute)
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 (auto simp: consistent_def)

lemma witnessed_diamond: ‹witnessed S ⟹ (i, ❙◇ p) ∈ S ⟹ ∃k. (i, ❙◇ (❙∙k)) ∈ S ∧ (k, p) ∈ S›
  unfolding witnessed_def by (metis insert_subset witness.simps(1))

lemma witnessed_global: ‹witnessed S ⟹ (i, ❙¬ ❙A p) ∈ S ⟹ ∃k. (k, ❙¬ p) ∈ S›
  unfolding witnessed_def by (metis insert_subset witness.simps(2))

interpretation Derivations_Cut_MCS consistent Calculus
proof
  show ‹⋀S. consistent S = (∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢⇩@(q)))›
    unfolding consistent_def using FlsE by fast
next
  fix A B and p q :: ‹('i, 'p) lbd›
  assume ‹A ⊢⇩@(p)› ‹p # B ⊢⇩@(q)›
  then show ‹A @ B ⊢⇩@(q)›
    by (cases p, cases q) (meson Cut)
qed

interpretation Derivations_Bot consistent Calculus ‹(i, ❙⊥)›
proof qed auto

interpretation Derivations_Not consistent Calculus ‹(i, ❙⊥)› ‹λ(i, p). (i, ❙¬ p)›
proof qed auto

lemma MCS_impE': ‹consistent S ⟹ maximal S ⟹ (i, p ❙⟶ q) ∈ S ⟹ (i, p) ∈ S ⟶ (i, q) ∈ S›
  by (metis MCS_derive deduct1 insert_subset list.simps(15))

interpretation Derivations_Uni consistent witness nominals_lbd Calculus ‹(i, ❙⊥)› ‹λ(i, p). (i, ❙¬ p)›
  ‹λ(i, p). (i, ❙A p)› ‹λk (i, p). (k, p)›
proof
  have ‹⋀S S' i p. MCS S ⟹ witness (i, ❙¬ ❙A p) S' ⊆ S ⟹ ∃k. (k, ❙¬ p) ∈ S›
    by auto
  then show ‹⋀S S' p. MCS S ⟹
       witness (case case p of (i, p) ⇒ (i, ❙A p) of (i, p) ⇒ (i, ❙¬ p)) S' ⊆ S ⟹
       ∃t. (case case p of (i, p) ⇒ (t, p) of (i, p) ⇒ (i, ❙¬ p)) ∈ S›
    by fast
next
  have ‹⋀A i p k. A ⊢⇩@ (i, ❙A p) ⟹ A ⊢⇩@ (k, p)›
    ..
  then show ‹⋀A p t. A ⊢⇩@ (case p of (i, p) ⇒ (i, ❙A p)) ⟹ A ⊢⇩@ (case p of (i, p) ⇒ (t, p))›
    by fast
qed

lemma conE1 [elim]: ‹A ⊢⇩@ (i, p ❙∧ q) ⟹ A ⊢⇩@ (i, p)›
  by (meson Clas FlsE deduct1)

lemma conE2 [elim]: ‹A ⊢⇩@ (i, p ❙∧ q) ⟹ A ⊢⇩@ (i, q)›
  by (meson Assm_head Boole ImpE ImpI Weak)

lemma conI [intro]: ‹A ⊢⇩@ (i, p) ⟹ A ⊢⇩@ (i, q) ⟹ A ⊢⇩@ (i, p ❙∧ q)›
  by (meson Assm_head ImpE ImpI Weak)

lemma MCS_con:
  assumes ‹MCS S›
  shows ‹(i, p ❙∧ q) ∈ S ⟷ (i, p) ∈ S ∧ (i, q) ∈ S›
  using assms MCS_derive conE1 conE2
  by (metis Boole MCS_explode MCS_impE' derive_assm list.set_intros(1))

interpretation Derivations_Exi consistent witness nominals_lbd Calculus
  ‹λ(i, p). (i, ❙◇ p)› ‹λk (i, p). (i, ❙@k p ❙∧ ❙◇(❙∙k))›
proof
  have ‹⋀S S' i p. MCS S ⟹ witness (i, ❙◇ p) S' ⊆ S ⟹ ∃k. (i, ❙@ k p ❙∧ ❙◇ (❙∙ k)) ∈ S›
    unfolding witness.simps using MCS_con by (metis MCS_derive SatI insert_subset)
  then show ‹⋀S S' p. MCS S ⟹ witness (case p of (i, p) ⇒ (i, ❙◇ p)) S' ⊆ S ⟹ ∃t. (case p of (i, p) ⇒ (i, ❙@ t p ❙∧ ❙◇ (❙∙ t))) ∈ S›
    by fast
next
  have ‹⋀A i k p. A ⊢⇩@ (i, ❙@ k p ❙∧ ❙◇ (❙∙ k)) ⟹ A ⊢⇩@ (i, ❙◇ p)›
    by (metis DiaI SatE conE1 conE2)
  then show ‹⋀A p t. A ⊢⇩@ (case p of (i, p) ⇒ (i, ❙@ t p ❙∧ ❙◇ (❙∙ t))) ⟹ A ⊢⇩@ (case p of (i, p) ⇒ (i, ❙◇ p))›
    by fast
qed

corollary MCS_uni':
  assumes ‹MCS S› ‹witnessed S›
  shows ‹(i, ❙A p) ∈ S ⟷ (∀k. (k, p) ∈ S)›
  using assms MCS_uni by fastforce

corollary MCS_exi':
  assumes ‹MCS S› ‹witnessed S›
  shows ‹(i, ❙◇ p) ∈ S ⟷ (∃k. (i, ❙@k p ❙∧ ❙◇ (❙∙k)) ∈ S)›
  using assms MCS_exi by fastforce

section ‹Nominals›

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

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 ‹[(i, ❙∙j), (j, ❙∙k)] ⊢⇩@ (i, ❙∙j)› ‹[(i, ❙∙j), (j, ❙∙k)] ⊢⇩@ (j, ❙∙k)›
    by simp_all
  then have ‹[(i, ❙∙j), (j, ❙∙k)] ⊢⇩@ (i, ❙∙k)›
    using Nom Ref by metis
  then show ?thesis
    using assms MCS_derive
    by (metis bot.extremum insert_subset list.set(1) list.simps(15))
qed

section ‹Truth Lemma›

fun semics :: ‹('i, 'p, 'w) ctx ⇒ (('i, 'p, 'w) ctx ⇒ ('i, 'p) fm ⇒ bool) ⇒ ('i, 'p) fm ⇒ bool›
  (‹(_ ⟦_⟧⇩@ _)› [55, 0, 55] 55) where
  ‹_ ⟦_⟧⇩@ ❙⊥ ⟷ 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 ∈ W M ∩ R M w. ℛ (M, g, v) p)›
| ‹(M, g, _) ⟦ℛ⟧⇩@ ❙@i p ⟷ ℛ (M, g, g i) p›
| ‹(M, g, _) ⟦ℛ⟧⇩@ ❙A p ⟷ (∀v ∈ W M. ℛ (M, g, v) p)›

fun rel :: ‹('i, 'p) lbd set ⇒ ('i, 'p, 'i) ctx ⇒ ('i, 'p) fm ⇒ bool› (‹ℛ⇩@›) where
  ‹ℛ⇩@(S) (_, _, i) p ⟷ (i, p) ∈ S›

definition equiv_nom :: ‹('i, 'p) lbd set ⇒ 'i ⇒ 'i ⇒ bool› where
  ‹equiv_nom S i k ≡ (i, ❙∙k) ∈ S›

lemma equiv_nom_reflp:
  assumes ‹consistent S› ‹maximal S›
  shows ‹reflp (equiv_nom S)›
  unfolding equiv_nom_def reflp_def using assms MCS_Nom_refl by fast

lemma equiv_nom_symp:
  assumes ‹consistent S› ‹maximal S›
  shows ‹symp (equiv_nom S)›
  unfolding equiv_nom_def symp_def using assms MCS_Nom_sym by fast

lemma equiv_nom_transp:
  assumes ‹consistent S› ‹maximal S›
  shows ‹transp (equiv_nom S)›
  unfolding equiv_nom_def transp_def using assms MCS_Nom_trans by fast

lemma equiv_nom_equivp:
  assumes ‹consistent S› ‹maximal S›
  shows ‹equivp (equiv_nom S)›
  using assms by (simp add: equivpI equiv_nom_reflp equiv_nom_symp equiv_nom_transp)

definition assign :: ‹'i ⇒ ('i, 'p) lbd set ⇒ 'i› (‹[_]⇩_› [0, 100] 100) where
  ‹[i]⇩S ≡ minim ( |UNIV| ) {k. equiv_nom S i k}›

lemma equiv_nom_ne:
  assumes ‹consistent S› ‹maximal S›
  shows ‹{k. equiv_nom S i k} ≠ {}›
  unfolding equiv_nom_def using assms MCS_Nom_refl by fast

lemma equiv_nom_assign:
  assumes ‹consistent S› ‹maximal S›
  shows ‹equiv_nom S i ([i]⇩S)›
  unfolding assign_def using assms equiv_nom_ne wo_rel.minim_in
  by (metis Field_card_of card_of_well_order_on mem_Collect_eq top.extremum wo_rel_def)

lemma equiv_nom_Nom:
  assumes ‹consistent S› ‹maximal S› ‹equiv_nom S i k› ‹(i, p) ∈ S›
  shows ‹(k, p) ∈ S›
proof -
  have ‹[(i, ❙∙k), (i, p)] ⊢⇩@ (k, p)›
    by (meson Assm_head Nom Weak)
  then show ?thesis
    using assms MCS_derive unfolding equiv_nom_def by force
qed

definition reach :: ‹('i, 'p) lbd set ⇒ 'i ⇒ 'i set› where
  ‹reach S i ≡ {[k]⇩S |k. (i, ❙◇ (❙∙k)) ∈ S}›

primrec canonical :: ‹('i, 'p) lbd set × 'i ⇒ ('i, 'p, 'i) ctx› (‹ℳ⇩@›) where
  ‹ℳ⇩@(S, i) = (Model {[k]⇩S | k. True} (reach S) (λi P. (i, ❙⋅P) ∈ S), λi. [i]⇩S, [i]⇩S)›

theorem saturated_model:
  assumes ‹⋀p i. ℳ⇩@(S, i) ⟦ℛ⇩@(S)⟧⇩@(p) ⟷ ℛ⇩@(S) (ℳ⇩@(S, i)) p› ‹M ∈ {ℳ⇩@(S, i) |i. True}›
  shows ‹ℛ⇩@(S) (ℳ⇩@(S, i)) p ⟷ ℳ⇩@(S, 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(1)[of i x] assms(2)
    by (cases x) (auto simp: reach_def)
qed

lemma reach_assign: ‹reach S ([i]⇩S) ⊆ {[k]⇩S | k. True}›
  unfolding reach_def assign_def by blast

theorem saturated_MCS:
  assumes ‹MCS S›
  shows ‹ℳ⇩@(S, i) ⟦ℛ⇩@(S)⟧⇩@(p) ⟷ ℛ⇩@(S) (ℳ⇩@(S, i)) p›
proof (cases p)
  case (Nom k)
  have ‹([i]⇩S = [k]⇩S) ⟷ ([i]⇩S, ❙∙k) ∈ S›
    using assms equiv_nom_equivp equiv_nom_assign by (metis assign_def equivp_def equiv_nom_def)
  then show ?thesis
    using Nom by simp
next
  case (Imp p q)
  have ‹(([i]⇩S, p) ∈ S ⟶ ([i]⇩S, q) ∈ S) ⟷ ([i]⇩S, p ❙⟶ q) ∈ S›
    using assms MCS_derive MCS_explode MCS_impE' by (metis ImpI Weaken set_subset_Cons)
  then show ?thesis
    using Imp by simp
next
  case (Dia p)
  have ‹([i]⇩S, ❙◇ p) ∈ S ⟷ (∃k. ([i]⇩S, ❙@k p ❙∧ ❙◇(❙∙k)) ∈ S)›
    using assms MCS_exi by fastforce

  moreover have ‹([i]⇩S, ❙@k p ❙∧ ❙◇(❙∙k)) ∈ S ⟷ ([i]⇩S, ❙@k p) ∈ S ∧ ([i]⇩S, ❙◇(❙∙k)) ∈ S› for k
    using assms MCS_con by fast
  moreover have ‹([i]⇩S, ❙@k p) ∈ S ⟷ (k, p) ∈ S› for k
    using assms by (meson MCS_derive SatE SatI)
  moreover have ‹(k, p) ∈ S ⟷ ([k]⇩S, p) ∈ S› for k
    using assms by (meson MCS_Nom_refl equiv_nom_Nom equiv_nom_assign equiv_nom_def)
  moreover have ‹([i]⇩S, ❙◇(❙∙k)) ∈ S ⟹ [k]⇩S ∈ reach S ([i]⇩S)› for k
    unfolding reach_def by blast

  ultimately have ‹([i]⇩S, ❙◇ p) ∈ S ⟷ (∃k ∈ reach S ([i]⇩S). (k, p) ∈ S)›
    unfolding reach_def by blast
  then show ?thesis
    using Dia reach_assign by fastforce
next
  case (Sat k p)
  have ‹([k]⇩S, p) ∈ S ⟷ ([i]⇩S, ❙@k p) ∈ S›
    by (metis SatE SatI assms MCS_derive equiv_nom_Nom equiv_nom_assign equiv_nom_symp sympD)
  then show ?thesis
    using Sat by simp
next
  case (All p)
  have ‹([i]⇩S, ❙A p) ∈ S ⟷ (∀k. (k, p) ∈ S)›
    using assms MCS_uni by fastforce
  then have ‹([i]⇩S, ❙A p) ∈ S ⟷ (∀k. ([k]⇩S, p) ∈ S)›
    by (meson MCS_Nom_sym assms equiv_nom_Nom equiv_nom_assign equiv_nom_def)
  then show ?thesis
    using All by auto
qed (use assms in auto)

interpretation Truth_Witness semics semantics ‹λS. {ℳ⇩@(S, i) |i. True}› rel consistent witness nominals_lbd
proof
  fix p and M :: ‹('i, 'p, 'w) ctx›
  show ‹(M ⊨⇩@ p) = M ⟦semantics⟧⇩@(p)›
    by (cases M, induct p) auto
next
  fix p M and S :: ‹('i, 'p) lbd set›
  assume ‹∀p. ∀M∈{ℳ⇩@ (S, i) |i. True}. M ⟦ℛ⇩@(S)⟧⇩@ p ⟷ ℛ⇩@(S) M p› ‹M ∈ {ℳ⇩@(S, i) |i. True}›
  then show ‹M ⊨⇩@ p ⟷ ℛ⇩@(S) M p›
    using saturated_model by fast
next                
  fix S :: ‹('i, 'p) lbd set›
  assume ‹MCS S›
  then show ‹∀p. ∀M∈{ℳ⇩@(S, i) |i. True}. M ⟦ℛ⇩@(S)⟧⇩@ p ⟷ ℛ⇩@(S) M p›
    using saturated_MCS by fastforce
qed

lemma Truth_lemma:
  assumes ‹MCS S›
  shows ‹ℳ⇩@(S, i) ⊨⇩@ p ⟷ (i, p) ∈ S›
proof -
  have ‹ℳ⇩@(S, i) ⊨⇩@ p ⟷ ([i]⇩S, p) ∈ S›
    using assms truth_lemma by fastforce
  then show ?thesis
    using assms by (meson MCS_Nom_sym equiv_nom_Nom equiv_nom_assign equiv_nom_def)
qed

section ‹Cardinalities›

datatype marker = FlsM | ImpM | DiaM | SatM | AllM

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)›
abbreviation ‹GLO ≡ Inr (AllM, 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›
| ‹encode (❙A p) = GLO # 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 i p)
  then show ?case
    by (cases q) auto
next
  case (All p)
  then show ?case
    by (cases q) auto
qed

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, AllM}› 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 ∈ W M. range g ⊆ W M ⟶
      (∀(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 ⊆ {(i, ❙¬ p)} ∪ X ⟶ ¬ A ⊢⇩@ (a, ❙⊥)›
    using Boole FlsE by (metis derive_split1 insert_is_Un subset_insert)

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

  have ‹consistent ?X›
    unfolding consistent_def using * by blast
  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 ?X|›
    by (metis UN_insert insert_is_Un sup_commute)
  then have ‹|UNIV :: ('i, 'p) lbd set| ≤o |UNIV - nominals ?X|›
    using assms card_of_lbd ordLeq_transitive by blast
  ultimately have ‹MCS ?S›
    using MCS_Extend by fast
  then have ‹ℳ⇩@(?S, i) ⊨⇩@ p ⟷ (i, p) ∈ ?S› for i p
    using Truth_lemma by fast
  then have ‹(i, p) ∈ ?X ⟹ ℳ⇩@(?S, i) ⊨⇩@ p› for i p
    using Extend_subset by blast
  then have ‹ℳ⇩@(?S, i) ⊨⇩@ ❙¬ p› ‹∀(k, q) ∈ X. ℳ⇩@(?S, k) ⊨⇩@ q›
    by blast+
  moreover from this have ‹ℳ⇩@(?S, i) ⊨⇩@ p›
    using assms(1) by force
  ultimately show False
    by simp
qed

abbreviation valid :: ‹('i, 'p) fm ⇒ bool› where
  ‹valid p ≡ ∀(M :: ('i, 'p) model) g. ∀w ∈ W M. range g ⊆ W M ⟶ (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