diff --git a/thys/Epistemic_Logic/Epistemic_Logic.thy b/thys/Epistemic_Logic/Epistemic_Logic.thy
--- a/thys/Epistemic_Logic/Epistemic_Logic.thy
+++ b/thys/Epistemic_Logic/Epistemic_Logic.thy
@@ -1,1268 +1,1395 @@
 (*
   File:      Epistemic_Logic.thy
   Author:    Asta Halkjær From
 
   This work is a formalization of epistemic logic with countably many agents.
   It includes proofs of soundness and completeness for the axiom system K.
   The completeness proof is based on the textbook "Reasoning About Knowledge"
   by Fagin, Halpern, Moses and Vardi (MIT Press 1995).
   The extensions of system K (T, KB, K4, S4, S5) and their completeness proofs
   are based on the textbook "Modal Logic" by Blackburn, de Rijke and Venema
-  (Cambridge University Press 2001).
+  (Cambridge University Press 5001).
 *)
 
 theory Epistemic_Logic imports "HOL-Library.Countable" begin
 
 section \<open>Syntax\<close>
 
 type_synonym id = string
 
 datatype 'i fm
   = FF (\<open>\<^bold>\<bottom>\<close>)
   | Pro id
-  | Dis \<open>'i fm\<close> \<open>'i fm\<close> (infixr \<open>\<^bold>\<or>\<close> 30)
-  | Con \<open>'i fm\<close> \<open>'i fm\<close> (infixr \<open>\<^bold>\<and>\<close> 35)
-  | Imp \<open>'i fm\<close> \<open>'i fm\<close> (infixr \<open>\<^bold>\<longrightarrow>\<close> 25)
+  | Dis \<open>'i fm\<close> \<open>'i fm\<close> (infixr \<open>\<^bold>\<or>\<close> 60)
+  | Con \<open>'i fm\<close> \<open>'i fm\<close> (infixr \<open>\<^bold>\<and>\<close> 65)
+  | Imp \<open>'i fm\<close> \<open>'i fm\<close> (infixr \<open>\<^bold>\<longrightarrow>\<close> 55)
   | K 'i \<open>'i fm\<close>
 
 abbreviation TT (\<open>\<^bold>\<top>\<close>) where
   \<open>TT \<equiv> \<^bold>\<bottom> \<^bold>\<longrightarrow> \<^bold>\<bottom>\<close>
 
-abbreviation Neg (\<open>\<^bold>\<not> _\<close> [40] 40) where
+abbreviation Neg (\<open>\<^bold>\<not> _\<close> [70] 70) where
   \<open>Neg p \<equiv> p \<^bold>\<longrightarrow> \<^bold>\<bottom>\<close>
 
 abbreviation \<open>L i p \<equiv> \<^bold>\<not> K i (\<^bold>\<not> p)\<close>
 
 section \<open>Semantics\<close>
 
 datatype ('i, 'w) kripke =
   Kripke (\<W>: \<open>'w set\<close>) (\<pi>: \<open>'w \<Rightarrow> id \<Rightarrow> bool\<close>) (\<K>: \<open>'i \<Rightarrow> 'w \<Rightarrow> 'w set\<close>)
 
 primrec semantics :: \<open>('i, 'w) kripke \<Rightarrow> 'w \<Rightarrow> 'i fm \<Rightarrow> bool\<close> (\<open>_, _ \<Turnstile> _\<close> [50, 50] 50) where
   \<open>(M, w \<Turnstile> \<^bold>\<bottom>) = False\<close>
 | \<open>(M, w \<Turnstile> Pro x) = \<pi> M w x\<close>
-| \<open>(M, w \<Turnstile> (p \<^bold>\<or> q)) = ((M, w \<Turnstile> p) \<or> (M, w \<Turnstile> q))\<close>
-| \<open>(M, w \<Turnstile> (p \<^bold>\<and> q)) = ((M, w \<Turnstile> p) \<and> (M, w \<Turnstile> q))\<close>
-| \<open>(M, w \<Turnstile> (p \<^bold>\<longrightarrow> q)) = ((M, w \<Turnstile> p) \<longrightarrow> (M, w \<Turnstile> q))\<close>
+| \<open>(M, w \<Turnstile> p \<^bold>\<or> q) = ((M, w \<Turnstile> p) \<or> (M, w \<Turnstile> q))\<close>
+| \<open>(M, w \<Turnstile> p \<^bold>\<and> q) = ((M, w \<Turnstile> p) \<and> (M, w \<Turnstile> q))\<close>
+| \<open>(M, w \<Turnstile> p \<^bold>\<longrightarrow> q) = ((M, w \<Turnstile> p) \<longrightarrow> (M, w \<Turnstile> q))\<close>
 | \<open>(M, w \<Turnstile> K i p) = (\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> p)\<close>
 
 section \<open>S5 Axioms\<close>
 
 definition reflexive :: \<open>('i, 'w) kripke \<Rightarrow> bool\<close> where
   \<open>reflexive M \<equiv> \<forall>i. \<forall>w \<in> \<W> M. w \<in> \<K> M i w\<close>
 
 definition symmetric :: \<open>('i, 'w) kripke \<Rightarrow> bool\<close> where
   \<open>symmetric M \<equiv> \<forall>i. \<forall>v \<in> \<W> M. \<forall>w \<in> \<W> M. v \<in> \<K> M i w \<longleftrightarrow> w \<in> \<K> M i v\<close>
 
 definition transitive :: \<open>('i, 'w) kripke \<Rightarrow> bool\<close> where
   \<open>transitive M \<equiv> \<forall>i. \<forall>u \<in> \<W> M. \<forall>v \<in> \<W> M. \<forall>w \<in> \<W> M.
     w \<in> \<K> M i v \<and> u \<in> \<K> M i w \<longrightarrow> u \<in> \<K> M i v\<close>
 
 abbreviation refltrans :: \<open>('i, 'w) kripke \<Rightarrow> bool\<close> where
   \<open>refltrans M \<equiv> reflexive M \<and> transitive M\<close>
 
 abbreviation equivalence :: \<open>('i, 'w) kripke \<Rightarrow> bool\<close> where
   \<open>equivalence M \<equiv> reflexive M \<and> symmetric M \<and> transitive M\<close>
 
-lemma Imp_intro [intro]: \<open>(M, w \<Turnstile> p \<Longrightarrow> M, w \<Turnstile> q) \<Longrightarrow> M, w \<Turnstile> (p \<^bold>\<longrightarrow> q)\<close>
+definition Euclidean :: \<open>('i, 'w) kripke \<Rightarrow> bool\<close> where
+  \<open>Euclidean M \<equiv> \<forall>i. \<forall>u \<in> \<W> M. \<forall>v \<in> \<W> M. \<forall>w \<in> \<W> M.
+    v \<in> \<K> M i u \<longrightarrow> w \<in> \<K> M i u \<longrightarrow> w \<in> \<K> M i v\<close>
+
+lemma Imp_intro [intro]: \<open>(M, w \<Turnstile> p \<Longrightarrow> M, w \<Turnstile> q) \<Longrightarrow> M, w \<Turnstile> p \<^bold>\<longrightarrow> q\<close>
   by simp
 
-theorem distribution: \<open>M, w \<Turnstile> (K i p \<^bold>\<and> K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i q)\<close>
+theorem distribution: \<open>M, w \<Turnstile> K i p \<^bold>\<and> K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i q\<close>
 proof
-  assume \<open>M, w \<Turnstile> (K i p \<^bold>\<and> K i (p \<^bold>\<longrightarrow> q))\<close>
+  assume \<open>M, w \<Turnstile> K i p \<^bold>\<and> K i (p \<^bold>\<longrightarrow> q)\<close>
   then have \<open>M, w \<Turnstile> K i p\<close> \<open>M, w \<Turnstile> K i (p \<^bold>\<longrightarrow> q)\<close>
     by simp_all
-  then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> p\<close> \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> (p \<^bold>\<longrightarrow> q)\<close>
+  then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> p\<close> \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> p \<^bold>\<longrightarrow> q\<close>
     by simp_all
   then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> q\<close>
     by simp
   then show \<open>M, w \<Turnstile> K i q\<close>
     by simp
 qed
 
 theorem generalization:
   assumes valid: \<open>\<forall>(M :: ('i, 'w) kripke) w. M, w \<Turnstile> p\<close>
   shows \<open>(M :: ('i, 'w) kripke), w \<Turnstile> K i p\<close>
 proof -
   have \<open>\<forall>w' \<in> \<K> M i w. M, w' \<Turnstile> p\<close>
     using valid by blast
   then show \<open>M, w \<Turnstile> K i p\<close>
     by simp
 qed
 
 theorem truth:
   assumes \<open>reflexive M\<close> \<open>w \<in> \<W> M\<close>
-  shows \<open>M, w \<Turnstile> (K i p \<^bold>\<longrightarrow> p)\<close>
+  shows \<open>M, w \<Turnstile> K i p \<^bold>\<longrightarrow> p\<close>
 proof
   assume \<open>M, w \<Turnstile> K i p\<close>
   then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> p\<close>
     by simp
   moreover have \<open>w \<in> \<K> M i w\<close>
     using \<open>reflexive M\<close> \<open>w \<in> \<W> M\<close> unfolding reflexive_def by blast
   ultimately show \<open>M, w \<Turnstile> p\<close>
     using \<open>w \<in> \<W> M\<close> by simp
 qed
 
 theorem pos_introspection:
   assumes \<open>transitive M\<close> \<open>w \<in> \<W> M\<close>
-  shows \<open>M, w \<Turnstile> (K i p \<^bold>\<longrightarrow> K i (K i p))\<close>
+  shows \<open>M, w \<Turnstile> K i p \<^bold>\<longrightarrow> K i (K i p)\<close>
 proof
   assume \<open>M, w \<Turnstile> K i p\<close>
   then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> p\<close>
     by simp
   then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. \<forall>u \<in> \<W> M \<inter> \<K> M i v. M, u \<Turnstile> p\<close>
     using \<open>transitive M\<close> \<open>w \<in> \<W> M\<close> unfolding transitive_def by blast
   then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> K i p\<close>
     by simp
   then show \<open>M, w \<Turnstile> K i (K i p)\<close>
     by simp
 qed
 
 theorem neg_introspection:
   assumes \<open>symmetric M\<close> \<open>transitive M\<close> \<open>w \<in> \<W> M\<close>
-  shows \<open>M, w \<Turnstile> (\<^bold>\<not> K i p \<^bold>\<longrightarrow> K i (\<^bold>\<not> K i p))\<close>
+  shows \<open>M, w \<Turnstile> \<^bold>\<not> K i p \<^bold>\<longrightarrow> K i (\<^bold>\<not> K i p)\<close>
 proof
   assume \<open>M, w \<Turnstile> \<^bold>\<not> (K i p)\<close>
   then obtain u where \<open>u \<in> \<K> M i w\<close> \<open>\<not> (M, u \<Turnstile> p)\<close> \<open>u \<in> \<W> M\<close>
     by auto
   moreover have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. u \<in> \<W> M \<inter> \<K> M i v\<close>
     using \<open>u \<in> \<K> M i w\<close> \<open>symmetric M\<close> \<open>transitive M\<close> \<open>u \<in> \<W> M\<close> \<open>w \<in> \<W> M\<close>
     unfolding symmetric_def transitive_def by blast
   ultimately have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile> \<^bold>\<not> K i p\<close>
     by auto
   then show \<open>M, w \<Turnstile> K i (\<^bold>\<not> K i p)\<close>
     by simp
 qed
 
 section \<open>Normal Modal Logic\<close>
 
 primrec eval :: \<open>(id \<Rightarrow> bool) \<Rightarrow> ('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm \<Rightarrow> bool\<close> where
   \<open>eval _ _ \<^bold>\<bottom> = False\<close>
 | \<open>eval g _ (Pro x) = g x\<close>
 | \<open>eval g h (p \<^bold>\<or> q) = (eval g h p \<or> eval g h q)\<close>
 | \<open>eval g h (p \<^bold>\<and> q) = (eval g h p \<and> eval g h q)\<close>
 | \<open>eval g h (p \<^bold>\<longrightarrow> q) = (eval g h p \<longrightarrow> eval g h q)\<close>
 | \<open>eval _ h (K i p) = h (K i p)\<close>
 
 abbreviation \<open>tautology p \<equiv> \<forall>g h. eval g h p\<close>
 
-inductive AK :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm \<Rightarrow> bool\<close> (\<open>_ \<turnstile> _\<close> [20, 20] 20)
+inductive AK :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm \<Rightarrow> bool\<close> (\<open>_ \<turnstile> _\<close> [50, 50] 50)
   for A :: \<open>'i fm \<Rightarrow> bool\<close> where
     A1: \<open>tautology p \<Longrightarrow> A \<turnstile> p\<close>
   | A2: \<open>A \<turnstile> K i p \<^bold>\<and> K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i q\<close>
   | Ax: \<open>A p \<Longrightarrow> A \<turnstile> p\<close>
   | R1: \<open>A \<turnstile> p \<Longrightarrow> A \<turnstile> p \<^bold>\<longrightarrow> q \<Longrightarrow> A \<turnstile> q\<close>
   | R2: \<open>A \<turnstile> p \<Longrightarrow> A \<turnstile> K i p\<close>
 
-primrec imply :: \<open>'i fm list \<Rightarrow> 'i fm \<Rightarrow> 'i fm\<close> (infixr \<open>\<^bold>\<leadsto>\<close> 26) where
+primrec imply :: \<open>'i fm list \<Rightarrow> 'i fm \<Rightarrow> 'i fm\<close> (infixr \<open>\<^bold>\<leadsto>\<close> 56) where
   \<open>([] \<^bold>\<leadsto> q) = q\<close>
 | \<open>(p # ps \<^bold>\<leadsto> q) = (p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q)\<close>
 
-abbreviation AK_assms (\<open>_, _ \<turnstile> _\<close> [20, 20, 20] 20) where
-  \<open>A, G \<turnstile> p \<equiv> \<exists>qs. set qs \<subseteq> G \<and> (A \<turnstile> qs \<^bold>\<leadsto> p)\<close>
+abbreviation AK_assms (\<open>_; _ \<turnstile> _\<close> [50, 50, 50] 50) where
+  \<open>A; G \<turnstile> p \<equiv> \<exists>qs. set qs \<subseteq> G \<and> (A \<turnstile> qs \<^bold>\<leadsto> p)\<close>
 
 section \<open>Soundness\<close>
 
 lemma eval_semantics: \<open>eval (pi w) (\<lambda>q. Kripke W pi r, w \<Turnstile> q) p = (Kripke W pi r, w \<Turnstile> p)\<close>
   by (induct p) simp_all
 
 lemma tautology:
   assumes \<open>tautology p\<close>
   shows \<open>M, w \<Turnstile> p\<close>
 proof -
   from assms have \<open>eval (g w) (\<lambda>q. Kripke W g r, w \<Turnstile> q) p\<close> for W g r
     by simp
   then have \<open>Kripke W g r, w \<Turnstile> p\<close> for W g r
     using eval_semantics by fast
   then show \<open>M, w \<Turnstile> p\<close>
     by (metis kripke.collapse)
 qed
 
 theorem soundness:
   assumes \<open>\<And>M w p. A p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   shows \<open>A \<turnstile> p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   by (induct p arbitrary: w rule: AK.induct) (auto simp: assms tautology)
 
 section \<open>Derived rules\<close>
 
 lemma K_A2': \<open>A \<turnstile> K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i p \<^bold>\<longrightarrow> K i q\<close>
 proof -
   have \<open>A \<turnstile> K i p \<^bold>\<and> K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i q\<close>
     using A2 by fast
   moreover have \<open>A \<turnstile> (P \<^bold>\<and> Q \<^bold>\<longrightarrow> R) \<^bold>\<longrightarrow> (Q \<^bold>\<longrightarrow> P \<^bold>\<longrightarrow> R)\<close> for P Q R
     by (simp add: A1)
   ultimately show ?thesis
     using R1 by fast
 qed
 
 lemma K_map:
   assumes \<open>A \<turnstile> p \<^bold>\<longrightarrow> q\<close>
   shows \<open>A \<turnstile> K i p \<^bold>\<longrightarrow> K i q\<close>
 proof -
   note \<open>A \<turnstile> p \<^bold>\<longrightarrow> q\<close>
   then have \<open>A \<turnstile> K i (p \<^bold>\<longrightarrow> q)\<close>
     using R2 by fast
   moreover have \<open>A \<turnstile> K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i p \<^bold>\<longrightarrow> K i q\<close>
     using K_A2' by fast
   ultimately show ?thesis
     using R1 by fast
 qed
 
 lemma K_LK: \<open>A \<turnstile> (L i (\<^bold>\<not> p) \<^bold>\<longrightarrow> \<^bold>\<not> K i p)\<close>
 proof -
   have \<open>A \<turnstile> (p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p)\<close>
     by (simp add: A1)
   moreover have \<open>A \<turnstile> ((P \<^bold>\<longrightarrow> Q) \<^bold>\<longrightarrow> (\<^bold>\<not> Q \<^bold>\<longrightarrow> \<^bold>\<not> P))\<close> for P Q
     using A1 by force
   ultimately show ?thesis
     using K_map R1 by fast
 qed
 
 lemma K_imply_head: \<open>A \<turnstile> (p # ps \<^bold>\<leadsto> p)\<close>
 proof -
   have \<open>tautology (p # ps \<^bold>\<leadsto> p)\<close>
     by (induct ps) simp_all
   then show ?thesis
     using A1 by blast
 qed
 
 lemma K_imply_Cons:
   assumes \<open>A \<turnstile> ps \<^bold>\<leadsto> q\<close>
   shows \<open>A \<turnstile> p # ps \<^bold>\<leadsto> q\<close>
 proof -
   have \<open>A \<turnstile> (ps \<^bold>\<leadsto> q \<^bold>\<longrightarrow> p # ps \<^bold>\<leadsto> q)\<close>
     by (simp add: A1)
   with R1 assms show ?thesis .
 qed
 
 lemma K_right_mp:
   assumes \<open>A \<turnstile> ps \<^bold>\<leadsto> p\<close> \<open>A \<turnstile> ps \<^bold>\<leadsto> (p \<^bold>\<longrightarrow> q)\<close>
   shows \<open>A \<turnstile> ps \<^bold>\<leadsto> q\<close>
 proof -
   have \<open>tautology (ps \<^bold>\<leadsto> p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q)\<close>
     by (induct ps) simp_all
   with A1 have \<open>A \<turnstile> ps \<^bold>\<leadsto> p \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> ps \<^bold>\<leadsto> q\<close> .
   then show ?thesis
     using assms R1 by blast
 qed
 
 lemma tautology_imply_superset:
   assumes \<open>set ps \<subseteq> set qs\<close>
   shows \<open>tautology (ps \<^bold>\<leadsto> r \<^bold>\<longrightarrow> qs \<^bold>\<leadsto> r)\<close>
 proof (rule ccontr)
   assume \<open>\<not> tautology (ps \<^bold>\<leadsto> r \<^bold>\<longrightarrow> qs \<^bold>\<leadsto> r)\<close>
   then obtain g h where \<open>\<not> eval g h (ps \<^bold>\<leadsto> r \<^bold>\<longrightarrow> qs \<^bold>\<leadsto> r)\<close>
     by blast
   then have \<open>eval g h (ps \<^bold>\<leadsto> r)\<close> \<open>\<not> eval g h (qs \<^bold>\<leadsto> r)\<close>
     by simp_all
   then consider (np) \<open>\<exists>p \<in> set ps. \<not> eval g h p\<close> | (r) \<open>\<forall>p \<in> set ps. eval g h p\<close> \<open>eval g h r\<close>
     by (induct ps) auto
   then show False
   proof cases
     case np
     then have \<open>\<exists>p \<in> set qs. \<not> eval g h p\<close>
       using \<open>set ps \<subseteq> set qs\<close> by blast
     then have \<open>eval g h (qs \<^bold>\<leadsto> r)\<close>
       by (induct qs) simp_all
     then show ?thesis
       using \<open>\<not> eval g h (qs \<^bold>\<leadsto> r)\<close> by blast
   next
     case r
     then have \<open>eval g h (qs \<^bold>\<leadsto> r)\<close>
       by (induct qs) simp_all
     then show ?thesis
       using \<open>\<not> eval g h (qs \<^bold>\<leadsto> r)\<close> by blast
   qed
 qed
 
 lemma K_imply_weaken:
   assumes \<open>A \<turnstile> ps \<^bold>\<leadsto> q\<close> \<open>set ps \<subseteq> set ps'\<close>
   shows \<open>A \<turnstile> ps' \<^bold>\<leadsto> q\<close>
 proof -
   have \<open>tautology (ps \<^bold>\<leadsto> q \<^bold>\<longrightarrow> ps' \<^bold>\<leadsto> q)\<close>
     using \<open>set ps \<subseteq> set ps'\<close> tautology_imply_superset by blast
-  then have \<open>A \<turnstile> (ps \<^bold>\<leadsto> q \<^bold>\<longrightarrow> ps' \<^bold>\<leadsto> q)\<close>
+  then have \<open>A \<turnstile> ps \<^bold>\<leadsto> q \<^bold>\<longrightarrow> ps' \<^bold>\<leadsto> q\<close>
     using A1 by blast
   then show ?thesis
     using \<open>A \<turnstile> ps \<^bold>\<leadsto> q\<close> R1 by blast
 qed
 
 lemma imply_append: \<open>(ps @ ps' \<^bold>\<leadsto> q) = (ps \<^bold>\<leadsto> ps' \<^bold>\<leadsto> q)\<close>
   by (induct ps) simp_all
 
 lemma K_ImpI:
   assumes \<open>A \<turnstile> p # G \<^bold>\<leadsto> q\<close>
   shows \<open>A \<turnstile> G \<^bold>\<leadsto> (p \<^bold>\<longrightarrow> q)\<close>
 proof -
   have \<open>set (p # G) \<subseteq> set (G @ [p])\<close>
     by simp
   then have \<open>A \<turnstile> G @ [p] \<^bold>\<leadsto> q\<close>
     using assms K_imply_weaken by blast
   then have \<open>A \<turnstile> G \<^bold>\<leadsto> [p] \<^bold>\<leadsto> q\<close>
     using imply_append by metis
   then show ?thesis
     by simp
 qed
 
 lemma K_Boole:
   assumes \<open>A \<turnstile> (\<^bold>\<not> p) # G \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
   shows \<open>A \<turnstile> G \<^bold>\<leadsto> p\<close>
 proof -
   have \<open>A \<turnstile> G \<^bold>\<leadsto> \<^bold>\<not> \<^bold>\<not> p\<close>
     using assms K_ImpI by blast
   moreover have \<open>tautology (G \<^bold>\<leadsto> \<^bold>\<not> \<^bold>\<not> p \<^bold>\<longrightarrow> G \<^bold>\<leadsto> p)\<close>
     by (induct G) simp_all
   then have \<open>A \<turnstile> (G \<^bold>\<leadsto> \<^bold>\<not> \<^bold>\<not> p \<^bold>\<longrightarrow> G \<^bold>\<leadsto> p)\<close>
     using A1 by blast
   ultimately show ?thesis
     using R1 by blast
 qed
 
 lemma K_DisE:
   assumes \<open>A \<turnstile> p # G \<^bold>\<leadsto> r\<close> \<open>A \<turnstile> q # G \<^bold>\<leadsto> r\<close> \<open>A \<turnstile> G \<^bold>\<leadsto> p \<^bold>\<or> q\<close>
   shows \<open>A \<turnstile> G \<^bold>\<leadsto> r\<close>
 proof -
   have \<open>tautology (p # G \<^bold>\<leadsto> r \<^bold>\<longrightarrow> q # G \<^bold>\<leadsto> r \<^bold>\<longrightarrow> G \<^bold>\<leadsto> p \<^bold>\<or> q \<^bold>\<longrightarrow> G \<^bold>\<leadsto> r)\<close>
     by (induct G) auto
   then have \<open>A \<turnstile> p # G \<^bold>\<leadsto> r \<^bold>\<longrightarrow> q # G \<^bold>\<leadsto> r \<^bold>\<longrightarrow> G \<^bold>\<leadsto> p \<^bold>\<or> q \<^bold>\<longrightarrow> G \<^bold>\<leadsto> r\<close>
     using A1 by blast
   then show ?thesis
     using assms R1 by blast
 qed
 
 lemma K_mp: \<open>A \<turnstile> p # (p \<^bold>\<longrightarrow> q) # G \<^bold>\<leadsto> q\<close>
   by (meson K_imply_head K_imply_weaken K_right_mp set_subset_Cons)
 
 lemma K_swap:
   assumes \<open>A \<turnstile> p # q # G \<^bold>\<leadsto> r\<close>
   shows \<open>A \<turnstile> q # p # G \<^bold>\<leadsto> r\<close>
   using assms K_ImpI by (metis imply.simps(1-2))
 
 lemma K_DisL:
   assumes \<open>A \<turnstile> p # ps \<^bold>\<leadsto> q\<close> \<open>A \<turnstile> p' # ps \<^bold>\<leadsto> q\<close>
   shows \<open>A \<turnstile> (p \<^bold>\<or> p') # ps \<^bold>\<leadsto> q\<close>
 proof -
   have \<open>A \<turnstile> p # (p \<^bold>\<or> p') # ps \<^bold>\<leadsto> q\<close> \<open>A \<turnstile> p' # (p \<^bold>\<or> p') # ps \<^bold>\<leadsto> q\<close>
     using assms K_swap K_imply_Cons by blast+
   moreover have \<open>A \<turnstile> (p \<^bold>\<or> p') # ps \<^bold>\<leadsto> p \<^bold>\<or> p'\<close>
     using K_imply_head by blast
   ultimately show ?thesis
     using K_DisE by blast
 qed
 
 lemma K_distrib_K_imp:
   assumes \<open>A \<turnstile> K i (G \<^bold>\<leadsto> q)\<close>
   shows \<open>A \<turnstile> map (K i) G \<^bold>\<leadsto> K i q\<close>
 proof -
   have \<open>A \<turnstile> (K i (G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> map (K i) G \<^bold>\<leadsto> K i q)\<close>
   proof (induct G)
     case Nil
     then show ?case
       by (simp add: A1)
   next
     case (Cons a G)
     have \<open>A \<turnstile> K i a \<^bold>\<and> K i (a # G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> K i (G \<^bold>\<leadsto> q)\<close>
       by (simp add: A2)
     moreover have
       \<open>A \<turnstile> ((K i a \<^bold>\<and> K i (a # G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> K i (G \<^bold>\<leadsto> q)) \<^bold>\<longrightarrow>
         (K i (G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> map (K i) G \<^bold>\<leadsto> K i q) \<^bold>\<longrightarrow>
         (K i a \<^bold>\<and> K i (a # G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> map (K i) G \<^bold>\<leadsto> K i q))\<close>
       by (simp add: A1)
     ultimately have \<open>A \<turnstile> K i a \<^bold>\<and> K i (a # G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> map (K i) G \<^bold>\<leadsto> K i q\<close>
       using Cons R1 by blast
     moreover have
       \<open>A \<turnstile> ((K i a \<^bold>\<and> K i (a # G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> map (K i) G \<^bold>\<leadsto> K i q) \<^bold>\<longrightarrow>
         (K i (a # G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> K i a \<^bold>\<longrightarrow> map (K i) G \<^bold>\<leadsto> K i q))\<close>
       by (simp add: A1)
     ultimately have \<open>A \<turnstile> (K i (a # G \<^bold>\<leadsto> q) \<^bold>\<longrightarrow> K i a \<^bold>\<longrightarrow> map (K i) G \<^bold>\<leadsto> K i q)\<close>
       using R1 by blast
     then show ?case
       by simp
   qed
   then show ?thesis
     using assms R1 by blast
 qed
 
+lemma K_trans: \<open>A \<turnstile> (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> (q \<^bold>\<longrightarrow> r) \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> r\<close>
+  by (auto intro: A1)
+
+lemma K_L_dual: \<open>A \<turnstile> \<^bold>\<not> L i (\<^bold>\<not> p) \<^bold>\<longrightarrow> K i p\<close>
+proof -
+  have \<open>A \<turnstile> K i p \<^bold>\<longrightarrow> K i p\<close> \<open>A \<turnstile> \<^bold>\<not> \<^bold>\<not> p \<^bold>\<longrightarrow> p\<close>
+    by (auto intro: A1)
+  then have \<open>A \<turnstile> K i (\<^bold>\<not> \<^bold>\<not> p) \<^bold>\<longrightarrow> K i p\<close>
+    by (auto intro: K_map)
+  moreover have \<open>A \<turnstile> (P \<^bold>\<longrightarrow> Q) \<^bold>\<longrightarrow> (\<^bold>\<not> \<^bold>\<not> P \<^bold>\<longrightarrow> Q)\<close> for P Q
+    by (auto intro: A1)
+  ultimately show \<open>A \<turnstile> \<^bold>\<not> \<^bold>\<not> K i (\<^bold>\<not> \<^bold>\<not> p) \<^bold>\<longrightarrow> K i p\<close>
+    by (auto intro: R1)
+qed
+
 section \<open>Strong Soundness\<close>
 
 abbreviation validStar :: \<open>(('i, 'w) kripke \<Rightarrow> bool) \<Rightarrow> 'i fm set \<Rightarrow> 'i fm \<Rightarrow> bool\<close> (\<open>valid\<star>\<close>) where
   \<open>valid\<star> P G p \<equiv> \<forall>M. \<forall>w \<in> \<W> M. P M \<longrightarrow> (\<forall>q \<in> G. M, w \<Turnstile> q) \<longrightarrow> M, w \<Turnstile> p\<close>
 
 corollary soundness_imply:
   assumes \<open>\<And>M w p. A p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   shows \<open>A \<turnstile> ps \<^bold>\<leadsto> p \<Longrightarrow> valid\<star> P (set ps) p\<close>
 proof (induct ps arbitrary: p)
   case Nil
   then show ?case
     using soundness[of A P p] assms by simp
 next
   case (Cons a ps)
   then show ?case
     using K_ImpI by fastforce
 qed
 
 theorem strong_soundness:
   assumes \<open>\<And>M w p. A p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
-  shows \<open>A, G \<turnstile> p \<Longrightarrow> valid\<star> P G p\<close>
+  shows \<open>A; G \<turnstile> p \<Longrightarrow> valid\<star> P G p\<close>
 proof safe
   fix qs w and M :: \<open>('a, 'b) kripke\<close>
   assume \<open>A \<turnstile> qs \<^bold>\<leadsto> p\<close>
   moreover assume \<open>set qs \<subseteq> G\<close> \<open>\<forall>q \<in> G. M, w \<Turnstile> q\<close>
   then have \<open>\<forall>q \<in> set qs. M, w \<Turnstile> q\<close>
     using \<open>set qs \<subseteq> G\<close> by blast
   moreover assume \<open>P M\<close> \<open>w \<in> \<W> M\<close>
   ultimately show \<open>M, w \<Turnstile> p\<close>
     using soundness_imply[of A P qs p] assms by blast
 qed
 
 section \<open>Completeness\<close>
 
 subsection \<open>Consistent sets\<close>
 
 definition consistent :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm set \<Rightarrow> bool\<close> where
-  \<open>consistent A S \<equiv> \<nexists>S'. set S' \<subseteq> S \<and> (A \<turnstile> S' \<^bold>\<leadsto> \<^bold>\<bottom>)\<close>
+  \<open>consistent A S \<equiv> \<not> (A; S \<turnstile> \<^bold>\<bottom>)\<close>
 
 lemma inconsistent_subset:
   assumes \<open>consistent A V\<close> \<open>\<not> consistent A ({p} \<union> V)\<close>
   obtains V' where \<open>set V' \<subseteq> V\<close> \<open>A \<turnstile> p # V' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
 proof -
   obtain V' where V': \<open>set V' \<subseteq> ({p} \<union> V)\<close> \<open>p \<in> set V'\<close> \<open>A \<turnstile> V' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     using assms unfolding consistent_def by blast
   then have *: \<open>A \<turnstile> p # V' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     using K_imply_Cons by blast
 
   let ?S = \<open>removeAll p V'\<close>
   have \<open>set (p # V') \<subseteq> set (p # ?S)\<close>
     by auto
   then have \<open>A \<turnstile> p # ?S \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     using * K_imply_weaken by blast
   moreover have \<open>set ?S \<subseteq> V\<close>
     using V'(1) by (metis Diff_subset_conv set_removeAll)
   ultimately show ?thesis
     using that by blast
 qed
 
 lemma consistent_consequent:
   assumes \<open>consistent A V\<close> \<open>p \<in> V\<close> \<open>A \<turnstile> p \<^bold>\<longrightarrow> q\<close>
   shows \<open>consistent A ({q} \<union> V)\<close>
 proof -
   have \<open>\<forall>V'. set V' \<subseteq> V \<longrightarrow> \<not> (A \<turnstile> p # V' \<^bold>\<leadsto> \<^bold>\<bottom>)\<close>
     using \<open>consistent A V\<close> \<open>p \<in> V\<close> unfolding consistent_def
     by (metis insert_subset list.simps(15))
   then have \<open>\<forall>V'. set V' \<subseteq> V \<longrightarrow> \<not> (A \<turnstile> q # V' \<^bold>\<leadsto> \<^bold>\<bottom>)\<close>
     using \<open>A \<turnstile> (p \<^bold>\<longrightarrow> q)\<close> K_imply_head K_right_mp by (metis imply.simps(1-2))
   then show ?thesis
     using \<open>consistent A V\<close> inconsistent_subset by metis
 qed
 
 lemma consistent_consequent':
   assumes \<open>consistent A V\<close> \<open>p \<in> V\<close> \<open>tautology (p \<^bold>\<longrightarrow> q)\<close>
   shows \<open>consistent A ({q} \<union> V)\<close>
   using assms consistent_consequent A1 by blast
 
 lemma consistent_disjuncts:
   assumes \<open>consistent A V\<close> \<open>(p \<^bold>\<or> q) \<in> V\<close>
   shows \<open>consistent A ({p} \<union> V) \<or> consistent A ({q} \<union> V)\<close>
 proof (rule ccontr)
   assume \<open>\<not> ?thesis\<close>
   then have \<open>\<not> consistent A ({p} \<union> V)\<close> \<open>\<not> consistent A ({q} \<union> V)\<close>
     by blast+
 
   then obtain S' T' where
     S': \<open>set S' \<subseteq> V\<close> \<open>A \<turnstile> p # S' \<^bold>\<leadsto> \<^bold>\<bottom>\<close> and
     T': \<open>set T' \<subseteq> V\<close> \<open>A \<turnstile> q # T' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     using \<open>consistent A V\<close> inconsistent_subset by metis
 
   from S' have p: \<open>A \<turnstile> p # S' @ T' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     by (metis K_imply_weaken Un_upper1 append_Cons set_append)
   moreover from T' have q: \<open>A \<turnstile> q # S' @ T' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     by (metis K_imply_head K_right_mp R1 imply.simps(2) imply_append)
   ultimately have \<open>A \<turnstile> (p \<^bold>\<or> q) # S' @ T' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     using K_DisL by blast
   then have \<open>A \<turnstile> S' @ T' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     using S'(1) T'(1) p q \<open>consistent A V\<close> \<open>(p \<^bold>\<or> q) \<in> V\<close> unfolding consistent_def
     by (metis Un_subset_iff insert_subset list.simps(15) set_append)
   moreover have \<open>set (S' @ T') \<subseteq> V\<close>
     by (simp add: S'(1) T'(1))
   ultimately show False
     using \<open>consistent A V\<close> unfolding consistent_def by blast
 qed
 
 lemma exists_finite_inconsistent:
   assumes \<open>\<not> consistent A ({\<^bold>\<not> p} \<union> V)\<close>
   obtains W where \<open>{\<^bold>\<not> p} \<union> W \<subseteq> {\<^bold>\<not> p} \<union> V\<close> \<open>(\<^bold>\<not> p) \<notin> W\<close> \<open>finite W\<close> \<open>\<not> consistent A ({\<^bold>\<not> p} \<union> W)\<close>
 proof -
   obtain W' where W': \<open>set W' \<subseteq> {\<^bold>\<not> p} \<union> V\<close> \<open>A \<turnstile> W' \<^bold>\<leadsto> \<^bold>\<bottom>\<close>
     using assms unfolding consistent_def by blast
   let ?S = \<open>removeAll (\<^bold>\<not> p) W'\<close>
   have \<open>\<not> consistent A ({\<^bold>\<not> p} \<union> set ?S)\<close>
     unfolding consistent_def using W'(2) by auto
   moreover have \<open>finite (set ?S)\<close>
     by blast
   moreover have \<open>{\<^bold>\<not> p} \<union> set ?S \<subseteq> {\<^bold>\<not> p} \<union> V\<close>
     using W'(1) by auto
   moreover have \<open>(\<^bold>\<not> p) \<notin> set ?S\<close>
     by simp
   ultimately show ?thesis
     by (meson that)
 qed
 
 lemma inconsistent_imply:
   assumes \<open>\<not> consistent A ({\<^bold>\<not> p} \<union> set G)\<close>
   shows \<open>A \<turnstile> G \<^bold>\<leadsto> p\<close>
   using assms K_Boole K_imply_weaken unfolding consistent_def
   by (metis insert_is_Un list.simps(15))
 
 subsection \<open>Maximal consistent sets\<close>
 
 definition maximal :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm set \<Rightarrow> bool\<close> where
   \<open>maximal A S \<equiv> \<forall>p. p \<notin> S \<longrightarrow> \<not> consistent A ({p} \<union> S)\<close>
 
 theorem deriv_in_maximal:
   assumes \<open>consistent A V\<close> \<open>maximal A V\<close> \<open>A \<turnstile> p\<close>
   shows \<open>p \<in> V\<close>
   using assms R1 inconsistent_subset unfolding consistent_def maximal_def
   by (metis imply.simps(2))
 
 theorem exactly_one_in_maximal:
   assumes \<open>consistent A V\<close> \<open>maximal A V\<close>
   shows \<open>p \<in> V \<longleftrightarrow> (\<^bold>\<not> p) \<notin> V\<close>
 proof
   assume \<open>p \<in> V\<close>
   then show \<open>(\<^bold>\<not> p) \<notin> V\<close>
     using assms K_mp unfolding consistent_def maximal_def
     by (metis empty_subsetI insert_subset list.set(1) list.simps(15))
 next
   assume \<open>(\<^bold>\<not> p) \<notin> V\<close>
   have \<open>A \<turnstile> (p \<^bold>\<or> \<^bold>\<not> p)\<close>
     by (simp add: A1)
   then have \<open>(p \<^bold>\<or> \<^bold>\<not> p) \<in> V\<close>
     using assms deriv_in_maximal by blast
   then have \<open>consistent A ({p} \<union> V) \<or> consistent A ({\<^bold>\<not> p} \<union> V)\<close>
     using assms consistent_disjuncts by blast
   then show \<open>p \<in> V\<close>
     using \<open>maximal A V\<close> \<open>(\<^bold>\<not> p) \<notin> V\<close> unfolding maximal_def by blast
 qed
 
 theorem consequent_in_maximal:
   assumes \<open>consistent A V\<close> \<open>maximal A V\<close> \<open>p \<in> V\<close> \<open>(p \<^bold>\<longrightarrow> q) \<in> V\<close>
   shows \<open>q \<in> V\<close>
 proof -
   have \<open>\<forall>V'. set V' \<subseteq> V \<longrightarrow> \<not> (A \<turnstile> p # (p \<^bold>\<longrightarrow> q) # V' \<^bold>\<leadsto> \<^bold>\<bottom>)\<close>
     using \<open>consistent A V\<close> \<open>p \<in> V\<close> \<open>(p \<^bold>\<longrightarrow> q) \<in> V\<close> unfolding consistent_def
     by (metis insert_subset list.simps(15))
   then have \<open>\<forall>V'. set V' \<subseteq> V \<longrightarrow> \<not> (A \<turnstile> q # V' \<^bold>\<leadsto> \<^bold>\<bottom>)\<close>
     by (meson K_mp K_ImpI K_imply_weaken K_right_mp set_subset_Cons)
   then have \<open>consistent A ({q} \<union> V)\<close>
     using \<open>consistent A V\<close> inconsistent_subset by metis
   then show ?thesis
     using \<open>maximal A V\<close> unfolding maximal_def by fast
 qed
 
 theorem ax_in_maximal:
   assumes \<open>consistent A V\<close> \<open>maximal A V\<close> \<open>A p\<close>
   shows \<open>p \<in> V\<close>
   using assms deriv_in_maximal Ax by blast
 
 theorem mcs_properties:
   assumes \<open>consistent A V\<close> and \<open>maximal A V\<close>
   shows \<open>A \<turnstile> p \<Longrightarrow> p \<in> V\<close>
     and \<open>p \<in> V \<longleftrightarrow> (\<^bold>\<not> p) \<notin> V\<close>
     and \<open>p \<in> V \<Longrightarrow> (p \<^bold>\<longrightarrow> q) \<in> V \<Longrightarrow> q \<in> V\<close>
   using assms deriv_in_maximal exactly_one_in_maximal consequent_in_maximal by blast+
 
 subsection \<open>Lindenbaum extension\<close>
 
 instantiation fm :: (countable) countable begin
 instance by countable_datatype
 end
 
 primrec extend :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm set \<Rightarrow> (nat \<Rightarrow> 'i fm) \<Rightarrow> nat \<Rightarrow> 'i fm set\<close> where
   \<open>extend A S f 0 = S\<close>
 | \<open>extend A S f (Suc n) =
     (if consistent A ({f n} \<union> extend A S f n)
      then {f n} \<union> extend A S f n
      else extend A S f n)\<close>
 
 definition Extend :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm set \<Rightarrow> (nat \<Rightarrow> 'i fm) \<Rightarrow> 'i fm set\<close> where
   \<open>Extend A S f \<equiv> \<Union>n. extend A S f n\<close>
 
 lemma Extend_subset: \<open>S \<subseteq> Extend A S f\<close>
   unfolding Extend_def using Union_upper extend.simps(1) range_eqI
   by metis
 
 lemma extend_bound: \<open>(\<Union>n \<le> m. extend A S f n) = extend A S f m\<close>
   by (induct m) (simp_all add: atMost_Suc)
 
 lemma consistent_extend: \<open>consistent A S \<Longrightarrow> consistent A (extend A S f n)\<close>
   by (induct n) simp_all
 
 lemma UN_finite_bound:
   assumes \<open>finite A\<close> \<open>A \<subseteq> (\<Union>n. f n)\<close>
   shows \<open>\<exists>m :: nat. A \<subseteq> (\<Union>n \<le> m. f n)\<close>
   using assms
 proof (induct rule: finite_induct)
   case (insert x A)
   then obtain m where \<open>A \<subseteq> (\<Union>n \<le> m. f n)\<close>
     by fast
   then have \<open>A \<subseteq> (\<Union>n \<le> (m + k). f n)\<close> for k
     by fastforce
   moreover obtain m' where \<open>x \<in> f m'\<close>
     using insert(4) by blast
   ultimately have \<open>{x} \<union> A \<subseteq> (\<Union>n \<le> m + m'. f n)\<close>
     by auto
   then show ?case
     by blast
 qed simp
 
 lemma consistent_Extend:
   assumes \<open>consistent A S\<close>
   shows \<open>consistent A (Extend A S f)\<close>
   unfolding Extend_def
 proof (rule ccontr)
   assume \<open>\<not> consistent A (\<Union>n. extend A S f n)\<close>
   then obtain S' where \<open>A \<turnstile> S' \<^bold>\<leadsto> \<^bold>\<bottom>\<close> \<open>set S' \<subseteq> (\<Union>n. extend A S f n)\<close>
     unfolding consistent_def by blast
   then obtain m where \<open>set S' \<subseteq> (\<Union>n \<le> m. extend A S f n)\<close>
     using UN_finite_bound by (metis List.finite_set)
   then have \<open>set S' \<subseteq> extend A S f m\<close>
     using extend_bound by blast
   moreover have \<open>consistent A (extend A S f m)\<close>
     using assms consistent_extend by blast
   ultimately show False
     unfolding consistent_def using \<open>A \<turnstile> S' \<^bold>\<leadsto> \<^bold>\<bottom>\<close> by blast
 qed
 
 lemma maximal_Extend:
   assumes \<open>surj f\<close>
   shows \<open>maximal A (Extend A S f)\<close>
 proof (rule ccontr)
   assume \<open>\<not> maximal A (Extend A S f)\<close>
   then obtain p where \<open>p \<notin> Extend A S f\<close> \<open>consistent A ({p} \<union> Extend A S f)\<close>
     unfolding maximal_def using assms consistent_Extend by blast
   obtain k where n: \<open>f k = p\<close>
     using \<open>surj f\<close> unfolding surj_def by metis
   then have \<open>p \<notin> extend A S f (Suc k)\<close>
     using \<open>p \<notin> Extend A S f\<close> unfolding Extend_def by blast
   then have \<open>\<not> consistent A ({p} \<union> extend A S f k)\<close>
     using n by fastforce
   moreover have \<open>{p} \<union> extend A S f k \<subseteq> {p} \<union> Extend A S f\<close>
     unfolding Extend_def by blast
   ultimately have \<open>\<not> consistent A ({p} \<union> Extend A S f)\<close>
     unfolding consistent_def by fastforce
   then show False
     using \<open>consistent A ({p} \<union> Extend A S f)\<close> by blast
 qed
 
 lemma maximal_extension:
   fixes V :: \<open>('i :: countable) fm set\<close>
   assumes \<open>consistent A V\<close>
   obtains W where \<open>V \<subseteq> W\<close> \<open>consistent A W\<close> \<open>maximal A W\<close>
 proof -
   let ?W = \<open>Extend A V from_nat\<close>
   have \<open>V \<subseteq> ?W\<close>
     using Extend_subset by blast
   moreover have \<open>consistent A ?W\<close>
     using assms consistent_Extend by blast
   moreover have \<open>maximal A ?W\<close>
     using assms maximal_Extend surj_from_nat by blast
   ultimately show ?thesis
     using that by blast
 qed
 
 subsection \<open>Canonical model\<close>
 
 abbreviation pi :: \<open>'i fm set \<Rightarrow> id \<Rightarrow> bool\<close> where
   \<open>pi V x \<equiv> Pro x \<in> V\<close>
 
 abbreviation known :: \<open>'i fm set \<Rightarrow> 'i \<Rightarrow> 'i fm set\<close> where
   \<open>known V i \<equiv> {p. K i p \<in> V}\<close>
 
 abbreviation reach :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i \<Rightarrow> 'i fm set \<Rightarrow> 'i fm set set\<close> where
   \<open>reach A i V \<equiv> {W. known V i \<subseteq> W}\<close>
 
 abbreviation mcss :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> 'i fm set set\<close> where
   \<open>mcss A \<equiv> {W. consistent A W \<and> maximal A W}\<close>
 
 abbreviation canonical :: \<open>('i fm \<Rightarrow> bool) \<Rightarrow> ('i, 'i fm set) kripke\<close> where
   \<open>canonical A \<equiv> Kripke (mcss A) pi (reach A)\<close>
 
 lemma truth_lemma:
-  fixes A and p :: \<open>('i :: countable) fm\<close>
+  fixes p :: \<open>('i :: countable) fm\<close>
   assumes \<open>consistent A V\<close> and \<open>maximal A V\<close>
   shows \<open>p \<in> V \<longleftrightarrow> canonical A, V \<Turnstile> p\<close>
   using assms
 proof (induct p arbitrary: V)
   case FF
   then show ?case
   proof safe
     assume \<open>\<^bold>\<bottom> \<in> V\<close>
     then have False
       using \<open>consistent A V\<close> K_imply_head unfolding consistent_def
       by (metis bot.extremum insert_subset list.set(1) list.simps(15))
     then show \<open>canonical A, V \<Turnstile> \<^bold>\<bottom>\<close> ..
   next
     assume \<open>canonical A, V \<Turnstile> \<^bold>\<bottom>\<close>
     then show \<open>\<^bold>\<bottom> \<in> V\<close>
       by simp
   qed
 next
   case (Pro x)
   then show ?case
     by simp
 next
   case (Dis p q)
   then show ?case
   proof safe
     assume \<open>(p \<^bold>\<or> q) \<in> V\<close>
     then have \<open>consistent A ({p} \<union> V) \<or> consistent A ({q} \<union> V)\<close>
       using \<open>consistent A V\<close> consistent_disjuncts by blast
     then have \<open>p \<in> V \<or> q \<in> V\<close>
       using \<open>maximal A V\<close> unfolding maximal_def by fast
     then show \<open>canonical A, V \<Turnstile> (p \<^bold>\<or> q)\<close>
       using Dis by simp
   next
     assume \<open>canonical A, V \<Turnstile> (p \<^bold>\<or> q)\<close>
     then consider \<open>canonical A, V \<Turnstile> p\<close> | \<open>canonical A, V \<Turnstile> q\<close>
       by auto
     then have \<open>p \<in> V \<or> q \<in> V\<close>
       using Dis by auto
     moreover have \<open>A \<turnstile> p \<^bold>\<longrightarrow> p \<^bold>\<or> q\<close> \<open>A \<turnstile> q \<^bold>\<longrightarrow> p \<^bold>\<or> q\<close>
       by (auto simp: A1)
     ultimately show \<open>(p \<^bold>\<or> q) \<in> V\<close>
       using Dis.prems deriv_in_maximal consequent_in_maximal by blast
   qed
 next
   case (Con p q)
   then show ?case
   proof safe
     assume \<open>(p \<^bold>\<and> q) \<in> V\<close>
     then have \<open>consistent A ({p} \<union> V)\<close> \<open>consistent A ({q} \<union> V)\<close>
       using \<open>consistent A V\<close> consistent_consequent' by fastforce+
     then have \<open>p \<in> V\<close> \<open>q \<in> V\<close>
       using \<open>maximal A V\<close> unfolding maximal_def by fast+
     then show \<open>canonical A, V \<Turnstile> (p \<^bold>\<and> q)\<close>
       using Con by simp
   next
     assume \<open>canonical A, V \<Turnstile> (p \<^bold>\<and> q)\<close>
     then have \<open>canonical A, V \<Turnstile> p\<close> \<open>canonical A, V \<Turnstile> q\<close>
       by auto
     then have \<open>p \<in> V\<close> \<open>q \<in> V\<close>
       using Con by auto
     moreover have \<open>A \<turnstile> p \<^bold>\<longrightarrow> q \<^bold>\<longrightarrow> p \<^bold>\<and> q\<close>
       by (auto simp: A1)
     ultimately show \<open>(p \<^bold>\<and> q) \<in> V\<close>
       using Con.prems deriv_in_maximal consequent_in_maximal by blast
   qed
 next
   case (Imp p q)
   then show ?case
   proof safe
     assume \<open>(p \<^bold>\<longrightarrow> q) \<in> V\<close>
     then have \<open>consistent A ({\<^bold>\<not> p \<^bold>\<or> q} \<union> V)\<close>
       using \<open>consistent A V\<close> consistent_consequent' by fastforce
     then have \<open>consistent A ({\<^bold>\<not> p} \<union> V) \<or> consistent A ({q} \<union> V)\<close>
       using \<open>consistent A V\<close> \<open>maximal A V\<close> consistent_disjuncts unfolding maximal_def by blast
     then have \<open>(\<^bold>\<not> p) \<in> V \<or> q \<in> V\<close>
       using \<open>maximal A V\<close> unfolding maximal_def by fast
     then have \<open>p \<notin> V \<or> q \<in> V\<close>
       using Imp.prems exactly_one_in_maximal by blast
     then show \<open>canonical A, V \<Turnstile> (p \<^bold>\<longrightarrow> q)\<close>
       using Imp by simp
   next
     assume \<open>canonical A, V \<Turnstile> (p \<^bold>\<longrightarrow> q)\<close>
     then consider \<open>\<not> canonical A, V \<Turnstile> p\<close> | \<open>canonical A, V \<Turnstile> q\<close>
       by auto
     then have \<open>p \<notin> V \<or> q \<in> V\<close>
       using Imp by auto
     then have \<open>(\<^bold>\<not> p) \<in> V \<or> q \<in> V\<close>
       using Imp.prems exactly_one_in_maximal by blast
     moreover have \<open>A \<turnstile> \<^bold>\<not> p \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> q\<close> \<open>A \<turnstile> q \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> q\<close>
       by (auto simp: A1)
     ultimately show \<open>(p \<^bold>\<longrightarrow> q) \<in> V\<close>
       using Imp.prems deriv_in_maximal consequent_in_maximal by blast
   qed
 next
   case (K i p)
   then show ?case
   proof safe
     assume \<open>K i p \<in> V\<close>
     then show \<open>canonical A, V \<Turnstile> K i p\<close>
       using K.hyps by auto
   next
     assume \<open>canonical A, V \<Turnstile> K i p\<close>
 
     have \<open>\<not> consistent A ({\<^bold>\<not> p} \<union> known V i)\<close>
     proof
       assume \<open>consistent A ({\<^bold>\<not> p} \<union> known V i)\<close>
       then obtain W where W: \<open>{\<^bold>\<not> p} \<union> known V i \<subseteq> W\<close> \<open>consistent A W\<close> \<open>maximal A W\<close>
         using \<open>consistent A V\<close> maximal_extension by blast
       then have \<open>canonical A, W \<Turnstile> \<^bold>\<not> p\<close>
         using K \<open>consistent A V\<close> exactly_one_in_maximal by auto
       moreover have \<open>W \<in> reach A i V\<close> \<open>W \<in> mcss A\<close>
         using W by simp_all
       ultimately have \<open>canonical A, V \<Turnstile> \<^bold>\<not> K i p\<close>
         by auto
       then show False
         using \<open>canonical A, V \<Turnstile> K i p\<close> by auto
     qed
 
     then obtain W where W:
       \<open>{\<^bold>\<not> p} \<union> W \<subseteq> {\<^bold>\<not> p} \<union> known V i\<close> \<open>(\<^bold>\<not> p) \<notin> W\<close> \<open>finite W\<close> \<open>\<not> consistent A ({\<^bold>\<not> p} \<union> W)\<close>
       using exists_finite_inconsistent by metis
 
     obtain L where L: \<open>set L = W\<close>
       using \<open>finite W\<close> finite_list by blast
 
     then have \<open>A \<turnstile> L \<^bold>\<leadsto> p\<close>
       using W(4) inconsistent_imply by blast
     then have \<open>A \<turnstile> K i (L \<^bold>\<leadsto> p)\<close>
       using R2 by fast
     then have \<open>A \<turnstile> map (K i) L \<^bold>\<leadsto> K i p\<close>
       using K_distrib_K_imp by fast
     then have \<open>(map (K i) L \<^bold>\<leadsto> K i p) \<in> V\<close>
       using deriv_in_maximal K.prems(1, 2) by blast
     then show \<open>K i p \<in> V\<close>
       using L W(1-2)
     proof (induct L arbitrary: W)
       case (Cons a L)
       then have \<open>K i a \<in> V\<close>
         by auto
       then have \<open>(map (K i) L \<^bold>\<leadsto> K i p) \<in> V\<close>
         using Cons(2) \<open>consistent A V\<close> \<open>maximal A V\<close> consequent_in_maximal by auto
       then show ?case
         using Cons by auto
     qed simp
   qed
 qed
 
 lemma canonical_model:
   assumes \<open>consistent A S\<close> and \<open>p \<in> S\<close>
   defines \<open>V \<equiv> Extend A S from_nat\<close> and \<open>M \<equiv> canonical A\<close>
   shows \<open>M, V \<Turnstile> p\<close> and \<open>consistent A V\<close> and \<open>maximal A V\<close>
 proof -
   have \<open>consistent A V\<close>
     using \<open>consistent A S\<close> unfolding V_def using consistent_Extend by blast
   have \<open>maximal A V\<close>
     unfolding V_def using maximal_Extend surj_from_nat by blast
-
   { fix x
     assume \<open>x \<in> S\<close>
     then have \<open>x \<in> V\<close>
       unfolding V_def using Extend_subset by blast
     then have \<open>M, V \<Turnstile> x\<close>
       unfolding M_def using truth_lemma \<open>consistent A V\<close> \<open>maximal A V\<close> by blast }
   then show \<open>M, V \<Turnstile> p\<close>
     using \<open>p \<in> S\<close> by blast+
   show \<open>consistent A V\<close> \<open>maximal A V\<close>
     by fact+
 qed
 
 subsection \<open>Completeness\<close>
 
 abbreviation valid :: \<open>(('i :: countable, 'i fm set) kripke \<Rightarrow> bool) \<Rightarrow> 'i fm set \<Rightarrow> 'i fm \<Rightarrow> bool\<close>
-  (\<open>valid\<close>) where \<open>valid \<equiv> valid\<star>\<close>
+  where \<open>valid \<equiv> valid\<star>\<close>
 
 theorem strong_completeness:
   assumes \<open>valid P G p\<close> and \<open>P (canonical A)\<close>
-  shows \<open>\<exists>qs. set qs \<subseteq> G \<and> (A \<turnstile> qs \<^bold>\<leadsto> p)\<close>
+  shows \<open>A; G \<turnstile> p\<close>
 proof (rule ccontr)
   assume \<open>\<nexists>qs. set qs \<subseteq> G \<and> (A \<turnstile> qs \<^bold>\<leadsto> p)\<close>
   then have *: \<open>\<forall>qs. set qs \<subseteq> G \<longrightarrow> \<not> (A \<turnstile> (\<^bold>\<not> p) # qs \<^bold>\<leadsto> \<^bold>\<bottom>)\<close>
     using K_Boole by blast
 
   let ?S = \<open>{\<^bold>\<not> p} \<union> G\<close>
   let ?V = \<open>Extend A ?S from_nat\<close>
   let ?M = \<open>canonical A\<close>
 
   have \<open>consistent A ?S\<close>
     using * by (metis K_imply_Cons consistent_def inconsistent_subset)
   then have \<open>?M, ?V \<Turnstile> (\<^bold>\<not> p)\<close> \<open>\<forall>q \<in> G. ?M, ?V \<Turnstile> q\<close>
     using canonical_model by fastforce+
   moreover have \<open>?V \<in> mcss A\<close>
     using \<open>consistent A ?S\<close> consistent_Extend maximal_Extend surj_from_nat by blast
   ultimately have \<open>?M, ?V \<Turnstile> p\<close>
     using assms by simp
   then show False
     using \<open>?M, ?V \<Turnstile> (\<^bold>\<not> p)\<close> by simp
 qed
 
 corollary completeness:
   assumes \<open>valid P {} p\<close> and \<open>P (canonical A)\<close>
   shows \<open>A \<turnstile> p\<close>
   using assms strong_completeness[where G=\<open>{}\<close>] by simp
 
 corollary completeness\<^sub>A:
   assumes \<open>valid (\<lambda>_. True) {} p\<close>
   shows \<open>A \<turnstile> p\<close>
   using assms completeness by blast
 
 section \<open>System K\<close>
 
 abbreviation SystemK (\<open>_ \<turnstile>\<^sub>K _\<close> [50] 50) where
-  \<open>G \<turnstile>\<^sub>K p \<equiv> (\<lambda>_. False), G \<turnstile> p\<close>
+  \<open>G \<turnstile>\<^sub>K p \<equiv> (\<lambda>_. False); G \<turnstile> p\<close>
 
 lemma strong_soundness\<^sub>K: \<open>G \<turnstile>\<^sub>K p \<Longrightarrow> valid\<star> P G p\<close>
   using strong_soundness[of \<open>\<lambda>_. False\<close> \<open>\<lambda>_. True\<close>] by fast
 
 abbreviation \<open>valid\<^sub>K \<equiv> valid (\<lambda>_. True)\<close>
 
 lemma strong_completeness\<^sub>K: \<open>valid\<^sub>K G p \<Longrightarrow> G \<turnstile>\<^sub>K p\<close>
   using strong_completeness[of \<open>\<lambda>_. True\<close>] by blast
 
 theorem main\<^sub>K: \<open>valid\<^sub>K G p \<longleftrightarrow> G \<turnstile>\<^sub>K p\<close>
   using strong_soundness\<^sub>K[of G p] strong_completeness\<^sub>K[of G p] by fast
 
 corollary \<open>valid\<^sub>K G p \<Longrightarrow> valid\<star> (\<lambda>_. True) G p\<close>
   using strong_soundness\<^sub>K[of G p] strong_completeness\<^sub>K[of G p] by fast
 
 section \<open>System T\<close>
 
 text \<open>Also known as System M\<close>
 
 inductive AxT :: \<open>'i fm \<Rightarrow> bool\<close> where
   \<open>AxT (K i p \<^bold>\<longrightarrow> p)\<close>
 
 abbreviation SystemT (\<open>_ \<turnstile>\<^sub>T _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>T p \<equiv> AxT, G \<turnstile> p\<close>
+  \<open>G \<turnstile>\<^sub>T p \<equiv> AxT; G \<turnstile> p\<close>
 
 lemma soundness_AxT: \<open>AxT p \<Longrightarrow> reflexive M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   by (induct p rule: AxT.induct) (meson truth)
 
 lemma strong_soundness\<^sub>T: \<open>G \<turnstile>\<^sub>T p \<Longrightarrow> valid\<star> reflexive G p\<close>
   using strong_soundness soundness_AxT .
 
 lemma AxT_reflexive:
   assumes \<open>AxT \<le> A\<close> and \<open>consistent A V\<close> and \<open>maximal A V\<close>
   shows \<open>V \<in> reach A i V\<close>
 proof -
   have \<open>(K i p \<^bold>\<longrightarrow> p) \<in> V\<close> for p
     using assms ax_in_maximal AxT.intros by fast
   then have \<open>p \<in> V\<close> if \<open>K i p \<in> V\<close> for p
     using that assms consequent_in_maximal by blast
   then show ?thesis
     using assms by blast
 qed
 
 lemma reflexive\<^sub>T:
   assumes \<open>AxT \<le> A\<close>
   shows \<open>reflexive (canonical A)\<close>
   unfolding reflexive_def
 proof safe
   fix i V
   assume \<open>V \<in> \<W> (canonical A)\<close>
   then have \<open>consistent A V\<close> \<open>maximal A V\<close>
     by simp_all
   with AxT_reflexive assms have \<open>V \<in> reach A i V\<close> .
   then show \<open>V \<in> \<K> (canonical A) i V\<close>
     by simp
 qed
 
 abbreviation \<open>valid\<^sub>T \<equiv> valid reflexive\<close>
 
 lemma strong_completeness\<^sub>T: \<open>valid\<^sub>T G p \<Longrightarrow> G \<turnstile>\<^sub>T p\<close>
   using strong_completeness reflexive\<^sub>T by blast
 
 theorem main\<^sub>T: \<open>valid\<^sub>T G p \<longleftrightarrow> G \<turnstile>\<^sub>T p\<close>
   using strong_soundness\<^sub>T[of G p] strong_completeness\<^sub>T[of G p] by fast
 
 corollary \<open>valid\<^sub>T G p \<longrightarrow> valid\<star> reflexive G p\<close>
   using strong_soundness\<^sub>T[of G p] strong_completeness\<^sub>T[of G p] by fast
 
 section \<open>System KB\<close>
 
 inductive AxB :: \<open>'i fm \<Rightarrow> bool\<close> where
   \<open>AxB (p \<^bold>\<longrightarrow> K i (L i p))\<close>
 
 abbreviation SystemKB (\<open>_ \<turnstile>\<^sub>K\<^sub>B _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>K\<^sub>B p \<equiv> AxB, G \<turnstile> p\<close>
+  \<open>G \<turnstile>\<^sub>K\<^sub>B p \<equiv> AxB; G \<turnstile> p\<close>
 
 lemma soundness_AxB: \<open>AxB p \<Longrightarrow> symmetric M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   unfolding symmetric_def by (induct p rule: AxB.induct) auto
 
 lemma strong_soundness\<^sub>K\<^sub>B: \<open>G \<turnstile>\<^sub>K\<^sub>B p \<Longrightarrow> valid\<star> symmetric G p\<close>
   using strong_soundness soundness_AxB .
 
 lemma AxB_symmetric':
   assumes \<open>AxB \<le> A\<close> \<open>consistent A V\<close> \<open>maximal A V\<close> \<open>consistent A W\<close> \<open>maximal A W\<close>
     and \<open>W \<in> reach A i V\<close>
   shows \<open>V \<in> reach A i W\<close>
 proof -
   have \<open>\<forall>p. K i p \<in> W \<longrightarrow> p \<in> V\<close>
-  proof (intro allI impI, rule ccontr)
+  proof (safe, rule ccontr)
     fix p
     assume \<open>K i p \<in> W\<close> \<open>p \<notin> V\<close>
     then have \<open>(\<^bold>\<not> p) \<in> V\<close>
       using assms(2-3) exactly_one_in_maximal by fast
     then have \<open>K i (L i (\<^bold>\<not> p)) \<in> V\<close>
       using assms(1-3) ax_in_maximal AxB.intros consequent_in_maximal by fast
     then have \<open>L i (\<^bold>\<not> p) \<in> W\<close>
       using \<open>W \<in> reach A i V\<close> by fast
     then have \<open>(\<^bold>\<not> K i p) \<in> W\<close>
       using assms(4-5) by (meson K_LK consistent_consequent maximal_def)
     then show False
       using \<open>K i p \<in> W\<close> assms(4-5) exactly_one_in_maximal by fast
   qed
   then have \<open>known W i \<subseteq> V\<close>
     by blast
   then show ?thesis
     using assms(2-3) by simp
 qed
 
 lemma symmetric\<^sub>K\<^sub>B:
   assumes \<open>AxB \<le> A\<close>
   shows \<open>symmetric (canonical A)\<close>
   unfolding symmetric_def
 proof (intro allI ballI)
   fix i V W
   assume \<open>V \<in> \<W> (canonical A)\<close> \<open>W \<in> \<W> (canonical A)\<close>
   then have \<open>consistent A V\<close> \<open>maximal A V\<close> \<open>consistent A W\<close> \<open>maximal A W\<close>
     by simp_all
   with AxB_symmetric' assms have \<open>W \<in> reach A i V \<longleftrightarrow> V \<in> reach A i W\<close>
     by metis
   then show \<open>(W \<in> \<K> (canonical A) i V) = (V \<in> \<K> (canonical A) i W)\<close>
     by simp
 qed
 
 abbreviation \<open>valid\<^sub>K\<^sub>B \<equiv> valid symmetric\<close>
 
 lemma strong_completeness\<^sub>K\<^sub>B: \<open>valid\<^sub>K\<^sub>B G p \<Longrightarrow> G \<turnstile>\<^sub>K\<^sub>B p\<close>
   using strong_completeness symmetric\<^sub>K\<^sub>B by blast
 
 theorem main\<^sub>K\<^sub>B: \<open>valid\<^sub>K\<^sub>B G p \<longleftrightarrow> G \<turnstile>\<^sub>K\<^sub>B p\<close>
   using strong_soundness\<^sub>K\<^sub>B[of G p] strong_completeness\<^sub>K\<^sub>B[of G p] by fast
 
 corollary \<open>valid\<^sub>K\<^sub>B G p \<longrightarrow> valid\<star> symmetric G p\<close>
   using strong_soundness\<^sub>K\<^sub>B[of G p] strong_completeness\<^sub>K\<^sub>B[of G p] by fast
 
 section \<open>System K4\<close>
 
 inductive Ax4 :: \<open>'i fm \<Rightarrow> bool\<close> where
   \<open>Ax4 (K i p \<^bold>\<longrightarrow> K i (K i p))\<close>
 
 abbreviation SystemK4 (\<open>_ \<turnstile>\<^sub>K\<^sub>4 _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>K\<^sub>4 p \<equiv> Ax4, G \<turnstile> p\<close>
+  \<open>G \<turnstile>\<^sub>K\<^sub>4 p \<equiv> Ax4; G \<turnstile> p\<close>
 
 lemma soundness_Ax4: \<open>Ax4 p \<Longrightarrow> transitive M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   by (induct p rule: Ax4.induct) (meson pos_introspection)
 
 lemma strong_soundness\<^sub>K\<^sub>4: \<open>G \<turnstile>\<^sub>K\<^sub>4 p \<Longrightarrow> valid\<star> transitive G p\<close>
   using strong_soundness soundness_Ax4 .
 
 lemma Ax4_transitive:
   assumes \<open>Ax4 \<le> A\<close> \<open>consistent A V\<close> \<open>maximal A V\<close>
     and \<open>W \<in> reach A i V\<close> \<open>U \<in> reach A i W\<close>
   shows \<open>U \<in> reach A i V\<close>
 proof -
   have \<open>(K i p \<^bold>\<longrightarrow> K i (K i p)) \<in> V\<close> for p
     using assms(1-3) ax_in_maximal Ax4.intros by fast
   then have \<open>K i (K i p) \<in> V\<close> if \<open>K i p \<in> V\<close> for p
     using that assms(2-3) consequent_in_maximal by blast
   then show ?thesis
     using assms(4-5) by blast
 qed
 
 lemma transitive\<^sub>K\<^sub>4:
   assumes \<open>Ax4 \<le> A\<close>
   shows \<open>transitive (canonical A)\<close>
   unfolding transitive_def
 proof safe
   fix i U V W
   assume \<open>V \<in> \<W> (canonical A)\<close>
   then have \<open>consistent A V\<close> \<open>maximal A V\<close>
     by simp_all
   moreover assume
     \<open>W \<in> \<K> (canonical A) i V\<close>
     \<open>U \<in> \<K> (canonical A) i W\<close>
   ultimately have \<open>U \<in> reach A i V\<close>
     using Ax4_transitive assms by simp
   then show \<open>U \<in> \<K> (canonical A) i V\<close>
     by simp
 qed
 
 abbreviation \<open>valid\<^sub>K\<^sub>4 \<equiv> valid transitive\<close>
 
 lemma strong_completeness\<^sub>K\<^sub>4: \<open>valid\<^sub>K\<^sub>4 G p \<Longrightarrow> G \<turnstile>\<^sub>K\<^sub>4 p\<close>
   using strong_completeness transitive\<^sub>K\<^sub>4 by blast
 
 theorem main\<^sub>K\<^sub>4: \<open>valid\<^sub>K\<^sub>4 G p \<longleftrightarrow> G \<turnstile>\<^sub>K\<^sub>4 p\<close>
   using strong_soundness\<^sub>K\<^sub>4[of G p] strong_completeness\<^sub>K\<^sub>4[of G p] by fast
 
 corollary \<open>valid\<^sub>K\<^sub>4 G p \<longrightarrow> valid\<star> transitive G p\<close>
   using strong_soundness\<^sub>K\<^sub>4[of G p] strong_completeness\<^sub>K\<^sub>4[of G p] by fast
 
+section \<open>System K5\<close>
+
+inductive Ax5 :: \<open>'i fm \<Rightarrow> bool\<close> where
+  \<open>Ax5 (L i p \<^bold>\<longrightarrow> K i (L i p))\<close>
+
+abbreviation SystemK5 (\<open>_ \<turnstile>\<^sub>K\<^sub>5 _\<close> [50, 50] 50) where
+  \<open>G \<turnstile>\<^sub>K\<^sub>5 p \<equiv> Ax5; G \<turnstile> p\<close>
+
+lemma soundness_Ax5: \<open>Ax5 p \<Longrightarrow> Euclidean M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
+  by (induct p rule: Ax5.induct) (unfold Euclidean_def semantics.simps, blast)
+
+lemma strong_soundness\<^sub>K\<^sub>5: \<open>G \<turnstile>\<^sub>K\<^sub>5 p \<Longrightarrow> valid\<star> Euclidean G p\<close>
+  using strong_soundness soundness_Ax5 .
+
+lemma Ax5_Euclidean:
+  assumes \<open>Ax5 \<le> A\<close>
+    \<open>consistent A U\<close> \<open>maximal A U\<close>
+    \<open>consistent A V\<close> \<open>maximal A V\<close>
+    \<open>consistent A W\<close> \<open>maximal A W\<close>
+    and \<open>V \<in> reach A i U\<close> \<open>W \<in> reach A i U\<close>
+  shows \<open>W \<in> reach A i V\<close>
+  using assms
+proof -
+  { fix p
+    assume \<open>K i p \<in> V\<close> \<open>p \<notin> W\<close>
+    then have \<open>(\<^bold>\<not> p) \<in> W\<close>
+      using assms(6-7) exactly_one_in_maximal by fast
+    then have \<open>L i (\<^bold>\<not> p) \<in> U\<close>
+      using assms(2-3, 6-7, 9) exactly_one_in_maximal by blast
+    then have \<open>K i (L i (\<^bold>\<not> p)) \<in> U\<close>
+      using assms(1-3) ax_in_maximal Ax5.intros consequent_in_maximal by fast
+    then have \<open>L i (\<^bold>\<not> p) \<in> V\<close>
+      using assms(8) by blast
+    then have \<open>\<^bold>\<not> K i p \<in> V\<close>
+      using assms(4-5) K_LK consequent_in_maximal deriv_in_maximal by fast
+    then have False
+      using assms(4-5) \<open>K i p \<in> V\<close> exactly_one_in_maximal by fast
+  }
+  then show ?thesis
+    by blast
+qed
+
+lemma Euclidean\<^sub>K\<^sub>5:
+  assumes \<open>Ax5 \<le> A\<close>
+  shows \<open>Euclidean (canonical A)\<close>
+  unfolding Euclidean_def
+proof safe
+  fix i U V W
+  assume \<open>U \<in> \<W> (canonical A)\<close> \<open>V \<in> \<W> (canonical A)\<close> \<open>W \<in> \<W> (canonical A)\<close>
+  then have
+    \<open>consistent A U\<close> \<open>maximal A U\<close>
+    \<open>consistent A V\<close> \<open>maximal A V\<close>
+    \<open>consistent A W\<close> \<open>maximal A W\<close>
+    by simp_all
+  moreover assume
+    \<open>V \<in> \<K> (canonical A) i U\<close>
+    \<open>W \<in> \<K> (canonical A) i U\<close>
+  ultimately have \<open>W \<in> reach A i V\<close>
+    using Ax5_Euclidean assms by simp
+  then show \<open>W \<in> \<K> (canonical A) i V\<close>
+    by simp
+qed
+
+abbreviation \<open>valid\<^sub>K\<^sub>5 \<equiv> valid Euclidean\<close>
+
+lemma strong_completeness\<^sub>K\<^sub>5: \<open>valid\<^sub>K\<^sub>5 G p \<Longrightarrow> G \<turnstile>\<^sub>K\<^sub>5 p\<close>
+  using strong_completeness Euclidean\<^sub>K\<^sub>5 by blast
+
+theorem main\<^sub>K\<^sub>5: \<open>valid\<^sub>K\<^sub>5 G p \<longleftrightarrow> G \<turnstile>\<^sub>K\<^sub>5 p\<close>
+  using strong_soundness\<^sub>K\<^sub>5[of G p] strong_completeness\<^sub>K\<^sub>5[of G p] by fast
+
+corollary \<open>valid\<^sub>K\<^sub>5 G p \<longrightarrow> valid\<star> Euclidean G p\<close>
+  using strong_soundness\<^sub>K\<^sub>5[of G p] strong_completeness\<^sub>K\<^sub>5[of G p] by fast
+
 section \<open>System S4\<close>
 
 abbreviation Or :: \<open>('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool\<close> (infixl \<open>\<oplus>\<close> 65) where
-  \<open>A \<oplus> A' \<equiv> \<lambda>x. A x \<or> A' x\<close>
+  \<open>(A \<oplus> A') p \<equiv> A p \<or> A' p\<close>
 
 abbreviation SystemS4 (\<open>_ \<turnstile>\<^sub>S\<^sub>4 _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>S\<^sub>4 p \<equiv> AxT \<oplus> Ax4, G \<turnstile> p\<close>
+  \<open>G \<turnstile>\<^sub>S\<^sub>4 p \<equiv> AxT \<oplus> Ax4; G \<turnstile> p\<close>
 
 lemma soundness_AxT4: \<open>(AxT \<oplus> Ax4) p \<Longrightarrow> reflexive M \<and> transitive M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   using soundness_AxT soundness_Ax4 by fast
 
 lemma strong_soundness\<^sub>S\<^sub>4: \<open>G \<turnstile>\<^sub>S\<^sub>4 p \<Longrightarrow> valid\<star> refltrans G p\<close>
   using strong_soundness soundness_AxT4 .
 
 abbreviation \<open>valid\<^sub>S\<^sub>4 \<equiv> valid refltrans\<close>
 
 lemma strong_completeness\<^sub>S\<^sub>4: \<open>valid\<^sub>S\<^sub>4 G p \<Longrightarrow> G \<turnstile>\<^sub>S\<^sub>4 p\<close>
   using strong_completeness[of refltrans] reflexive\<^sub>T[of \<open>AxT \<oplus> Ax4\<close>] transitive\<^sub>K\<^sub>4[of \<open>AxT \<oplus> Ax4\<close>]
   by blast
 
 theorem main\<^sub>S\<^sub>4: \<open>valid\<^sub>S\<^sub>4 G p \<longleftrightarrow> G \<turnstile>\<^sub>S\<^sub>4 p\<close>
   using strong_soundness\<^sub>S\<^sub>4[of G p] strong_completeness\<^sub>S\<^sub>4[of G p] by fast
 
 corollary \<open>valid\<^sub>S\<^sub>4 G p \<longrightarrow> valid\<star> refltrans G p\<close>
   using strong_soundness\<^sub>S\<^sub>4[of G p] strong_completeness\<^sub>S\<^sub>4[of G p] by fast
 
 section \<open>System S5\<close>
 
+subsection \<open>T + B + 4\<close>
+
 abbreviation SystemS5 (\<open>_ \<turnstile>\<^sub>S\<^sub>5 _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>S\<^sub>5 p \<equiv> AxT \<oplus> AxB \<oplus> Ax4, G \<turnstile> p\<close>
+  \<open>G \<turnstile>\<^sub>S\<^sub>5 p \<equiv> AxT \<oplus> AxB \<oplus> Ax4; G \<turnstile> p\<close>
 
 abbreviation AxTB4 :: \<open>'i fm \<Rightarrow> bool\<close> where
   \<open>AxTB4 \<equiv> AxT \<oplus> AxB \<oplus> Ax4\<close>
 
 lemma soundness_AxTB4: \<open>AxTB4 p \<Longrightarrow> equivalence M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
   using soundness_AxT soundness_AxB soundness_Ax4 by fast
 
 lemma strong_soundness\<^sub>S\<^sub>5: \<open>G \<turnstile>\<^sub>S\<^sub>5 p \<Longrightarrow> valid\<star> equivalence G p\<close>
   using strong_soundness soundness_AxTB4 .
 
 abbreviation \<open>valid\<^sub>S\<^sub>5 \<equiv> valid equivalence\<close>
 
 lemma strong_completeness\<^sub>S\<^sub>5: \<open>valid\<^sub>S\<^sub>5 G p \<Longrightarrow> G \<turnstile>\<^sub>S\<^sub>5 p\<close>
   using strong_completeness[of equivalence]
     reflexive\<^sub>T[of AxTB4] symmetric\<^sub>K\<^sub>B[of AxTB4] transitive\<^sub>K\<^sub>4[of AxTB4]
   by blast
 
 theorem main\<^sub>S\<^sub>5: \<open>valid\<^sub>S\<^sub>5 G p \<longleftrightarrow> G \<turnstile>\<^sub>S\<^sub>5 p\<close>
   using strong_soundness\<^sub>S\<^sub>5[of G p] strong_completeness\<^sub>S\<^sub>5[of G p] by fast
 
 corollary \<open>valid\<^sub>S\<^sub>5 G p \<longrightarrow> valid\<star> equivalence G p\<close>
   using strong_soundness\<^sub>S\<^sub>5[of G p] strong_completeness\<^sub>S\<^sub>5[of G p] by fast
 
-subsection \<open>Traditional formulation\<close>
-
-inductive SystemS5' :: \<open>'i fm \<Rightarrow> bool\<close> (\<open>\<turnstile>\<^sub>S\<^sub>5'' _\<close> [20] 20) where
-  A1': \<open>tautology p \<Longrightarrow> \<turnstile>\<^sub>S\<^sub>5' p\<close>
-| A2': \<open>\<turnstile>\<^sub>S\<^sub>5' K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i p \<^bold>\<longrightarrow> K i q\<close>
-| AT': \<open>\<turnstile>\<^sub>S\<^sub>5' K i p \<^bold>\<longrightarrow> p\<close>
-| A5': \<open>\<turnstile>\<^sub>S\<^sub>5' \<^bold>\<not> K i p \<^bold>\<longrightarrow> K i (\<^bold>\<not> K i p)\<close>
-| R1': \<open>\<turnstile>\<^sub>S\<^sub>5' p \<Longrightarrow> \<turnstile>\<^sub>S\<^sub>5' p \<^bold>\<longrightarrow> q \<Longrightarrow> \<turnstile>\<^sub>S\<^sub>5' q\<close>
-| R2': \<open>\<turnstile>\<^sub>S\<^sub>5' p \<Longrightarrow> \<turnstile>\<^sub>S\<^sub>5' K i p\<close>
-
-lemma S5'_trans: \<open>\<turnstile>\<^sub>S\<^sub>5' (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> (q \<^bold>\<longrightarrow> r) \<^bold>\<longrightarrow> p \<^bold>\<longrightarrow> r\<close>
-  by (simp add: A1')
-
-lemma S5'_L: \<open>\<turnstile>\<^sub>S\<^sub>5' p \<^bold>\<longrightarrow> L i p\<close>
-proof -
-  have \<open>\<turnstile>\<^sub>S\<^sub>5' K i (\<^bold>\<not> p) \<^bold>\<longrightarrow> \<^bold>\<not> p\<close>
-    using AT' by fast
-  moreover have \<open>\<turnstile>\<^sub>S\<^sub>5' (P \<^bold>\<longrightarrow> \<^bold>\<not> Q) \<^bold>\<longrightarrow> Q \<^bold>\<longrightarrow> \<^bold>\<not> P\<close> for P Q :: \<open>'i fm\<close>
-    using A1' by force
-  ultimately show ?thesis
-    using R1' by blast
-qed
+subsection \<open>T + 5\<close>
 
-lemma S5'_B: \<open>\<turnstile>\<^sub>S\<^sub>5' p \<^bold>\<longrightarrow> K i (L i p)\<close>
-  using A5' S5'_L R1' S5'_trans by metis
+abbreviation SystemS5' (\<open>_ \<turnstile>\<^sub>S\<^sub>5'' _\<close> [50, 50] 50) where
+  \<open>G \<turnstile>\<^sub>S\<^sub>5' p \<equiv> AxT \<oplus> Ax5; G \<turnstile> p\<close>
 
-lemma S5'_map_K:
-  assumes \<open>\<turnstile>\<^sub>S\<^sub>5' p \<^bold>\<longrightarrow> q\<close>
-  shows \<open>\<turnstile>\<^sub>S\<^sub>5' K i p \<^bold>\<longrightarrow> K i q\<close>
+abbreviation AxT5 :: \<open>'i fm \<Rightarrow> bool\<close> where
+  \<open>AxT5 \<equiv> AxT \<oplus> Ax5\<close>
+
+lemma symm_trans_Euclid: \<open>symmetric M \<Longrightarrow> transitive M \<Longrightarrow> Euclidean M\<close>
+  unfolding symmetric_def transitive_def Euclidean_def by blast
+
+lemma soundness_AxT5: \<open>AxT5 p \<Longrightarrow> equivalence M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile> p\<close>
+  using soundness_AxT[of p M w] soundness_Ax5[of p M w] symm_trans_Euclid by blast
+
+lemma strong_soundness\<^sub>S\<^sub>5': \<open>G \<turnstile>\<^sub>S\<^sub>5' p \<Longrightarrow> valid\<star> equivalence G p\<close>
+  using strong_soundness soundness_AxT5 .
+
+lemma refl_Euclid_equiv: \<open>reflexive M \<Longrightarrow> Euclidean M \<Longrightarrow> equivalence M\<close>
+  unfolding reflexive_def symmetric_def transitive_def Euclidean_def by metis
+
+lemma strong_completeness\<^sub>S\<^sub>5': \<open>valid\<^sub>S\<^sub>5 G p \<Longrightarrow> G \<turnstile>\<^sub>S\<^sub>5' p\<close>
+  using strong_completeness[of equivalence]
+    reflexive\<^sub>T[of AxT5] Euclidean\<^sub>K\<^sub>5[of AxT5] refl_Euclid_equiv by blast
+
+theorem main\<^sub>S\<^sub>5': \<open>valid\<^sub>S\<^sub>5 G p \<longleftrightarrow> G \<turnstile>\<^sub>S\<^sub>5' p\<close>
+  using strong_soundness\<^sub>S\<^sub>5'[of G p] strong_completeness\<^sub>S\<^sub>5'[of G p] by fast
+
+subsection \<open>Equivalence between systems\<close>
+
+subsubsection \<open>Axiom 5 from B and 4\<close>
+
+lemma K4_L:
+  assumes \<open>Ax4 \<le> A\<close>
+  shows \<open>A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p\<close>
 proof -
-  note \<open>\<turnstile>\<^sub>S\<^sub>5' p \<^bold>\<longrightarrow> q\<close>
-  then have \<open>\<turnstile>\<^sub>S\<^sub>5' K i (p \<^bold>\<longrightarrow> q)\<close>
-    using R2' by fast
-  moreover have \<open>\<turnstile>\<^sub>S\<^sub>5' K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i p \<^bold>\<longrightarrow> K i q\<close>
-    using A2' by fast
-  ultimately show ?thesis
-    using R1' by fast
-qed
-
-lemma S5'_L_dual: \<open>\<turnstile>\<^sub>S\<^sub>5' \<^bold>\<not> L i (\<^bold>\<not> p) \<^bold>\<longrightarrow> K i p\<close>
-proof -
-  have \<open>\<turnstile>\<^sub>S\<^sub>5' K i p \<^bold>\<longrightarrow> K i p\<close> \<open>\<turnstile>\<^sub>S\<^sub>5' \<^bold>\<not> \<^bold>\<not> p \<^bold>\<longrightarrow> p\<close>
-    by (simp_all add: A1')
-  then have \<open>\<turnstile>\<^sub>S\<^sub>5' K i (\<^bold>\<not> \<^bold>\<not> p) \<^bold>\<longrightarrow> K i p\<close>
-    by (simp add: S5'_map_K)
-  moreover have \<open>\<turnstile>\<^sub>S\<^sub>5' (P \<^bold>\<longrightarrow> Q) \<^bold>\<longrightarrow> (\<^bold>\<not> \<^bold>\<not> P \<^bold>\<longrightarrow> Q)\<close> for P Q :: \<open>'i fm\<close>
-    by (simp add: A1')
-  ultimately show \<open>\<turnstile>\<^sub>S\<^sub>5' \<^bold>\<not> \<^bold>\<not> K i (\<^bold>\<not> \<^bold>\<not> p) \<^bold>\<longrightarrow> K i p\<close>
-    using R1' by blast
+  have \<open>A \<turnstile> K i (\<^bold>\<not> p) \<^bold>\<longrightarrow> K i (K i (\<^bold>\<not> p))\<close>
+    using assms by (auto intro: Ax Ax4.intros)
+  then show ?thesis
+    by (meson K_LK K_trans R1)
 qed
 
-lemma S5'_4: \<open>\<turnstile>\<^sub>S\<^sub>5' K i p \<^bold>\<longrightarrow> K i (K i p)\<close>
+lemma KB4_5:
+  assumes \<open>AxB \<le> A\<close> \<open>Ax4 \<le> A\<close>
+  shows \<open>A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)\<close>
 proof -
-  have \<open>\<turnstile>\<^sub>S\<^sub>5' L i (\<^bold>\<not> p) \<^bold>\<longrightarrow> K i (L i (\<^bold>\<not> p))\<close>
-    using A5' by fast
-  moreover have \<open>\<turnstile>\<^sub>S\<^sub>5' (P \<^bold>\<longrightarrow> Q) \<^bold>\<longrightarrow> \<^bold>\<not> Q \<^bold>\<longrightarrow> \<^bold>\<not> P\<close> for P Q :: \<open>'i fm\<close>
-    using A1' by force
-  ultimately have \<open>\<turnstile>\<^sub>S\<^sub>5' \<^bold>\<not> K i (L i (\<^bold>\<not> p)) \<^bold>\<longrightarrow> \<^bold>\<not> L i (\<^bold>\<not> p)\<close>
-    using R1' by fast
-  then have \<open>\<turnstile>\<^sub>S\<^sub>5' L i (K i (\<^bold>\<not> \<^bold>\<not> p)) \<^bold>\<longrightarrow> \<^bold>\<not> L i (\<^bold>\<not> p)\<close>
-    by blast
-  moreover have \<open>\<turnstile>\<^sub>S\<^sub>5' p \<^bold>\<longrightarrow> \<^bold>\<not> \<^bold>\<not> p\<close>
-    by (simp add: A1')
-  ultimately have \<open>\<turnstile>\<^sub>S\<^sub>5' L i (K i p) \<^bold>\<longrightarrow> \<^bold>\<not> L i (\<^bold>\<not> p)\<close>
-    by (metis (no_types, opaque_lifting) R1' S5'_map_K S5'_trans)
-  then have \<open>\<turnstile>\<^sub>S\<^sub>5' L i (K i p) \<^bold>\<longrightarrow> K i p\<close>
-    by (meson S5'_L_dual R1' S5'_trans)
-  then show ?thesis
-    by (metis A2' R1' R2' S5'_B S5'_trans)
+  have \<open>A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))\<close>
+    using assms by (auto intro: Ax AxB.intros)
+  moreover have \<open>A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p\<close>
+    using assms by (auto intro: K4_L)
+  then have \<open>A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)\<close>
+    using K_map by fast
+  ultimately show ?thesis
+    using K_trans R1 by metis
 qed
 
-lemma S5_S5': \<open>AxTB4 \<turnstile> p \<Longrightarrow> \<turnstile>\<^sub>S\<^sub>5' p\<close>
-proof (induct p rule: AK.induct)
-  case (A2 i p q)
-  have \<open>\<turnstile>\<^sub>S\<^sub>5' K i (p \<^bold>\<longrightarrow> q) \<^bold>\<longrightarrow> K i p \<^bold>\<longrightarrow> K i q\<close>
-    using A2' .
-  moreover have \<open>\<turnstile>\<^sub>S\<^sub>5' (P \<^bold>\<longrightarrow> Q \<^bold>\<longrightarrow> R) \<^bold>\<longrightarrow> (Q \<^bold>\<and> P \<^bold>\<longrightarrow> R)\<close> for P Q R :: \<open>'i fm\<close>
-    by (simp add: A1')
-  ultimately show ?case
-    using R1' by blast
-next
-  case (Ax p)
-  then show ?case
-    using AT' S5'_B S5'_4
-    by (metis Ax4.cases AxB.cases AxT.cases)
-qed (meson SystemS5'.intros)+
+subsubsection \<open>Axioms B and 4 from T and 5\<close>
 
-lemma S5'_S5:
-  fixes p :: \<open>('i :: countable) fm\<close>
-  shows \<open>\<turnstile>\<^sub>S\<^sub>5' p \<Longrightarrow> AxTB4 \<turnstile> p\<close>
-proof (induct p rule: SystemS5'.induct)
-  case (AT' i p)
-  then show ?case
-    by (simp add: Ax AxT.intros)
-next
-  case (A5' i p)
-  let ?p = \<open>\<^bold>\<not> K i p \<^bold>\<longrightarrow> K i (\<^bold>\<not> K i p)\<close>
-  have \<open>valid\<^sub>S\<^sub>5 {} ?p\<close>
-    by (meson neg_introspection)
-  then show ?case
-    using strong_completeness\<^sub>S\<^sub>5[of \<open>{}\<close> \<open>?p\<close>] by fastforce 
-qed (meson AK.intros K_A2')+
+lemma T_L:
+  assumes \<open>AxT \<le> A\<close>
+  shows \<open>A \<turnstile> p \<^bold>\<longrightarrow> L i p\<close>
+proof -
+  have \<open>A \<turnstile> K i (\<^bold>\<not> p) \<^bold>\<longrightarrow> \<^bold>\<not> p\<close>
+    using assms by (auto intro: Ax AxT.intros)
+  moreover have \<open>A \<turnstile> (P \<^bold>\<longrightarrow> \<^bold>\<not> Q) \<^bold>\<longrightarrow> Q \<^bold>\<longrightarrow> \<^bold>\<not> P\<close> for P Q
+    by (auto intro: A1)
+  ultimately show ?thesis
+    by (auto intro: R1)
+qed
 
-theorem strong_completeness\<^sub>S\<^sub>5':
-  assumes \<open>valid\<^sub>S\<^sub>5 G p\<close>
-  shows \<open>\<exists>qs. set qs \<subseteq> G \<and> (\<turnstile>\<^sub>S\<^sub>5' qs \<^bold>\<leadsto> p)\<close>
-  using assms strong_completeness\<^sub>S\<^sub>5 S5_S5' S5'_S5 by blast
+lemma S5'_B:
+  assumes \<open>AxT \<le> A\<close> \<open>Ax5 \<le> A\<close>
+  shows \<open>A \<turnstile> p \<^bold>\<longrightarrow> K i (L i p)\<close>
+proof -
+  have \<open>A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)\<close>
+    using assms(2) by (auto intro: Ax Ax5.intros)
+  moreover have \<open>A \<turnstile> p \<^bold>\<longrightarrow> L i p\<close>
+    using assms(1) by (auto intro: T_L)
+  ultimately show ?thesis
+    using K_trans R1 by metis
+qed
 
-theorem main\<^sub>S\<^sub>5': \<open>valid\<^sub>S\<^sub>5 {} p \<longleftrightarrow> (\<turnstile>\<^sub>S\<^sub>5' p)\<close>
-  using main\<^sub>S\<^sub>5[of \<open>{}\<close> p] S5_S5' S5'_S5 by auto
+lemma K5_L:
+  assumes \<open>Ax5 \<le> A\<close>
+  shows \<open>A \<turnstile> L i (K i p) \<^bold>\<longrightarrow> K i p\<close>
+proof -
+  have \<open>A \<turnstile> L i (\<^bold>\<not> p) \<^bold>\<longrightarrow> K i (L i (\<^bold>\<not> p))\<close>
+    using assms by (auto intro: Ax Ax5.intros)
+  then have \<open>A \<turnstile> L i (\<^bold>\<not> p) \<^bold>\<longrightarrow> K i (\<^bold>\<not> K i p)\<close>
+    using K_LK by (metis K_map K_trans R1)
+  moreover have \<open>A \<turnstile> (P \<^bold>\<longrightarrow> Q) \<^bold>\<longrightarrow> \<^bold>\<not> Q \<^bold>\<longrightarrow> \<^bold>\<not> P\<close> for P Q
+    by (auto intro: A1)
+  ultimately have \<open>A \<turnstile> \<^bold>\<not> K i (\<^bold>\<not> K i p) \<^bold>\<longrightarrow> \<^bold>\<not> L i (\<^bold>\<not> p)\<close>
+    using R1 by blast
+  then have \<open>A \<turnstile> \<^bold>\<not> K i (\<^bold>\<not> K i p) \<^bold>\<longrightarrow> K i p\<close>
+    using K_L_dual R1 K_trans by metis
+  then show ?thesis
+    by blast
+qed
+
+lemma S5'_4:
+  assumes \<open>AxT \<le> A\<close> \<open>Ax5 \<le> A\<close>
+  shows \<open>A \<turnstile> K i p \<^bold>\<longrightarrow> K i (K i p)\<close>
+proof -
+  have \<open>A \<turnstile> L i (K i p) \<^bold>\<longrightarrow> K i (L i (K i p))\<close>
+    using assms(2) by (auto intro: Ax Ax5.intros)
+  moreover have \<open>A \<turnstile> K i p \<^bold>\<longrightarrow> L i (K i p)\<close>
+    using assms(1) by (auto intro: T_L)
+  ultimately have \<open>A \<turnstile> K i p \<^bold>\<longrightarrow> K i (L i (K i p))\<close>
+    using K_trans R1 by metis
+  moreover have \<open>A \<turnstile> L i (K i p) \<^bold>\<longrightarrow> K i p\<close>
+    using assms(2) K5_L by metis
+  then have \<open>A \<turnstile> K i (L i (K i p)) \<^bold>\<longrightarrow> K i (K i p)\<close>
+    using K_map by fast
+  ultimately show ?thesis
+    using R1 K_trans by metis
+qed
+
+lemma S5_S5': \<open>AxTB4 \<turnstile> p \<Longrightarrow> AxT5 \<turnstile> p\<close>
+proof (induct p rule: AK.induct)
+  case (Ax p)
+  moreover have \<open>AxT5 \<turnstile> p\<close> if \<open>AxT p\<close>
+    using that AK.Ax by metis
+  moreover have \<open>AxT5 \<turnstile> p\<close> if \<open>AxB p\<close>
+    using that S5'_B by (metis (no_types, lifting) AxB.cases predicate1I)
+  moreover have \<open>AxT5 \<turnstile> p\<close> if \<open>Ax4 p\<close>
+    using that S5'_4 by (metis (no_types, lifting) Ax4.cases predicate1I)
+  ultimately show ?case
+    by blast
+qed (auto intro: AK.intros)
+
+lemma S5'_S5: \<open>AxT5 \<turnstile> p \<Longrightarrow> AxTB4 \<turnstile> p\<close>
+proof (induct p rule: AK.induct)
+  case (Ax p)
+  moreover have \<open>AxTB4 \<turnstile> p\<close> if \<open>AxT p\<close>
+    using that AK.Ax by metis
+  moreover have \<open>AxTB4 \<turnstile> p\<close> if \<open>Ax5 p\<close>
+    using that KB4_5 by (metis (no_types, lifting) Ax5.cases predicate1I)
+  ultimately show ?case
+    by blast
+qed (auto intro: AK.intros)
+
+corollary S5_S5'_assms: \<open>G \<turnstile>\<^sub>S\<^sub>5 p \<longleftrightarrow> G \<turnstile>\<^sub>S\<^sub>5' p\<close>
+  using S5_S5' S5'_S5 by blast
 
 section \<open>Acknowledgements\<close>
 
 text \<open>
 The formalization is inspired by Berghofer's formalization of Henkin-style completeness.
 
   \<^item> Stefan Berghofer:
   First-Order Logic According to Fitting.
   \<^url>\<open>https://www.isa-afp.org/entries/FOL-Fitting.shtml\<close>
 \<close>
 
 end
diff --git a/thys/Public_Announcement_Logic/PAL.thy b/thys/Public_Announcement_Logic/PAL.thy
--- a/thys/Public_Announcement_Logic/PAL.thy
+++ b/thys/Public_Announcement_Logic/PAL.thy
@@ -1,885 +1,999 @@
 (*
   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 a variant of the axiom system
+  It includes proofs of soundness and completeness for variants of the axiom system
     PA + DIST! + NEC!.
-  The completeness proof builds on the Epistemic Logic theory.
+  The completeness proofs build on the Epistemic Logic theory.
 *)
 
 theory PAL imports "Epistemic_Logic.Epistemic_Logic" begin
 
 section \<open>Syntax\<close>
 
 datatype 'i pfm
   = FF (\<open>\<^bold>\<bottom>\<^sub>!\<close>)
   | Pro' id (\<open>Pro\<^sub>!\<close>)
-  | Dis \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr \<open>\<^bold>\<or>\<^sub>!\<close> 30)
-  | Con \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr \<open>\<^bold>\<and>\<^sub>!\<close> 35)
-  | Imp \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr \<open>\<^bold>\<longrightarrow>\<^sub>!\<close> 25)
+  | Dis \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr \<open>\<^bold>\<or>\<^sub>!\<close> 60)
+  | Con \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr \<open>\<^bold>\<and>\<^sub>!\<close> 65)
+  | Imp \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr \<open>\<^bold>\<longrightarrow>\<^sub>!\<close> 55)
   | K' 'i \<open>'i pfm\<close> (\<open>K\<^sub>!\<close>)
-  | Ann \<open>'i pfm\<close> \<open>'i pfm\<close> (\<open>[_]\<^sub>! _\<close> [50, 50] 50)
+  | Ann \<open>'i pfm\<close> \<open>'i pfm\<close> (\<open>[_]\<^sub>! _\<close> [80, 80] 80)
 
-abbreviation PIff :: \<open>'i pfm \<Rightarrow> 'i pfm \<Rightarrow> 'i pfm\<close> (infixr \<open>\<^bold>\<longleftrightarrow>\<^sub>!\<close> 25) where
+abbreviation PIff :: \<open>'i pfm \<Rightarrow> 'i pfm \<Rightarrow> 'i pfm\<close> (infixr \<open>\<^bold>\<longleftrightarrow>\<^sub>!\<close> 55) where
   \<open>p \<^bold>\<longleftrightarrow>\<^sub>! q \<equiv> (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<and>\<^sub>! (q \<^bold>\<longrightarrow>\<^sub>! p)\<close>
 
-abbreviation PNeg (\<open>\<^bold>\<not>\<^sub>! _\<close> [40] 40) where
+abbreviation PNeg (\<open>\<^bold>\<not>\<^sub>! _\<close> [70] 70) where
   \<open>\<^bold>\<not>\<^sub>! p \<equiv> p \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!\<close>
 
 abbreviation PL (\<open>L\<^sub>!\<close>) where
   \<open>L\<^sub>! i p \<equiv> (\<^bold>\<not>\<^sub>! (K\<^sub>! i (\<^bold>\<not>\<^sub>! p)))\<close>
 
+primrec anns :: \<open>'i pfm \<Rightarrow> 'i pfm set\<close> where
+  \<open>anns \<^bold>\<bottom>\<^sub>! = {}\<close>
+| \<open>anns (Pro\<^sub>! _) = {}\<close>
+| \<open>anns (p \<^bold>\<or>\<^sub>! q) = (anns p \<union> anns q)\<close>
+| \<open>anns (p \<^bold>\<and>\<^sub>! q) = (anns p \<union> anns q)\<close>
+| \<open>anns (p \<^bold>\<longrightarrow>\<^sub>! q) = (anns p \<union> anns q)\<close>
+| \<open>anns (K\<^sub>! i p) = anns p\<close>
+| \<open>anns ([r]\<^sub>! p) = {r} \<union> anns r \<union> anns p\<close>
+
 section \<open>Semantics\<close>
 
 fun
   psemantics :: \<open>('i, 'w) kripke \<Rightarrow> 'w \<Rightarrow> 'i pfm \<Rightarrow> bool\<close> (\<open>_, _ \<Turnstile>\<^sub>! _\<close> [50, 50] 50) and
   restrict :: \<open>('i, 'w) kripke \<Rightarrow> 'i pfm \<Rightarrow> ('i, 'w) kripke\<close> where
   \<open>(M, w \<Turnstile>\<^sub>! \<^bold>\<bottom>\<^sub>!) = False\<close>
 | \<open>(M, w \<Turnstile>\<^sub>! Pro\<^sub>! x) = \<pi> M w x\<close>
-| \<open>(M, w \<Turnstile>\<^sub>! (p \<^bold>\<or>\<^sub>! q)) = ((M, w \<Turnstile>\<^sub>! p) \<or> (M, w \<Turnstile>\<^sub>! q))\<close>
-| \<open>(M, w \<Turnstile>\<^sub>! (p \<^bold>\<and>\<^sub>! q)) = ((M, w \<Turnstile>\<^sub>! p) \<and> (M, w \<Turnstile>\<^sub>! q))\<close>
-| \<open>(M, w \<Turnstile>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)) = ((M, w \<Turnstile>\<^sub>! p) \<longrightarrow> (M, w \<Turnstile>\<^sub>! q))\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! p \<^bold>\<or>\<^sub>! q) = ((M, w \<Turnstile>\<^sub>! p) \<or> (M, w \<Turnstile>\<^sub>! q))\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! p \<^bold>\<and>\<^sub>! q) = ((M, w \<Turnstile>\<^sub>! p) \<and> (M, w \<Turnstile>\<^sub>! q))\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q) = ((M, w \<Turnstile>\<^sub>! p) \<longrightarrow> (M, w \<Turnstile>\<^sub>! q))\<close>
 | \<open>(M, w \<Turnstile>\<^sub>! K\<^sub>! i p) = (\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile>\<^sub>! p)\<close>
 | \<open>(M, w \<Turnstile>\<^sub>! [r]\<^sub>! p) = ((M, w \<Turnstile>\<^sub>! r) \<longrightarrow> (restrict M r, w \<Turnstile>\<^sub>! p))\<close>
-| \<open>restrict M p = Kripke {w. w \<in> \<W> M \<and> M, w \<Turnstile>\<^sub>! p} (\<pi> M) (\<K> M)\<close>
+| \<open>restrict M r = Kripke {w. w \<in> \<W> M \<and> M, w \<Turnstile>\<^sub>! r} (\<pi> M) (\<K> M)\<close>
 
 primrec static :: \<open>'i pfm \<Rightarrow> bool\<close> where
   \<open>static \<^bold>\<bottom>\<^sub>! = True\<close>
 | \<open>static (Pro\<^sub>! _) = True\<close>
 | \<open>static (p \<^bold>\<or>\<^sub>! q) = (static p \<and> static q)\<close>
 | \<open>static (p \<^bold>\<and>\<^sub>! q) = (static p \<and> static q)\<close>
 | \<open>static (p \<^bold>\<longrightarrow>\<^sub>! q) = (static p \<and> static q)\<close>
 | \<open>static (K\<^sub>! i p) = static p\<close>
 | \<open>static ([r]\<^sub>! p) = False\<close>
 
 primrec lower :: \<open>'i pfm \<Rightarrow> 'i fm\<close> where
   \<open>lower \<^bold>\<bottom>\<^sub>! = \<^bold>\<bottom>\<close>
 | \<open>lower (Pro\<^sub>! x) = Pro x\<close>
 | \<open>lower (p \<^bold>\<or>\<^sub>! q) = (lower p \<^bold>\<or> lower q)\<close>
 | \<open>lower (p \<^bold>\<and>\<^sub>! q) = (lower p \<^bold>\<and> lower q)\<close>
 | \<open>lower (p \<^bold>\<longrightarrow>\<^sub>! q) = (lower p \<^bold>\<longrightarrow> lower q)\<close>
 | \<open>lower (K\<^sub>! i p) = K i (lower p)\<close>
 | \<open>lower ([r]\<^sub>! p) = undefined\<close>
 
 primrec lift :: \<open>'i fm \<Rightarrow> 'i pfm\<close> where
   \<open>lift \<^bold>\<bottom> = \<^bold>\<bottom>\<^sub>!\<close>
 | \<open>lift (Pro x) = Pro\<^sub>! x\<close>
 | \<open>lift (p \<^bold>\<or> q) = (lift p \<^bold>\<or>\<^sub>! lift q)\<close>
 | \<open>lift (p \<^bold>\<and> q) = (lift p \<^bold>\<and>\<^sub>! lift q)\<close>
 | \<open>lift (p \<^bold>\<longrightarrow> q) = (lift p \<^bold>\<longrightarrow>\<^sub>! lift q)\<close>
 | \<open>lift (K i p) = K\<^sub>! i (lift p)\<close>
 
 lemma lower_semantics:
   assumes \<open>static p\<close>
   shows \<open>(M, w \<Turnstile> lower p) \<longleftrightarrow> (M, w \<Turnstile>\<^sub>! p)\<close>
   using assms by (induct p arbitrary: w) simp_all
 
 lemma lift_semantics: \<open>(M, w \<Turnstile> p) \<longleftrightarrow> (M, w \<Turnstile>\<^sub>! lift p)\<close>
   by (induct p arbitrary: w) simp_all
 
 lemma lower_lift: \<open>lower (lift p) = p\<close>
   by (induct p) simp_all
 
 lemma lift_lower: \<open>static p \<Longrightarrow> lift (lower p) = p\<close>
   by (induct p) simp_all
 
 section \<open>Soundness of Reduction\<close>
 
 primrec reduce' :: \<open>'i pfm \<Rightarrow> 'i pfm \<Rightarrow> 'i pfm\<close> where
   \<open>reduce' r \<^bold>\<bottom>\<^sub>! = (r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!)\<close>
 | \<open>reduce' r (Pro\<^sub>! x) = (r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x)\<close>
 | \<open>reduce' r (p \<^bold>\<or>\<^sub>! q) = (reduce' r p \<^bold>\<or>\<^sub>! reduce' r q)\<close>
 | \<open>reduce' r (p \<^bold>\<and>\<^sub>! q) = (reduce' r p \<^bold>\<and>\<^sub>! reduce' r q)\<close>
 | \<open>reduce' r (p \<^bold>\<longrightarrow>\<^sub>! q) = (reduce' r p \<^bold>\<longrightarrow>\<^sub>! reduce' r q)\<close>
 | \<open>reduce' r (K\<^sub>! i p) = (r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce' r p))\<close>
 | \<open>reduce' r ([p]\<^sub>! q) = undefined\<close>
 
 primrec reduce :: \<open>'i pfm \<Rightarrow> 'i pfm\<close> where
   \<open>reduce \<^bold>\<bottom>\<^sub>! = \<^bold>\<bottom>\<^sub>!\<close>
 | \<open>reduce (Pro\<^sub>! x) = Pro\<^sub>! x\<close>
 | \<open>reduce (p \<^bold>\<or>\<^sub>! q) = (reduce p \<^bold>\<or>\<^sub>! reduce q)\<close>
 | \<open>reduce (p \<^bold>\<and>\<^sub>! q) = (reduce p \<^bold>\<and>\<^sub>! reduce q)\<close>
 | \<open>reduce (p \<^bold>\<longrightarrow>\<^sub>! q) = (reduce p \<^bold>\<longrightarrow>\<^sub>! reduce q)\<close>
 | \<open>reduce (K\<^sub>! i p) = K\<^sub>! i (reduce p)\<close>
 | \<open>reduce ([r]\<^sub>! p) = reduce' (reduce r) (reduce p)\<close>
 
 lemma static_reduce': \<open>static p \<Longrightarrow> static r \<Longrightarrow> static (reduce' r p)\<close>
   by (induct p) simp_all
 
 lemma static_reduce: \<open>static (reduce p)\<close>
   by (induct p) (simp_all add: static_reduce')
 
 lemma reduce'_semantics:
   assumes \<open>static q\<close>
-  shows \<open>((M, w \<Turnstile>\<^sub>! [p]\<^sub>! (q))) = (M, w \<Turnstile>\<^sub>! reduce' p q)\<close>
+  shows \<open>(M, w \<Turnstile>\<^sub>! [p]\<^sub>! q) = (M, w \<Turnstile>\<^sub>! reduce' p q)\<close>
   using assms by (induct q arbitrary: w) auto
 
 lemma reduce_semantics: \<open>(M, w \<Turnstile>\<^sub>! p) = (M, w \<Turnstile>\<^sub>! reduce p)\<close>
 proof (induct p arbitrary: M w)
   case (Ann p q)
   then show ?case
     using reduce'_semantics static_reduce by fastforce
 qed simp_all
 
 section \<open>Chains of Implications\<close>
 
-primrec implyP :: \<open>'i pfm list \<Rightarrow> 'i pfm \<Rightarrow> 'i pfm\<close> (infixr \<open>\<^bold>\<leadsto>\<^sub>!\<close> 26) where
+primrec implyP :: \<open>'i pfm list \<Rightarrow> 'i pfm \<Rightarrow> 'i pfm\<close> (infixr \<open>\<^bold>\<leadsto>\<^sub>!\<close> 56) where
   \<open>([] \<^bold>\<leadsto>\<^sub>! q) = q\<close>
 | \<open>(p # ps \<^bold>\<leadsto>\<^sub>! q) = (p \<^bold>\<longrightarrow>\<^sub>! ps \<^bold>\<leadsto>\<^sub>! q)\<close>
 
 lemma lift_implyP: \<open>lift (ps \<^bold>\<leadsto> q) = (map lift ps \<^bold>\<leadsto>\<^sub>! lift q)\<close>
   by (induct ps) auto
 
 lemma reduce_implyP: \<open>reduce (ps \<^bold>\<leadsto>\<^sub>! q) = (map reduce ps \<^bold>\<leadsto>\<^sub>! reduce q)\<close>
   by (induct ps) auto
 
 section \<open>Proof System\<close>
 
 primrec peval :: \<open>(id \<Rightarrow> bool) \<Rightarrow> ('i pfm \<Rightarrow> bool) \<Rightarrow> 'i pfm \<Rightarrow> bool\<close> where
   \<open>peval _ _ \<^bold>\<bottom>\<^sub>! = False\<close>
 | \<open>peval g _ (Pro\<^sub>! x) = g x\<close>
 | \<open>peval g h (p \<^bold>\<or>\<^sub>! q) = (peval g h p \<or> peval g h q)\<close>
 | \<open>peval g h (p \<^bold>\<and>\<^sub>! q) = (peval g h p \<and> peval g h q)\<close>
 | \<open>peval g h (p \<^bold>\<longrightarrow>\<^sub>! q) = (peval g h p \<longrightarrow> peval g h q)\<close>
 | \<open>peval _ h (K\<^sub>! i p) = h (K\<^sub>! i p)\<close>
 | \<open>peval _ h ([r]\<^sub>! p) = h ([r]\<^sub>! p)\<close>
 
 abbreviation \<open>ptautology p \<equiv> \<forall>g h. peval g h p\<close>
 
-inductive PAK :: \<open>('i pfm \<Rightarrow> bool) \<Rightarrow> 'i pfm \<Rightarrow> bool\<close> (\<open>_ \<turnstile>\<^sub>! _\<close> [20, 20] 20)
-  for A :: \<open>'i pfm \<Rightarrow> bool\<close> where
-    PA1: \<open>ptautology p \<Longrightarrow> A \<turnstile>\<^sub>! p\<close>
-  | PA2: \<open>A \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<and>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
-  | PAx: \<open>A p \<Longrightarrow> A \<turnstile>\<^sub>! p\<close>
-  | PR1: \<open>A \<turnstile>\<^sub>! p \<Longrightarrow> A \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q \<Longrightarrow> A \<turnstile>\<^sub>! q\<close>
-  | PR2: \<open>A \<turnstile>\<^sub>! p \<Longrightarrow> A \<turnstile>\<^sub>! K\<^sub>! i p\<close>
-  | PFF: \<open>A \<turnstile>\<^sub>! [r]\<^sub>! \<^bold>\<bottom>\<^sub>! \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!)\<close>
-  | PPro: \<open>A \<turnstile>\<^sub>! [r]\<^sub>! Pro\<^sub>! x \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x)\<close>
-  | PDis: \<open>A \<turnstile>\<^sub>! [r]\<^sub>! (p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q\<close>
-  | PCon: \<open>A \<turnstile>\<^sub>! [r]\<^sub>! (p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q\<close>
-  | PImp: \<open>A \<turnstile>\<^sub>! ([r]\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q)\<close>
-  | PK: \<open>A \<turnstile>\<^sub>! ([r]\<^sub>! K\<^sub>! i p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i ([r]\<^sub>! p))\<close>
-  | PAnn: \<open>A \<turnstile>\<^sub>! p \<Longrightarrow> A \<turnstile>\<^sub>! [r]\<^sub>! p\<close>
+inductive PAK :: \<open>('i pfm \<Rightarrow> bool) \<Rightarrow> ('i pfm \<Rightarrow> bool) \<Rightarrow> 'i pfm \<Rightarrow> bool\<close>
+  (\<open>_; _ \<turnstile>\<^sub>! _\<close> [50, 50, 50] 50)
+  for A B :: \<open>'i pfm \<Rightarrow> bool\<close> where
+    PA1: \<open>ptautology p \<Longrightarrow> A; B \<turnstile>\<^sub>! p\<close>
+  | PA2: \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<and>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
+  | PAx: \<open>A p \<Longrightarrow> A; B \<turnstile>\<^sub>! p\<close>
+  | PR1: \<open>A; B \<turnstile>\<^sub>! p \<Longrightarrow> A; B \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q \<Longrightarrow> A; B \<turnstile>\<^sub>! q\<close>
+  | PR2: \<open>A; B \<turnstile>\<^sub>! p \<Longrightarrow> A; B \<turnstile>\<^sub>! K\<^sub>! i p\<close>
+  | PAnn: \<open>A; B \<turnstile>\<^sub>! p \<Longrightarrow> B r \<Longrightarrow> A; B \<turnstile>\<^sub>! [r]\<^sub>! p\<close>
+  | PFF: \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! \<^bold>\<bottom>\<^sub>! \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!)\<close>
+  | PPro: \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! Pro\<^sub>! x \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x)\<close>
+  | PDis: \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! (p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q\<close>
+  | PCon: \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! (p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q\<close>
+  | PImp: \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q)\<close>
+  | PK: \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i ([r]\<^sub>! p))\<close>
 
-abbreviation PAK_assms (\<open>_, _ \<turnstile>\<^sub>! _\<close> [20, 20, 20] 20) where
-  \<open>A, G \<turnstile>\<^sub>! p \<equiv> \<exists>qs. set qs \<subseteq> G \<and> (A \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p)\<close>
+abbreviation PAK_assms (\<open>_; _; _ \<turnstile>\<^sub>! _\<close> [50, 50, 50, 50] 50) where
+  \<open>A; B; G \<turnstile>\<^sub>! p \<equiv> \<exists>qs. set qs \<subseteq> G \<and> (A; B \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p)\<close>
 
 lemma eval_peval: \<open>eval h (g o lift) p = peval h g (lift p)\<close>
   by (induct p) simp_all
 
 lemma tautology_ptautology: \<open>tautology p \<Longrightarrow> ptautology (lift p)\<close>
   using eval_peval by blast
 
-theorem AK_PAK: \<open>A o lift \<turnstile> p \<Longrightarrow> A \<turnstile>\<^sub>! lift p\<close>
+theorem AK_PAK: \<open>A o lift \<turnstile> p \<Longrightarrow> A; B \<turnstile>\<^sub>! lift p\<close>
   by (induct p rule: AK.induct) (auto intro: PAK.intros(1-5) simp: tautology_ptautology)
 
 abbreviation validPS :: \<open>(('i, 'w) kripke \<Rightarrow> bool) \<Rightarrow> 'i pfm set \<Rightarrow> 'i pfm \<Rightarrow> bool\<close> (\<open>valid\<^sub>!\<star>\<close>)
   where \<open>valid\<^sub>!\<star> P G p \<equiv> \<forall>M. \<forall>w \<in> \<W> M. P M \<longrightarrow> (\<forall>q \<in> G. M, w \<Turnstile>\<^sub>! q) \<longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
 
 abbreviation validP
   :: \<open>(('i :: countable, 'i fm set) kripke \<Rightarrow> bool) \<Rightarrow> 'i pfm set \<Rightarrow> 'i pfm \<Rightarrow> bool\<close> (\<open>valid\<^sub>!\<close>)
   where \<open>valid\<^sub>! \<equiv> valid\<^sub>!\<star>\<close>
 
 lemma set_map_inv:
   assumes \<open>set xs \<subseteq> f ` X\<close>
   shows \<open>\<exists>ys. set ys \<subseteq> X \<and> map f ys = xs\<close>
   using assms
 proof (induct xs)
   case (Cons x xs)
   then obtain ys where \<open>set ys \<subseteq> X\<close> \<open>map f ys = xs\<close>
     by auto
   moreover obtain y where \<open>y \<in> X\<close> \<open>f y = x\<close>
     using Cons.prems by auto
   ultimately have \<open>set (y # ys) \<subseteq> X\<close> \<open>map f (y # ys) = x # xs\<close>
     by simp_all
   then show ?case
     by meson
 qed simp
 
 lemma strong_static_completeness':
   assumes \<open>static p\<close> and \<open>\<forall>q \<in> G. static q\<close> and \<open>valid\<^sub>! P G p\<close>
-    and \<open>valid\<star> P (lower ` G) (lower p) \<Longrightarrow> A o lift, lower ` G \<turnstile> lower p\<close>
-  shows \<open>A, G \<turnstile>\<^sub>! p\<close>
+    and \<open>valid\<star> P (lower ` G) (lower p) \<Longrightarrow> A o lift; lower ` G \<turnstile> lower p\<close>
+  shows \<open>A; B; G \<turnstile>\<^sub>! p\<close>
 proof -
   have \<open>valid P (lower ` G) (lower p)\<close>
     using assms by (simp add: lower_semantics)
-  then have \<open>A o lift, lower ` G \<turnstile> lower p\<close>
+  then have \<open>A o lift; lower ` G \<turnstile> lower p\<close>
     using assms(4) by blast
   then obtain qs where \<open>set qs \<subseteq> G\<close> and \<open>A o lift \<turnstile> map lower qs \<^bold>\<leadsto> lower p\<close>
     using set_map_inv by blast
-  then have \<open>A \<turnstile>\<^sub>! lift (map lower qs \<^bold>\<leadsto> lower p)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! lift (map lower qs \<^bold>\<leadsto> lower p)\<close>
     using AK_PAK by fast
-  then have \<open>A \<turnstile>\<^sub>! map lift (map lower qs) \<^bold>\<leadsto>\<^sub>! lift (lower p)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! map lift (map lower qs) \<^bold>\<leadsto>\<^sub>! lift (lower p)\<close>
     using lift_implyP by metis
-  then have \<open>A \<turnstile>\<^sub>! map (lift o lower) qs \<^bold>\<leadsto>\<^sub>! lift (lower p)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! map (lift o lower) qs \<^bold>\<leadsto>\<^sub>! lift (lower p)\<close>
     by simp
   then show ?thesis
     using assms(1-2) \<open>set qs \<subseteq> G\<close> lift_lower
     by (metis (mono_tags, lifting) comp_apply map_idI subset_eq)
 qed
 
 theorem strong_static_completeness:
   assumes \<open>static p\<close> and \<open>\<forall>q \<in> G. static q\<close> and \<open>valid\<^sub>! P G p\<close>
-    and \<open>\<And>G p. valid P G p \<Longrightarrow> A o lift, G \<turnstile> p\<close>
-  shows \<open>A, G \<turnstile>\<^sub>! p\<close>
+    and \<open>\<And>G p. valid P G p \<Longrightarrow> A o lift; G \<turnstile> p\<close>
+  shows \<open>A; B; G \<turnstile>\<^sub>! p\<close>
   using strong_static_completeness' assms .
 
 corollary static_completeness':
   assumes \<open>static p\<close> and \<open>valid\<^sub>! P {} p\<close>
     and \<open>valid P {} (lower p) \<Longrightarrow> A o lift \<turnstile> lower p\<close>
-  shows \<open>A \<turnstile>\<^sub>! p\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p\<close>
   using assms strong_static_completeness'[where G=\<open>{}\<close> and p=p] by simp
 
 corollary static_completeness:
   assumes \<open>static p\<close> and \<open>valid\<^sub>! P {} p\<close> and \<open>\<And>p. valid P {} p \<Longrightarrow> A o lift \<turnstile> p\<close>
-  shows \<open>A \<turnstile>\<^sub>! p\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p\<close>
   using static_completeness' assms .
 
 corollary
   assumes \<open>static p\<close> \<open>valid\<^sub>! (\<lambda>_. True) {} p\<close>
-  shows \<open>A \<turnstile>\<^sub>! p\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p\<close>
   using assms static_completeness[where P=\<open>\<lambda>_. True\<close> and p=p] completeness\<^sub>A by blast
 
 section \<open>Soundness\<close>
 
 lemma peval_semantics: \<open>peval (val w) (\<lambda>q. Kripke W val r, w \<Turnstile>\<^sub>! q) p = (Kripke W val r, w \<Turnstile>\<^sub>! p)\<close>
   by (induct p) simp_all
 
 lemma ptautology:
   assumes \<open>ptautology p\<close>
   shows \<open>M, w \<Turnstile>\<^sub>! p\<close>
 proof -
   from assms have \<open>peval (g w) (\<lambda>q. Kripke W g r, w \<Turnstile>\<^sub>! q) p\<close> for W g r
     by simp
   then have \<open>Kripke W g r, w \<Turnstile>\<^sub>! p\<close> for W g r
     using peval_semantics by fast
   then show \<open>M, w \<Turnstile>\<^sub>! p\<close>
     by (metis kripke.collapse)
 qed
 
-theorem soundness:
+theorem soundness\<^sub>P:
   assumes
     \<open>\<And>M p w. A p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
-    \<open>\<And>M p. P M \<Longrightarrow> P (restrict M p)\<close>
-  shows \<open>A \<turnstile>\<^sub>! p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
+    \<open>\<And>M r. P M \<Longrightarrow> B r \<Longrightarrow> P (restrict M r)\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
 proof (induct p arbitrary: M w rule: PAK.induct)
   case (PAnn p r)
-  moreover have \<open>P (restrict M r)\<close>
-    using PAnn(3) assms(2) by simp
-  ultimately show ?case
-    by simp
+  then show ?case
+    using assms by simp
 qed (simp_all add: assms ptautology)
 
-corollary \<open>(\<lambda>_. False) \<turnstile>\<^sub>! p \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
-  using soundness[where P=\<open>\<lambda>_. True\<close>] by metis
+corollary \<open>(\<lambda>_. False); B \<turnstile>\<^sub>! p \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
+  using soundness\<^sub>P[where P=\<open>\<lambda>_. True\<close>] by metis
 
 section \<open>Strong Soundness\<close>
 
 lemma ptautology_imply_superset:
   assumes \<open>set ps \<subseteq> set qs\<close>
   shows \<open>ptautology (ps \<^bold>\<leadsto>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! r)\<close>
 proof (rule ccontr)
   assume \<open>\<not> ?thesis\<close>
   then obtain g h where \<open>\<not> peval g h (ps \<^bold>\<leadsto>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! r)\<close>
     by blast
   then have \<open>peval g h (ps \<^bold>\<leadsto>\<^sub>! r)\<close> \<open>\<not> peval g h (qs \<^bold>\<leadsto>\<^sub>! r)\<close>
     by simp_all
   then consider (np) \<open>\<exists>p \<in> set ps. \<not> peval g h p\<close> | (r) \<open>\<forall>p \<in> set ps. peval g h p\<close> \<open>peval g h r\<close>
     by (induct ps) auto
   then show False
   proof cases
     case np
     then have \<open>\<exists>p \<in> set qs. \<not> peval g h p\<close>
       using \<open>set ps \<subseteq> set qs\<close> by blast
     then have \<open>peval g h (qs \<^bold>\<leadsto>\<^sub>! r)\<close>
       by (induct qs) simp_all
     then show ?thesis
       using \<open>\<not> peval g h (qs \<^bold>\<leadsto>\<^sub>! r)\<close> by blast
   next
     case r
     then have \<open>peval g h (qs \<^bold>\<leadsto>\<^sub>! r)\<close>
       by (induct qs) simp_all
     then show ?thesis
       using \<open>\<not> peval g h (qs \<^bold>\<leadsto>\<^sub>! r)\<close> by blast
   qed
 qed
 
 lemma PK_imply_weaken:
-  assumes \<open>A \<turnstile>\<^sub>! ps \<^bold>\<leadsto>\<^sub>! q\<close> \<open>set ps \<subseteq> set ps'\<close>
-  shows \<open>A \<turnstile>\<^sub>! ps' \<^bold>\<leadsto>\<^sub>! q\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! ps \<^bold>\<leadsto>\<^sub>! q\<close> \<open>set ps \<subseteq> set ps'\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! ps' \<^bold>\<leadsto>\<^sub>! q\<close>
 proof -
   have \<open>ptautology (ps \<^bold>\<leadsto>\<^sub>! q \<^bold>\<longrightarrow>\<^sub>! ps' \<^bold>\<leadsto>\<^sub>! q)\<close>
     using \<open>set ps \<subseteq> set ps'\<close> ptautology_imply_superset by blast
-  then have \<open>A \<turnstile>\<^sub>! ps \<^bold>\<leadsto>\<^sub>! q \<^bold>\<longrightarrow>\<^sub>! ps' \<^bold>\<leadsto>\<^sub>! q\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! ps \<^bold>\<leadsto>\<^sub>! q \<^bold>\<longrightarrow>\<^sub>! ps' \<^bold>\<leadsto>\<^sub>! q\<close>
     using PA1 by blast
   then show ?thesis
-    using \<open>A \<turnstile>\<^sub>! ps \<^bold>\<leadsto>\<^sub>! q\<close> PR1 by blast
+    using \<open>A; B \<turnstile>\<^sub>! ps \<^bold>\<leadsto>\<^sub>! q\<close> PR1 by blast
 qed
 
 lemma implyP_append: \<open>(ps @ ps' \<^bold>\<leadsto>\<^sub>! q) = (ps \<^bold>\<leadsto>\<^sub>! ps' \<^bold>\<leadsto>\<^sub>! q)\<close>
   by (induct ps) simp_all
 
 lemma PK_ImpI:
-  assumes \<open>A \<turnstile>\<^sub>! p # G \<^bold>\<leadsto>\<^sub>! q\<close>
-  shows \<open>A \<turnstile>\<^sub>! G \<^bold>\<leadsto>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p # G \<^bold>\<leadsto>\<^sub>! q\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! G \<^bold>\<leadsto>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
 proof -
   have \<open>set (p # G) \<subseteq> set (G @ [p])\<close>
     by simp
-  then have \<open>A \<turnstile>\<^sub>! G @ [p] \<^bold>\<leadsto>\<^sub>! q\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! G @ [p] \<^bold>\<leadsto>\<^sub>! q\<close>
     using assms PK_imply_weaken by blast
-  then have \<open>A \<turnstile>\<^sub>! G \<^bold>\<leadsto>\<^sub>! [p] \<^bold>\<leadsto>\<^sub>! q\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! G \<^bold>\<leadsto>\<^sub>! [p] \<^bold>\<leadsto>\<^sub>! q\<close>
     using implyP_append by metis
   then show ?thesis
     by simp
 qed
 
-corollary soundness_imply:
+corollary soundness_imply\<^sub>P:
   assumes
     \<open>\<And>M p w. A p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
-    \<open>\<And>M p. P M \<Longrightarrow> P (restrict M p)\<close>
-  shows \<open>A \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> \<forall>q \<in> set qs. M, w \<Turnstile>\<^sub>! q \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
+    \<open>\<And>M r. P M \<Longrightarrow> B r \<Longrightarrow> P (restrict M r)\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> \<forall>q \<in> set qs. M, w \<Turnstile>\<^sub>! q \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
 proof (induct qs arbitrary: p)
   case Nil
   then show ?case
-    using soundness[of A P p M w] assms by simp
+    using soundness\<^sub>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:
+theorem strong_soundness\<^sub>P:
   assumes
     \<open>\<And>M w p. A p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
-    \<open>\<And>M p. P M \<Longrightarrow> P (restrict M p)\<close>
- shows \<open>A, G \<turnstile>\<^sub>! p \<Longrightarrow> valid\<^sub>!\<star> P G p\<close>
+    \<open>\<And>M r. P M \<Longrightarrow> B r \<Longrightarrow> P (restrict M r)\<close>
+  shows \<open>A; B; G \<turnstile>\<^sub>! p \<Longrightarrow> valid\<^sub>!\<star> P G p\<close>
 proof safe
   fix qs w and M :: \<open>('a, 'b) kripke\<close>
-  assume \<open>A \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p\<close>
+  assume \<open>A; B \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p\<close>
   moreover assume \<open>set qs \<subseteq> G\<close> \<open>\<forall>q \<in> G. M, w \<Turnstile>\<^sub>! q\<close>
   then have \<open>\<forall>q \<in> set qs. M, w \<Turnstile>\<^sub>! q\<close>
     using \<open>set qs \<subseteq> G\<close> by blast
   moreover assume \<open>P M\<close> \<open>w \<in> \<W> M\<close>
   ultimately show \<open>M, w \<Turnstile>\<^sub>! p\<close>
-    using soundness_imply[of A P qs p] assms by blast
+    using soundness_imply\<^sub>P[of A P B qs p] assms by blast
 qed
 
 section \<open>Completeness\<close>
 
 lemma ConE:
-  assumes \<open>A \<turnstile>\<^sub>! p \<^bold>\<and>\<^sub>! q\<close>
-  shows \<open>A \<turnstile>\<^sub>! p\<close> \<open>A \<turnstile>\<^sub>! q\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<and>\<^sub>! q\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p\<close> \<open>A; B \<turnstile>\<^sub>! q\<close>
   using assms by (metis PA1 PR1 peval.simps(4-5))+
 
 lemma Iff_Dis:
-  assumes \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! q'\<close>
-  shows \<open>A \<turnstile>\<^sub>! ((p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<or>\<^sub>! q'))\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A; B \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! q'\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! ((p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<or>\<^sub>! q'))\<close>
 proof -
-  have \<open>A \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<or>\<^sub>! q'))\<close>
+  have \<open>A; B \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<or>\<^sub>! q'))\<close>
     by (simp add: PA1)
   then show ?thesis
     using assms PR1 by blast
 qed
 
 lemma Iff_Con:
-  assumes \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! q'\<close>
-  shows \<open>A \<turnstile>\<^sub>! (p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<and>\<^sub>! q')\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A; B \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! q'\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! (p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<and>\<^sub>! q')\<close>
 proof -
-  have \<open>A \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<and>\<^sub>! q'))\<close>
+  have \<open>A; B \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<and>\<^sub>! q'))\<close>
     by (simp add: PA1)
   then show ?thesis
     using assms PR1 by blast
 qed
 
 lemma Iff_Imp:
-  assumes \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! q'\<close>
-  shows \<open>A \<turnstile>\<^sub>! ((p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<longrightarrow>\<^sub>! q'))\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A; B \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! q'\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! ((p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<longrightarrow>\<^sub>! q'))\<close>
 proof -
-  have \<open>A \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<longrightarrow>\<^sub>! q'))\<close>
+  have \<open>A; B \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<longrightarrow>\<^sub>! q'))\<close>
     by (simp add: PA1)
   then show ?thesis
     using assms PR1 by blast
 qed
 
-lemma Iff_sym: \<open>(A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! q) = (A \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! p)\<close>
+lemma Iff_sym: \<open>(A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! q) = (A; B \<turnstile>\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! p)\<close>
 proof -
-  have \<open>A \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! p)\<close>
+  have \<open>A; B \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! p)\<close>
     by (simp add: PA1)
   then show ?thesis
     using PR1 ConE by blast
 qed
 
 lemma Iff_Iff:
-  assumes \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! q\<close>
-  shows \<open>A \<turnstile>\<^sub>! p' \<^bold>\<longleftrightarrow>\<^sub>! q\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! q\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p' \<^bold>\<longleftrightarrow>\<^sub>! q\<close>
 proof -
   have \<open>ptautology ((p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! (p' \<^bold>\<longleftrightarrow>\<^sub>! q))\<close>
     by (metis peval.simps(4-5))
-  with PA1 have \<open>A \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! (p' \<^bold>\<longleftrightarrow>\<^sub>! q)\<close> .
+  with PA1 have \<open>A; B \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! (p' \<^bold>\<longleftrightarrow>\<^sub>! q)\<close> .
   then show ?thesis
     using assms PR1 by blast
 qed
 
-lemma K'_A2': \<open>A \<turnstile>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
+lemma K'_A2': \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
 proof -
-  have \<open>A \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<and>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
+  have \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<and>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
     using PA2 by fast
-  moreover have \<open>A \<turnstile>\<^sub>! (P \<^bold>\<and>\<^sub>! Q \<^bold>\<longrightarrow>\<^sub>! R) \<^bold>\<longrightarrow>\<^sub>! (Q \<^bold>\<longrightarrow>\<^sub>! P \<^bold>\<longrightarrow>\<^sub>! R)\<close> for P Q R
+  moreover have \<open>A; B \<turnstile>\<^sub>! (P \<^bold>\<and>\<^sub>! Q \<^bold>\<longrightarrow>\<^sub>! R) \<^bold>\<longrightarrow>\<^sub>! (Q \<^bold>\<longrightarrow>\<^sub>! P \<^bold>\<longrightarrow>\<^sub>! R)\<close> for P Q R
     by (simp add: PA1)
   ultimately show ?thesis
     using PR1 by fast
 qed
 
 lemma K'_map:
-  assumes \<open>A \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q\<close>
-  shows \<open>A \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
 proof -
-  note \<open>A \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q\<close>
-  then have \<open>A \<turnstile>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
+  note \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
     using PR2 by fast
-  moreover have \<open>A \<turnstile>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
+  moreover have \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q\<close>
     using K'_A2' by fast
   ultimately show ?thesis
     using PR1 by fast
 qed
 
 lemma ConI:
-  assumes \<open>A \<turnstile>\<^sub>! p\<close> \<open>A \<turnstile>\<^sub>! q\<close>
-  shows \<open>A \<turnstile>\<^sub>! p \<^bold>\<and>\<^sub>! q\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p\<close> \<open>A; B \<turnstile>\<^sub>! q\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<and>\<^sub>! q\<close>
 proof -
-  have \<open>A \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q \<^bold>\<longrightarrow>\<^sub>! p \<^bold>\<and>\<^sub>! q\<close>
+  have \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! q \<^bold>\<longrightarrow>\<^sub>! p \<^bold>\<and>\<^sub>! q\<close>
     by (simp add: PA1)
   then show ?thesis
     using assms PR1 by blast
 qed
 
 lemma Iff_wk:
-  assumes \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! q\<close>
-  shows \<open>A \<turnstile>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! q)\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! q\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! q)\<close>
 proof -
-  have \<open>A \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! q))\<close>
+  have \<open>A; B \<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! q))\<close>
     by (simp add: PA1)
   then show ?thesis
     using assms PR1 by blast
 qed
 
 lemma Iff_reduce':
   assumes \<open>static p\<close>
-  shows \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' r p\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' r p\<close>
   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 \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<or>\<^sub>! q)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<or>\<^sub>! q)\<close>
     using Iff_Dis by fastforce
-  moreover have \<open>A \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<or>\<^sub>! q))\<close>
+  moreover have \<open>A; B \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<or>\<^sub>! q))\<close>
     using PDis Iff_sym by fastforce
   ultimately show ?case
     using PA1 PR1 Iff_Iff by blast
 next
   case (Con p q)
-  then have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<and>\<^sub>! q)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<and>\<^sub>! q)\<close>
     using Iff_Con by fastforce
-  moreover have \<open>A \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<and>\<^sub>! q))\<close>
+  moreover have \<open>A; B \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<and>\<^sub>! q))\<close>
     using PCon Iff_sym by fastforce
   ultimately show ?case
     using PA1 PR1 Iff_Iff by blast
 next
   case (Imp p q)
-  then have \<open>A \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
     using Iff_Imp by fastforce
-  moreover have \<open>A \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q))\<close>
+  moreover have \<open>A; B \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q))\<close>
     using PImp Iff_sym by fastforce
   ultimately show ?case
     using PA1 PR1 Iff_Iff by blast
 next
   case (K' i p)
-  then have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' r p\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' r p\<close>
     by simp
-  then have \<open>A \<turnstile>\<^sub>! K\<^sub>! i ([r]\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i (reduce' r p)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i ([r]\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i (reduce' r p)\<close>
     using K'_map ConE ConI by metis
-  moreover have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i ([r]\<^sub>! p)\<close>
+  moreover have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i ([r]\<^sub>! p)\<close>
     using PK .
-  ultimately have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce' r p)\<close>
+  ultimately have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce' r p)\<close>
     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: \<open>A \<turnstile>\<^sub>! r \<^bold>\<longleftrightarrow>\<^sub>! r'\<close> and \<open>static p\<close>
-  shows \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p\<close>
+  assumes r: \<open>A; B \<turnstile>\<^sub>! r \<^bold>\<longleftrightarrow>\<^sub>! r'\<close> and \<open>static p\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p\<close>
   using assms(2-)
 proof (induct p)
   case FF
-  have \<open>A \<turnstile>\<^sub>! (r \<^bold>\<longleftrightarrow>\<^sub>! r') \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!))\<close>
+  have \<open>A; B \<turnstile>\<^sub>! (r \<^bold>\<longleftrightarrow>\<^sub>! r') \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!))\<close>
     by (auto intro: PA1)
-  then have \<open>A \<turnstile>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!)\<close>
     using r PR1 by blast
   then show ?case
     by (meson PFF Iff_Iff Iff_sym)
 next
   case (Pro' x)
-  have \<open>A \<turnstile>\<^sub>! (r \<^bold>\<longleftrightarrow>\<^sub>! r') \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x))\<close>
+  have \<open>A; B \<turnstile>\<^sub>! (r \<^bold>\<longleftrightarrow>\<^sub>! r') \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x))\<close>
     by (auto intro: PA1)
-  then have \<open>A \<turnstile>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x)\<close>
     using r PR1 by blast
   then show ?case
     by (meson PPro Iff_Iff Iff_sym)
 next
   case (Dis p q)
-  then have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p \<^bold>\<or>\<^sub>! [r']\<^sub>! q\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p \<^bold>\<or>\<^sub>! [r']\<^sub>! q\<close>
     by (simp add: Iff_Dis)
   then show ?case
     by (meson PDis Iff_Iff Iff_sym)
 next
   case (Con p q)
-  then have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p \<^bold>\<and>\<^sub>! [r']\<^sub>! q\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p \<^bold>\<and>\<^sub>! [r']\<^sub>! q\<close>
     by (simp add: Iff_Con)
   then show ?case
     by (meson PCon Iff_Iff Iff_sym)
 next
   case (Imp p q)
-  then have \<open>A \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r']\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r']\<^sub>! q)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r']\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r']\<^sub>! q)\<close>
     by (simp add: Iff_Imp)
   then show ?case
     by (meson PImp Iff_Iff Iff_sym)
 next
   case (K' i p)
-  then have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p\<close>
     by simp
-  then have \<open>A \<turnstile>\<^sub>! K\<^sub>! i ([r]\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i ([r']\<^sub>! p)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i ([r]\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i ([r']\<^sub>! p)\<close>
     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 \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close>
-  shows \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p'\<close>
+  assumes \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! p'\<close> and \<open>B r\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p'\<close>
   using assms PAnn ConE ConI PImp PR1 by metis
 
-lemma Iff_reduce: \<open>A \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce p\<close>
+lemma Iff_reduce:
+  assumes \<open>\<forall>r \<in> anns p. B r\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce p\<close>
+  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)
-  have
-    \<open>A \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce p)\<close>
-    \<open>A \<turnstile>\<^sub>! K\<^sub>! i (reduce p) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p\<close>
-    using K' K'_map ConE by fast+
-  then have \<open>A \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i (reduce p)\<close>
+  then have
+    \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce p)\<close>
+    \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i (reduce p) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p\<close>
+    using K'_map ConE by fastforce+
+  then have \<open>A; B \<turnstile>\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i (reduce p)\<close>
     using ConI by blast
   then show ?case
     by simp
 next
   case (Ann r p)
-  have \<open>A \<turnstile>\<^sub>! [reduce r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p)\<close>
+  then have \<open>B r\<close>
+    by simp
+  have \<open>A; B \<turnstile>\<^sub>! [reduce r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p)\<close>
     using Iff_reduce' static_reduce by blast
-  moreover have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! [reduce r]\<^sub>! reduce p\<close>
-    using Ann(1) Iff_Ann1 static_reduce by blast
-  ultimately have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p)\<close>
+  moreover have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! [reduce r]\<^sub>! reduce p\<close>
+    using Ann Iff_Ann1 static_reduce by fastforce
+  ultimately have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p)\<close>
     using Iff_Iff Iff_sym by blast
-  moreover have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p\<close>
-    by (meson Ann(2) static_reduce Iff_Ann2 Iff_sym)
-  ultimately have \<open>A \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p)\<close>
+  moreover have \<open>\<forall>r \<in> anns p. B r\<close>
+    using Ann.prems by simp
+  then have \<open>A; B \<turnstile>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce p\<close>
+    using Ann.hyps(2) by blast
+  then have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p\<close>
+    using \<open>B r\<close> Iff_Ann2 Iff_sym by blast
+  ultimately have \<open>A; B \<turnstile>\<^sub>! [r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p)\<close>
     using Iff_Iff by blast
   then show ?case
     by simp
 qed (simp_all add: PA1)
 
+lemma anns_implyP [simp]:
+  \<open>anns (ps \<^bold>\<leadsto>\<^sub>! q) =  anns q \<union> (\<Union>p \<in> set ps. anns p)\<close>
+  by (induct ps) auto
+
 lemma strong_completeness\<^sub>P':
   assumes \<open>valid\<^sub>! P G p\<close>
+    and \<open>\<forall>r \<in> anns p. B r\<close> \<open>\<forall>q \<in> G. \<forall>r \<in> anns q. B r\<close>
     and \<open>valid\<star> P (lower ` reduce ` G) (lower (reduce p)) \<Longrightarrow>
-      A o lift, lower ` reduce ` G \<turnstile> lower (reduce p)\<close>
-  shows \<open>A, G \<turnstile>\<^sub>! p\<close>
+      A o lift; lower ` reduce ` G \<turnstile> lower (reduce p)\<close>
+  shows \<open>A; B; G \<turnstile>\<^sub>! p\<close>
 proof -
   have \<open>valid\<^sub>! P (reduce ` G) (reduce p)\<close>
     using assms(1) reduce_semantics by fast
   moreover have \<open>static (reduce p)\<close> \<open>\<forall>q \<in> reduce ` G. static q\<close>
     using static_reduce by fast+
-  ultimately have \<open>A, reduce ` G \<turnstile>\<^sub>! reduce p\<close>
-    using assms(2) strong_static_completeness'[where G=\<open>reduce ` G\<close> and p=\<open>reduce p\<close>]
+  ultimately have \<open>A; B; reduce ` G \<turnstile>\<^sub>! reduce p\<close>
+    using assms(4) strong_static_completeness'[where G=\<open>reduce ` G\<close> and p=\<open>reduce p\<close>]
     by presburger
-  then have \<open>\<exists>qs. set qs \<subseteq> G \<and> (A \<turnstile>\<^sub>! map reduce qs \<^bold>\<leadsto>\<^sub>! reduce p)\<close>
+  then have \<open>\<exists>qs. set qs \<subseteq> G \<and> (A; B \<turnstile>\<^sub>! map reduce qs \<^bold>\<leadsto>\<^sub>! reduce p)\<close>
     using set_map_inv by fast
-  then obtain qs where qs: \<open>set qs \<subseteq> G\<close> and \<open>A \<turnstile>\<^sub>! map reduce qs \<^bold>\<leadsto>\<^sub>! reduce p\<close>
+  then obtain qs where qs: \<open>set qs \<subseteq> G\<close> and \<open>A; B \<turnstile>\<^sub>! map reduce qs \<^bold>\<leadsto>\<^sub>! reduce p\<close>
     by blast
-  then have \<open>A \<turnstile>\<^sub>! reduce (qs \<^bold>\<leadsto>\<^sub>! p)\<close>
+  then have \<open>A; B \<turnstile>\<^sub>! reduce (qs \<^bold>\<leadsto>\<^sub>! p)\<close>
     using reduce_implyP by metis
-  moreover have \<open>A \<turnstile>\<^sub>! (qs \<^bold>\<leadsto>\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! reduce (qs \<^bold>\<leadsto>\<^sub>! p)\<close>
+  moreover have \<open>\<forall>r \<in> anns (qs \<^bold>\<leadsto>\<^sub>! p). B r\<close>
+    using assms(2-3) qs by auto
+  then have \<open>A; B \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce (qs \<^bold>\<leadsto>\<^sub>! p)\<close>
     using Iff_reduce by blast
-  ultimately have \<open>A \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p\<close>
+  ultimately have \<open>A; B \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p\<close>
     using ConE(2) PR1 by blast
   then show ?thesis
     using qs by blast
 qed
 
 theorem strong_completeness\<^sub>P:
   assumes \<open>valid\<^sub>! P G p\<close>
-    and \<open>\<And>G p. valid\<star> P G p \<Longrightarrow> A o lift, G \<turnstile> p\<close>
-  shows \<open>\<exists>qs. set qs \<subseteq> G \<and> (A \<turnstile>\<^sub>! qs \<^bold>\<leadsto>\<^sub>! p)\<close>
+    and \<open>\<forall>r \<in> anns p. B r\<close> \<open>\<forall>q \<in> G. \<forall>r \<in> anns q. B r\<close>
+    and \<open>\<And>G p. valid\<star> P G p \<Longrightarrow> A o lift; G \<turnstile> p\<close>
+  shows \<open>A; B; G \<turnstile>\<^sub>! p\<close>
   using strong_completeness\<^sub>P' assms .
 
+theorem main\<^sub>P:
+  assumes \<open>\<And>M w p. A p \<Longrightarrow> P M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
+    and \<open>\<And>M r. P M \<Longrightarrow> B r \<Longrightarrow> P (restrict M r)\<close>
+    and \<open>\<forall>r \<in> anns p. B r\<close> \<open>\<forall>q \<in> G. \<forall>r \<in> anns q. B r\<close>
+    and \<open>\<And>G p. valid\<star> P G p \<Longrightarrow> A o lift; G \<turnstile> p\<close>
+  shows \<open>valid\<^sub>! P G p \<longleftrightarrow> A; B; G \<turnstile>\<^sub>! p\<close>
+  using strong_soundness\<^sub>P[of A P B G p] strong_completeness\<^sub>P[of P G p B A] assms by blast
+
+corollary strong_completeness\<^sub>P\<^sub>B:
+  assumes \<open>valid\<^sub>! P G p\<close>
+    and \<open>\<And>G p. valid\<star> P G p \<Longrightarrow> A o lift; G \<turnstile> p\<close>
+  shows \<open>A; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
+  using strong_completeness\<^sub>P[where B=\<open>\<lambda>_. True\<close>] assms by blast
+
 corollary completeness\<^sub>P':
-  assumes \<open>valid\<^sub>! P {} p\<close> and \<open>\<And>p. valid P {} (lower p) \<Longrightarrow> A o lift \<turnstile> lower p\<close>
-  shows \<open>A \<turnstile>\<^sub>! p\<close>
+  assumes \<open>valid\<^sub>! P {} p\<close>
+    and \<open>\<forall>r \<in> anns p. B r\<close>
+    and \<open>\<And>p. valid P {} (lower p) \<Longrightarrow> A o lift \<turnstile> lower p\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p\<close>
   using assms strong_completeness\<^sub>P'[where P=P and G=\<open>{}\<close>] by simp
 
 corollary completeness\<^sub>P:
-  assumes \<open>valid\<^sub>! P {} p\<close> and \<open>\<And>p. valid P {} p \<Longrightarrow> A o lift \<turnstile> p\<close>
-  shows \<open>A \<turnstile>\<^sub>! p\<close>
+  assumes \<open>valid\<^sub>! P {} p\<close>
+    and \<open>\<forall>r \<in> anns p. B r\<close>
+    and \<open>\<And>p. valid P {} p \<Longrightarrow> A o lift \<turnstile> p\<close>
+  shows \<open>A; B \<turnstile>\<^sub>! p\<close>
   using completeness\<^sub>P' assms .
 
 corollary completeness\<^sub>P\<^sub>A:
   assumes \<open>valid\<^sub>! (\<lambda>_. True) {} p\<close>
-  shows \<open>A \<turnstile>\<^sub>! p\<close>
-  using assms completeness\<^sub>P[where P=\<open>\<lambda>_. True\<close> and p=p] completeness\<^sub>A by blast
+  shows \<open>A; (\<lambda>_. True) \<turnstile>\<^sub>! p\<close>
+  using assms completeness\<^sub>P[of \<open>\<lambda>_. True\<close> p \<open>\<lambda>_. True\<close>] completeness\<^sub>A by blast
 
 section \<open>System PAL + K\<close>
 
 abbreviation SystemPK (\<open>_ \<turnstile>\<^sub>!\<^sub>K _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>!\<^sub>K p \<equiv> (\<lambda>_. False), G \<turnstile>\<^sub>! p\<close>
+  \<open>G \<turnstile>\<^sub>!\<^sub>K p \<equiv> (\<lambda>_. False); (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
 
 lemma strong_soundness\<^sub>P\<^sub>K: \<open>G \<turnstile>\<^sub>!\<^sub>K p \<Longrightarrow> valid\<^sub>!\<star> (\<lambda>_. True) G p\<close>
-  using strong_soundness[of \<open>\<lambda>_. False\<close> \<open>\<lambda>_. True\<close>] by fast
+  using strong_soundness\<^sub>P[of \<open>\<lambda>_. False\<close> \<open>\<lambda>_. True\<close>] by fast
 
 abbreviation validPK (\<open>valid\<^sub>!\<^sub>K\<close>) where
   \<open>valid\<^sub>!\<^sub>K \<equiv> valid\<^sub>! (\<lambda>_. True)\<close>
 
 lemma strong_completeness\<^sub>P\<^sub>K:
   assumes \<open>valid\<^sub>!\<^sub>K G p\<close>
   shows \<open>G \<turnstile>\<^sub>!\<^sub>K p\<close>
-  using strong_completeness\<^sub>P assms strong_completeness\<^sub>K unfolding comp_apply .
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>K unfolding comp_apply .
 
 theorem main\<^sub>P\<^sub>K: \<open>valid\<^sub>!\<^sub>K G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>K p\<close>
   using strong_soundness\<^sub>P\<^sub>K[of G p] strong_completeness\<^sub>P\<^sub>K[of G p] by fast
 
 corollary \<open>valid\<^sub>!\<^sub>K G p \<Longrightarrow> valid\<^sub>!\<star> (\<lambda>_. True) G p\<close>
   using strong_soundness\<^sub>P\<^sub>K[of G p] strong_completeness\<^sub>P\<^sub>K[of G p] by fast
 
 section \<open>System PAL + T\<close>
 
 text \<open>Also known as System PAL + M\<close>
 
 inductive AxPT :: \<open>'i pfm \<Rightarrow> bool\<close> where
   \<open>AxPT (K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! p)\<close>
 
 abbreviation SystemPT (\<open>_ \<turnstile>\<^sub>!\<^sub>T _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>!\<^sub>T p \<equiv> AxPT, G \<turnstile>\<^sub>! p\<close>
+  \<open>G \<turnstile>\<^sub>!\<^sub>T p \<equiv> AxPT; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
 
 lemma soundness_AxPT: \<open>AxPT p \<Longrightarrow> reflexive M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
   unfolding reflexive_def by (induct p rule: AxPT.induct) simp
 
 lemma reflexive_restrict: \<open>reflexive M \<Longrightarrow> reflexive (restrict M p)\<close>
   unfolding reflexive_def by simp
 
 lemma strong_soundness\<^sub>P\<^sub>T: \<open>G \<turnstile>\<^sub>!\<^sub>T p \<Longrightarrow> valid\<^sub>!\<star> reflexive G p\<close>
-  using strong_soundness[of AxPT reflexive G p] soundness_AxPT reflexive_restrict by fast
+  using strong_soundness\<^sub>P[of AxPT reflexive \<open>\<lambda>_. True\<close> G p]
+    soundness_AxPT reflexive_restrict by fast
 
 lemma AxT_AxPT: \<open>AxT = AxPT o lift\<close>
   unfolding comp_apply using lower_lift
   by (metis AxPT.simps AxT.simps lift.simps(5-6) lower.simps(5-6))
 
 abbreviation validPT (\<open>valid\<^sub>!\<^sub>T\<close>) where
   \<open>valid\<^sub>!\<^sub>T \<equiv> valid\<^sub>! reflexive\<close>
 
 lemma strong_completeness\<^sub>P\<^sub>T:
   assumes \<open>valid\<^sub>!\<^sub>T G p\<close>
   shows \<open>G \<turnstile>\<^sub>!\<^sub>T p\<close>
-  using strong_completeness\<^sub>P assms strong_completeness\<^sub>T unfolding AxT_AxPT .
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>T unfolding AxT_AxPT .
 
 theorem main\<^sub>P\<^sub>T: \<open>valid\<^sub>!\<^sub>T G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>T p\<close>
   using strong_soundness\<^sub>P\<^sub>T[of G p] strong_completeness\<^sub>P\<^sub>T[of G p] by fast
 
 corollary \<open>valid\<^sub>!\<^sub>T G p \<Longrightarrow> valid\<^sub>!\<star> reflexive G p\<close>
   using strong_soundness\<^sub>P\<^sub>T[of G p] strong_completeness\<^sub>P\<^sub>T[of G p] by fast
 
 section \<open>System PAL + KB\<close>
 
 inductive AxPB :: \<open>'i pfm \<Rightarrow> bool\<close> where
   \<open>AxPB (p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (L\<^sub>! i p))\<close>
 
 abbreviation SystemPKB (\<open>_ \<turnstile>\<^sub>!\<^sub>K\<^sub>B _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>B p \<equiv> AxPB, G \<turnstile>\<^sub>! p\<close>
+  \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>B p \<equiv> AxPB; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
 
 lemma soundness_AxPB: \<open>AxPB p \<Longrightarrow> symmetric M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
   unfolding symmetric_def by (induct p rule: AxPB.induct) auto
 
 lemma symmetric_restrict: \<open>symmetric M \<Longrightarrow> symmetric (restrict M p)\<close>
   unfolding symmetric_def by simp
 
 lemma strong_soundness\<^sub>P\<^sub>K\<^sub>B: \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>B p \<Longrightarrow> valid\<^sub>!\<star> symmetric G p\<close>
-  using strong_soundness[of AxPB symmetric G p] soundness_AxPB symmetric_restrict by fast
+  using strong_soundness\<^sub>P[of AxPB symmetric \<open>\<lambda>_. True\<close> G p]
+    soundness_AxPB symmetric_restrict by fast
 
 lemma AxB_AxPB: \<open>AxB = AxPB o lift\<close>
 proof
   fix p :: \<open>'i fm\<close>
   show \<open>AxB p = (AxPB \<circ> lift) p\<close>
     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 (\<open>valid\<^sub>!\<^sub>K\<^sub>B\<close>) where
   \<open>valid\<^sub>!\<^sub>K\<^sub>B \<equiv> valid\<^sub>! symmetric\<close>
 
 lemma strong_completeness\<^sub>P\<^sub>K\<^sub>B:
   assumes \<open>valid\<^sub>!\<^sub>K\<^sub>B G p\<close>
   shows \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>B p\<close>
-  using strong_completeness\<^sub>P assms strong_completeness\<^sub>K\<^sub>B unfolding AxB_AxPB .
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>K\<^sub>B unfolding AxB_AxPB .
 
 theorem main\<^sub>P\<^sub>K\<^sub>B: \<open>valid\<^sub>!\<^sub>K\<^sub>B G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>K\<^sub>B p\<close>
   using strong_soundness\<^sub>P\<^sub>K\<^sub>B[of G p] strong_completeness\<^sub>P\<^sub>K\<^sub>B[of G p] by fast
 
 corollary \<open>valid\<^sub>!\<^sub>K\<^sub>B G p \<Longrightarrow> valid\<^sub>!\<star> symmetric G p\<close>
   using strong_soundness\<^sub>P\<^sub>K\<^sub>B[of G p] strong_completeness\<^sub>P\<^sub>K\<^sub>B[of G p] by fast
 
 section \<open>System PAL + K4\<close>
 
 inductive AxP4 :: \<open>'i pfm \<Rightarrow> bool\<close> where
   \<open>AxP4 (K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (K\<^sub>! i p))\<close>
 
 abbreviation SystemPK4 (\<open>_ \<turnstile>\<^sub>!\<^sub>K\<^sub>4 _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>4 p \<equiv> AxP4, G \<turnstile>\<^sub>! p\<close>
+  \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>4 p \<equiv> AxP4; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
 
 lemma pos_introspection:
   assumes \<open>transitive M\<close> \<open>w \<in> \<W> M\<close>
   shows \<open>M, w \<Turnstile>\<^sub>! (K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (K\<^sub>! i p))\<close>
 proof -
   { assume \<open>M, w \<Turnstile>\<^sub>! K\<^sub>! i p\<close>
     then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile>\<^sub>! p\<close>
       by simp
     then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. \<forall>u \<in> \<W> M \<inter> \<K> M i v. M, u \<Turnstile>\<^sub>! p\<close>
       using \<open>transitive M\<close> \<open>w \<in> \<W> M\<close> unfolding transitive_def by blast
     then have \<open>\<forall>v \<in> \<W> M \<inter> \<K> M i w. M, v \<Turnstile>\<^sub>! K\<^sub>! i p\<close>
       by simp
     then have \<open>M, w \<Turnstile>\<^sub>! K\<^sub>! i (K\<^sub>! i p)\<close>
       by simp }
   then show ?thesis
     by fastforce
 qed
 
 lemma soundness_AxP4: \<open>AxP4 p \<Longrightarrow> transitive M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
   by (induct p rule: AxP4.induct) (metis pos_introspection)
 
 lemma transitive_restrict: \<open>transitive M \<Longrightarrow> transitive (restrict M p)\<close>
   unfolding transitive_def
   by (metis (no_types, lifting) kripke.exhaust_sel kripke.inject mem_Collect_eq restrict.elims)
 
 lemma strong_soundness\<^sub>P\<^sub>K\<^sub>4: \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>4 p \<Longrightarrow> valid\<^sub>!\<star> transitive G p\<close>
-  using strong_soundness[of AxP4 transitive G p] soundness_AxP4 transitive_restrict by fast
+  using strong_soundness\<^sub>P[of AxP4 transitive \<open>\<lambda>_. True\<close> G p]
+    soundness_AxP4 transitive_restrict by fast
 
 lemma Ax4_AxP4: \<open>Ax4 = AxP4 o lift\<close>
 proof
   fix p :: \<open>'i fm\<close>
   show \<open>Ax4 p = (AxP4 \<circ> lift) p\<close>
     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 (\<open>valid\<^sub>!\<^sub>K\<^sub>4\<close>) where
   \<open>valid\<^sub>!\<^sub>K\<^sub>4 \<equiv> valid\<^sub>! transitive\<close>
 
 lemma strong_completeness\<^sub>P\<^sub>K\<^sub>4:
   assumes \<open>valid\<^sub>!\<^sub>K\<^sub>4 G p\<close>
   shows \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>4 p\<close>
-  using strong_completeness\<^sub>P assms strong_completeness\<^sub>K\<^sub>4 unfolding Ax4_AxP4 .
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>K\<^sub>4 unfolding Ax4_AxP4 .
 
 theorem main\<^sub>P\<^sub>K\<^sub>4: \<open>valid\<^sub>!\<^sub>K\<^sub>4 G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>K\<^sub>4 p\<close>
   using strong_soundness\<^sub>P\<^sub>K\<^sub>4[of G p] strong_completeness\<^sub>P\<^sub>K\<^sub>4[of G p] by fast
 
 corollary \<open>valid\<^sub>!\<^sub>K\<^sub>4 G p \<Longrightarrow> valid\<^sub>!\<star> transitive G p\<close>
   using strong_soundness\<^sub>P\<^sub>K\<^sub>4[of G p] strong_completeness\<^sub>P\<^sub>K\<^sub>4[of G p] by fast
 
+section \<open>System PAL + K5\<close>
+
+inductive AxP5 :: \<open>'i pfm \<Rightarrow> bool\<close> where
+  \<open>AxP5 (L\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (L\<^sub>! i p))\<close>
+
+abbreviation SystemPK5 (\<open>_ \<turnstile>\<^sub>!\<^sub>K\<^sub>5 _\<close> [50, 50] 50) where
+  \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>5 p \<equiv> AxP5; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
+
+lemma soundness_AxP5: \<open>AxP5 p \<Longrightarrow> Euclidean M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
+  by (induct p rule: AxP5.induct) (unfold Euclidean_def psemantics.simps, blast)
+
+lemma Euclidean_restrict: \<open>Euclidean M \<Longrightarrow> Euclidean (restrict M p)\<close>
+  unfolding Euclidean_def by auto
+
+lemma strong_soundness\<^sub>P\<^sub>K\<^sub>5: \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>5 p \<Longrightarrow> valid\<^sub>!\<star> Euclidean G p\<close>
+  using strong_soundness\<^sub>P[of AxP5 Euclidean \<open>\<lambda>_. True\<close> G p]
+    soundness_AxP5 Euclidean_restrict by fast
+
+lemma Ax5_AxP5: \<open>Ax5 = AxP5 o lift\<close>
+proof
+  fix p :: \<open>'i fm\<close>
+  show \<open>Ax5 p = (AxP5 \<circ> lift) p\<close>
+    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 (\<open>valid\<^sub>!\<^sub>K\<^sub>5\<close>) where
+  \<open>valid\<^sub>!\<^sub>K\<^sub>5 \<equiv> valid\<^sub>! Euclidean\<close>
+
+lemma strong_completeness\<^sub>P\<^sub>K\<^sub>5:
+  assumes \<open>valid\<^sub>!\<^sub>K\<^sub>5 G p\<close>
+  shows \<open>G \<turnstile>\<^sub>!\<^sub>K\<^sub>5 p\<close>
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>K\<^sub>5 unfolding Ax5_AxP5 .
+
+theorem main\<^sub>P\<^sub>K\<^sub>5: \<open>valid\<^sub>!\<^sub>K\<^sub>5 G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>K\<^sub>5 p\<close>
+  using strong_soundness\<^sub>P\<^sub>K\<^sub>5[of G p] strong_completeness\<^sub>P\<^sub>K\<^sub>5[of G p] by fast
+
+corollary \<open>valid\<^sub>!\<^sub>K\<^sub>5 G p \<Longrightarrow> valid\<^sub>!\<star> Euclidean G p\<close>
+  using strong_soundness\<^sub>P\<^sub>K\<^sub>5[of G p] strong_completeness\<^sub>P\<^sub>K\<^sub>5[of G p] by fast
+
 section \<open>System PAL + S4\<close>
 
 abbreviation SystemPS4 (\<open>_ \<turnstile>\<^sub>!\<^sub>S\<^sub>4 _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>4 p \<equiv> AxPT \<oplus> AxP4, G \<turnstile>\<^sub>! p\<close>
+  \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>4 p \<equiv> AxPT \<oplus> AxP4; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
 
 lemma soundness_AxPT4: \<open>(AxPT \<oplus> AxP4) p \<Longrightarrow> refltrans M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
   using soundness_AxPT soundness_AxP4 by fast
 
 lemma refltrans_restrict: \<open>refltrans M \<Longrightarrow> refltrans (restrict M p)\<close>
   using reflexive_restrict transitive_restrict by blast
 
 lemma strong_soundness\<^sub>P\<^sub>S\<^sub>4: \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>4 p \<Longrightarrow> valid\<^sub>!\<star> refltrans G p\<close>
-  using strong_soundness[of \<open>AxPT \<oplus> AxP4\<close> refltrans G p] soundness_AxPT4 refltrans_restrict by fast
+  using strong_soundness\<^sub>P[of \<open>AxPT \<oplus> AxP4\<close> refltrans \<open>\<lambda>_. True\<close> G p]
+    soundness_AxPT4 refltrans_restrict by fast
 
 lemma AxT4_AxPT4: \<open>(AxT \<oplus> Ax4) = (AxPT \<oplus> AxP4) o lift\<close>
   using AxT_AxPT Ax4_AxP4 unfolding comp_apply by metis
 
 abbreviation validPS4 (\<open>valid\<^sub>!\<^sub>S\<^sub>4\<close>) where
   \<open>valid\<^sub>!\<^sub>S\<^sub>4 \<equiv> valid\<^sub>! refltrans\<close>
 
 theorem strong_completeness\<^sub>P\<^sub>S\<^sub>4:
   assumes \<open>valid\<^sub>!\<^sub>S\<^sub>4 G p\<close>
   shows \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>4 p\<close>
-  using strong_completeness\<^sub>P assms strong_completeness\<^sub>S\<^sub>4 unfolding AxT4_AxPT4 .
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>S\<^sub>4 unfolding AxT4_AxPT4 .
 
 theorem main\<^sub>P\<^sub>S\<^sub>4: \<open>valid\<^sub>!\<^sub>S\<^sub>4 G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>S\<^sub>4 p\<close>
   using strong_soundness\<^sub>P\<^sub>S\<^sub>4[of G p] strong_completeness\<^sub>P\<^sub>S\<^sub>4[of G p] by fast
 
 corollary \<open>valid\<^sub>!\<^sub>S\<^sub>4 G p \<Longrightarrow> valid\<^sub>!\<star> refltrans G p\<close>
   using strong_soundness\<^sub>P\<^sub>S\<^sub>4[of G p] strong_completeness\<^sub>P\<^sub>S\<^sub>4[of G p] by fast
 
 section \<open>System PAL + S5\<close>
 
 abbreviation SystemPS5 (\<open>_ \<turnstile>\<^sub>!\<^sub>S\<^sub>5 _\<close> [50, 50] 50) where
-  \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>5 p \<equiv> AxPT \<oplus> AxPB \<oplus> AxP4, G \<turnstile>\<^sub>! p\<close>
+  \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>5 p \<equiv> AxPT \<oplus> AxPB \<oplus> AxP4; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
 
 abbreviation AxPTB4 :: \<open>'i pfm \<Rightarrow> bool\<close> where
   \<open>AxPTB4 \<equiv> AxPT \<oplus> AxPB \<oplus> AxP4\<close>
 
 lemma soundness_AxPTB4: \<open>AxPTB4 p \<Longrightarrow> equivalence M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
   using soundness_AxPT soundness_AxPB soundness_AxP4 by fast
 
 lemma equivalence_restrict: \<open>equivalence M \<Longrightarrow> equivalence (restrict M p)\<close>
   using reflexive_restrict symmetric_restrict transitive_restrict by blast
 
 lemma strong_soundness\<^sub>P\<^sub>S\<^sub>5: \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>5 p \<Longrightarrow> valid\<^sub>!\<star> equivalence G p\<close>
-  using strong_soundness[of AxPTB4 equivalence G p] soundness_AxPTB4 equivalence_restrict by fast
+  using strong_soundness\<^sub>P[of AxPTB4 equivalence \<open>\<lambda>_. True\<close> G p]
+    soundness_AxPTB4 equivalence_restrict by fast
 
 lemma AxTB4_AxPTB4: \<open>AxTB4 = AxPTB4 o lift\<close>
   using AxT_AxPT AxB_AxPB Ax4_AxP4 unfolding comp_apply by metis
 
 abbreviation validPS5 (\<open>valid\<^sub>!\<^sub>S\<^sub>5\<close>) where
   \<open>valid\<^sub>!\<^sub>S\<^sub>5 \<equiv> valid\<^sub>! equivalence\<close>
 
 theorem strong_completeness\<^sub>P\<^sub>S\<^sub>5:
   assumes \<open>valid\<^sub>!\<^sub>S\<^sub>5 G p\<close>
   shows \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>5 p\<close>
-  using strong_completeness\<^sub>P assms strong_completeness\<^sub>S\<^sub>5 unfolding AxTB4_AxPTB4 .
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>S\<^sub>5 unfolding AxTB4_AxPTB4 .
 
 theorem main\<^sub>P\<^sub>S\<^sub>5: \<open>valid\<^sub>!\<^sub>S\<^sub>5 G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>S\<^sub>5 p\<close>
   using strong_soundness\<^sub>P\<^sub>S\<^sub>5[of G p] strong_completeness\<^sub>P\<^sub>S\<^sub>5[of G p] by fast
 
 corollary \<open>valid\<^sub>!\<^sub>S\<^sub>5 G p \<Longrightarrow> valid\<^sub>!\<star> equivalence G p\<close>
   using strong_soundness\<^sub>P\<^sub>S\<^sub>5[of G p] strong_completeness\<^sub>P\<^sub>S\<^sub>5[of G p] by fast
 
+section \<open>System PAL + S5'\<close>
+
+abbreviation SystemPS5' (\<open>_ \<turnstile>\<^sub>!\<^sub>S\<^sub>5'' _\<close> [50, 50] 50) where
+  \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>5' p \<equiv> AxPT \<oplus> AxP5; (\<lambda>_. True); G \<turnstile>\<^sub>! p\<close>
+
+abbreviation AxPT5 :: \<open>'i pfm \<Rightarrow> bool\<close> where
+  \<open>AxPT5 \<equiv> AxPT \<oplus> AxP5\<close>
+
+lemma soundness_AxPT5: \<open>AxPT5 p \<Longrightarrow> equivalence M \<Longrightarrow> w \<in> \<W> M \<Longrightarrow> M, w \<Turnstile>\<^sub>! p\<close>
+  using soundness_AxPT soundness_AxPT soundness_AxP5 symm_trans_Euclid by fast
+
+lemma strong_soundness\<^sub>P\<^sub>S\<^sub>5': \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>5' p \<Longrightarrow> valid\<^sub>!\<star> equivalence G p\<close>
+  using strong_soundness\<^sub>P[of AxPT5 equivalence \<open>\<lambda>_. True\<close> G p]
+    soundness_AxPT5 equivalence_restrict by fast
+
+lemma AxT5_AxPT5: \<open>AxT5 = AxPT5 o lift\<close>
+  using AxT_AxPT Ax5_AxP5 unfolding comp_apply by metis
+
+theorem strong_completeness\<^sub>P\<^sub>S\<^sub>5':
+  assumes \<open>valid\<^sub>!\<^sub>S\<^sub>5 G p\<close>
+  shows \<open>G \<turnstile>\<^sub>!\<^sub>S\<^sub>5' p\<close>
+  using strong_completeness\<^sub>P\<^sub>B assms strong_completeness\<^sub>S\<^sub>5' unfolding AxT5_AxPT5 .
+
+theorem main\<^sub>P\<^sub>S\<^sub>5': \<open>valid\<^sub>!\<^sub>S\<^sub>5 G p \<longleftrightarrow> G \<turnstile>\<^sub>!\<^sub>S\<^sub>5' p\<close>
+  using strong_soundness\<^sub>P\<^sub>S\<^sub>5'[of G p] strong_completeness\<^sub>P\<^sub>S\<^sub>5'[of G p] by fast
+
 end
diff --git a/thys/Public_Announcement_Logic/document/root.tex b/thys/Public_Announcement_Logic/document/root.tex
--- a/thys/Public_Announcement_Logic/document/root.tex
+++ b/thys/Public_Announcement_Logic/document/root.tex
@@ -1,67 +1,67 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
 \usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
 
 %\usepackage{eurosym}
   %for \<euro>
 
 %\usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 
 %\usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
 
 %\usepackage{textcomp}
   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   %\<currency>
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 
 \begin{document}
 
 \title{Public Announcement Logic}
 \author{Asta Halkjær From}
 \maketitle
 
 \begin{abstract}
   This work is a formalization of public announcement logic with countably many agents.
-  It includes proofs of soundness and completeness for a variant of the axiom system PA + DIST! + NEC!~\cite{WangC13}. The completeness proof builds on the Epistemic Logic theory.
+  It includes proofs of soundness and completeness for variants of the axiom system PA + DIST! + NEC!~\cite{WangC13}. The completeness proofs build on the Epistemic Logic theory.
 \end{abstract}
 
 \tableofcontents
 
 \newpage
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 % optional bibliography
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End: