Theory Bisimulation_Logic

(* 

  A meta-modal logic for bisimulations
  Authors: Alfredo Burrieza, Fernando Soler-Toscano, Antonio Yuste-Ginel

*)

text ‹This theory introduces a modal logic for reasoning about bisimulations (more details on 
  \<^cite>‹"burrieza2025metamodallogicbisimulations"›). The proofs rely on various results concerning 
  maximally consistent sets, drawn from the APF entry \emph{Synthetic Completeness} by 
  Asta Halkjær From \<^cite>‹"HalkSyntComp"›.›

theory Bisimulation_Logic 
  imports "Synthetic_Completeness.Derivations" 
begin

section ‹Syntax›

text ‹First, the language ‹ℒ⇩□⇩[⇩b⇩]› is introduced:›

datatype 'p fm
  = Fls (‹❙⊥›)
  | Pro 'p (‹❙⋅›)
  | Imp ‹'p fm› ‹'p fm› (infixr ‹❙⟶› 55)
  | Box ‹'p fm› (‹❙□ _› [70] 70)
  | FrB ‹'p fm› (‹❙[b❙] _› [70] 70)

text ‹Defined connectives.›

abbreviation Not (‹❙¬ _› [70] 70) where
  ‹❙¬ p ≡ p ❙⟶ ❙⊥›
abbreviation Tru (‹❙⊤›) where 
  ‹❙⊤ ≡ ❙¬❙⊥›
abbreviation Dis (infixr ‹❙∨› 60) where
  ‹A ❙∨ B ≡ ❙¬A ❙⟶ B›
abbreviation Con (infixr ‹❙∧› 65) where
  ‹A ❙∧ B ≡ ❙¬(A ❙⟶ ❙¬B)›
abbreviation Iff (infixr ‹❙⟷› 55) where
  ‹A ❙⟷ B ≡ (A ❙⟶ B) ❙∧ (B ❙⟶ A)›
abbreviation Dia (‹❙◇ _› [70] 70) where 
  ‹❙◇A ≡ ❙¬❙□❙¬A›
abbreviation FrD (‹❙⟨b❙⟩ _› [70] 70) where 
  ‹❙⟨b❙⟩A ≡ ❙¬❙[b❙]❙¬A›

text ‹Iteration of modal operators ‹❙□› and ‹❙◇›.›

primrec chain_b :: ‹nat ⇒ 'p fm ⇒ 'p fm› (‹❙□^_ _› [70, 70] 70) where
  ‹❙□^0 f = f›
| ‹❙□^(Suc n) f = ❙□(❙□^n f)›

primrec chain_d :: ‹nat ⇒ 'p fm ⇒ 'p fm› (‹❙◇^_ _› [70, 70] 70) where
  ‹❙◇^0 f = f›
| ‹❙◇^(Suc n) f = ❙◇(❙◇^n f)›

lemma chain_bd_sum:
  ‹❙□^n (❙□^m F) = ❙□^(n+m) F› and 
  ‹❙◇^n (❙◇^m F) = ❙◇^(n+m) F›
  by (induct n) simp_all

section ‹Semantics›

text ‹This is the type of both left and right models:›

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

text ‹Given a model ‹ℳ› ‹W ℳ› denotes its set of worlds, ‹R ℳ› the accessibility relation and 
‹V ℳ› the valuation function.›

text ‹This is the type of a model in ‹ℒ⇩□⇩[⇩b⇩]›:›

datatype ('p, 'w) modelLb =
  ModelLb (M1: ‹('p, 'w) model›) (M2: ‹('p, 'w) model›) (Z : ‹('w × 'w) set›) 

text ‹Given a model ‹𝔐› of ‹ℒ⇩□⇩[⇩b⇩]›, ‹M1 𝔐› denotes the model on the left, ‹M2 𝔐› the model on 
the right and ‹Z 𝔐› the bisimulation relation.›

text ‹Bi-models are a relevant class of ‹ℒ⇩□⇩[⇩b⇩]›, as we will prove soundness and completeness of 
  the proof system ‹⊢⇩B› for bi-models. First, the conditions for ‹𝔐› to be a ‹bi-model› are 
introduced.›

definition bi_model :: ‹('p, 'w) modelLb ⇒ bool› where
  ‹bi_model 𝔐  ≡
    ― ‹‹M1› and ‹M2› have non-empty domains›
    W (M1 𝔐) ≠ {} ∧ W (M2 𝔐) ≠ {} ∧ 
    ― ‹‹R1› and ‹R2› are defined in the corresponding domains›
    R (M1 𝔐) ⊆ (W (M1 𝔐)) × (W (M1 𝔐)) ∧
    R (M2 𝔐) ⊆ (W (M2 𝔐)) × (W (M2 𝔐)) ∧
    ― ‹‹Z› is a non-empty relation from ‹W (M1 𝔐)› to ‹W (M2 𝔐)› ›
    Z 𝔐 ≠ {} ∧ Z 𝔐 ⊆ (W (M1 𝔐)) × (W (M2 𝔐)) ∧
    ― ‹Atomic harmony›
    (∀ w w' . (w, w') ∈ Z 𝔐 ⟶ ((V (M1 𝔐)) w) = ((V (M2 𝔐)) w')) ∧
    ― ‹Forth›
    (∀ w w' v . (w, w') ∈ Z 𝔐 ∧ (w,v) ∈ R (M1 𝔐) ⟶ 
        (∃ v' . (v,v') ∈ Z 𝔐 ∧ (w', v') ∈ R (M2 𝔐))) ∧
    ― ‹Back›
    (∀ w w' v' . (w, w') ∈ Z 𝔐 ∧ (w',v') ∈ R (M2 𝔐) ⟶ (∃ v . (v,v') ∈ Z 𝔐 ∧ (w,v) ∈ R (M1 𝔐)))›

text ‹In the semantics, formulas are evaluated differently depending on the pointed world is on the
  left (‹ℳ›) or on the right (‹ℳ'›). Datatype ‹ep› (evaluation point) indicates the side of a 
  model in which a given formula is evaluated.›

datatype ep = 𝗆 | 𝗆'

― ‹Pointed model ‹(ℳ,w)›.›
type_synonym ('p, 'w) Mctx  = ‹('p, 'w) model  × 'w›

― ‹Pointed ‹ℒ⇩□⇩[⇩b⇩]›-modelLb ‹(𝔐,ℳ⇧('⇧),w)›.›
type_synonym ('p, 'w) MLbCtx = ‹('p, 'w) modelLb × ep × 'w›

text ‹Definition of truth in a pointed ‹ℒ⇩□⇩[⇩b⇩]›-modelLb.›

fun semantics :: ‹('p, 'w) MLbCtx ⇒ 'p fm ⇒ bool› (infix ‹⊨⇩B› 50) where
  ‹_ ⊨⇩B( ❙⊥::('p fm)) ⟷ False›
| ‹(𝔐, 𝗆, w)  ⊨⇩B ❙⋅P ⟷ V (M1 𝔐) w P›
| ‹(𝔐, 𝗆', w) ⊨⇩B ❙⋅P ⟷ V (M2 𝔐) w P›
| ‹(𝔐, e, w) ⊨⇩B A ❙⟶ B ⟷ (𝔐, e, w) ⊨⇩B A ⟶ (𝔐, e, w) ⊨⇩B B›
| ‹(𝔐, 𝗆, w) ⊨⇩B ❙□A ⟷ (∀ v ∈ W (M1 𝔐) . (w,v) ∈ R (M1 𝔐) ⟶ (𝔐, 𝗆, v) ⊨⇩B A)›
| ‹(𝔐, 𝗆', w) ⊨⇩B ❙□A ⟷ (∀ v ∈ W (M2 𝔐) . (w,v) ∈ R (M2 𝔐) ⟶ (𝔐, 𝗆', v) ⊨⇩B A)›
| ‹(𝔐, 𝗆, w) ⊨⇩B ❙[b❙]A ⟷ (∀ w' ∈ W (M2 𝔐) . (w,w') ∈ (Z 𝔐) ⟶ (𝔐, 𝗆', w') ⊨⇩B A)›
| ‹(𝔐, 𝗆', w) ⊨⇩B ❙[b❙]A ⟷ True›

section ‹Calculus›

text ‹Function ‹eval› and ‹tautology› define what is a propositional tautology.›

primrec eval :: ‹('p ⇒ bool) ⇒ ('p fm ⇒ bool) ⇒ 'p fm ⇒ bool› where
  ‹eval _ _ ❙⊥ = False›
| ‹eval g _ (❙⋅P) = g P›
| ‹eval g h (A ❙⟶ B) = (eval g h A ⟶ eval g h B)›
| ‹eval _ h (❙□A) = h (❙□A)›
| ‹eval _ h (❙[b❙]A) = h (❙[b❙]A)›

abbreviation ‹tautology p ≡ ∀g h. eval g h p›

― ‹Example of propositional tautology›
lemma ‹tautology (❙[b❙]A ❙∨ ❙¬❙[b❙]A)› by simp

text ‹Finally, the axiom system ‹⊢⇩B› is presented.›

inductive Calculus :: ‹'p fm ⇒ bool› (‹⊢⇩B _› [50] 50) where
  TAU:   ‹tautology A ⟹ ⊢⇩B A›
| KSq:   ‹⊢⇩B ❙□ (A ❙⟶ B) ❙⟶ (❙□A ❙⟶ ❙□B)›
| Kb:    ‹⊢⇩B ❙[b❙](A ❙⟶ B) ❙⟶ (❙[b❙]A ❙⟶❙[b❙]B)›
| FORTH: ‹⊢⇩B (❙⟨b❙⟩A ❙∧ ❙◇❙[b❙]B) ❙⟶ ❙⟨b❙⟩(A ❙∧ ❙◇B)›    
| BACK:  ‹⊢⇩B ❙⟨b❙⟩❙◇A ❙⟶ ❙◇❙⟨b❙⟩A›                    
| HARM:  ‹(l = ❙⋅p ∨ l = ❙¬❙⋅p) ⟹ ⊢⇩B l ❙⟶ ❙[b❙]l›
| NTS:   ‹⊢⇩B ❙[b❙]❙[b❙]❙⊥›                            
| MP:    ‹⊢⇩B A ❙⟶ B ⟹ ⊢⇩B A ⟹ ⊢⇩B B›
| NSq:   ‹⊢⇩B A ⟹ ⊢⇩B ❙□A›
| Nb:    ‹⊢⇩B A ⟹ ⊢⇩B ❙[b❙]A›

text ‹Proofs use nested conditionals. Given a list ‹A = [A⇩1, ..., A⇩n]› of formulas, 
‹A ❙↝ B› represents ‹A⇩1 ⟶ (A⇩2 ⟶ ... (A⇩n ⟶ B))›.› 

primrec imply :: ‹'p fm list ⇒ 'p fm ⇒ 'p fm› (infixr ‹❙↝› 56) where
  ‹([] ❙↝ B) = B›
| ‹(A # Λ ❙↝ B) = (A ❙⟶ Λ ❙↝ B)›

abbreviation Calculus_assms (infix ‹⊢⇩B› 50) where
  ‹Λ ⊢⇩B A ≡ ⊢⇩B Λ ❙↝ A›

section ‹Soundness›

text ‹These lemmas will be used to prove soundness.›

lemma atomic_harm:
  assumes ‹bi_model 𝔐›
  and "(w,w')∈ Z 𝔐"
shows "((V (M1 𝔐)) w p) = ((V (M2 𝔐)) w' p)" using assms bi_model_def by metis

lemma eval_semantics: 
  assumes ‹bi_model 𝔐›
  shows ‹eval (V (M1 𝔐) w) (λq. (𝔐, 𝗆, w) ⊨⇩B q) p = ((𝔐, 𝗆, w) ⊨⇩B p)› and
        ‹eval (V (M2 𝔐) w) (λq. (𝔐, 𝗆', w) ⊨⇩B q) p = ((𝔐, 𝗆', w) ⊨⇩B p)›
  by (induct p) simp_all

text ‹Tautologies are always true.›

lemma tautology:
  assumes ‹tautology A› 
    and ‹bi_model 𝔐›
  shows ‹(𝔐, e, w) ⊨⇩B A› 
  by (metis (full_types) assms(1,2) ep.exhaust eval_semantics(1,2))

text ‹Axiom FORTH is valid in all worlds in ‹ℳ› of bi-models.›

lemma b_forth:
  assumes ‹bi_model 𝔐› and
  ‹w ∈ W (M1 𝔐)›
  shows 
    ‹(𝔐, 𝗆, w)  ⊨⇩B (❙⟨b❙⟩F ❙∧ ❙◇❙[b❙]G) ❙⟶ ❙⟨b❙⟩(F ❙∧ ❙◇G)› 
proof -
  {assume A: ‹(𝔐, 𝗆, w)  ⊨⇩B (❙⟨b❙⟩F ❙∧ ❙◇❙[b❙]G)›
    then obtain w' where w': 
     ‹w' ∈ W (M2 𝔐) ∧ (w,w') ∈ Z 𝔐 ∧ ((𝔐, 𝗆', w')  ⊨⇩B F)›
      by fastforce
    obtain w2 where w2: ‹w2 ∈ W (M1 𝔐) ∧ (w, w2) ∈ R (M1 𝔐) ∧ 
      (𝔐, 𝗆, w2)  ⊨⇩B ❙[b❙]G› using A assms by auto
    then obtain w2' where w2': ‹w2' ∈ W (M2 𝔐) ∧ (w', w2') ∈ R (M2 𝔐) ∧ 
      (w2, w2') ∈ Z 𝔐› using bi_model_def assms w' 
      by (smt (verit, ccfv_SIG) SigmaD2 in_mono)  
    hence ‹(𝔐, 𝗆, w) ⊨⇩B ❙⟨b❙⟩(F ❙∧ ❙◇G)› using assms w' w2 by auto}
  thus ?thesis by auto
qed

text ‹Axiom FORTH is valid in all worlds on ‹ℳ'› (bi-models).›

lemma b_forth2:
  assumes ‹bi_model 𝔐› and
  ‹w ∈ W (M2 𝔐)›
  shows 
    ‹(𝔐, 𝗆', w)  ⊨⇩B (❙⟨b❙⟩F ❙∧ ❙◇❙[b❙]G) ❙⟶ ❙⟨b❙⟩(F ❙∧ ❙◇G)› 
  by simp

text ‹Axiom BACK is valid in all worlds on ‹ℳ› (bi-models).›

lemma b_back:
  assumes ‹bi_model 𝔐› and
  ‹w ∈ W (M1 𝔐)›
  shows 
    ‹(𝔐, 𝗆, w) ⊨⇩B ❙⟨b❙⟩❙◇F ❙⟶ ❙◇❙⟨b❙⟩F› 
proof -
  {assume ‹(𝔐, 𝗆, w) ⊨⇩B ❙⟨b❙⟩❙◇F›
    then obtain w' where w': ‹w' ∈ W (M2 𝔐) ∧ 
      (w,w') ∈ Z 𝔐 ∧ (𝔐, 𝗆', w')  ⊨⇩B ❙◇F› by auto
    then obtain w2' where w2': ‹w' ∈ W (M2 𝔐) ∧ 
      (w',w2') ∈ R (M2 𝔐) ∧ (𝔐, 𝗆', w2')  ⊨⇩B F› by auto
    then obtain w2 where w2: ‹w2 ∈ W (M1 𝔐) ∧ (w,w2) ∈ R (M1 𝔐) ∧ 
      (w2,w2') ∈ Z 𝔐› using assms bi_model_def w' w2' 
      by (smt (verit, best) SigmaD2 bi_model_def in_mono)
    hence ‹(𝔐, 𝗆, w2) ⊨⇩B ❙⟨b❙⟩F› using assms w2' w2 
      by (metis (no_types, lifting) SigmaD2 bi_model_def in_mono
          semantics.simps(1,4,7))
    hence ‹(𝔐, 𝗆, w) ⊨⇩B ❙◇❙⟨b❙⟩F› using w2 assms by auto
  } 
  thus ?thesis by simp
qed

text ‹Axiom BACK is valid in all worlds on ‹ℳ'› (bi-models).›

lemma b_back2:
  assumes ‹bi_model 𝔐› and
  ‹w ∈ W (M2 𝔐)›
  shows 
    ‹(𝔐, 𝗆', w)  ⊨⇩B ❙⟨b❙⟩❙◇F ❙⟶ ❙◇❙⟨b❙⟩F› by simp

text ‹Soundness theorem›

theorem soundness: 
  ‹ ⊢⇩B A ⟹ bi_model 𝔐 ⟹ 
    (w ∈ W (M1 𝔐) ⟶ (𝔐, 𝗆, w) ⊨⇩B A) ∧ 
    (w ∈ W (M2 𝔐) ⟶ (𝔐, 𝗆', w) ⊨⇩B A)› 
proof (induct A arbitrary: w rule: Calculus.induct)
  case (TAU F)
  then show ?case 
    by (simp add: tautology)
next
  case (FORTH F G)
  then show ?case by (metis b_forth2 b_forth)
next
  case (BACK F)
  then show ?case by (metis b_back b_back2)
next
  case (HARM l)
  then show ?case using atomic_harm by fastforce
qed auto

section ‹Admissible rules›

text ‹These lemmas are mostly from the AFP entry ``Synthetic Completeness'' by Asta Halkjær From.›

lemma K_imply_head: ‹p # A ⊢⇩B p›
proof -
  have ‹tautology (p # A ❙↝ p)›
    by (induct A) simp_all
  then show ?thesis using TAU by blast
qed

lemma K_imply_Cons:
  assumes ‹A ⊢⇩B q›
  shows ‹p # A ⊢⇩B q›
  using assms 
  by (metis K_imply_head MP imply.simps(1,2))

lemma K_right_mp:
  assumes ‹A ⊢⇩B p› ‹A ⊢⇩B p ❙⟶ q›
  shows ‹A ⊢⇩B q›
proof -
  have ‹tautology (A ❙↝ p ❙⟶ A ❙↝ (p ❙⟶ q) ❙⟶ A ❙↝ q)›
    by (induct A) simp_all
  with TAU have ‹⊢⇩B A ❙↝ p ❙⟶ A ❙↝ (p ❙⟶ q) ❙⟶ A ❙↝ q› .
  then show ?thesis
    using assms MP by blast
qed

lemma deduct1: ‹A ⊢⇩B p ❙⟶ q ⟹ p # A ⊢⇩B q›
  by (meson K_right_mp K_imply_Cons K_imply_head)

lemma imply_append [iff]: ‹(A @ B ❙↝ r) = (A ❙↝ B ❙↝ r)›
  by (induct A) simp_all

lemma imply_swap_append: ‹A @ B ⊢⇩B r ⟹ B @ A ⊢⇩B r›
proof (induct B arbitrary: A)
  case Cons
  then show ?case
    by (metis deduct1 imply.simps(2) imply_append)
qed simp

lemma K_ImpI: ‹p # A ⊢⇩B q ⟹ A ⊢⇩B p ❙⟶ q›
  by (metis imply.simps imply_append imply_swap_append)

lemma imply_mem [simp]: ‹p ∈ set A ⟹ A ⊢⇩B p›
  using K_imply_head K_imply_Cons by (induct A) fastforce+

lemma add_imply [simp]: ‹⊢⇩B q ⟹ A ⊢⇩B q›
  using K_imply_head MP by auto

lemma K_imply_weaken: ‹A ⊢⇩B q ⟹ set A ⊆ set A' ⟹ A' ⊢⇩B q›
  by (induct A arbitrary: q) (simp, metis K_right_mp K_ImpI 
      imply_mem insert_subset list.set(2))

lemma K_Boole:
  assumes ‹(❙¬ p) # A ⊢⇩B ❙⊥›
  shows ‹A ⊢⇩B p›
proof -
  have T: ‹tautology ((❙¬ p ❙⟶ ❙⊥) ❙⟶  ❙¬❙¬p)› 
    by simp
  have ‹A ⊢⇩B ❙¬ ❙¬ p›
    using assms K_ImpI T 
    using TAU K_right_mp add_imply by blast 
  moreover have ‹tautology (A ❙↝ ❙¬ ❙¬ p ❙⟶ A ❙↝ p)›
    by (induct A) simp_all
  then have ‹⊢⇩B (A ❙↝ ❙¬ ❙¬ p ❙⟶ A ❙↝ p)›
    using TAU by blast
  ultimately show ?thesis
    using MP by blast
qed

lemma MP_chain:
  assumes ‹⊢⇩B A ❙⟶ B›
  and ‹⊢⇩B B ❙⟶ C›
shows ‹⊢⇩B A ❙⟶ C› 
proof -
  have ‹⊢⇩B (A ❙⟶ B) ❙⟶ (( B ❙⟶ C) ❙⟶ (A ❙⟶ C))› using TAU by force
  thus ?thesis using assms MP by auto
qed

text ‹This locale is use to prove common results of normal modal operators. As both ‹❙□› and ‹❙[b❙]› 
  are normal, result involving ‹❙K› in ‹Kop› will be applied to them.›

locale Kop =
  fixes K :: "'p fm ⇒ 'p fm"  (‹❙K _› [70] 70)
  assumes Kax: "⊢⇩B ❙K (A ❙⟶ B) ❙⟶ (❙K A ❙⟶ ❙K B)"
    and KN:  "⊢⇩B A ⟹ ⊢⇩B ❙K A"

context Kop begin

abbreviation P (‹❙P _› [70] 70) where ‹❙P A ≡ ❙¬❙K❙¬A›

lemma K_distrib_K_imp:
  assumes ‹⊢⇩B ❙K (A ❙↝ q)›
  shows ‹map (λ x . ❙K x) A ⊢⇩B ❙K q›
proof -
  have ‹⊢⇩B ❙K (A ❙↝ q) ❙⟶ map  (λ x . ❙K x) A ❙↝ ❙K q›
  proof (induct A)
    case Nil
    then show ?case
      by (simp add: TAU)
  next
    case (Cons a A)
    have ‹⊢⇩B ❙K (a # A ❙↝ q) ❙⟶ ❙K a ❙⟶ ❙K (A ❙↝ q)›
      by (simp add: Kax)
    moreover have
      ‹⊢⇩B ((❙K (a # A ❙↝ q) ❙⟶ ❙K a ❙⟶ ❙K (A ❙↝ q)) ❙⟶
        (❙K (A ❙↝ q) ❙⟶ map  (λ x . ❙K x) A ❙↝ ❙K q) ❙⟶
        (❙K (a # A ❙↝ q) ❙⟶ ❙K a ❙⟶ map  (λ x . ❙K x) A ❙↝ ❙K q))›
      using TAU by force
    ultimately have ‹⊢⇩B ❙K (a # A ❙↝ q) ❙⟶ ❙K a ❙⟶ map  (λ x . ❙K x) A ❙↝ ❙K  q›
      using Cons MP by blast
    then show ?case
      by simp
  qed
  then show ?thesis
    using assms MP by blast
qed

lemma Kpos:
  shows ‹⊢⇩B ❙K(A ❙⟶ B) ❙⟶ (❙PA ❙⟶ ❙PB)›
proof-
  have ‹⊢⇩B (A ❙⟶ B) ❙⟶ (❙¬B ❙⟶ ❙¬A)› using TAU by force
  hence 1: ‹⊢⇩B ❙K(A ❙⟶ B) ❙⟶ (❙K❙¬B ❙⟶ ❙K❙¬A)› 
   by (meson KN Kax MP MP_chain)
  have ‹⊢⇩B  (❙K❙¬B ❙⟶ ❙K❙¬A) ❙⟶ (❙PA ❙⟶ ❙PB)› using TAU by force
  thus ?thesis using 1 MP_chain by blast
qed

end

text ‹Both ‹❙□› and ‹❙[b❙]› are normal modal operators.›

interpretation KBox: Kop "λ A . ❙□ A" 
  by (simp add: KSq Kop_def NSq)

interpretation KFrB: Kop "λ A . ❙[b❙] A"
  by (simp add: Kb Kop.intro Nb)

text ‹Some other useful theorems of ‹⊢⇩B› that are used in later proofs.›

text ‹First, the box-version of BACK axiom.›

lemma BACK_rev:
  ‹⊢⇩B ❙□❙[b❙]F ❙⟶ ❙[b❙]❙□F›  
proof -
  have A: ‹ ⊢⇩B (❙¬❙[b❙]❙¬❙¬❙□❙¬❙¬F ❙⟶ ❙¬ ❙□❙¬❙¬❙[b❙]❙¬❙¬F)› using BACK .
  have ‹ ⊢⇩B (❙¬❙[b❙]❙¬❙¬❙□❙¬❙¬F ❙⟶ ❙¬ ❙□❙¬❙¬❙[b❙]❙¬❙¬F) ❙⟶ ( ❙□❙¬❙¬❙[b❙]❙¬❙¬F ❙⟶ ❙[b❙]❙¬❙¬❙□❙¬❙¬F)› 
    using TAU MP by force
  hence f1: ‹⊢⇩B ❙□❙¬❙¬❙[b❙]❙¬❙¬F ❙⟶ ❙[b❙]❙¬❙¬❙□❙¬❙¬F› using A MP by auto
  have ‹⊢⇩B  ❙□(❙[b❙]❙¬❙¬F ❙⟶ ❙¬❙¬❙[b❙]❙¬❙¬F)› using TAU NSq by force
  hence f2: ‹⊢⇩B  ❙□❙[b❙]❙¬❙¬F ❙⟶ ❙□❙¬❙¬❙[b❙]❙¬❙¬F› using KSq MP by auto
  have ‹⊢⇩B ❙[b❙](F ❙⟶ ❙¬❙¬F)› using TAU Nb by force
  hence ‹⊢⇩B ❙□(❙[b❙]F ❙⟶ ❙[b❙]❙¬❙¬F)› using Kb NSq MP by force
  hence ‹⊢⇩B ❙□❙[b❙]F ❙⟶ ❙□❙[b❙]❙¬❙¬F› using KSq MP by auto
  hence f3: ‹⊢⇩B ❙□❙[b❙]F ❙⟶ ❙[b❙]❙¬❙¬❙□❙¬❙¬F› using f1 f2 MP_chain by blast
  have ‹⊢⇩B ❙[b❙](❙¬❙¬❙□❙¬❙¬F ❙⟶ ❙□❙¬❙¬F)› using TAU Nb by force
  hence f4: ‹⊢⇩B ❙[b❙]❙¬❙¬❙□❙¬❙¬F ❙⟶ ❙[b❙]❙□❙¬❙¬F› using Kb MP by auto
  have ‹⊢⇩B ❙[b❙]❙□(❙¬❙¬F ❙⟶ F)› using  TAU Nb NSq by force
  hence ‹⊢⇩B ❙[b❙]❙□❙¬❙¬F ❙⟶ ❙[b❙]❙□F› using KSq Kb MP Nb by metis
  thus ?thesis using f3 f4 MP_chain by blast
qed

― ‹Generalization of axiom NTS.›
lemma NTSgen:
  ‹⊢⇩B ❙[b❙] ❙□^n ❙[b❙]❙⊥› 
proof (induct n)
  case 0
  then show ?case using NTS chain_b_def by simp
next
  case (Suc n)
  fix n
  assume ‹⊢⇩B ❙[b❙] ❙□^n ❙[b❙] (❙⊥::'p fm)›
  hence ‹⊢⇩B  ❙□ ❙[b❙] ❙□^n ❙[b❙] (❙⊥::'p fm)› using NSq by auto
  thus ‹⊢⇩B  ❙[b❙] ❙□^(Suc n) ❙[b❙] (❙⊥::'p fm)› using BACK_rev MP by auto
qed


section ‹Maximal Consistent Sets›

text ‹These definitions and lemmas are mostly from the AFP entry ``Synthetic Completeness'' by 
  Asta Halkjær From.›

― ‹Definition of consistency and several useful lemmas›
definition consistent :: ‹'p fm set ⇒ bool› where
  ‹consistent S ≡ ∀A. set A ⊆ S ⟶ ¬ A ⊢⇩B ❙⊥›

interpretation MCS_No_Witness_UNIV consistent
proof
  show ‹infinite (UNIV :: 'p fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed (auto simp: consistent_def)

interpretation Derivations_Cut_MCS consistent Calculus_assms
proof
  fix A B and p :: ‹'p fm›
  assume ‹⊢⇩B A ❙↝ p› ‹set A = set B›
  then show ‹⊢⇩B B ❙↝ p›
    using K_imply_weaken by blast
next
  fix S :: ‹'p fm set›
  show ‹consistent S = (∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢⇩B q))›
    unfolding consistent_def using K_Boole K_imply_Cons by blast
next
  fix A B and p q :: ‹'p fm›
  assume ‹A ⊢⇩B p› ‹p # B ⊢⇩B q›
  then show ‹A @ B ⊢⇩B q›
    by (metis K_right_mp add_imply imply.simps(2) imply_append)
qed simp

interpretation Derivations_Bot consistent Calculus_assms ‹❙⊥›
proof
  show ‹⋀A r. A ⊢⇩B ❙⊥ ⟹ A ⊢⇩B r›
    using K_Boole K_imply_Cons by blast
qed

interpretation Derivations_Imp consistent Calculus_assms ‹λp q. p ❙⟶ q›
proof
  show ‹⋀A p q. p # A ⊢⇩B q ⟹ A ⊢⇩B p ❙⟶ q›
    using K_ImpI by blast
  show ‹⋀A p q. A ⊢⇩B p ⟹ A ⊢⇩B p ❙⟶ q ⟹ A ⊢⇩B q›
    using K_right_mp by blast
qed

theorem deriv_in_maximal:
  assumes ‹consistent S› ‹maximal S› ‹⊢⇩B p›
  shows ‹p ∈ S›
  using assms MCS_derive by fastforce

lemma dia_not_box_bot:
  assumes ‹consistent S› ‹maximal S› ‹❙⟨b❙⟩ F ∈ S›
  shows ‹❙¬❙[b❙]❙⊥ ∈ S› 
proof -
  have ‹❙¬❙[b❙]❙¬F ∈ S› using assms(3) by simp
  have ‹❙⊥ ❙⟶ ❙¬F ∈ S› by (simp add: MCS_impI assms(1,2))
  hence ‹❙[b❙](❙⊥ ❙⟶ ❙¬F) ∈ S› using Calculus.Nb 
    by (metis K_imply_head assms(1,2) deriv_in_maximal imply.simps(1,2))
  hence ‹❙[b❙]❙⊥ ❙⟶ ❙[b❙]❙¬F ∈ S›
    by (meson Kb MCS_imp assms(1,2) deriv_in_maximal)
  thus ‹❙¬❙[b❙]❙⊥ ∈ S› using ‹❙¬❙[b❙]❙¬F ∈ S›
    by (simp add: MCS_imp assms(1,2))
qed

text ‹Some other useful lemmas that are repeatedly used in proofs.›

lemma not_empty:
  assumes ‹a ∈ A›
  shows ‹A ≠ {}› 
  using assms by auto

lemma MPcons:
  assumes ‹⊢⇩B A ❙⟶ (B ❙⟶ C)›
  and ‹⊢⇩B B›
shows ‹⊢⇩B A ❙⟶ C› 
  by (metis K_right_mp add_imply assms(1,2) imply.simps(1,2))

lemma multiple_MP_MCS:
  assumes ‹MCS S›
  and ‹set A ⊆ S›
  and ‹A ❙↝ f ∈ S›
shows ‹f ∈ S› using assms by (induct A) auto

lemma not_imp_to_conj:
  assumes ‹MCS A›
  and ‹❙¬(B ❙↝ ❙⊥) ∈ A›
shows ‹set B ⊆ A› 
proof (rule ccontr)
  assume ‹¬ set B ⊆ A›
  then obtain f where f: ‹f ∈ set B ∧ f ∉ A› by auto
  hence ‹(B ❙↝ ❙⊥) ∈ A› 
    by (smt (verit, ccfv_SIG) MCS_derive MCS_explode assms(1) derive_assm 
        derive_cut imply_append imply_swap_append)
  thus False using assms(2) 
    using MCS_bot assms(1) by blast
qed

text ‹Several lemmas of ‹Kop›, valid for normal modal operators.›

context Kop begin

lemma not_pos_to_nec_not:
  shows ‹⊢⇩B ❙¬❙PF ❙⟶ ❙K❙¬F› 
proof -
  have P1: ‹⊢⇩B ((❙PF ❙⟷ ❙¬❙K❙¬F) ❙⟶ (❙¬❙PF ❙⟶ ❙K❙¬F))› using TAU by force
  have ‹⊢⇩B ❙PF ❙⟷ ❙¬❙K❙¬F› using TAU by force
  thus ?thesis using P1 MP by auto
qed

lemma not_pos_to_nec_not_deriv:
  assumes ‹⊢⇩B ❙¬F ❙⟶ G›
  shows ‹⊢⇩B ❙¬❙PF ❙⟶ ❙KG›
  by (metis KN K_imply_Cons K_right_mp Kax assms 
      imply.simps(1,2) not_pos_to_nec_not)

lemma pos_not_to_not_nec:
  shows ‹⊢⇩B ❙P❙¬F ❙⟶ ❙¬❙KF›
proof -
  have P1: ‹⊢⇩B ❙P❙¬F ❙⟷ ❙¬❙K❙¬❙¬F› using TAU by force
  have ‹⊢⇩B ❙K(F ❙⟶ ❙¬❙¬F)› using TAU KN by force
  hence P2: ‹⊢⇩B ❙KF ❙⟶ ❙K❙¬❙¬F› using Kax MP by auto
  have ‹⊢⇩B (❙P❙¬F ❙⟷ ❙¬❙K❙¬❙¬F) ❙⟶ (❙KF ❙⟶ ❙K❙¬❙¬F) ❙⟶ (❙P❙¬F ❙⟶ ❙¬❙KF)› 
    using TAU by force
  thus ?thesis using P1 P2 MP by auto
qed

lemma not_nec_to_pos_not:
  shows ‹⊢⇩B ❙¬❙KF ❙⟶ ❙P❙¬F›
proof -
  have P1: ‹⊢⇩B ❙P❙¬F ❙⟷ ❙¬❙K❙¬❙¬F› using TAU by force
  have ‹⊢⇩B ❙K(❙¬❙¬F ❙⟶ F)› using TAU KN by force
  hence P2: ‹⊢⇩B ❙K❙¬❙¬F ❙⟶ ❙KF› using Kax MP by auto
  have ‹⊢⇩B (❙P❙¬F ❙⟷ ❙¬❙K❙¬❙¬F) ❙⟶ (❙K❙¬❙¬F ❙⟶ ❙KF) ❙⟶ (❙¬❙KF ❙⟶ ❙P❙¬F)› 
    using TAU by force
  thus ?thesis using P1 P2 MP by auto
qed

lemma pos_not_to_not_nec_MCS:
  assumes ‹MCS A›
    and ‹❙P❙¬F ∈ A› 
  shows ‹❙¬❙KF ∈  A› using pos_not_to_not_nec 
    by (meson MCS_imp assms(1,2) deriv_in_maximal)

lemma pos_subset:
  assumes ‹MCS A› and ‹MCS B›
  shows ‹{ F | F . ❙K F ∈ A} ⊆ B ⟷ {❙PF | F . F ∈ B} ⊆ A› 
proof
  assume As: ‹{ F | F . ❙K F ∈ A} ⊆ B›
  show ‹{❙PF | F . F ∈ B} ⊆ A›
  proof
    fix F
    assume ‹F ∈ {❙P F |F. F ∈ B}›
    then obtain G where P: ‹F = ❙PG ∧ G∈B› by auto
    show ‹F ∈ A›
    proof (rule ccontr)
      assume ‹F ∉ A›
      hence ‹❙K❙¬G ∈ A› using assms(1) P ‹F ∉ A› 
        by (metis (no_types, opaque_lifting) MCS_impI)
      thus False using As P assms(2) MCS_bot by blast
    qed
  qed
next
  assume As: ‹{❙PF | F . F ∈ B} ⊆ A›
  show ‹{ F | F . ❙K F ∈ A} ⊆ B›
  proof
    fix F
    assume ‹F ∈ { F | F . ❙K F ∈ A}›
    hence ‹❙K F ∈ A› by simp
    show ‹F ∈ B›
    proof (rule ccontr)
      assume ‹F ∉ B›
      hence ‹❙¬❙KF ∈  A› 
        using As assms pos_not_to_not_nec_MCS by auto
      thus False
        using ‹❙K F ∈ A› MCS_bot assms(1) by blast
    qed
  qed
qed

end

text ‹Lemmas involving the negation of a chain of  ‹❙□› or  ‹❙◇›.›

lemma not_chain_d_to_chain_b_not:
  assumes ‹⊢⇩B ❙¬F ❙⟶ G›
  shows ‹⊢⇩B ❙¬ (❙◇^n F) ❙⟶ (❙□^n G)›
proof (induct n)
  case 0
  then show ?case using assms by auto
next
  case (Suc n)
  assume ‹⊢⇩B ❙¬ (❙◇^n F) ❙⟶ (❙□^n G)›
  hence H: ‹⊢⇩B ❙□❙¬(❙◇^n F) ❙⟶ ❙□(❙□^n G)› using KSq MP NSq by blast
  have H2: ‹⋀ A B C . ⊢⇩B (A ❙⟶ B) ❙⟶ (B ❙⟶ C) ❙⟶ (A ❙⟶ C)› using TAU by force
  have ‹⊢⇩B ❙¬(❙◇❙◇^n F) ❙⟶ ❙□❙¬(❙◇^n F)› 
    using KBox.not_pos_to_nec_not chain_d_def by auto 
  hence ‹⊢⇩B ❙¬(❙◇❙◇^n F) ❙⟶ ❙□(❙□^n G)› using H H2 MP by blast
  thus ?case using chain_b_def chain_d_def by simp
qed


lemma not_chain_b_to_chain_d_not:
  assumes ‹⊢⇩B ❙¬F ❙⟶ G›
  shows ‹⊢⇩B ❙¬ (❙□^n F) ❙⟶ (❙◇^n G)›
proof (induct n)
  case 0
  then show ?case using assms by auto
next
  case (Suc n)
  assume P1: ‹⊢⇩B ❙¬ (❙□^n F) ❙⟶ (❙◇^n G)›
  have T: ‹⋀ A B . ⊢⇩B (A ❙⟶ B)  ❙⟶ (❙¬ B ❙⟶ ❙¬ A)› using TAU by force
  hence ‹⊢⇩B ❙¬ (❙◇^n G) ❙⟶ ❙¬❙¬ (❙□^n F)› using P1 MP by auto
  hence ‹⊢⇩B ❙□❙¬(❙◇^n G) ❙⟶ ❙□❙¬❙¬(❙□^n F)› using KSq MP NSq by blast
  hence P2: ‹⊢⇩B ❙◇❙¬(❙□^n F) ❙⟶ ❙◇(❙◇^n G)› using T MP by auto
  have P3: ‹⊢⇩B ❙¬ (❙□^(n+1) F) ❙⟶ ❙◇❙¬(❙□^n F)›
    using KBox.not_nec_to_pos_not by auto
  have ‹⋀ A B C . ⊢⇩B (A ❙⟶ B) ❙⟶ (B ❙⟶ C) ❙⟶ (A ❙⟶ C)› using TAU by force
  hence ‹⊢⇩B (❙¬❙□^(n+1) F) ❙⟶ ❙◇(❙◇^n G)› using P2 P3 MP by blast
  thus ?case using chain_b_def P2 MP chain_d_def by simp
qed

lemma not_chain_b_to_chain_d_not_rev:
  assumes ‹⊢⇩B F ❙⟶ ❙¬G›
  shows ‹⊢⇩B (❙◇^n G) ❙⟶  ❙¬ (❙□^n F)›
proof (induct n)
  case 0
  have ‹⊢⇩B (F ❙⟶ ❙¬G) ❙⟶ (G ❙⟶ ❙¬F)› using TAU by force
  then show ?case using assms chain_b_def chain_d_def MP by auto
next
  case (Suc n)
  assume P1: ‹⊢⇩B (❙◇^n G) ❙⟶  ❙¬ (❙□^n F)›
  have T: ‹⋀ A B . ⊢⇩B (A ❙⟶ ❙¬B)  ❙⟶ (B ❙⟶ ❙¬ A)› using TAU by force
  hence ‹⊢⇩B (❙□^n F) ❙⟶ ❙¬(❙◇^n G)› using P1 MP by auto
  hence ‹⊢⇩B ❙□(❙□^n F) ❙⟶ ❙□❙¬(❙◇^n G)› using KSq MP NSq by blast
  hence P2: ‹⊢⇩B (❙□^(n+1) F) ❙⟶ ❙□❙¬(❙◇^n G)› using T MP chain_b_def by simp
  have ‹⋀ A B . ⊢⇩B (A ❙⟶ B)  ❙⟶ (❙¬B ❙⟶ ❙¬ A)› using TAU by force
  hence P3: ‹⊢⇩B ❙¬❙□❙¬(❙◇^n G) ❙⟶ ❙¬(❙□^(n+1) F)› using P2 MP by blast 
  thus ?case using chain_d_def by simp
qed

section ‹Elements for the Canonical model›

text ‹First, we introduce some relations that will by used to define the components of the 
  Canonical Model. The first one is the chain relation ‹Chn›:›

abbreviation Chn :: ‹('p fm set × 'p fm set) set› where
  ‹Chn ≡ {(Sa,Sb) . MCS Sa ∧ MCS Sb ∧ {f . ❙□f ∈ Sa} ⊆ Sb}›

text ‹Now, the eelation ‹Zmc› linking MCS that will produce the bisimilarity relation:›

abbreviation Zmc :: ‹('p fm set × 'p fm set) set› where
  ‹Zmc ≡ {(Sa,Sb) . MCS Sa ∧ MCS Sb ∧ {f. ❙[b❙]f ∈ Sa} ⊆ Sb}›

text ‹Truth of propositional variables in MCS:›

abbreviation Vmc :: ‹'p fm set ⇒ 'p ⇒ bool› where
  ‹Vmc ≡ (λ S P. ❙⋅P ∈ S)›

text ‹Sets ‹MC1› and ‹MC2› will constitute the worlds on the left and on the right model of the 
  canonical model for ‹ℒ⇩□⇩[⇩b⇩]›. All mc-sets are in ‹MC1›, while ‹MC2› contains only mc-sets containing
  ‹❙□^n❙[b❙]❙⊥› for all ‹n›.›

abbreviation MC1 :: ‹'p fm set set› where
  ‹MC1 ≡ {A . MCS A}›

abbreviation MC2 :: ‹'p fm set set› where
  ‹MC2 ≡ {A . MCS A ∧ (∀ n . ❙□^n ❙[b❙]❙⊥ ∈ A)}›


text ‹This lemma shows that ‹Zmc› goes from worlds not in ‹MC2› to worlds in ‹MC2›.›

lemma Z_from_MC1_to_MC2:
  assumes ‹(A,B) ∈ Zmc›
  shows ‹A ∉ MC2 ∧ B ∈ MC2›
proof - 
  have ‹❙⊤ ∈ B› using assms by auto
  hence ‹❙⟨b❙⟩❙⊤ ∈ A› using KFrB.pos_subset assms by force
  have ‹A ∉ MC2› 
  proof
    assume ‹A ∈ MC2›
    hence ‹❙[b❙]❙⊥ ∈ A› by (metis (no_types, lifting) mem_Collect_eq chain_b.simps(1))
    thus False using ‹❙⟨b❙⟩❙⊤ ∈ A› assms by fastforce 
  qed
  have ‹∀ n . ❙[b❙] ❙□^n ❙[b❙] ❙⊥ ∈ A› using assms NTSgen deriv_in_maximal by auto
  hence ‹∀ n .  ❙□^n ❙[b❙] ❙⊥ ∈ B› using assms by auto
  hence ‹B ∈ MC2› using assms by blast
  thus ?thesis using ‹A ∉ MC2› by simp
qed

text ‹The following lemma is important for the proof of existence. It proves that if
  ‹{f . ❙□f ∈ A} ⊆ B› and ‹A ∈ MC2›, then ‹B ∈ MC2›.›

lemma Chn_from_to_2:
  assumes ‹(A,B) ∈ Chn› and ‹A ∈ MC2› 
  shows ‹B ∈ MC2› 
proof -
  have Amc2: ‹∀ n . ❙□^n ❙[b❙]❙⊥ ∈ A› 
    using assms(2) by auto
  have ‹∀ m . ❙□^(m+1) ❙[b❙] ❙⊥ ∈ A ⟶ ❙□^m ❙[b❙] ❙⊥ ∈ B› using assms(1) by force
  hence ‹∀ n . ❙□^n ❙[b❙]❙⊥ ∈ B› using Amc2 by blast
  thus ?thesis using assms by blast
qed

text ‹Lemmas used to prove existence.›

lemma pos_r1_sub:
  assumes ‹A ∈ MC1› and ‹B ∈ MC1›
  shows ‹(A,B) ∈ Chn ⟷ {❙◇F | F . F ∈ B} ⊆ A› 
proof -
  have ‹MCS A› using assms(1) by simp
  have ‹MCS B› using assms(2) by simp
  have P: ‹(A,B) ∈ Chn ⟷ {f . ❙□f ∈ A} ⊆ B› using assms by simp
  have ‹({F |F. ❙□ F ∈ A} ⊆ B) ⟷ ({❙◇ F |F. F ∈ B} ⊆ A)› 
    using ‹MCS A› ‹MCS B› KBox.pos_subset by simp
  thus ?thesis using P by simp 
qed

lemma pos_r2_sub:
  assumes ‹A ∈ MC2› and ‹B ∈ MC2›
  shows ‹(A,B) ∈ Chn ⟷ {❙◇F | F . F ∈ B} ⊆ A› 
proof -
  have ‹MCS A› using assms(1) by simp
  have ‹MCS B› using assms(2) by simp
  have P: ‹(A,B) ∈ Chn ⟷ {f . ❙□f ∈ A} ⊆ B› using assms by simp
  have ‹({F |F. ❙□ F ∈ A} ⊆ B) ⟷ ({❙◇ F |F. F ∈ B} ⊆ A)› 
    using ‹MCS A› ‹MCS B› KBox.pos_subset by simp
  thus ?thesis using P by simp 
qed

lemma pos_b_r2_sub:
  assumes ‹A ∈ MC1› and ‹B ∈ MC2›
  shows ‹(A,B) ∈ Zmc ⟷ {❙⟨b❙⟩F | F . F ∈ B} ⊆ A› 
proof -
  have ‹MCS A› using assms(1) by simp
  have ‹MCS B› using assms(2) by simp
  have P: ‹(A,B) ∈ Zmc ⟷ {f . ❙[b❙]f ∈ A} ⊆ B› using assms by simp
  have ‹({F |F. ❙[b❙]F ∈ A} ⊆ B) ⟷ ({ ❙⟨b❙⟩ F |F. F ∈ B} ⊆ A)› 
    using ‹MCS A› ‹MCS B› KFrB.pos_subset by simp
  thus ?thesis using P by simp 
qed

text ‹All mc-sets in ‹MC2› contain ‹❙[b❙]F› for every ‹F›.›

lemma all_box_b_in_MC2:
  assumes ‹S ∈ MC2›
  shows ‹❙[b❙]F ∈ S›
proof -
  have ‹⊢⇩B ❙⊥ ❙⟶ F› using TAU by force
  have ‹❙[b❙]❙⊥ ∈ S› using assms chain_b.simps(1)
    by (metis (no_types, lifting) mem_Collect_eq)
  thus ?thesis using ‹⊢⇩B ❙⊥ ❙⟶ F› 
    by (smt (verit, best) KFrB.KN KFrB.Kax MCS_imp assms deriv_in_maximal
        mem_Collect_eq)
qed

section ‹Existence›

text ‹First, we prove a general result for all normal modal operators.›

context Kop begin

lemma Kop_existence:
  assumes ‹MCS A›
  and ‹❙PF ∈ A›
shows ‹consistent ({F} ∪ {G . ❙KG ∈ A})›
proof (rule ccontr)
  assume ‹¬ consistent ({F} ∪ {G . ❙KG ∈ A})›
  then obtain S where S: ‹set S ⊆ {G . ❙KG ∈ A} ∧ F#S ⊢⇩B ❙⊥› 
    by (metis (no_types, lifting) K_imply_Cons consistent_def 
        derive_split1 insert_is_Un subset_insert)  
  hence ‹S ⊢⇩B ❙¬ F› 
    using K_ImpI by blast
  hence ‹⊢⇩B S ❙↝ ❙¬F› by simp
  hence D: ‹⊢⇩B map (λ f . ❙Kf) S ❙↝ ❙K❙¬F› 
    using KN K_distrib_K_imp by blast
  have ‹set(map (λ f . ❙Kf) S) ⊆ A› using S by auto
  hence ‹❙K❙¬F ∈ A› using D 
    by (meson MCS_derive assms(1))
  hence ‹❙¬❙K❙¬F ∉ A› 
    using MCS_bot assms(1) by blast
  thus False using assms(2) by auto
qed

end


lemma Chn_iff:
  assumes ‹MCS A›
  shows ‹❙□F ∈ A ⟷ (∀ B . (A,B) ∈ Chn ⟶ F∈B)› 
proof 
  assume ‹❙□F ∈ A›
  thus ‹∀ B . (A,B) ∈ Chn ⟶ F ∈ B› by auto
next
  assume A: ‹∀ B . (A,B) ∈ Chn ⟶ F∈B›
  show ‹❙□F ∈ A›
  proof (rule ccontr)
    assume ‹❙□F ∉ A›
    hence ‹❙◇ ❙¬F ∈ A› 
      by (meson KBox.not_nec_to_pos_not MCS_imp assms deriv_in_maximal)
    hence ‹consistent ({❙¬F} ∪ {G . ❙□ G ∈ A})› 
      using ‹MCS A› KBox.Kop_existence by auto  
    hence ‹∃ S . (MCS S ∧ ({❙¬F} ∪ {G . ❙□ G ∈ A}) ⊆ S)› 
      using Extend_subset MCS_Extend' by metis
    then obtain S where S: ‹(A,S) ∈ Chn ∧ ❙¬F ∈ S ∧ F ∈ S› using A assms by auto
    thus False using MCS_bot by blast
  qed
qed

text ‹Existence for ‹❙◇› in ‹MC1›.›

lemma existenceChn_1:
  assumes ‹❙◇F ∈ A› and ‹A ∈ MC1› 
  shows ‹∃ B . B ∈ MC1 ∧ {F} ∪ {G . ❙□G ∈ A}⊆B›  
proof -
  have ‹consistent ({F} ∪ {G . ❙□G ∈ A})› using assms KBox.Kop_existence by auto
  then obtain S where S: ‹MCS S ∧ ({F} ∪ {G . ❙□G ∈ A}) ⊆ S› 
    by (metis Extend_subset MCS_Extend')
  hence ‹(A,S) ∈ Chn› using assms by simp
  thus ?thesis using S by auto
qed

text ‹Existence for ‹❙◇› in ‹MC2›.›

lemma existenceChn_2:
  assumes ‹❙◇F ∈ A› and ‹A ∈ MC2› 
  shows ‹∃ B . B ∈ MC2 ∧ {F} ∪ {G . ❙□G ∈ A}⊆B›  
proof -
  have ‹consistent ({F} ∪ {G . ❙□G ∈ A})› using assms KBox.Kop_existence by auto
  then obtain S where S: ‹MCS S ∧ ({F} ∪ {G . ❙□G ∈ A}) ⊆ S› 
    by (metis Extend_subset MCS_Extend')
  hence ‹(A,S) ∈ Chn› using assms by simp
  thus ?thesis 
    by (metis (mono_tags, lifting) Chn_from_to_2 S assms(2))
qed

text ‹Existence for ‹❙⟨b❙⟩› in ‹MC1›.›

lemma existenceZmc:
  assumes ‹❙⟨b❙⟩F ∈ A› and ‹A ∈ MC1› 
  shows ‹∃ B . B ∈ MC2 ∧ {F} ∪ {G . ❙[b❙]G ∈ A}⊆B›  
proof -
  have ‹consistent ({F} ∪ {G . ❙[b❙]G ∈ A})› using assms KFrB.Kop_existence by auto
  then obtain S where S: ‹MCS S ∧ ({F} ∪ {G . ❙[b❙]G ∈ A}) ⊆ S› 
    by (metis Extend_subset MCS_Extend')
  hence ‹(A,S) ∈ Zmc› using assms by simp
  thus ?thesis 
    by (metis (mono_tags, lifting) S Z_from_MC1_to_MC2)
qed

section ‹Atomic harmony of ‹Zmc›.›

text ‹MCS linked by ‹Zmc› contain the same propositional variables.›

lemma Zmc_atomic_harmony:
  assumes ‹(A,B) ∈ Zmc›
  shows ‹❙⋅l ∈ A ⟷ ❙⋅l ∈ B› 
proof
  assume ‹❙⋅l ∈ A›
  hence ‹❙[b❙]❙⋅l ∈ A› 
    by (metis (mono_tags, lifting) HARM assms deriv_in_maximal Derivations_Imp.MCS_impE 
        Derivations_Imp_axioms mem_Collect_eq old.prod.case)
  thus ‹❙⋅l ∈ B› using assms by auto
next
  assume ‹❙⋅l ∈ B›
  thus ‹❙⋅l ∈ A› 
    by (smt (verit, del_insts) HARM MCS_bot MCS_imp assms deriv_in_maximal
        mem_Collect_eq prod.simps(2) subsetD)
qed

section ‹Forth and Back›

text ‹First, an auxiliary lemma used in the proofs of forth and back properties of the Canonical
  Model.›

lemma nec_As_to_nec_conj:
  assumes ‹S ∈ MC1›
  and ‹{❙[b❙]f | f. f ∈ set A} ⊆ S›
  shows ‹❙[b❙]❙¬(A ❙↝ ❙⊥) ∈ S› 
proof (rule ccontr)
  assume ‹❙[b❙] ❙¬(A ❙↝ ❙⊥) ∉ S›
  hence ‹❙¬❙[b❙] ❙¬ (A ❙↝ ❙⊥) ∈ S› using assms(1) by blast
  hence ‹❙⟨b❙⟩ (A ❙↝ ❙⊥) ∈ S› by simp
  then obtain S2 where S2: ‹(MCS S2) ∧ ({A ❙↝ ❙⊥} ∪ {G . ❙[b❙]G ∈ S}) ⊆ S2› using assms(1)
    existenceZmc by (metis (mono_tags, lifting) mem_Collect_eq)
  hence ‹({A ❙↝ ❙⊥} ∪ set A) ⊆ S2› using assms(2) mem_Collect_eq by auto
  hence ‹❙⊥ ∈ S2› using multiple_MP_MCS S2 by (metis insert_is_Un insert_subset)
  thus False using multiple_MP_MCS S2 insert_is_Un insert_subset by simp
qed

text ‹Lemmas that will be used to prove that the Canonical Model satisfies forth and back
  properties.›

lemma forth_cm:
  assumes ‹(G1, G2) ∈ Zmc›
  and ‹(G1, G3) ∈ Chn›
shows ‹∃ G4 . (G3, G4) ∈ Zmc ∧ (G2, G4) ∈ Chn›
proof -
  have GS: ‹G1 ∈ MC1 ∧ G2 ∈ MC2 ∧ G3 ∈ MC1› 
    using assms Z_from_MC1_to_MC2 by auto
  have ‹consistent ({A . ❙[b❙]A ∈ G3} ∪ {B | B. ❙□B ∈ G2})› (is ‹consistent (?L ∪ ?R)›)
  proof (rule ccontr)
    assume ‹¬ consistent (?L ∪ ?R)›
    then obtain AsBs where AB1: ‹set AsBs ⊆ ?L ∪ ?R ∧ (AsBs ⊢⇩B ❙⊥)› 
      using consistent_def by blast
    then obtain As Bs where AB: ‹set As = (set AsBs ∩ ?L) ∧ 
      set Bs = (set AsBs ∩ ?R)› 
      by (metis (lifting) inf_commute inter_set_filter) 
    hence ‹set As ∪ set Bs = set AsBs› using AB1 by auto
    hence ‹(Bs@As ⊢⇩B ❙⊥)› using AB 
      by (metis AB1 K_imply_weaken dual_order.refl set_append sup.commute)
    hence ‹⊢⇩B Bs ❙↝ As ❙↝ ❙⊥› by simp
    hence D: ‹⊢⇩B (map (λ f. ❙□ f) Bs) ❙↝ ❙□(As ❙↝ ❙⊥)› 
      using KBox.KN KBox.K_distrib_K_imp by blast
    have ‹finite (set As)› using ‹(Bs@As ⊢⇩B ❙⊥)› by simp
    have ‹set (map (λ f. ❙□ f) Bs) ⊆ G2› using AB by auto
    hence ‹❙□(As ❙↝ ❙⊥) ∈ G2› using D 
      by (metis (no_types, lifting) MCS_derive assms(1) case_prod_conv
          mem_Collect_eq)
    hence f1: ‹❙⟨b❙⟩❙□(As ❙↝ ❙⊥) ∈ G1› (is ‹❙⟨b❙⟩❙□?F1 ∈ G1›) 
      by (metis (mono_tags, lifting) MCS_bot MCS_impE MCS_impI assms(1) 
          mem_Collect_eq prod.simps(2) subsetD)
    obtain NecAs where NecAs: ‹NecAs = (map (λ f. ❙[b❙]f) As)› by simp
    hence sAs: ‹set NecAs ⊆ G3 ∧ finite (set NecAs)› 
      using AB assms by auto
    hence ‹{❙[b❙] f |f. f ∈ set As} ⊆ G3› using AB by blast
    hence ‹❙[b❙]❙¬(As ❙↝ ❙⊥) ∈ G3› using GS nec_As_to_nec_conj[of "G3" "As"] by simp
    hence ‹❙◇❙[b❙]❙¬ (As ❙↝ ❙⊥) ∈ G1› (is ‹❙◇❙[b❙]?F2 ∈ G1›) using assms KBox.pos_subset by force
    hence ‹❙⟨b❙⟩❙□?F1 ❙∧ ❙◇❙[b❙]?F2 ∈ G1› 
      using f1 Derivations_Imp.MCS_imp Derivations_Imp_axioms assms(1) by fastforce 
    hence ‹❙⟨b❙⟩(❙□?F1 ❙∧ ❙◇?F2) ∈ G1› (is ‹❙⟨b❙⟩?F12 ∈ G1›) using FORTH MP 
      Derivations_Imp.MCS_imp Derivations_Imp_axioms GS deriv_in_maximal by fastforce
    then obtain A where A: ‹(G1,A)∈Zmc ∧ A ∈ MC2 ∧ (❙□?F1 ❙∧ ❙◇?F2 ∈ A)› 
      using assms(1) existenceZmc[of "?F12" "G1"] Z_from_MC1_to_MC2[of "G1"] 
      by auto
    hence ‹{❙□?F1, ❙◇?F2} ⊆ A› 
      by (metis (mono_tags, lifting) MCS_bot MCS_imp empty_subsetI insert_subset
          mem_Collect_eq) 
    then obtain B where B: ‹B ∈ MC2 ∧ {?F1, ?F2} ⊆ B› 
      using A existenceChn_2[of "?F2"] 
      by (metis (mono_tags, lifting) KBox.pos_not_to_not_nec_MCS MCS_bot MCS_imp mem_Collect_eq)
    hence ‹❙⊥ ∈ B› by blast
    thus False using B by auto
  qed
  then obtain G4 where G4: ‹(?L ∪ ?R) ⊆ G4 ∧ MCS G4› 
    using Extend_subset MCS_Extend' by fastforce
  hence ‹{B | B. ❙□B ∈ G2} ⊆ G4› by simp
  hence T1: ‹(G2, G4) ∈ Chn› using G4 GS by simp
  hence ‹(G3, G4) ∈ Zmc› using G4 GS Chn_from_to_2 by auto 
  thus ?thesis using T1 by auto
qed


lemma back_cm:
  assumes ‹(G1, G2) ∈ Zmc›
  and ‹(G2, G3) ∈ Chn›
shows ‹∃ G4 . (G1, G4) ∈ Chn ∧ (G4, G3) ∈ Zmc› 
proof -
  have GS: ‹G1 ∈ MC1 ∧ G2 ∈ MC2 ∧ G3 ∈ MC2› 
    using assms Chn_from_to_2 Z_from_MC1_to_MC2 
    by (metis (mono_tags, lifting) case_prodD mem_Collect_eq)
  have ‹consistent ({❙⟨b❙⟩A | A. A ∈ G3} ∪ {B | B. ❙□B ∈ G1})› (is ‹consistent (?L ∪ ?R)›)
  proof (rule ccontr)
    assume ‹¬ consistent (?L ∪ ?R)›
    then obtain PosAsBs where AB1: ‹set PosAsBs ⊆ ?L ∪ ?R ∧ (PosAsBs ⊢⇩B ❙⊥)› 
      using consistent_def by blast
    then obtain PosAs Bs where AB: ‹set PosAs = (set PosAsBs ∩ ?L) ∧ 
      set Bs = (set PosAsBs ∩ ?R)› 
      by (metis (lifting) inf_commute inter_set_filter) 
    hence ‹set PosAs ∪ set Bs = set PosAsBs› using AB1 by auto
    hence ‹(Bs@PosAs ⊢⇩B ❙⊥)› using AB 
      by (metis AB1 K_imply_weaken dual_order.refl set_append sup.commute)
    hence ‹⊢⇩B Bs ❙↝ PosAs ❙↝ ❙⊥› by simp
    hence D: ‹⊢⇩B (map (λ f. ❙□ f) Bs) ❙↝ ❙□(PosAs ❙↝ ❙⊥)› 
      using KBox.KN KBox.K_distrib_K_imp by blast
    have ‹finite (set PosAs)› using ‹(Bs@PosAs ⊢⇩B ❙⊥)› by simp
    have ‹set (map (λ f. ❙□ f) Bs) ⊆ G1› using AB by auto
    hence X1: ‹❙□(PosAs ❙↝ ❙⊥) ∈ G1› using D 
      by (metis (no_types, lifting) MCS_derive assms(1) case_prod_conv
          mem_Collect_eq)
    obtain As where As: ‹As = (map (λ f. THE p . f = ❙⟨b❙⟩p) PosAs)› by simp
    hence sAs: ‹set As ⊆ G3 ∧ finite (set As)› 
      using AB assms by auto
    have ‹∀ f . f ∈ set PosAs ⟶ (∃ g . f = ❙⟨b❙⟩g)› using AB by auto
    hence X: ‹set PosAs = {❙⟨b❙⟩g | g. g ∈ set As}› using As by force
    have ‹As ❙↝ ❙⊥ ∉ G3› using multiple_MP_MCS MCS_bot assms(2) sAs by auto
    hence ‹❙¬ (As ❙↝ ❙⊥) ∈ G3› (is ‹?F2 ∈ G3›) using assms(2) by blast
    hence ‹❙◇?F2 ∈ G2›  
      by (smt (verit, ccfv_threshold) assms KBox.pos_subset GS 
          mem_Collect_eq pos_r2_sub subsetD)
    hence ‹❙⟨b❙⟩❙◇?F2 ∈ G1› using assms KFrB.pos_subset by fastforce
    hence X2: ‹❙◇❙⟨b❙⟩ ?F2 ∈ G1› by (metis (mono_tags, lifting) BACK[of "?F2"] 
      deriv_in_maximal GS MCS_impE mem_Collect_eq)
    then obtain B where B: ‹(G1,B)∈Chn ∧ B ∈ MC1 ∧ {❙⟨b❙⟩?F2} ∪ {f . ❙□ f ∈ G1}⊆ B› 
      using assms GS existenceChn_1[of "❙⟨b❙⟩?F2" "G1"] by auto
    hence X3: ‹{❙⟨b❙⟩❙¬ (As ❙↝ ❙⊥), PosAs ❙↝ ❙⊥} ⊆ B› using X1 by auto
    then obtain C where C: ‹MCS C ∧ ({❙¬ (As ❙↝ ❙⊥)} ∪ {f .❙[b❙]f ∈ B}) ⊆ C› 
      using existenceZmc[of "❙¬ (As ❙↝ ❙⊥)" "B"] B by auto 
    hence ‹(B,C) ∈ Zmc› using B C by simp
    hence BC: ‹({❙⟨b❙⟩f | f. f ∈ C}) ⊆ B› 
      using pos_b_r2_sub[of "B" "C"] Z_from_MC1_to_MC2[of "B" "C"] by simp
    have ‹set As ⊆ C› using C not_imp_to_conj by auto
    hence ‹{❙⟨b❙⟩f | f. f ∈ set As} ⊆ B› using BC by auto
    hence ‹set PosAs ⊆ B› using X by simp
    hence ‹❙⊥ ∈ B› using B X3
      by (simp add: multiple_MP_MCS)
    thus False using B by simp
  qed
  then obtain G4 where G4: ‹(?L ∪ ?R) ⊆ G4 ∧ MCS G4› 
    using Extend_subset MCS_Extend' by fastforce
  hence ‹{B | B. ❙□B ∈ G1} ⊆ G4› by simp
  hence T1: ‹(G1, G4) ∈ Chn› using G4 GS by simp
  hence ‹G4 ∈ MC1› using G4 by auto  
  hence ‹(G4, G3) ∈ Zmc› using G4 pos_b_r2_sub GS by auto 
  thus ?thesis using T1 by auto
qed

section ‹Existence of elements in ‹Zmc›.›

lemma Zmc_not_empty:
  ‹Zmc ≠ {}› 
proof -
  let ?V = ‹λ w p . False›
  let ?M1 = ‹Model {0::nat} {} ?V›
  let ?M2 = ‹Model {0} {} ?V›
  let ?M  =  ‹ModelLb ?M1 ?M2 {(0,0)}›
  have ‹bi_model ?M› using bi_model_def by force 
  have ‹¬ (?M, 𝗆, 0) ⊨⇩B ❙⟨b❙⟩❙⊤ ❙⟶ ❙⊥› by auto
  hence ‹¬ [❙⟨b❙⟩❙⊤] ⊢⇩B ❙⊥› using soundness ‹bi_model ?M› by fastforce
  hence ‹consistent {❙⟨b❙⟩❙⊤}›
    by (metis K_imply_weaken consistent_def empty_set list.simps(15))
  hence ‹∃ A . ❙⟨b❙⟩❙⊤ ∈ A ∧ MCS A›
    using MCS_Extend' Extend_subset insert_subset by metis
  hence ‹∃ A . ❙⟨b❙⟩❙⊤ ∈ A ∧ A ∈ MC1› by auto
  hence ‹∃ A B . ❙⟨b❙⟩❙⊤ ∈ A ∧ A ∈ MC1 ∧ MCS B ∧ {F . ❙[b❙]F ∈ A} ⊆ B› 
    using existenceZmc by force
  hence ‹∃ A B . (A, B) ∈ Zmc› by auto
  thus ?thesis by auto
qed

section ‹Canonical Model›

text ‹The Canonical Model is defined in terms of ‹MC1›, ‹MC2›, ‹Chn› and ‹Zmc›.›

text ‹‹R1› and ‹R2› are the modal acessibility relations of the models on the left and right of the
  Canonical Model for ‹ℒ⇩□⇩[⇩b⇩]›. They are defined as restrictions of ‹Chn› for  ‹MC1› and  ‹MC2›, 
  respectively. The valuation function ‹Vc› is common for two models, it assigns True to a variable
  iff it belongs to the corresponding world. The bisimulation relation ‹Zc› is defined from ‹Zmc›.›

abbreviation R1 :: ‹('p fm set × 'p fm set) set› where
  ‹R1 ≡ {(w1, w2) . w1 ∈ MC1 ∧ w2 ∈ MC1 ∧ (w1, w2) ∈ Chn}›

abbreviation R2 :: ‹('p fm set × 'p fm set) set› where
  ‹R2 ≡ {(w1, w2) . w1 ∈ MC2 ∧ w2 ∈ MC2 ∧ (w1, w2) ∈ Chn}›

abbreviation Vc :: ‹'p fm set ⇒ 'p ⇒ bool› where
  ‹Vc w p ≡ ❙⋅p ∈ w›

abbreviation Zc :: ‹('p fm set × 'p fm set) set› where
  ‹Zc ≡ {(w1, w2) . w1 ∈ MC1 ∧ w2 ∈ MC2 ∧ (w1, w2) ∈ Zmc}›

text ‹Now, models ‹Mc1› and ‹Mc2› are introduced. These are the models on the left and right, of
  the Canonical Model.›

abbreviation Mc1 :: ‹('p, 'p fm set) model› where
  ‹Mc1 ≡ Model MC1 R1 Vc›

abbreviation Mc2 :: ‹('p, 'p fm set) model› where
  ‹Mc2 ≡ Model MC2 R2 Vc›

text ‹Finally, the Canonical Model is introduced.›

abbreviation CanMod :: ‹('p, 'p fm set) modelLb› where
  ‹CanMod ≡ ModelLb Mc1 Mc2 Zc›


lemma Chn_Rc2:
  ‹((S,T) ∈ Chn ∧ S ∈ MC2 ∧ T ∈ MC2) ⟷ (S,T) ∈ R2› (is ‹?L ⟷ ?R›)
proof
  assume ‹?L›
  hence ‹T ∈ MC2› 
    by (metis (mono_tags, lifting)) 
  hence ‹S ∈ MC2 ∧ T ∈ MC2› using ‹?L› by simp
  thus ‹?R› using ‹?L› by simp
next
  assume ‹?R›
  thus ‹?L› by simp
qed

section ‹Canonocity›

text ‹The Canonical Model is a bi-model.›

lemma bi_model_CM:
  ‹bi_model CanMod› 
proof -
  ― ‹Properties of Z and W sets›
  have ‹Zmc ≠ {}› using Zmc_not_empty by simp
  hence ‹∃ A B . A ∈ MC1 ∧ B ∈ MC2 ∧ (A, B) ∈ Zmc›  
    by (metis (mono_tags, lifting) Z_from_MC1_to_MC2 Collect_empty_eq 
     case_prodE mem_Collect_eq)
  hence ‹MC1 ≠ {} ∧ MC2 ≠ {} ∧ Zc ≠ {}› 
    by (smt (verit, ccfv_SIG) case_prodE not_empty mem_Collect_eq 
        prod.inject split_cong) 
  hence WZ: ‹W (M1 CanMod) ≠ {} ∧ W (M2 CanMod) ≠ {} ∧ Z CanMod ≠ {} ∧ 
      Z CanMod ⊆ (W (M1 CanMod)) × (W (M2 CanMod))› by auto
  ― ‹Properties of R1 and R2›
  have R1: ‹R (M1 CanMod) ⊆ (W (M1 CanMod)) × (W (M1 CanMod))› by auto
  have R2: ‹R (M2 CanMod) ⊆ (W (M2 CanMod)) × (W (M2 CanMod))› by auto
  ― ‹Atomic Harmony›
  have ‹∀ w w' l . (w, w') ∈ Z CanMod ⟶ 
    (❙⋅l ∈ w ⟷ ❙⋅l ∈ w')› by (metis (mono_tags, lifting) 
    Zmc_atomic_harmony mem_Collect_eq modelLb.sel(3) old.prod.case)
  hence AtHarm: ‹∀ w w' . (w, w') ∈ Z CanMod ⟶ 
    ((V (M1 CanMod)) w) = ((V (M2 CanMod)) w')› by auto
  ― ‹Forth›
  have Forth: ‹∀ w w' v . (w, w') ∈ Z CanMod ∧ (w,v) ∈ R (M1 CanMod) ⟶ 
        (∃ v' . (v,v') ∈ Z CanMod ∧ (w', v') ∈ R (M2 CanMod))› 
    by (smt (z3) forth_cm Chn_from_to_2 mem_Collect_eq model.sel(2) modelLb.sel(1,2,3)
        old.prod.case)
  ― ‹Back›
  have Back: ‹∀ w w' v' . (w, w') ∈ Z CanMod ∧ (w',v') ∈ R (M2 CanMod) ⟶ 
      (∃ v . (v,v') ∈ Z CanMod ∧ (w,v) ∈ R (M1 CanMod))›
    by (smt (z3) back_cm Chn_from_to_2 mem_Collect_eq model.sel(2) modelLb.sel(1,2,3)
        old.prod.case)
  show ?thesis unfolding bi_model_def using WZ R1 R2 AtHarm Forth Back
    by blast
qed

section ‹Truth Lemma›

text ‹This is the key lemma for Completeness: a formula ‹F› is true in a given world ‹w› of the 
  Canonical Model iff ‹F ∈ w›.›

lemma Truth_Lemma:
  ‹∀ (S::'p fm set) . (MCS S ⟶ ((S ∈ MC1 ⟶ ((CanMod, 𝗆, S)⊨⇩B F ⟷ F ∈ S)) ∧
      (S ∈ MC2 ⟶ ((CanMod, 𝗆', S)⊨⇩B F ⟷ F ∈ S))))› (is ‹?TL F›)
proof (induct F)
  case Fls
  thus ?case by simp
next
  case (Pro x)
  thus ?case by simp
next
  case (Imp F1 F2)
  assume KSq: ‹?TL F1›
  assume Kb: ‹?TL F2›
  have ‹∀ S . MCS S ⟶ (F1 ❙⟶ F2 ∈ S ⟷ (F1 ∈ S ⟶ F2 ∈ S))› by auto
  thus ?case using KSq Kb by simp 
next
  case (Box F)
  assume A: ‹?TL F›
  have B: ‹∀ S . MCS S ∧ S ∈ MC1 ⟶ 
      ((CanMod, 𝗆, S) ⊨⇩B ❙□F ⟷ 
          (∀ T . (S,T) ∈ R1 ⟶ (CanMod, 𝗆, T) ⊨⇩B F))› 
    by (smt (z3) mem_Collect_eq model.sel(1,2) modelLb.sel(1) old.prod.case
        semantics.simps(5))
  have B': ‹∀ S . MCS S ∧ S ∈ MC2 ⟶ 
      ((CanMod, 𝗆', S) ⊨⇩B ❙□F ⟷ 
          (∀ T . (S,T) ∈ R2 ⟶ (CanMod, 𝗆', T) ⊨⇩B F))› 
    by (smt (z3) mem_Collect_eq model.sel(1,2) modelLb.sel(2) old.prod.case
        semantics.simps(6))
  have C: ‹∀ S . MCS S ∧ S ∈ MC1 ⟶ 
      (❙□F ∈ S ⟷ (∀ T . ((S,T) ∈ R1) ⟶ F ∈ T))› 
    by (metis (mono_tags, lifting) Chn_iff mem_Collect_eq old.prod.case) 
  have C': ‹∀ S . MCS S ∧ S ∈ MC2 ⟶ 
      (❙□F ∈ S ⟷ (∀ T . ((S,T) ∈ R2) ⟶ F ∈ T))› 
    by (metis (mono_tags, lifting) Chn_Rc2 Chn_iff Chn_from_to_2 ) 
  thus ?case using A B B' C by simp
next
  case (FrB F)
  assume A: ‹?TL F›
  have D1: ‹∀ S . MCS S ∧ S ∈ MC1 ⟶ (❙[b❙]F ∈ S ⟷ 
          (∀ T . ((S,T) ∈ Zc) ⟶ F ∈ T))› 
  proof (intro allI HOL.impI)
    fix S
    assume S: ‹MCS (S::'p fm set) ∧ S ∈ MC1›
    show ‹❙[b❙]F ∈ S ⟷ (∀ T . ((S,T) ∈ Zc) ⟶ F ∈ T)›
    proof 
      assume ‹❙[b❙]F ∈ S›
      thus ‹∀ T . ((S,T) ∈ Zc) ⟶ F ∈ T› by fastforce
    next
      assume T: ‹∀ T . ((S,T) ∈ Zc) ⟶ F ∈ T› 
      show ‹❙[b❙]F ∈ S› 
      proof (rule ccontr)
        assume ‹❙[b❙]F ∉ S›
        hence ‹❙⟨b❙⟩❙¬F ∈ S› 
          by (meson KFrB.not_nec_to_pos_not MCS_imp S deriv_in_maximal)
        hence ‹∃ B . B ∈ MC2 ∧ {❙¬F} ∪ {G . ❙[b❙]G ∈ S}⊆B›
          using S existenceZmc[of "❙¬F" "S"] by fastforce
        then obtain B where ‹(S,B) ∈ Zmc ∧ B ∈ MC2 ∧ ❙¬F ∈ B› 
          using S by auto
        hence B': ‹(S,B) ∈ Zc ∧ F ∉ B› using S MCS_imp by auto
        hence ‹F ∈ B› using T by auto
        thus False using B' by simp
      qed
    qed
  qed
  have ‹∀ S . MCS S ∧ S ∈ MC2 ⟶ ❙[b❙]F ∈ S ∧ (CanMod, 𝗆', S) ⊨⇩B ❙[b❙]F› 
    using all_box_b_in_MC2 by auto
  thus ?case using A D1 by auto
qed

corollary truth_lemma_MC1:
  assumes ‹S ∈ MC1›
  shows ‹∀ F . F ∈ S ⟷ (CanMod, 𝗆, S) ⊨⇩B F› 
  using assms Truth_Lemma by auto

corollary truth_lemma_MC2:
  assumes ‹S ∈ MC2›
  shows ‹∀ F . F ∈ S ⟷ (CanMod, 𝗆', S) ⊨⇩B F› 
  using assms Truth_Lemma by auto 


section ‹Completeness›

text ‹Proof of strong completeness.›

theorem strong_completeness:
  assumes ‹∀ (M :: ('p, 'p fm set) modelLb) ep w . 
      (bi_model M ⟶ (
          (w ∈ W (M1 M) ⟶ ((∀ γ ∈ set Γ . (M, 𝗆, w) ⊨⇩B γ) ⟶ (M, 𝗆, w) ⊨⇩B G)) ∧
          (w ∈ W (M2 M) ⟶ ((∀ γ ∈ set Γ . (M, 𝗆', w) ⊨⇩B γ) ⟶ (M, 𝗆', w) ⊨⇩B G))))›
  shows ‹Γ ⊢⇩B G› 
proof (rule ccontr)
  assume ‹¬ (Γ ⊢⇩B G)›
  hence ‹¬ (❙¬G#Γ ⊢⇩B ❙⊥)› using K_Boole by blast
  hence ‹consistent (set (❙¬G#Γ))› 
    using K_imply_weaken consistent_underivable by blast
  then obtain S where S: ‹MCS S ∧ set (❙¬G#Γ) ⊆ S› 
    using Extend_subset MCS_Extend' by blast
  have ‹S ∈ MC1› using S by auto
  hence N: ‹(∀ F ∈ set Γ . (CanMod, 𝗆, S) ⊨⇩B F) ∧ ((CanMod, 𝗆, S) ⊨⇩B ❙¬G)› 
    using S ‹S ∈ MC1› Truth_Lemma 
    by (smt (z3) insert_subset list.simps(15) subsetD)
  hence ‹(CanMod, 𝗆, S) ⊨⇩B G› using bi_model_CM ‹S ∈ MC1› assms by auto
  thus False using N semantics.simps by auto
qed

text ‹Definition of validity in bi-models:›

abbreviation bi_model_valid :: ‹'p fm ⇒ bool› where
  ‹bi_model_valid p ≡ ∀ (M :: ('p, 'p fm set) modelLb) w. bi_model M ⟶ 
      ((w ∈ W (M1 M) ⟶ (M, 𝗆, w)  ⊨⇩B p) ∧
       (w ∈ W (M2 M) ⟶ (M, 𝗆', w) ⊨⇩B p))›

text ‹Weak completeness and main result:›

corollary completeness: ‹bi_model_valid p ⟹ ⊢⇩B p› 
  by (metis imply.simps(1) strong_completeness) 

theorem main: ‹(bi_model_valid p) ⟷ ⊢⇩B p›
  using soundness completeness by metis


section ‹Extension of atomic harmony to all formulas in ‹ℒ⇩□››

text ‹Set of formulas in ‹ℒ⇩□›.›

inductive_set Lbox :: ‹'p fm set› where
  Fls: ‹❙⊥ ∈ Lbox›
| Pro: ‹❙⋅l ∈ Lbox› 
| Imp: ‹A ∈ Lbox ⟹ B ∈ Lbox ⟹ A❙⟶B ∈ Lbox›
| Box:   ‹A ∈ Lbox ⟹ ❙□A ∈ Lbox›

text ‹Auxiliary lemmas for the induction.›

lemma BotPos:
  shows ‹⊢⇩B ❙⊥ ❙⟶ ❙[b❙]❙⊥› using TAU by force

lemma BotNeg:
  shows ‹⊢⇩B ❙¬❙⊥ ❙⟶ ❙[b❙]❙¬❙⊥›
  by (metis K_imply_Cons K_imply_head Nb imply.simps(1,2))

lemma impPos:
  assumes ‹⊢⇩B ❙¬A ❙⟶ ❙[b❙]❙¬A›
    and ‹⊢⇩B B ❙⟶ ❙[b❙]B›
  shows ‹⊢⇩B (A ❙⟶ B) ❙⟶ ❙[b❙](A ❙⟶ B)›
proof -
  have ‹⊢⇩B ❙¬A ❙⟶ (A ❙⟶ B)› using TAU by force
  hence ‹⊢⇩B ❙[b❙]❙¬A ❙⟶ ❙[b❙](A ❙⟶ B)› using Nb Kb MP by force
  hence 1: ‹⊢⇩B ❙¬A ❙⟶ ❙[b❙](A ❙⟶ B)› using assms(1) MP_chain by auto
  have ‹⊢⇩B B ❙⟶ (A ❙⟶ B)› using TAU by force
  hence ‹⊢⇩B ❙[b❙]B ❙⟶ ❙[b❙](A ❙⟶ B)› using Nb Kb MP by force
  hence 2: ‹⊢⇩B B ❙⟶ ❙[b❙](A ❙⟶ B)› using assms(2) MP_chain by auto
  have ‹⊢⇩B (A ❙⟶ B) ❙⟶ (❙¬A ❙⟶ ❙[b❙](A ❙⟶ B)) ❙⟶ 
      (B ❙⟶ ❙[b❙](A ❙⟶ B)) ❙⟶ ❙[b❙](A ❙⟶ B)› using TAU by force
  thus ?thesis using 1 2 MPcons by blast  
qed  

lemma impNeg:
  assumes ‹⊢⇩B A ❙⟶ ❙[b❙]A›
    and ‹⊢⇩B ❙¬B ❙⟶ ❙[b❙]❙¬B›
  shows ‹⊢⇩B ❙¬(A ❙⟶ B) ❙⟶ ❙[b❙]❙¬(A ❙⟶ B)›
proof -
  have 1: ‹⊢⇩B ❙¬(A ❙⟶ B) ❙⟶ A ❙∧ ❙¬B› using TAU by force
  have ‹⊢⇩B (A ❙∧ ❙¬B) ❙⟶ (A ❙⟶ ❙[b❙]A) ❙⟶ (❙¬B ❙⟶ ❙[b❙]❙¬B) ❙⟶ ❙[b❙]A ❙∧ ❙[b❙]❙¬B› 
    using TAU by force
  hence 2: ‹⊢⇩B ❙¬(A ❙⟶ B) ❙⟶ ❙[b❙]A ❙∧ ❙[b❙]❙¬B› using 1 MP_chain MPcons assms by blast
  have ‹⊢⇩B A ❙⟶ ❙¬B ❙⟶ ❙¬(A ❙⟶ B)› using TAU by force
  hence 3: ‹⊢⇩B ❙[b❙]A ❙⟶ ❙[b❙]❙¬B ❙⟶ ❙[b❙]❙¬(A ❙⟶ B)› by (metis MP_chain Nb MP Kb)
  have ‹⊢⇩B (❙[b❙]A ❙⟶ ❙[b❙]❙¬B ❙⟶ ❙[b❙]❙¬(A ❙⟶ B)) ❙⟶ ❙[b❙]A ❙∧ ❙[b❙]❙¬B ❙⟶ ❙[b❙]❙¬(A ❙⟶ B)› 
    using TAU by force
  hence 4: ‹⊢⇩B ❙[b❙]A ❙∧ ❙[b❙]❙¬B ❙⟶ ❙[b❙]❙¬(A ❙⟶ B)› using 3 MP by force
  thus ?thesis using 2 MP_chain by auto
qed  

lemma NSqPos:
  assumes ‹⊢⇩B A ❙⟶ ❙[b❙]A›
  shows ‹⊢⇩B ❙□A ❙⟶ ❙[b❙]❙□A›
  using BACK_rev KSq MP MP_chain NSq assms by blast

lemma NSqNeg:
  assumes ‹⊢⇩B ❙¬A ❙⟶ ❙[b❙]❙¬A›
shows ‹⊢⇩B ❙¬❙□A ❙⟶ ❙[b❙]❙¬❙□A› 
proof -
  have 1: ‹⊢⇩B ❙¬❙□A ❙⟶ ❙◇❙¬A›
    by (simp add: KBox.not_nec_to_pos_not)
  have 2: ‹⊢⇩B ❙◇❙¬A ❙⟶ ❙◇❙[b❙]❙¬A› using assms KBox.KN KBox.Kpos MP by blast
  have 3: ‹⊢⇩B (❙¬❙[b❙]❙¬❙□A ❙∧ ❙◇❙[b❙]❙¬A ❙⟶ ❙⊥) ❙⟶ (❙◇❙[b❙]❙¬A ❙⟶ ❙[b❙]❙¬❙□A)› using TAU by force
  have 4: ‹⊢⇩B ❙¬❙[b❙]❙¬❙□A ❙∧ ❙◇❙[b❙]❙¬A ❙⟶ ❙⟨b❙⟩(❙□A ❙∧ ❙◇❙¬A)› using FORTH by force
  have 5: ‹⊢⇩B ❙◇❙¬A ❙⟶ ❙¬❙□A› by (simp add: KBox.pos_not_to_not_nec) 
  have  ‹⊢⇩B (❙◇❙¬A ❙⟶ ❙¬❙□A) ❙⟶ ❙¬(❙□A ❙∧ ❙◇❙¬A)› using TAU by force
  hence ‹⊢⇩B ❙¬(❙□A ❙∧ ❙◇❙¬A)› using 5 MP by auto
  hence ‹⊢⇩B ❙[b❙]❙¬(❙□A ❙∧ ❙◇❙¬A)› using Nb by blast
  hence 6: ‹⊢⇩B ❙⟨b❙⟩(❙□A ❙∧ ❙◇❙¬A) ❙⟶ ❙⊥› 
    by (meson KFrB.not_nec_to_pos_not KFrB.not_pos_to_nec_not 
        KFrB.pos_not_to_not_nec MP MPcons) 
  hence ‹⊢⇩B ❙¬❙[b❙]❙¬❙□A ❙∧ ❙◇❙[b❙]❙¬A ❙⟶ ❙⊥› using 4 MP_chain by blast
  hence ‹⊢⇩B ❙◇❙[b❙]❙¬A ❙⟶ ❙[b❙]❙¬❙□A› using 3 MP by blast
  thus ?thesis using 1 2 MP_chain by blast
qed

text ‹The following lemma extends atomic harmony (HARM) to all formulas in ‹ℒ⇩□›.›

lemma Lbox_harm:
  assumes ‹A ∈ Lbox›
  shows‹⊢⇩B A ❙⟶ ❙[b❙]A› 
proof -
  have ‹⊢⇩B A ❙⟶ ❙[b❙]A ∧ ⊢⇩B ❙¬A ❙⟶ ❙[b❙]❙¬A›
    using assms
  proof (induct A rule: Lbox.induct)
    case Fls
    thus ?case using BotPos BotNeg by simp
  next
    case (Pro l)
    thus ?case using HARM by fastforce
  next
    case (Imp A B)
    thus ?case using impPos impNeg by fastforce
  next
    case (Box A)
    thus ?case using NSqPos NSqNeg by fastforce
  qed
  thus ?thesis by simp
qed

end