Theory PAL

(*
  File:      PAL.thy
  Author:    Asta Halkjær From

  This work is a formalization of public announcement logic.
  It includes proofs of soundness and completeness for variants of the axiom system
    PA + DIST! + NEC!.
  The completeness proofs build on the Epistemic Logic theory.
*)

theory PAL imports "Epistemic_Logic.Epistemic_Logic" begin

section ‹Syntax›

datatype 'i pfm
  = FF (‹❙⊥⇩!›)
  | Pro' id (‹Pro⇩!›)
  | Dis ‹'i pfm› ‹'i pfm› (infixr ‹❙∨⇩!› 60)
  | Con ‹'i pfm› ‹'i pfm› (infixr ‹❙∧⇩!› 65)
  | Imp ‹'i pfm› ‹'i pfm› (infixr ‹❙⟶⇩!› 55)
  | K' 'i ‹'i pfm› (‹K⇩!›)
  | Ann ‹'i pfm› ‹'i pfm› (‹[_]⇩! _› [80, 80] 80)

abbreviation PIff :: ‹'i pfm ⇒ 'i pfm ⇒ 'i pfm› (infixr ‹❙⟷⇩!› 55) where
  ‹p ❙⟷⇩! q ≡ (p ❙⟶⇩! q) ❙∧⇩! (q ❙⟶⇩! p)›

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

abbreviation PL (‹L⇩!›) where
  ‹L⇩! i p ≡ (❙¬⇩! (K⇩! i (❙¬⇩! p)))›

primrec anns :: ‹'i pfm ⇒ 'i pfm set› where
  ‹anns ❙⊥⇩! = {}›
| ‹anns (Pro⇩! _) = {}›
| ‹anns (p ❙∨⇩! q) = (anns p ∪ anns q)›
| ‹anns (p ❙∧⇩! q) = (anns p ∪ anns q)›
| ‹anns (p ❙⟶⇩! q) = (anns p ∪ anns q)›
| ‹anns (K⇩! i p) = anns p›
| ‹anns ([r]⇩! p) = {r} ∪ anns r ∪ anns p›

section ‹Semantics›

fun
  psemantics :: ‹('i, 'w) kripke ⇒ 'w ⇒ 'i pfm ⇒ bool› (‹_, _ ⊨⇩! _› [50, 50, 50] 50) and
  restrict :: ‹('i, 'w) kripke ⇒ 'i pfm ⇒ ('i, 'w) kripke› (‹_[_!]› [50, 50] 50) where
  ‹M, w ⊨⇩! ❙⊥⇩! ⟷ False›
| ‹M, w ⊨⇩! Pro⇩! x ⟷ π M w x›
| ‹M, w ⊨⇩! p ❙∨⇩! q ⟷ M, w ⊨⇩! p ∨ M, w ⊨⇩! q›
| ‹M, w ⊨⇩! p ❙∧⇩! q ⟷ M, w ⊨⇩! p ∧ M, w ⊨⇩! q›
| ‹M, w ⊨⇩! p ❙⟶⇩! q ⟷ M, w ⊨⇩! p ⟶ M, w ⊨⇩! q›
| ‹M, w ⊨⇩! K⇩! i p ⟷ (∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨⇩! p)›
| ‹M, w ⊨⇩! [r]⇩! p ⟷ M, w ⊨⇩! r ⟶ M[r!], w ⊨⇩! p›
| ‹M[r!] = M ⦇𝒲 := {w. w ∈ 𝒲 M ∧ M, w ⊨⇩! r}⦈›

abbreviation validPStar :: ‹(('i, 'w) kripke ⇒ bool) ⇒ 'i pfm set ⇒ 'i pfm ⇒ bool›
  (‹_; _ ⊫⇩!⋆ _› [50, 50, 50] 50) where
  ‹P; G ⊫⇩!⋆ p ≡ ∀M. P M ⟶ (∀w ∈ 𝒲 M. (∀q ∈ G. M, w ⊨⇩! q) ⟶ M, w ⊨⇩! p)›

primrec static :: ‹'i pfm ⇒ bool› where
  ‹static ❙⊥⇩! = True›
| ‹static (Pro⇩! _) = True›
| ‹static (p ❙∨⇩! q) = (static p ∧ static q)›
| ‹static (p ❙∧⇩! q) = (static p ∧ static q)›
| ‹static (p ❙⟶⇩! q) = (static p ∧ static q)›
| ‹static (K⇩! i p) = static p›
| ‹static ([r]⇩! p) = False›

primrec lower :: ‹'i pfm ⇒ 'i fm› where
  ‹lower ❙⊥⇩! = ❙⊥›
| ‹lower (Pro⇩! x) = Pro x›
| ‹lower (p ❙∨⇩! q) = (lower p ❙∨ lower q)›
| ‹lower (p ❙∧⇩! q) = (lower p ❙∧ lower q)›
| ‹lower (p ❙⟶⇩! q) = (lower p ❙⟶ lower q)›
| ‹lower (K⇩! i p) = K i (lower p)›
| ‹lower ([r]⇩! p) = undefined›

primrec lift :: ‹'i fm ⇒ 'i pfm› where
  ‹lift ❙⊥ = ❙⊥⇩!›
| ‹lift (Pro x) = Pro⇩! x›
| ‹lift (p ❙∨ q) = (lift p ❙∨⇩! lift q)›
| ‹lift (p ❙∧ q) = (lift p ❙∧⇩! lift q)›
| ‹lift (p ❙⟶ q) = (lift p ❙⟶⇩! lift q)›
| ‹lift (K i p) = K⇩! i (lift p)›

lemma lower_semantics:
  assumes ‹static p›
  shows ‹(M, w ⊨ lower p) ⟷ (M, w ⊨⇩! p)›
  using assms by (induct p arbitrary: w) simp_all

lemma lift_semantics: ‹(M, w ⊨ p) ⟷ (M, w ⊨⇩! lift p)›
  by (induct p arbitrary: w) simp_all

lemma lower_lift: ‹lower (lift p) = p›
  by (induct p) simp_all

lemma lift_lower: ‹static p ⟹ lift (lower p) = p›
  by (induct p) simp_all

section ‹Soundness of Reduction›

primrec reduce' :: ‹'i pfm ⇒ 'i pfm ⇒ 'i pfm› where
  ‹reduce' r ❙⊥⇩! = (r ❙⟶⇩! ❙⊥⇩!)›
| ‹reduce' r (Pro⇩! x) = (r ❙⟶⇩! Pro⇩! x)›
| ‹reduce' r (p ❙∨⇩! q) = (reduce' r p ❙∨⇩! reduce' r q)›
| ‹reduce' r (p ❙∧⇩! q) = (reduce' r p ❙∧⇩! reduce' r q)›
| ‹reduce' r (p ❙⟶⇩! q) = (reduce' r p ❙⟶⇩! reduce' r q)›
| ‹reduce' r (K⇩! i p) = (r ❙⟶⇩! K⇩! i (reduce' r p))›
| ‹reduce' r ([p]⇩! q) = undefined›

primrec reduce :: ‹'i pfm ⇒ 'i pfm› where
  ‹reduce ❙⊥⇩! = ❙⊥⇩!›
| ‹reduce (Pro⇩! x) = Pro⇩! x›
| ‹reduce (p ❙∨⇩! q) = (reduce p ❙∨⇩! reduce q)›
| ‹reduce (p ❙∧⇩! q) = (reduce p ❙∧⇩! reduce q)›
| ‹reduce (p ❙⟶⇩! q) = (reduce p ❙⟶⇩! reduce q)›
| ‹reduce (K⇩! i p) = K⇩! i (reduce p)›
| ‹reduce ([r]⇩! p) = reduce' (reduce r) (reduce p)›

lemma static_reduce': ‹static p ⟹ static r ⟹ static (reduce' r p)›
  by (induct p) simp_all

lemma static_reduce: ‹static (reduce p)›
  by (induct p) (simp_all add: static_reduce')

lemma reduce'_semantics:
  assumes ‹static q›
  shows ‹(M, w ⊨⇩! [p]⇩! q) = (M, w ⊨⇩! reduce' p q)›
  using assms by (induct q arbitrary: w) auto

lemma reduce_semantics: ‹M, w ⊨⇩! p ⟷ M, w ⊨⇩! reduce p›
proof (induct p arbitrary: M w)
  case (Ann p q)
  then show ?case
    using reduce'_semantics static_reduce by fastforce
qed simp_all

section ‹Chains of Implications›

primrec implyP :: ‹'i pfm list ⇒ 'i pfm ⇒ 'i pfm› (infixr ‹❙↝⇩!› 56) where
  ‹([] ❙↝⇩! q) = q›
| ‹(p # ps ❙↝⇩! q) = (p ❙⟶⇩! ps ❙↝⇩! q)›

lemma lift_implyP: ‹lift (ps ❙↝ q) = (map lift ps ❙↝⇩! lift q)›
  by (induct ps) auto

lemma reduce_implyP: ‹reduce (ps ❙↝⇩! q) = (map reduce ps ❙↝⇩! reduce q)›
  by (induct ps) auto

section ‹Proof System›

primrec peval :: ‹(id ⇒ bool) ⇒ ('i pfm ⇒ bool) ⇒ 'i pfm ⇒ bool› where
  ‹peval _ _ ❙⊥⇩! = False›
| ‹peval g _ (Pro⇩! x) = g x›
| ‹peval g h (p ❙∨⇩! q) = (peval g h p ∨ peval g h q)›
| ‹peval g h (p ❙∧⇩! q) = (peval g h p ∧ peval g h q)›
| ‹peval g h (p ❙⟶⇩! q) = (peval g h p ⟶ peval g h q)›
| ‹peval _ h (K⇩! i p) = h (K⇩! i p)›
| ‹peval _ h ([r]⇩! p) = h ([r]⇩! p)›

abbreviation ‹ptautology p ≡ ∀g h. peval g h p›

inductive PAK :: ‹('i pfm ⇒ bool) ⇒ ('i pfm ⇒ bool) ⇒ 'i pfm ⇒ bool›
  (‹_; _ ⊢⇩! _› [50, 50, 50] 50)
  for A B :: ‹'i pfm ⇒ bool› where
    PA1: ‹ptautology p ⟹ A; B ⊢⇩! p›
  | PA2: ‹A; B ⊢⇩! K⇩! i p ❙∧⇩! K⇩! i (p ❙⟶⇩! q) ❙⟶⇩! K⇩! i q›
  | PAx: ‹A p ⟹ A; B ⊢⇩! p›
  | PR1: ‹A; B ⊢⇩! p ⟹ A; B ⊢⇩! p ❙⟶⇩! q ⟹ A; B ⊢⇩! q›
  | PR2: ‹A; B ⊢⇩! p ⟹ A; B ⊢⇩! K⇩! i p›
  | PAnn: ‹A; B ⊢⇩! p ⟹ B r ⟹ A; B ⊢⇩! [r]⇩! p›
  | PFF: ‹A; B ⊢⇩! [r]⇩! ❙⊥⇩! ❙⟷⇩! (r ❙⟶⇩! ❙⊥⇩!)›
  | PPro: ‹A; B ⊢⇩! [r]⇩! Pro⇩! x ❙⟷⇩! (r ❙⟶⇩! Pro⇩! x)›
  | PDis: ‹A; B ⊢⇩! [r]⇩! (p ❙∨⇩! q) ❙⟷⇩! [r]⇩! p ❙∨⇩! [r]⇩! q›
  | PCon: ‹A; B ⊢⇩! [r]⇩! (p ❙∧⇩! q) ❙⟷⇩! [r]⇩! p ❙∧⇩! [r]⇩! q›
  | PImp: ‹A; B ⊢⇩! [r]⇩! (p ❙⟶⇩! q) ❙⟷⇩! ([r]⇩! p ❙⟶⇩! [r]⇩! q)›
  | PK: ‹A; B ⊢⇩! [r]⇩! K⇩! i p ❙⟷⇩! (r ❙⟶⇩! K⇩! i ([r]⇩! p))›

abbreviation PAK_assms (‹_; _; _ ⊢⇩! _› [50, 50, 50, 50] 50) where
  ‹A; B; G ⊢⇩! p ≡ ∃qs. set qs ⊆ G ∧ (A; B ⊢⇩! qs ❙↝⇩! p)›

lemma eval_peval: ‹eval h (g o lift) p = peval h g (lift p)›
  by (induct p) simp_all

lemma tautology_ptautology: ‹tautology p ⟹ ptautology (lift p)›
  using eval_peval by blast

theorem AK_PAK: ‹A o lift ⊢ p ⟹ A; B ⊢⇩! lift p›
  by (induct p rule: AK.induct) (auto intro: PAK.intros(1-5) simp: tautology_ptautology)

abbreviation validP
  :: ‹(('i, 'i fm set) kripke ⇒ bool) ⇒ 'i pfm set ⇒ 'i pfm ⇒ bool›
  (‹_; _ ⊫⇩! _› [50, 50, 50] 50)
  where ‹P; G ⊫⇩! p ≡ P; G ⊫⇩!⋆ p›

lemma set_map_inv:
  assumes ‹set xs ⊆ f ` X›
  shows ‹∃ys. set ys ⊆ X ∧ map f ys = xs›
  using assms
proof (induct xs)
  case (Cons x xs)
  then obtain ys where ‹set ys ⊆ X› ‹map f ys = xs›
    by auto
  moreover obtain y where ‹y ∈ X› ‹f y = x›
    using Cons.prems by auto
  ultimately have ‹set (y # ys) ⊆ X› ‹map f (y # ys) = x # xs›
    by simp_all
  then show ?case
    by meson
qed simp

lemma strong_static_completeness':
  assumes ‹static p› and ‹∀q ∈ G. static q› and ‹P; G ⊫⇩! p›
    and ‹P; lower ` G ⊫⋆ lower p ⟹ A o lift; lower ` G ⊢ lower p›
  shows ‹A; B; G ⊢⇩! p›
proof -
  have ‹P; lower ` G ⊫⋆ lower p›
    using assms by (simp add: lower_semantics)
  then have ‹A o lift; lower ` G ⊢ lower p›
    using assms(4) by blast
  then obtain qs where ‹set qs ⊆ G› and ‹A o lift ⊢ map lower qs ❙↝ lower p›
    using set_map_inv by blast
  then have ‹A; B ⊢⇩! lift (map lower qs ❙↝ lower p)›
    using AK_PAK by fast
  then have ‹A; B ⊢⇩! map lift (map lower qs) ❙↝⇩! lift (lower p)›
    using lift_implyP by metis
  then have ‹A; B ⊢⇩! map (lift o lower) qs ❙↝⇩! lift (lower p)›
    by simp
  then show ?thesis
    using assms(1-2) ‹set qs ⊆ G› lift_lower
    by (metis (mono_tags, lifting) comp_apply map_idI subset_eq)
qed

theorem strong_static_completeness:
  assumes ‹static p› and ‹∀q ∈ G. static q› and ‹P; G ⊫⇩! p›
    and ‹⋀G p. P; G ⊫ p ⟹ A o lift; G ⊢ p›
  shows ‹A; B; G ⊢⇩! p›
  using strong_static_completeness' assms .

corollary static_completeness':
  assumes ‹static p› and ‹P; {} ⊫⇩!⋆ p›
    and ‹P; {} ⊫ lower p ⟹ A o lift ⊢ lower p›
  shows ‹A; B ⊢⇩! p›
  using assms strong_static_completeness'[where G=‹{}› and p=p] by simp

corollary static_completeness:
  assumes ‹static p› and ‹P; {} ⊫⇩!⋆ p› and ‹⋀p. P; {} ⊫ p ⟹ A o lift ⊢ p›
  shows ‹A; B ⊢⇩! p›
  using static_completeness' assms .

corollary
  assumes ‹static p› ‹(λ_. True); {} ⊫⇩! p›
  shows ‹A; B ⊢⇩! p›
  using assms static_completeness[where P=‹λ_. True› and p=p] completeness⇩A by blast

section ‹Soundness›

lemma peval_semantics:
  ‹peval (val w) (λq. ⦇𝒲 = W, 𝒦 = r, π = val⦈, w ⊨⇩! q) p = (⦇𝒲 = W, 𝒦 = r, π = val⦈, w ⊨⇩! p)›
  by (induct p) simp_all

lemma ptautology:
  assumes ‹ptautology p›
  shows ‹M, w ⊨⇩! p›
proof -
  from assms have ‹peval (g w) (λq. ⦇𝒲 = W, 𝒦 = r, π = g⦈, w ⊨⇩! q) p› for W g r
    by simp
  then have ‹⦇𝒲 = W, 𝒦 = r, π = g⦈, w ⊨⇩! p› for W g r
    using peval_semantics by fast
  then show ‹M, w ⊨⇩! p›
    by (metis kripke.cases)
qed

theorem soundness⇩P:
  assumes
    ‹⋀M p w. A p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
    ‹⋀M r. P M ⟹ B r ⟹ P (M[r!])›
  shows ‹A; B ⊢⇩! p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
proof (induct p arbitrary: M w rule: PAK.induct)
  case (PAnn p r)
  then show ?case
    using assms by simp
qed (simp_all add: assms ptautology)

corollary ‹(λ_. False); B ⊢⇩! p ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  using soundness⇩P[where P=‹λ_. True›] by metis

section ‹Strong Soundness›

lemma ptautology_imply_superset:
  assumes ‹set ps ⊆ set qs›
  shows ‹ptautology (ps ❙↝⇩! r ❙⟶⇩! qs ❙↝⇩! r)›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain g h where ‹¬ peval g h (ps ❙↝⇩! r ❙⟶⇩! qs ❙↝⇩! r)›
    by blast
  then have ‹peval g h (ps ❙↝⇩! r)› ‹¬ peval g h (qs ❙↝⇩! r)›
    by simp_all
  then consider (np) ‹∃p ∈ set ps. ¬ peval g h p› | (r) ‹∀p ∈ set ps. peval g h p› ‹peval g h r›
    by (induct ps) auto
  then show False
  proof cases
    case np
    then have ‹∃p ∈ set qs. ¬ peval g h p›
      using ‹set ps ⊆ set qs› by blast
    then have ‹peval g h (qs ❙↝⇩! r)›
      by (induct qs) simp_all
    then show ?thesis
      using ‹¬ peval g h (qs ❙↝⇩! r)› by blast
  next
    case r
    then have ‹peval g h (qs ❙↝⇩! r)›
      by (induct qs) simp_all
    then show ?thesis
      using ‹¬ peval g h (qs ❙↝⇩! r)› by blast
  qed
qed

lemma PK_imply_weaken:
  assumes ‹A; B ⊢⇩! ps ❙↝⇩! q› ‹set ps ⊆ set ps'›
  shows ‹A; B ⊢⇩! ps' ❙↝⇩! q›
proof -
  have ‹ptautology (ps ❙↝⇩! q ❙⟶⇩! ps' ❙↝⇩! q)›
    using ‹set ps ⊆ set ps'› ptautology_imply_superset by blast
  then have ‹A; B ⊢⇩! ps ❙↝⇩! q ❙⟶⇩! ps' ❙↝⇩! q›
    using PA1 by blast
  then show ?thesis
    using ‹A; B ⊢⇩! ps ❙↝⇩! q› PR1 by blast
qed

lemma implyP_append: ‹(ps @ ps' ❙↝⇩! q) = (ps ❙↝⇩! ps' ❙↝⇩! q)›
  by (induct ps) simp_all

lemma PK_ImpI:
  assumes ‹A; B ⊢⇩! p # G ❙↝⇩! q›
  shows ‹A; B ⊢⇩! G ❙↝⇩! (p ❙⟶⇩! q)›
proof -
  have ‹set (p # G) ⊆ set (G @ [p])›
    by simp
  then have ‹A; B ⊢⇩! G @ [p] ❙↝⇩! q›
    using assms PK_imply_weaken by blast
  then have ‹A; B ⊢⇩! G ❙↝⇩! [p] ❙↝⇩! q›
    using implyP_append by metis
  then show ?thesis
    by simp
qed

corollary soundness_imply⇩P:
  assumes
    ‹⋀M p w. A p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
    ‹⋀M r. P M ⟹ B r ⟹ P (M[r!])›
  shows ‹A; B ⊢⇩! qs ❙↝⇩! p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ ∀q ∈ set qs. M, w ⊨⇩! q ⟹ M, w ⊨⇩! p›
proof (induct qs arbitrary: p)
  case Nil
  then show ?case
    using soundness⇩P[of A P B p M w] assms by simp
next
  case (Cons q qs)
  then show ?case
    using PK_ImpI by fastforce
qed

theorem strong_soundness⇩P:
  assumes
    ‹⋀M w p. A p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
    ‹⋀M r. P M ⟹ B r ⟹ P (M[r!])›
  shows ‹A; B; G ⊢⇩! p ⟹ P; G ⊫⇩!⋆ p›
proof safe
  fix qs w and M :: ‹('a, 'b) kripke›
  assume ‹A; B ⊢⇩! qs ❙↝⇩! p›
  moreover assume ‹set qs ⊆ G› ‹∀q ∈ G. M, w ⊨⇩! q›
  then have ‹∀q ∈ set qs. M, w ⊨⇩! q›
    using ‹set qs ⊆ G› by blast
  moreover assume ‹P M› ‹w ∈ 𝒲 M›
  ultimately show ‹M, w ⊨⇩! p›
    using soundness_imply⇩P[of A P B qs p] assms by blast
qed

section ‹Completeness›

lemma ConE:
  assumes ‹A; B ⊢⇩! p ❙∧⇩! q›
  shows ‹A; B ⊢⇩! p› ‹A; B ⊢⇩! q›
  using assms by (metis PA1 PR1 peval.simps(4-5))+

lemma Iff_Dis:
  assumes ‹A; B ⊢⇩! p ❙⟷⇩! p'› ‹A; B ⊢⇩! q ❙⟷⇩! q'›
  shows ‹A; B ⊢⇩! ((p ❙∨⇩! q) ❙⟷⇩! (p' ❙∨⇩! q'))›
proof -
  have ‹A; B ⊢⇩! (p ❙⟷⇩! p') ❙⟶⇩! (q ❙⟷⇩! q') ❙⟶⇩! ((p ❙∨⇩! q) ❙⟷⇩! (p' ❙∨⇩! q'))›
    by (simp add: PA1)
  then show ?thesis
    using assms PR1 by blast
qed

lemma Iff_Con:
  assumes ‹A; B ⊢⇩! p ❙⟷⇩! p'› ‹A; B ⊢⇩! q ❙⟷⇩! q'›
  shows ‹A; B ⊢⇩! (p ❙∧⇩! q) ❙⟷⇩! (p' ❙∧⇩! q')›
proof -
  have ‹A; B ⊢⇩! (p ❙⟷⇩! p') ❙⟶⇩! (q ❙⟷⇩! q') ❙⟶⇩! ((p ❙∧⇩! q) ❙⟷⇩! (p' ❙∧⇩! q'))›
    by (simp add: PA1)
  then show ?thesis
    using assms PR1 by blast
qed

lemma Iff_Imp:
  assumes ‹A; B ⊢⇩! p ❙⟷⇩! p'› ‹A; B ⊢⇩! q ❙⟷⇩! q'›
  shows ‹A; B ⊢⇩! ((p ❙⟶⇩! q) ❙⟷⇩! (p' ❙⟶⇩! q'))›
proof -
  have ‹A; B ⊢⇩! (p ❙⟷⇩! p') ❙⟶⇩! (q ❙⟷⇩! q') ❙⟶⇩! ((p ❙⟶⇩! q) ❙⟷⇩! (p' ❙⟶⇩! q'))›
    by (simp add: PA1)
  then show ?thesis
    using assms PR1 by blast
qed

lemma Iff_sym: ‹(A; B ⊢⇩! p ❙⟷⇩! q) = (A; B ⊢⇩! q ❙⟷⇩! p)›
proof -
  have ‹A; B ⊢⇩! (p ❙⟷⇩! q) ❙⟷⇩! (q ❙⟷⇩! p)›
    by (simp add: PA1)
  then show ?thesis
    using PR1 ConE by blast
qed

lemma Iff_Iff:
  assumes ‹A; B ⊢⇩! p ❙⟷⇩! p'› ‹A; B ⊢⇩! p ❙⟷⇩! q›
  shows ‹A; B ⊢⇩! p' ❙⟷⇩! q›
proof -
  have ‹ptautology ((p ❙⟷⇩! p') ❙⟶⇩! (p ❙⟷⇩! q) ❙⟶⇩! (p' ❙⟷⇩! q))›
    by (metis peval.simps(4-5))
  with PA1 have ‹A; B ⊢⇩! (p ❙⟷⇩! p') ❙⟶⇩! (p ❙⟷⇩! q) ❙⟶⇩! (p' ❙⟷⇩! q)› .
  then show ?thesis
    using assms PR1 by blast
qed

lemma K'_A2': ‹A; B ⊢⇩! K⇩! i (p ❙⟶⇩! q) ❙⟶⇩! K⇩! i p ❙⟶⇩! K⇩! i q›
proof -
  have ‹A; B ⊢⇩! K⇩! i p ❙∧⇩! K⇩! i (p ❙⟶⇩! q) ❙⟶⇩! K⇩! i q›
    using PA2 by fast
  moreover have ‹A; B ⊢⇩! (P ❙∧⇩! Q ❙⟶⇩! R) ❙⟶⇩! (Q ❙⟶⇩! P ❙⟶⇩! R)› for P Q R
    by (simp add: PA1)
  ultimately show ?thesis
    using PR1 by fast
qed

lemma K'_map:
  assumes ‹A; B ⊢⇩! p ❙⟶⇩! q›
  shows ‹A; B ⊢⇩! K⇩! i p ❙⟶⇩! K⇩! i q›
proof -
  note ‹A; B ⊢⇩! p ❙⟶⇩! q›
  then have ‹A; B ⊢⇩! K⇩! i (p ❙⟶⇩! q)›
    using PR2 by fast
  moreover have ‹A; B ⊢⇩! K⇩! i (p ❙⟶⇩! q) ❙⟶⇩! K⇩! i p ❙⟶⇩! K⇩! i q›
    using K'_A2' by fast
  ultimately show ?thesis
    using PR1 by fast
qed

lemma ConI:
  assumes ‹A; B ⊢⇩! p› ‹A; B ⊢⇩! q›
  shows ‹A; B ⊢⇩! p ❙∧⇩! q›
proof -
  have ‹A; B ⊢⇩! p ❙⟶⇩! q ❙⟶⇩! p ❙∧⇩! q›
    by (simp add: PA1)
  then show ?thesis
    using assms PR1 by blast
qed

lemma Iff_wk:
  assumes ‹A; B ⊢⇩! p ❙⟷⇩! q›
  shows ‹A; B ⊢⇩! (r ❙⟶⇩! p) ❙⟷⇩! (r ❙⟶⇩! q)›
proof -
  have ‹A; B ⊢⇩! (p ❙⟷⇩! q) ❙⟶⇩! ((r ❙⟶⇩! p) ❙⟷⇩! (r ❙⟶⇩! q))›
    by (simp add: PA1)
  then show ?thesis
    using assms PR1 by blast
qed

lemma Iff_reduce':
  assumes ‹static p›
  shows ‹A; B ⊢⇩! [r]⇩! p ❙⟷⇩! reduce' r p›
  using assms
proof (induct p rule: pfm.induct)
  case FF
  then show ?case
    by (simp add: PFF)
next
  case (Pro' x)
  then show ?case
    by (simp add: PPro)
next
  case (Dis p q)
  then have ‹A; B ⊢⇩! [r]⇩! p ❙∨⇩! [r]⇩! q ❙⟷⇩! reduce' r (p ❙∨⇩! q)›
    using Iff_Dis by fastforce
  moreover have ‹A; B ⊢⇩! ([r]⇩! p ❙∨⇩! [r]⇩! q) ❙⟷⇩! ([r]⇩! (p ❙∨⇩! q))›
    using PDis Iff_sym by fastforce
  ultimately show ?case
    using PA1 PR1 Iff_Iff by blast
next
  case (Con p q)
  then have ‹A; B ⊢⇩! [r]⇩! p ❙∧⇩! [r]⇩! q ❙⟷⇩! reduce' r (p ❙∧⇩! q)›
    using Iff_Con by fastforce
  moreover have ‹A; B ⊢⇩! ([r]⇩! p ❙∧⇩! [r]⇩! q) ❙⟷⇩! ([r]⇩! (p ❙∧⇩! q))›
    using PCon Iff_sym by fastforce
  ultimately show ?case
    using PA1 PR1 Iff_Iff by blast
next
  case (Imp p q)
  then have ‹A; B ⊢⇩! ([r]⇩! p ❙⟶⇩! [r]⇩! q) ❙⟷⇩! reduce' r (p ❙⟶⇩! q)›
    using Iff_Imp by fastforce
  moreover have ‹A; B ⊢⇩! ([r]⇩! p ❙⟶⇩! [r]⇩! q) ❙⟷⇩! ([r]⇩! (p ❙⟶⇩! q))›
    using PImp Iff_sym by fastforce
  ultimately show ?case
    using PA1 PR1 Iff_Iff by blast
next
  case (K' i p)
  then have ‹A; B ⊢⇩! [r]⇩! p ❙⟷⇩! reduce' r p›
    by simp
  then have ‹A; B ⊢⇩! K⇩! i ([r]⇩! p) ❙⟷⇩! K⇩! i (reduce' r p)›
    using K'_map ConE ConI by metis
  moreover have ‹A; B ⊢⇩! [r]⇩! K⇩! i p ❙⟷⇩! r ❙⟶⇩! K⇩! i ([r]⇩! p)›
    using PK .
  ultimately have ‹A; B ⊢⇩! [r]⇩! K⇩! i p ❙⟷⇩! r ❙⟶⇩! K⇩! i (reduce' r p)›
    by (meson Iff_Iff Iff_sym Iff_wk)
  then show ?case
    by simp
next
  case (Ann r p)
  then show ?case
    by simp
qed

lemma Iff_Ann1:
  assumes r: ‹A; B ⊢⇩! r ❙⟷⇩! r'› and ‹static p›
  shows ‹A; B ⊢⇩! [r]⇩! p ❙⟷⇩! [r']⇩! p›
  using assms(2-)
proof (induct p)
  case FF
  have ‹A; B ⊢⇩! (r ❙⟷⇩! r') ❙⟶⇩! ((r ❙⟶⇩! ❙⊥⇩!) ❙⟷⇩! (r' ❙⟶⇩! ❙⊥⇩!))›
    by (auto intro: PA1)
  then have ‹A; B ⊢⇩! (r ❙⟶⇩! ❙⊥⇩!) ❙⟷⇩! (r' ❙⟶⇩! ❙⊥⇩!)›
    using r PR1 by blast
  then show ?case
    by (meson PFF Iff_Iff Iff_sym)
next
  case (Pro' x)
  have ‹A; B ⊢⇩! (r ❙⟷⇩! r') ❙⟶⇩! ((r ❙⟶⇩! Pro⇩! x) ❙⟷⇩! (r' ❙⟶⇩! Pro⇩! x))›
    by (auto intro: PA1)
  then have ‹A; B ⊢⇩! (r ❙⟶⇩! Pro⇩! x) ❙⟷⇩! (r' ❙⟶⇩! Pro⇩! x)›
    using r PR1 by blast
  then show ?case
    by (meson PPro Iff_Iff Iff_sym)
next
  case (Dis p q)
  then have ‹A; B ⊢⇩! [r]⇩! p ❙∨⇩! [r]⇩! q ❙⟷⇩! [r']⇩! p ❙∨⇩! [r']⇩! q›
    by (simp add: Iff_Dis)
  then show ?case
    by (meson PDis Iff_Iff Iff_sym)
next
  case (Con p q)
  then have ‹A; B ⊢⇩! [r]⇩! p ❙∧⇩! [r]⇩! q ❙⟷⇩! [r']⇩! p ❙∧⇩! [r']⇩! q›
    by (simp add: Iff_Con)
  then show ?case
    by (meson PCon Iff_Iff Iff_sym)
next
  case (Imp p q)
  then have ‹A; B ⊢⇩! ([r]⇩! p ❙⟶⇩! [r]⇩! q) ❙⟷⇩! ([r']⇩! p ❙⟶⇩! [r']⇩! q)›
    by (simp add: Iff_Imp)
  then show ?case
    by (meson PImp Iff_Iff Iff_sym)
next
  case (K' i p)
  then have ‹A; B ⊢⇩! [r]⇩! p ❙⟷⇩! [r']⇩! p›
    by simp
  then have ‹A; B ⊢⇩! K⇩! i ([r]⇩! p) ❙⟷⇩! K⇩! i ([r']⇩! p)›
    using K'_map ConE ConI by metis
  then show ?case
    by (meson Iff_Iff Iff_Imp Iff_sym PK r)
next
  case (Ann s p)
  then show ?case
    by simp
qed

lemma Iff_Ann2:
  assumes ‹A; B ⊢⇩! p ❙⟷⇩! p'› and ‹B r›
  shows ‹A; B ⊢⇩! [r]⇩! p ❙⟷⇩! [r]⇩! p'›
  using assms PAnn ConE ConI PImp PR1 by metis

lemma Iff_reduce:
  assumes ‹∀r ∈ anns p. B r›
  shows ‹A; B ⊢⇩! p ❙⟷⇩! reduce p›
  using assms
proof (induct p)
  case (Dis p q)
  then show ?case
    by (simp add: Iff_Dis)
next
  case (Con p q)
  then show ?case
    by (simp add: Iff_Con)
next
  case (Imp p q)
  then show ?case
    by (simp add: Iff_Imp)
next
  case (K' i p)
  then have
    ‹A; B ⊢⇩! K⇩! i p ❙⟶⇩! K⇩! i (reduce p)›
    ‹A; B ⊢⇩! K⇩! i (reduce p) ❙⟶⇩! K⇩! i p›
    using K'_map ConE by fastforce+
  then have ‹A; B ⊢⇩! K⇩! i p ❙⟷⇩! K⇩! i (reduce p)›
    using ConI by blast
  then show ?case
    by simp
next
  case (Ann r p)
  then have ‹B r›
    by simp
  have ‹A; B ⊢⇩! [reduce r]⇩! reduce p ❙⟷⇩! reduce' (reduce r) (reduce p)›
    using Iff_reduce' static_reduce by blast
  moreover have ‹A; B ⊢⇩! [r]⇩! reduce p ❙⟷⇩! [reduce r]⇩! reduce p›
    using Ann Iff_Ann1 static_reduce by fastforce
  ultimately have ‹A; B ⊢⇩! [r]⇩! reduce p ❙⟷⇩! reduce' (reduce r) (reduce p)›
    using Iff_Iff Iff_sym by blast
  moreover have ‹∀r ∈ anns p. B r›
    using Ann.prems by simp
  then have ‹A; B ⊢⇩! p ❙⟷⇩! reduce p›
    using Ann.hyps(2) by blast
  then have ‹A; B ⊢⇩! [r]⇩! reduce p ❙⟷⇩! [r]⇩! p›
    using ‹B r› Iff_Ann2 Iff_sym by blast
  ultimately have ‹A; B ⊢⇩! [r]⇩! p ❙⟷⇩! reduce' (reduce r) (reduce p)›
    using Iff_Iff by blast
  then show ?case
    by simp
qed (simp_all add: PA1)

lemma anns_implyP [simp]:
  ‹anns (ps ❙↝⇩! q) =  anns q ∪ (⋃p ∈ set ps. anns p)›
  by (induct ps) auto

lemma strong_completeness⇩P':
  assumes ‹P; G ⊫⇩! p›
    and ‹∀r ∈ anns p. B r› ‹∀q ∈ G. ∀r ∈ anns q. B r›
    and ‹P; lower ` reduce ` G ⊫⋆ lower (reduce p) ⟹
      A o lift; lower ` reduce ` G ⊢ lower (reduce p)›
  shows ‹A; B; G ⊢⇩! p›
proof -
  have ‹P; reduce ` G ⊫⇩!⋆ reduce p›
    using assms(1) reduce_semantics by fast
  moreover have ‹static (reduce p)› ‹∀q ∈ reduce ` G. static q›
    using static_reduce by fast+
  ultimately have ‹A; B; reduce ` G ⊢⇩! reduce p›
    using assms(4) strong_static_completeness'[where G=‹reduce ` G› and p=‹reduce p›]
    by presburger
  then have ‹∃qs. set qs ⊆ G ∧ (A; B ⊢⇩! map reduce qs ❙↝⇩! reduce p)›
    using set_map_inv by fast
  then obtain qs where qs: ‹set qs ⊆ G› and ‹A; B ⊢⇩! map reduce qs ❙↝⇩! reduce p›
    by blast
  then have ‹A; B ⊢⇩! reduce (qs ❙↝⇩! p)›
    using reduce_implyP by metis
  moreover have ‹∀r ∈ anns (qs ❙↝⇩! p). B r›
    using assms(2-3) qs by auto
  then have ‹A; B ⊢⇩! qs ❙↝⇩! p ❙⟷⇩! reduce (qs ❙↝⇩! p)›
    using Iff_reduce by blast
  ultimately have ‹A; B ⊢⇩! qs ❙↝⇩! p›
    using ConE(2) PR1 by blast
  then show ?thesis
    using qs by blast
qed

theorem strong_completeness⇩P:
  assumes ‹P; G ⊫⇩! p›
    and ‹∀r ∈ anns p. B r› ‹∀q ∈ G. ∀r ∈ anns q. B r›
    and ‹⋀G p. P; G ⊫⋆ p ⟹ A o lift; G ⊢ p›
  shows ‹A; B; G ⊢⇩! p›
  using strong_completeness⇩P' assms .

theorem main⇩P:
  assumes ‹⋀M w p. A p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
    and ‹⋀M r. P M ⟹ B r ⟹ P (M[r!])›
    and ‹∀r ∈ anns p. B r› ‹∀q ∈ G. ∀r ∈ anns q. B r›
    and ‹⋀G p. P; G ⊫⋆ p ⟹ A o lift; G ⊢ p›
  shows ‹P; G ⊫⇩! p ⟷ A; B; G ⊢⇩! p›
  using strong_soundness⇩P[of A P B G p] strong_completeness⇩P[of P G p B A] assms by blast

corollary strong_completeness⇩P⇩B:
  assumes ‹P; G ⊫⇩! p›
    and ‹⋀G p. P; G ⊫⋆ p ⟹ A o lift; G ⊢ p›
  shows ‹A; (λ_. True); G ⊢⇩! p›
  using strong_completeness⇩P[where B=‹λ_. True›] assms by blast

corollary completeness⇩P':
  assumes ‹P; {} ⊫⇩! p›
    and ‹∀r ∈ anns p. B r›
    and ‹⋀p. P; {} ⊫ lower p ⟹ A o lift ⊢ lower p›
  shows ‹A; B ⊢⇩! p›
  using assms strong_completeness⇩P'[where P=P and G=‹{}›] by simp

corollary completeness⇩P:
  assumes ‹P; {} ⊫⇩! p›
    and ‹∀r ∈ anns p. B r›
    and ‹⋀p. P; {} ⊫ p ⟹ A o lift ⊢ p›
  shows ‹A; B ⊢⇩! p›
  using completeness⇩P' assms .

corollary completeness⇩P⇩A:
  assumes ‹(λ_. True); {} ⊫⇩! p›
  shows ‹A; (λ_. True) ⊢⇩! p›
  using assms completeness⇩P[of ‹λ_. True› p ‹λ_. True›] completeness⇩A by blast

section ‹System PAL + K›

abbreviation SystemPK (‹_ ⊢⇩!⇩K _› [50, 50] 50) where
  ‹G ⊢⇩!⇩K p ≡ (λ_. False); (λ_. True); G ⊢⇩! p›

lemma strong_soundness⇩P⇩K: ‹G ⊢⇩!⇩K p ⟹ (λ_. True); G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of ‹λ_. False› ‹λ_. True›] by fast

abbreviation validPK (‹_ ⊫⇩!⇩K _› [50, 50] 50) where
  ‹G ⊫⇩!⇩K p ≡ (λ_. True); G ⊫⇩! p›

lemma strong_completeness⇩P⇩K:
  assumes ‹G ⊫⇩!⇩K p›
  shows ‹G ⊢⇩!⇩K p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩K unfolding comp_apply .

theorem main⇩P⇩K: ‹G ⊫⇩!⇩K p ⟷ G ⊢⇩!⇩K p›
  using strong_soundness⇩P⇩K[of G p] strong_completeness⇩P⇩K[of G p] by fast

corollary ‹G ⊫⇩!⇩K p ⟹ (λ_. True); G ⊫⇩!⋆ p›
  using strong_soundness⇩P⇩K[of G p] strong_completeness⇩P⇩K[of G p] by fast

section ‹System PAL + T›

text ‹Also known as System PAL + M›

inductive AxPT :: ‹'i pfm ⇒ bool› where
  ‹AxPT (K⇩! i p ❙⟶⇩! p)›

abbreviation SystemPT (‹_ ⊢⇩!⇩T _› [50, 50] 50) where
  ‹G ⊢⇩!⇩T p ≡ AxPT; (λ_. True); G ⊢⇩! p›

lemma soundness_AxPT: ‹AxPT p ⟹ reflexive M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  unfolding reflexive_def by (induct p rule: AxPT.induct) simp

lemma reflexive_restrict: ‹reflexive M ⟹ reflexive (M[r!])›
  unfolding reflexive_def by simp

lemma strong_soundness⇩P⇩T: ‹G ⊢⇩!⇩T p ⟹ reflexive; G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of AxPT reflexive ‹λ_. True› G p]
    soundness_AxPT reflexive_restrict by fast

lemma AxT_AxPT: ‹AxT = AxPT o lift›
  unfolding comp_apply using lower_lift
  by (metis AxPT.simps AxT.simps lift.simps(5-6) lower.simps(5-6))

abbreviation validPT (‹_ ⊫⇩!⇩T _› [50, 50] 50) where
  ‹G ⊫⇩!⇩T p ≡ reflexive; G ⊫⇩! p›

lemma strong_completeness⇩P⇩T:
  assumes ‹G ⊫⇩!⇩T p›
  shows ‹G ⊢⇩!⇩T p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩T unfolding AxT_AxPT .

theorem main⇩P⇩T: ‹G ⊫⇩!⇩T p ⟷ G ⊢⇩!⇩T p›
  using strong_soundness⇩P⇩T[of G p] strong_completeness⇩P⇩T[of G p] by fast

corollary ‹G ⊫⇩!⇩T p ⟹ reflexive; G ⊫⇩!⋆ p›
  using strong_soundness⇩P⇩T[of G p] strong_completeness⇩P⇩T[of G p] by fast

section ‹System PAL + KB›

inductive AxPB :: ‹'i pfm ⇒ bool› where
  ‹AxPB (p ❙⟶⇩! K⇩! i (L⇩! i p))›

abbreviation SystemPKB (‹_ ⊢⇩!⇩K⇩B _› [50, 50] 50) where
  ‹G ⊢⇩!⇩K⇩B p ≡ AxPB; (λ_. True); G ⊢⇩! p›

lemma soundness_AxPB: ‹AxPB p ⟹ symmetric M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  unfolding symmetric_def by (induct p rule: AxPB.induct) auto

lemma symmetric_restrict: ‹symmetric M ⟹ symmetric (M[r!])›
  unfolding symmetric_def by simp

lemma strong_soundness⇩P⇩K⇩B: ‹G ⊢⇩!⇩K⇩B p ⟹ symmetric; G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of AxPB symmetric ‹λ_. True› G p]
    soundness_AxPB symmetric_restrict by fast

lemma AxB_AxPB: ‹AxB = AxPB o lift›
proof
  fix p :: ‹'i fm›
  show ‹AxB p = (AxPB ∘ lift) p›
    unfolding comp_apply using lower_lift
    by (smt (verit, best) AxB.simps AxPB.simps lift.simps(1, 5-6) lower.simps(5-6))
qed

abbreviation validPKB (‹_ ⊫⇩!⇩K⇩B _› [50, 50] 50) where
  ‹G ⊫⇩!⇩K⇩B p ≡ symmetric; G ⊫⇩! p›

lemma strong_completeness⇩P⇩K⇩B:
  assumes ‹G ⊫⇩!⇩K⇩B p›
  shows ‹G ⊢⇩!⇩K⇩B p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩K⇩B unfolding AxB_AxPB .

theorem main⇩P⇩K⇩B: ‹G ⊫⇩!⇩K⇩B p ⟷ G ⊢⇩!⇩K⇩B p›
  using strong_soundness⇩P⇩K⇩B[of G p] strong_completeness⇩P⇩K⇩B[of G p] by fast

corollary ‹G ⊫⇩!⇩K⇩B p ⟹ symmetric; G ⊫⇩!⋆ p›
  using strong_soundness⇩P⇩K⇩B[of G p] strong_completeness⇩P⇩K⇩B[of G p] by fast

section ‹System PAL + K4›

inductive AxP4 :: ‹'i pfm ⇒ bool› where
  ‹AxP4 (K⇩! i p ❙⟶⇩! K⇩! i (K⇩! i p))›

abbreviation SystemPK4 (‹_ ⊢⇩!⇩K⇩4 _› [50, 50] 50) where
  ‹G ⊢⇩!⇩K⇩4 p ≡ AxP4; (λ_. True); G ⊢⇩! p›

lemma pos_introspection:
  assumes ‹transitive M› ‹w ∈ 𝒲 M›
  shows ‹M, w ⊨⇩! (K⇩! i p ❙⟶⇩! K⇩! i (K⇩! i p))›
proof -
  { assume ‹M, w ⊨⇩! K⇩! i p›
    then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨⇩! p›
      by simp
    then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. ∀u ∈ 𝒲 M ∩ 𝒦 M i v. M, u ⊨⇩! p›
      using ‹transitive M› ‹w ∈ 𝒲 M› unfolding transitive_def by blast
    then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨⇩! K⇩! i p›
      by simp
    then have ‹M, w ⊨⇩! K⇩! i (K⇩! i p)›
      by simp }
  then show ?thesis
    by fastforce
qed

lemma soundness_AxP4: ‹AxP4 p ⟹ transitive M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  by (induct p rule: AxP4.induct) (metis pos_introspection)

lemma transitive_restrict: ‹transitive M ⟹ transitive (M[r!])›
  unfolding transitive_def by (cases M) (metis (no_types, lifting) frame.select_convs(1-2)
      frame.update_convs(1) mem_Collect_eq restrict.simps)

lemma strong_soundness⇩P⇩K⇩4: ‹G ⊢⇩!⇩K⇩4 p ⟹ transitive; G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of AxP4 transitive ‹λ_. True› G p]
    soundness_AxP4 transitive_restrict by fast

lemma Ax4_AxP4: ‹Ax4 = AxP4 o lift›
proof
  fix p :: ‹'i fm›
  show ‹Ax4 p = (AxP4 ∘ lift) p›
    unfolding comp_apply using lower_lift
    by (smt (verit, best) Ax4.simps AxP4.simps lift.simps(1, 5-6) lower.simps(5-6))
qed

abbreviation validPK4 (‹_ ⊫⇩!⇩K⇩4 _› [50, 50] 50) where
  ‹G ⊫⇩!⇩K⇩4 p ≡ transitive; G ⊫⇩! p›

lemma strong_completeness⇩P⇩K⇩4:
  assumes ‹G ⊫⇩!⇩K⇩4 p›
  shows ‹G ⊢⇩!⇩K⇩4 p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩K⇩4 unfolding Ax4_AxP4 .

theorem main⇩P⇩K⇩4: ‹G ⊫⇩!⇩K⇩4 p ⟷ G ⊢⇩!⇩K⇩4 p›
  using strong_soundness⇩P⇩K⇩4[of G p] strong_completeness⇩P⇩K⇩4[of G p] by fast

corollary ‹G ⊫⇩!⇩K⇩4 p ⟹ transitive; G ⊫⇩!⋆ p›
  using strong_soundness⇩P⇩K⇩4[of G p] strong_completeness⇩P⇩K⇩4[of G p] by fast

section ‹System PAL + K5›

inductive AxP5 :: ‹'i pfm ⇒ bool› where
  ‹AxP5 (L⇩! i p ❙⟶⇩! K⇩! i (L⇩! i p))›

abbreviation SystemPK5 (‹_ ⊢⇩!⇩K⇩5 _› [50, 50] 50) where
  ‹G ⊢⇩!⇩K⇩5 p ≡ AxP5; (λ_. True); G ⊢⇩! p›

lemma soundness_AxP5: ‹AxP5 p ⟹ Euclidean M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  by (induct p rule: AxP5.induct) (unfold Euclidean_def psemantics.simps, blast)

lemma Euclidean_restrict: ‹Euclidean M ⟹ Euclidean (M[r!])›
  unfolding Euclidean_def by auto

lemma strong_soundness⇩P⇩K⇩5: ‹G ⊢⇩!⇩K⇩5 p ⟹ Euclidean; G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of AxP5 Euclidean ‹λ_. True› G p]
    soundness_AxP5 Euclidean_restrict by fast

lemma Ax5_AxP5: ‹Ax5 = AxP5 o lift›
proof
  fix p :: ‹'i fm›
  show ‹Ax5 p = (AxP5 ∘ lift) p›
    unfolding comp_apply using lower_lift
    by (smt (verit, best) Ax5.simps AxP5.simps lift.simps(1, 5-6) lower.simps(5-6))
qed

abbreviation validPK5 (‹_ ⊫⇩!⇩K⇩5 _› [50, 50] 50) where
  ‹G ⊫⇩!⇩K⇩5 p ≡ Euclidean; G ⊫⇩! p›

lemma strong_completeness⇩P⇩K⇩5:
  assumes ‹G ⊫⇩!⇩K⇩5 p›
  shows ‹G ⊢⇩!⇩K⇩5 p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩K⇩5 unfolding Ax5_AxP5 .

theorem main⇩P⇩K⇩5: ‹G ⊫⇩!⇩K⇩5 p ⟷ G ⊢⇩!⇩K⇩5 p›
  using strong_soundness⇩P⇩K⇩5[of G p] strong_completeness⇩P⇩K⇩5[of G p] by fast

corollary ‹G ⊫⇩!⇩K⇩5 p ⟹ Euclidean; G ⊫⇩!⋆ p›
  using strong_soundness⇩P⇩K⇩5[of G p] strong_completeness⇩P⇩K⇩5[of G p] by fast

section ‹System PAL + S4›

abbreviation SystemPS4 (‹_ ⊢⇩!⇩S⇩4 _› [50, 50] 50) where
  ‹G ⊢⇩!⇩S⇩4 p ≡ AxPT ⊕ AxP4; (λ_. True); G ⊢⇩! p›

lemma soundness_AxPT4: ‹(AxPT ⊕ AxP4) p ⟹ refltrans M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  using soundness_AxPT soundness_AxP4 by fast

lemma refltrans_restrict: ‹refltrans M ⟹ refltrans (M[r!])›
  using reflexive_restrict transitive_restrict by blast

lemma strong_soundness⇩P⇩S⇩4: ‹G ⊢⇩!⇩S⇩4 p ⟹ refltrans; G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of ‹AxPT ⊕ AxP4› refltrans ‹λ_. True› G p]
    soundness_AxPT4 refltrans_restrict by fast

lemma AxT4_AxPT4: ‹(AxT ⊕ Ax4) = (AxPT ⊕ AxP4) o lift›
  using AxT_AxPT Ax4_AxP4 unfolding comp_apply by metis

abbreviation validPS4 (‹_ ⊫⇩!⇩S⇩4 _› [50, 50] 50) where
  ‹G ⊫⇩!⇩S⇩4 p ≡ refltrans; G ⊫⇩! p›

theorem strong_completeness⇩P⇩S⇩4:
  assumes ‹G ⊫⇩!⇩S⇩4 p›
  shows ‹G ⊢⇩!⇩S⇩4 p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩S⇩4 unfolding AxT4_AxPT4 .

theorem main⇩P⇩S⇩4: ‹G ⊫⇩!⇩S⇩4 p ⟷ G ⊢⇩!⇩S⇩4 p›
  using strong_soundness⇩P⇩S⇩4[of G p] strong_completeness⇩P⇩S⇩4[of G p] by fast

corollary ‹G ⊫⇩!⇩S⇩4 p ⟹ refltrans; G ⊫⇩!⋆ p›
  using strong_soundness⇩P⇩S⇩4[of G p] strong_completeness⇩P⇩S⇩4[of G p] by fast

section ‹System PAL + S5›

abbreviation SystemPS5 (‹_ ⊢⇩!⇩S⇩5 _› [50, 50] 50) where
  ‹G ⊢⇩!⇩S⇩5 p ≡ AxPT ⊕ AxPB ⊕ AxP4; (λ_. True); G ⊢⇩! p›

abbreviation AxPTB4 :: ‹'i pfm ⇒ bool› where
  ‹AxPTB4 ≡ AxPT ⊕ AxPB ⊕ AxP4›

lemma soundness_AxPTB4: ‹AxPTB4 p ⟹ equivalence M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  using soundness_AxPT soundness_AxPB soundness_AxP4 by fast

lemma equivalence_restrict: ‹equivalence M ⟹ equivalence (M[r!])›
  using reflexive_restrict symmetric_restrict transitive_restrict by blast

lemma strong_soundness⇩P⇩S⇩5: ‹G ⊢⇩!⇩S⇩5 p ⟹ equivalence; G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of AxPTB4 equivalence ‹λ_. True› G p]
    soundness_AxPTB4 equivalence_restrict by fast

lemma AxTB4_AxPTB4: ‹AxTB4 = AxPTB4 o lift›
  using AxT_AxPT AxB_AxPB Ax4_AxP4 unfolding comp_apply by metis

abbreviation validPS5 (‹_ ⊫⇩!⇩S⇩5 _› [50, 50] 50) where
  ‹G ⊫⇩!⇩S⇩5 p ≡ equivalence; G ⊫⇩! p›

theorem strong_completeness⇩P⇩S⇩5:
  assumes ‹G ⊫⇩!⇩S⇩5 p›
  shows ‹G ⊢⇩!⇩S⇩5 p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩S⇩5 unfolding AxTB4_AxPTB4 .

theorem main⇩P⇩S⇩5: ‹G ⊫⇩!⇩S⇩5 p ⟷ G ⊢⇩!⇩S⇩5 p›
  using strong_soundness⇩P⇩S⇩5[of G p] strong_completeness⇩P⇩S⇩5[of G p] by fast

corollary ‹G ⊫⇩!⇩S⇩5 p ⟹ equivalence; G ⊫⇩!⋆ p›
  using strong_soundness⇩P⇩S⇩5[of G p] strong_completeness⇩P⇩S⇩5[of G p] by fast

section ‹System PAL + S5'›

abbreviation SystemPS5' (‹_ ⊢⇩!⇩S⇩5'' _› [50, 50] 50) where
  ‹G ⊢⇩!⇩S⇩5' p ≡ AxPT ⊕ AxP5; (λ_. True); G ⊢⇩! p›

abbreviation AxPT5 :: ‹'i pfm ⇒ bool› where
  ‹AxPT5 ≡ AxPT ⊕ AxP5›

lemma soundness_AxPT5: ‹AxPT5 p ⟹ equivalence M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨⇩! p›
  using soundness_AxPT soundness_AxPT soundness_AxP5 symm_trans_Euclid by fast

lemma strong_soundness⇩P⇩S⇩5': ‹G ⊢⇩!⇩S⇩5' p ⟹ equivalence; G ⊫⇩!⋆ p›
  using strong_soundness⇩P[of AxPT5 equivalence ‹λ_. True› G p]
    soundness_AxPT5 equivalence_restrict by fast

lemma AxT5_AxPT5: ‹AxT5 = AxPT5 o lift›
  using AxT_AxPT Ax5_AxP5 unfolding comp_apply by metis

theorem strong_completeness⇩P⇩S⇩5':
  assumes ‹G ⊫⇩!⇩S⇩5 p›
  shows ‹G ⊢⇩!⇩S⇩5' p›
  using strong_completeness⇩P⇩B assms strong_completeness⇩S⇩5' unfolding AxT5_AxPT5 .

theorem main⇩P⇩S⇩5': ‹G ⊫⇩!⇩S⇩5 p ⟷ G ⊢⇩!⇩S⇩5' p›
  using strong_soundness⇩P⇩S⇩5'[of G p] strong_completeness⇩P⇩S⇩5'[of G p] by fast

end