Theory PAL

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

  This work is a formalization of public announcement logic with countably many agents.
  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 :: countable, '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] completenessA 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 soundnessP:
  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 soundnessP[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_implyP:
  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 soundnessP[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_soundnessP:
  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_implyP[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_completenessP':
  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_completenessP:
  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_completenessP' assms .

theorem mainP:
  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_soundnessP[of A P B G p] strong_completenessP[of P G p B A] assms by blast

corollary strong_completenessPB:
  assumes P; G ! p
    and G p. P; G ⊫⋆ p  A o lift; G  p
  shows A; (λ_. True); G ! p
  using strong_completenessP[where B=λ_. True] assms by blast

corollary completenessP':
  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_completenessP'[where P=P and G={}] by simp

corollary completenessP:
  assumes P; {} ! p
    and r  anns p. B r
    and p. P; {}  p  A o lift  p
  shows A; B ! p
  using completenessP' assms .

corollary completenessPA:
  assumes (λ_. True); {} ! p
  shows A; (λ_. True) ! p
  using assms completenessP[of λ_. True p λ_. True] completenessA by blast

section System PAL + K

abbreviation SystemPK (_ !K _ [50, 50] 50) where
  G !K p  (λ_. False); (λ_. True); G ! p

lemma strong_soundnessPK: G !K p  (λ_. True); G ! p
  using strong_soundnessP[of λ_. False λ_. True] by fast

abbreviation validPK (_ !K _ [50, 50] 50) where
  G !K p  (λ_. True); G ! p

lemma strong_completenessPK:
  assumes G !K p
  shows G !K p
  using strong_completenessPB assms strong_completenessK unfolding comp_apply .

theorem mainPK: G !K p  G !K p
  using strong_soundnessPK[of G p] strong_completenessPK[of G p] by fast

corollary G !K p  (λ_. True); G ! p
  using strong_soundnessPK[of G p] strong_completenessPK[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_soundnessPT: G !T p  reflexive; G ! p
  using strong_soundnessP[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_completenessPT:
  assumes G !T p
  shows G !T p
  using strong_completenessPB assms strong_completenessT unfolding AxT_AxPT .

theorem mainPT: G !T p  G !T p
  using strong_soundnessPT[of G p] strong_completenessPT[of G p] by fast

corollary G !T p  reflexive; G ! p
  using strong_soundnessPT[of G p] strong_completenessPT[of G p] by fast

section System PAL + KB

inductive AxPB :: 'i pfm  bool where
  AxPB (p ! K! i (L! i p))

abbreviation SystemPKB (_ !KB _ [50, 50] 50) where
  G !KB 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_soundnessPKB: G !KB p  symmetric; G ! p
  using strong_soundnessP[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 (_ !KB _ [50, 50] 50) where
  G !KB p  symmetric; G ! p

lemma strong_completenessPKB:
  assumes G !KB p
  shows G !KB p
  using strong_completenessPB assms strong_completenessKB unfolding AxB_AxPB .

theorem mainPKB: G !KB p  G !KB p
  using strong_soundnessPKB[of G p] strong_completenessPKB[of G p] by fast

corollary G !KB p  symmetric; G ! p
  using strong_soundnessPKB[of G p] strong_completenessPKB[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 (_ !K4 _ [50, 50] 50) where
  G !K4 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_soundnessPK4: G !K4 p  transitive; G ! p
  using strong_soundnessP[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 (_ !K4 _ [50, 50] 50) where
  G !K4 p  transitive; G ! p

lemma strong_completenessPK4:
  assumes G !K4 p
  shows G !K4 p
  using strong_completenessPB assms strong_completenessK4 unfolding Ax4_AxP4 .

theorem mainPK4: G !K4 p  G !K4 p
  using strong_soundnessPK4[of G p] strong_completenessPK4[of G p] by fast

corollary G !K4 p  transitive; G ! p
  using strong_soundnessPK4[of G p] strong_completenessPK4[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 (_ !K5 _ [50, 50] 50) where
  G !K5 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_soundnessPK5: G !K5 p  Euclidean; G ! p
  using strong_soundnessP[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 (_ !K5 _ [50, 50] 50) where
  G !K5 p  Euclidean; G ! p

lemma strong_completenessPK5:
  assumes G !K5 p
  shows G !K5 p
  using strong_completenessPB assms strong_completenessK5 unfolding Ax5_AxP5 .

theorem mainPK5: G !K5 p  G !K5 p
  using strong_soundnessPK5[of G p] strong_completenessPK5[of G p] by fast

corollary G !K5 p  Euclidean; G ! p
  using strong_soundnessPK5[of G p] strong_completenessPK5[of G p] by fast

section System PAL + S4

abbreviation SystemPS4 (_ !S4 _ [50, 50] 50) where
  G !S4 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_soundnessPS4: G !S4 p  refltrans; G ! p
  using strong_soundnessP[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 (_ !S4 _ [50, 50] 50) where
  G !S4 p  refltrans; G ! p

theorem strong_completenessPS4:
  assumes G !S4 p
  shows G !S4 p
  using strong_completenessPB assms strong_completenessS4 unfolding AxT4_AxPT4 .

theorem mainPS4: G !S4 p  G !S4 p
  using strong_soundnessPS4[of G p] strong_completenessPS4[of G p] by fast

corollary G !S4 p  refltrans; G ! p
  using strong_soundnessPS4[of G p] strong_completenessPS4[of G p] by fast

section System PAL + S5

abbreviation SystemPS5 (_ !S5 _ [50, 50] 50) where
  G !S5 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_soundnessPS5: G !S5 p  equivalence; G ! p
  using strong_soundnessP[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 (_ !S5 _ [50, 50] 50) where
  G !S5 p  equivalence; G ! p

theorem strong_completenessPS5:
  assumes G !S5 p
  shows G !S5 p
  using strong_completenessPB assms strong_completenessS5 unfolding AxTB4_AxPTB4 .

theorem mainPS5: G !S5 p  G !S5 p
  using strong_soundnessPS5[of G p] strong_completenessPS5[of G p] by fast

corollary G !S5 p  equivalence; G ! p
  using strong_soundnessPS5[of G p] strong_completenessPS5[of G p] by fast

section System PAL + S5'

abbreviation SystemPS5' (_ !S5'' _ [50, 50] 50) where
  G !S5' 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_soundnessPS5': G !S5' p  equivalence; G ! p
  using strong_soundnessP[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_completenessPS5':
  assumes G !S5 p
  shows G !S5' p
  using strong_completenessPB assms strong_completenessS5' unfolding AxT5_AxPT5 .

theorem mainPS5': G !S5 p  G !S5' p
  using strong_soundnessPS5'[of G p] strong_completenessPS5'[of G p] by fast

end