Theory Stalnaker_Logic

(*
  File:      Stalnaker_Logic.thy
  Author:    Laura Gamboa Guzman

  This work is a formalization of Stalnaker's epistemic logic
  and its soundness and completeness theorems, as well as the 
  equivalence between the axiomatization of S4 available in the Epistemic 
  Logic theory and the topological one.
  It builds on the Epistemic_Logic theory by A.H. From.
*)

theory Stalnaker_Logic
  imports "Epistemic_Logic.Epistemic_Logic"

begin


section ‹Utility›

subsection ‹Some properties of Normal Modal Logics›

lemma duality_taut: ‹tautology (((K i p) ❙⟶ K i (❙¬q))❙⟶ ((L i q) ❙⟶ (❙¬ K i p)))›
  by force

lemma K_imp_trans: 
  assumes ‹A ⊢ (p ❙⟶ q)›  ‹A ⊢ (q ❙⟶ r)›
  shows  ‹A ⊢ (p ❙⟶ r)›
proof - 
  have ‹tautology  ((p ❙⟶ q) ❙⟶ ( (q ❙⟶ r) ❙⟶  (p ❙⟶ r)))›
    by fastforce
  then show ?thesis
    by (meson A1 R1 assms(1) assms(2))
qed

lemma K_imp_trans': 
  assumes ‹A ⊢ (q ❙⟶ r)›
  shows  ‹A ⊢ ((p ❙⟶ q) ❙⟶ (p ❙⟶ r))›
proof - 
  have ‹tautology  ((q ❙⟶ r) ❙⟶ ((p ❙⟶ q) ❙⟶ (p ❙⟶ r)))›
    by fastforce
  then show ?thesis 
    using A1 R1 assms by blast
qed

lemma K_imply_multi:
  assumes ‹A ⊢ (a ❙⟶ b)› and ‹A ⊢ (a ❙⟶ c)›
  shows ‹A ⊢ (a ❙⟶ (b❙∧c))›
proof -
  have ‹tautology ((a❙⟶b)❙⟶(a❙⟶c)❙⟶(a❙⟶(b❙∧c)))›
    by force
  then have ‹A ⊢ ((a❙⟶b)❙⟶(a❙⟶c)❙⟶(a❙⟶(b❙∧c)))›
    using A1 by blast
  then have ‹A ⊢ ((a❙⟶c)❙⟶(a❙⟶(b❙∧c)))›
    using assms(1) R1 by blast
  then show ?thesis 
    using assms(2) R1 by blast
qed

lemma K_multi_imply:
  assumes ‹A ⊢ (a ❙⟶ b ❙⟶ c)›
  shows ‹A ⊢ ((a❙∧b) ❙⟶ c)›
proof - 
  have ‹tautology ((a ❙⟶ b ❙⟶ c) ❙⟶ ((a❙∧b) ❙⟶ c))›
    by force
  then have ‹A ⊢ ((a ❙⟶ b ❙⟶ c) ❙⟶ ((a❙∧b) ❙⟶ c))›
    using A1 by blast
  then show ?thesis
    using assms R1 by blast 
qed

lemma K_thm: ‹A ⊢ ((K i p) ❙∧ (L i q) ❙⟶ L i (p ❙∧ q))›
proof -
  have ‹tautology (p ❙⟶ (❙¬(p ❙∧ q)) ❙⟶ ❙¬ q)›
    by force
  then have ‹A ⊢ (p ❙⟶ (❙¬(p ❙∧ q)) ❙⟶ ❙¬ q)›
    by (simp add: A1)
  then have ‹A ⊢ ((K i p) ❙⟶ K i ((❙¬(p ❙∧ q)) ❙⟶ ❙¬ q))› 
        and ‹A ⊢ (K i ((❙¬(p ❙∧ q)) ❙⟶ ❙¬ q) ❙⟶ K i (❙¬(p ❙∧ q)) ❙⟶ K i (❙¬ q))›
     apply (simp add: K_map)
    by (meson K_A2')
  then have ‹A ⊢ ((K i p) ❙⟶ K i (❙¬(p ❙∧ q)) ❙⟶ K i (❙¬ q))› 
    using K_imp_trans by blast
  then have ‹A ⊢ ((K i p) ❙⟶ L i (q) ❙⟶ L i (p ❙∧ q))› 
    by (metis AK.simps K_imp_trans duality_taut)
  then show ?thesis
    by (simp add: K_multi_imply)
qed

primrec conjunct :: ‹'i fm list ⇒ 'i fm› where
  ‹conjunct [] = ❙⊤›
| ‹conjunct (p#ps) = (p ❙∧ conjunct ps)›

lemma imply_conjunct: ‹tautology ((imply G p) ❙⟶ ((conjunct G) ❙⟶ p))›
  apply(induction G) 
  apply simp
  by force

lemma conjunct_imply: ‹tautology (((conjunct G) ❙⟶ p) ❙⟶(imply G p))›
  by (induct G) simp_all

lemma K_imply_conjunct:
  assumes ‹A ⊢ imply G p›
  shows ‹A ⊢ ((conjunct G) ❙⟶ p)›
  using A1 R1 assms imply_conjunct by blast

lemma K_conjunct_imply:
  assumes ‹A ⊢ ((conjunct G) ❙⟶ p)›
  shows ‹A ⊢ imply G p›
  using A1 R1 assms conjunct_imply by blast

lemma K_conj_imply_factor: 
  fixes A :: ‹('i fm ⇒ bool)›  
  shows ‹A ⊢ ((((K i p) ❙∧ (K i q)) ❙⟶ r) ❙⟶((K i (p ❙∧ q)) ❙⟶ r))›
proof -
  have *: ‹A ⊢ ((K i (p ❙∧ q)) ❙⟶ ((K i p) ❙∧ (K i q)))›
  proof (rule ccontr) 
    assume ‹¬ A ⊢ ((K i (p ❙∧ q)) ❙⟶ ((K i p) ❙∧ (K i q)))›
    then have ‹consistent A {❙¬((K i (p ❙∧ q)) ❙⟶ ((K i p) ❙∧ (K i q)))}›
      by (metis imply.simps(1) inconsistent_imply insert_is_Un list.set(1))
    let ?V = ‹Extend A {❙¬((K i (p ❙∧ q)) ❙⟶ ((K i p) ❙∧ (K i q)))}› 
    let ?M = ‹⦇𝒲 = mcss A, 𝒦 = reach A, π = pi⦈› 
    have ‹?V ∈ 𝒲 ?M ∧ ?M, ?V ⊨ ❙¬((K i (p ❙∧ q)) ❙⟶ ((K i p) ❙∧ (K i q)))›
      using canonical_model ‹consistent A {❙¬ (K i (p ❙∧ q) ❙⟶ K i p ❙∧ K i q)}› 
            insert_iff mem_Collect_eq by fastforce
    then have o: ‹?M, ?V ⊨ ((K i (p ❙∧ q)) ❙∧ ❙¬((K i p) ❙∧ (K i q)))›
      by auto
    then have ‹?M, ?V ⊨ (K i (p ❙∧ q))› ‹(?M, ?V ⊨ ❙¬(K i p)) ∨ (?M, ?V ⊨ ❙¬(K i q))›
      by auto
    then have ‹∀ U ∈ 𝒲 ?M ∩ 𝒦 ?M i ?V. ?M, U ⊨(p ❙∧ q)›
              ‹∃ U ∈ 𝒲 ?M ∩ 𝒦 ?M i ?V. ?M, U ⊨ ((❙¬p) ❙∨ (❙¬q))›
      using o by auto
    then show False 
      by simp
  qed
  then have ‹A ⊢ (((K i (p ❙∧ q)) ❙⟶ ((K i p) ❙∧ (K i q))) ❙⟶
                   ((((K i p) ❙∧ (K i q)) ❙⟶ r) ❙⟶ ((K i (p ❙∧ q)) ❙⟶ r)))›
    by (simp add: A1)
  then show ?thesis 
    using "*" R1 by blast
qed

lemma K_conjunction_in: ‹A ⊢ (K i (p ❙∧ q) ❙⟶ ((K i p) ❙∧ K i q))›
proof -
  have o1: ‹A ⊢ ((p❙∧q) ❙⟶ p)› and o2: ‹A ⊢ ((p❙∧q) ❙⟶ q)›
    apply(simp add: A1)
    by (simp add: A1)
  then have c1: ‹A ⊢ (K i (p ❙∧ q) ❙⟶ K i q)› and c2: ‹A ⊢ (K i (p ❙∧ q) ❙⟶ K i p)› 
    apply (simp add: K_map o2)
    by (simp add: K_map o1)
  then show ?thesis
    by (simp add: K_imply_multi)
qed

lemma K_conjunction_in_mult:  ‹A ⊢ ((K i (conjunct G)) ❙⟶ conjunct (map (K i) G))›
proof (induct G)
  case Nil
  then show ?case
    by (simp add: A1)
  case (Cons a G)
  then have ‹A ⊢ ((K i (conjunct (a#G))) ❙⟶ (K i (a ❙∧ conjunct G)))›
        and  ‹A ⊢ ((K i (a ❙∧ conjunct G)) ❙⟶ ((K i a) ❙∧ K i (conjunct G)))›
    apply (simp add: A1)
    by (metis K_conjunction_in)
  then have o1: ‹A ⊢ ((K i (conjunct (a#G))) ❙⟶ ((K i a) ❙∧ K i (conjunct G)))›
    using K_imp_trans by blast
  then have ‹A ⊢ (((K i a) ❙∧ K i (conjunct G)) ❙⟶ K i a)› 
        and o2: ‹A ⊢ (((K i a) ❙∧ K i (conjunct G)) ❙⟶ conjunct (map (K i) G))›
    apply (simp add: A1)
    by (metis Cons.hyps K_imply_Cons K_multi_imply imply.simps(1) imply.simps(2))
  then have ‹A ⊢ (((K i a) ❙∧ K i (conjunct G)) ❙⟶ (K i a) ❙∧ conjunct (map (K i) G))›
    using K_imply_multi by blast
  then show ?case 
    using K_imp_trans o1 by auto
qed

lemma K_conjunction_out: ‹A ⊢ ((K i p) ❙∧ (K i q) ❙⟶ K i (p ❙∧ q))›
proof -
  have ‹A ⊢ (p ❙⟶ q ❙⟶ p❙∧q)›
    by (simp add: A1)
  then have ‹A ⊢ K i (p ❙⟶ q ❙⟶ p❙∧q)›
    by (simp add: R2)
  then have ‹A ⊢ ((K i p) ❙⟶ K i (q ❙⟶ p❙∧q))›
    by (simp add: K_map ‹A ⊢ (p ❙⟶ q ❙⟶ p ❙∧ q)›)
  then have ‹A ⊢ ((K i p) ❙⟶ (K i q) ❙⟶ K i (p❙∧q))›
    by (meson K_A2' K_imp_trans)
  then show ?thesis
    using K_multi_imply by blast
qed

lemma K_conjunction_out_mult: ‹A ⊢ (conjunct (map (K i) G) ❙⟶ (K i (conjunct G)))›
proof (induct G)
  case Nil
  then show ?case
    by (metis A1 K_imply_conjunct Nil_is_map_conv R2 conjunct.simps(1) eval.simps(5) imply.simps(1))
  case (Cons a G)
  then have ‹A ⊢ ((conjunct (map (K i) (a#G))) ❙⟶ ((K i a) ❙∧ conjunct (map (K i) G)))›
    by (simp add: A1)
  then have *: ‹A ⊢ (((K i a) ❙∧ conjunct (map (K i) G))❙⟶ (K i a) ❙∧ K i (conjunct G))›
    by (metis Cons.hyps K_imply_Cons K_imply_head K_imply_multi K_multi_imply imply.simps(1) imply.simps(2))
  then have ‹A ⊢ (((K i a) ❙∧ K i (conjunct G))❙⟶ K i (conjunct (a#G)))›
    by (simp add: K_conjunction_out)
  then show ?case
    using "*" K_imp_trans by auto
qed

subsection ‹More on mcs's properties›

lemma mcs_conjunction: 
  assumes ‹consistent A V› and ‹maximal A V› 
  shows ‹p ∈ V ∧ q ∈ V ⟶ (p ❙∧ q) ∈ V›
proof - 
  have ‹tautology (p ❙⟶ q ❙⟶ (p❙∧q))›
    by force  
  then have ‹(p ❙⟶ q ❙⟶ (p❙∧q)) ∈ V›
    using A1 assms(1) assms(2) deriv_in_maximal by blast
  then have ‹p ∈ V ⟶ (q ❙⟶ (p❙∧q)) ∈ V›
    by (meson assms(1) assms(2) consequent_in_maximal)
  then show ?thesis
    using assms(1) assms(2) consequent_in_maximal by blast
qed

lemma mcs_conjunction_mult: 
 assumes ‹consistent A V› and ‹maximal A V› 
  shows ‹(set (S :: ('i fm list)) ⊆ V ∧ finite (set S)) ⟶ (conjunct S) ∈ V›
proof(induct S)
  case Nil
  then show ?case
    by (metis K_Boole assms(1) assms(2) conjunct.simps(1) consistent_def inconsistent_subset maximal_def)
  case (Cons a S)
  then have ‹set S ⊆ set (a#S)›
    by (meson set_subset_Cons)
  then have c1: ‹ set (a # S) ⊆ V ∧ finite (set (a # S)) ⟶ conjunct (S) ∈ V ∧ a ∈ V›
    using Cons by fastforce
  then have ‹ conjunct (S) ∈ V ∧ a ∈ V ⟶ (conjunct (a#S)) ∈ V ›
    using assms(1) assms(2) mcs_conjunction by auto
  then show ?case
    using c1 by fastforce
qed

lemma reach_dualK: 
  assumes ‹consistent A V› ‹maximal A V›
    and ‹consistent A W› ‹maximal A W› ‹W ∈ reach A i V›
  shows ‹∀p. p ∈ W ⟶ (L i p) ∈ V›
proof (rule ccontr)
  assume ‹¬ (∀p. p ∈ W ⟶ (L i p) ∈ V)›
  then obtain p' where *: ‹p' ∈ W ∧ (L i p') ∉ V›
    by presburger
  then have ‹(❙¬ L i p') ∈ V›
    using assms(1) assms(2) assms(3) assms(4) assms(5) exactly_one_in_maximal by blast
  then have ‹K i (❙¬ p') ∈ V›
    using assms(1) assms(2) exactly_one_in_maximal by blast
  then have ‹(❙¬ p') ∈ W›
    using assms(5) by blast
  then show False
    by (meson "*" assms(3) assms(4) exactly_one_in_maximal)
qed 

lemma dual_reach: 
  assumes ‹consistent A V› ‹maximal A V› 
  shows ‹(L i p) ∈ V ⟶ (∃ W. W ∈ reach A i V ∧ p ∈ W)›
proof -
  have ‹(∄W. W ∈ {W. known V i ⊆ W} ∧ p ∈ W) ⟶ (∀W. W ∈ {W. known V i ⊆ W} ⟶ (❙¬p) ∈ W)›
    by blast
  then have ‹(∀W. W ∈ {W. known V i ⊆ W} ⟶ (❙¬p) ∈ W) ⟶ (∀ W. W ∈ reach A i V ⟶ (❙¬p) ∈ W)›
    by fastforce
  then have ‹(∀ W. W ∈ reach A i V ⟶ (❙¬p) ∈ W) ⟶ ((K i (❙¬p)) ∈ V)›
    by blast
  then have ‹((K i (❙¬p)) ∈ V) ⟶ (¬((L i p) ∈ V))›
    using assms(1) assms(2) exactly_one_in_maximal by blast
  then have ‹(∄W. W ∈ {W. known V i ⊆ W} ∧ p ∈ W) ⟶ ¬((L i p) ∈ V)› 
    by blast
  then show ?thesis
    by blast
qed


section  ‹Ax.2›

definition weakly_directed :: ‹('i, 's) kripke ⇒ bool› where
  ‹weakly_directed M ≡ ∀i. ∀s ∈ 𝒲 M. ∀t ∈ 𝒲 M. ∀r ∈ 𝒲 M.
     (r ∈ 𝒦 M i s ∧ t ∈ 𝒦 M i s)⟶(∃ u ∈ 𝒲 M. (u ∈ 𝒦 M i r ∧ u ∈ 𝒦 M i t))›

inductive Ax_2 :: ‹'i fm ⇒ bool› where 
  ‹Ax_2 (❙¬ K i (❙¬ K i p) ❙⟶ K i (❙¬ K i (❙¬ p)))› 

subsection ‹Soundness›

theorem weakly_directed:
  assumes ‹weakly_directed M› ‹w ∈ 𝒲 M›
  shows ‹M, w ⊨ (L i (K i p) ❙⟶ K i (L i p))›
proof 
  assume ‹M, w ⊨ (L i (K i p))›
  then have ‹∃v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ K i p› 
    by simp
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. ∃u ∈ 𝒲 M ∩ 𝒦 M i v. M, u ⊨ p›
    using ‹weakly_directed M› ‹w ∈ 𝒲 M› unfolding weakly_directed_def
    by (metis IntE IntI semantics.simps(6)) 
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ L i p›
    by simp
  then show ‹M, w ⊨ K i (L i p)›
    by simp
qed

lemma soundness_Ax_2: ‹Ax_2 p ⟹ weakly_directed M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  by (induct p rule: Ax_2.induct) (meson weakly_directed)

subsection ‹Imply completeness›

lemma Ax_2_weakly_directed:
  fixes A :: ‹'i fm ⇒ bool›
  assumes ‹∀p. Ax_2 p ⟶ A p› ‹consistent A V› ‹maximal A V›
    and ‹consistent A W› ‹maximal A W› ‹consistent A U› ‹maximal A U›
    and ‹W ∈ reach A i V› ‹U ∈ reach A i V›
  shows ‹∃X. (consistent A X) ∧ (maximal A X) ∧ X ∈ (reach A i W) ∩ (reach A i U)›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  let ?S = ‹(known W i) ∪ (known U i)›
  have ‹¬ consistent A ?S› 
    by (smt (verit, best) Int_Collect ‹∄X. consistent A X ∧ maximal A X ∧ X ∈ {Wa. known W i ⊆ Wa} ∩ {W. known U i ⊆ W}› maximal_extension mem_Collect_eq sup.bounded_iff)
  then obtain S' where *: ‹A ⊢ imply S' ❙⊥› ‹set S' ⊆ ?S› ‹finite (set S')›
    unfolding consistent_def by blast 
  let ?U = ‹filter (λp. p ∈ (known U i)) S'›
  let ?W = ‹filter (λp. p ∈ (known W i)) S'›
  let ?p = ‹conjunct ?U› and ?q = ‹conjunct ?W›
  have ‹(set ?U) ∪ (set ?W) = (set S')›
    using * by auto
  then have ‹A ⊢ imply ?U (imply ?W ❙⊥)›
    using K_imply_weaken imply_append  
    by (metis (mono_tags, lifting) "*"(1) set_append subset_refl) 
  then have ‹A ⊢ (?p ❙⟶ (imply ?W ❙⊥))›
    using K_imply_conjunct by blast
  then have ‹tautology ((imply ?W ❙⊥) ❙⟶ (?q ❙⟶ ❙⊥))›
    using imply_conjunct by blast
  then have ‹A ⊢ ((imply ?W ❙⊥) ❙⟶ (?q ❙⟶ ❙⊥))›
    using A1 by blast
  then have ‹A ⊢ (?p ❙⟶ (?q ❙⟶ ❙⊥))›
    using K_imp_trans ‹A ⊢ (conjunct (filter (λp. p ∈ known U i) S') ❙⟶ imply (filter (λp. p ∈ known W i) S') ❙⊥)›
    by blast 
  then have o1: ‹A ⊢ ((?p ❙∧ ?q) ❙⟶ ❙⊥)›
    by (meson K_multi_imply)
  moreover have ‹set ?U ⊆ (known U i)› and ‹set ?W ⊆ (known W i)› 
                and ‹∀ p. p ∈ set ?U ⟶ (K i p) ∈ U› and ‹∀ p. p ∈ set ?W ⟶ (K i p) ∈ W› 
    by auto
  then have ‹set (map (K i) ?U) ⊆ U› and c1: ‹set (map (K i) ?W) ⊆ W›
     apply (metis (mono_tags, lifting) imageE set_map subsetI) 
    by auto
  then have c2: ‹conjunct (map (K i) ?U) ∈ U› and c2': ‹conjunct (map (K i) ?W) ∈ W›
    using assms(6) assms(7) mcs_conjunction_mult apply blast
    using assms(4) assms(5) c1 mcs_conjunction_mult by blast
  then have ‹((conjunct (map (K i) ?U)) ❙⟶ (K i ?p)) ∈ U› 
        and c3: ‹((conjunct (map (K i) ?W)) ❙⟶ (K i ?q)) ∈ W› 
    apply (meson K_conjunction_out_mult assms(6) assms(7) deriv_in_maximal)
    by (meson K_conjunction_out_mult assms(4) assms(5) deriv_in_maximal)
  then have c4: ‹(K i ?p) ∈ U› and c4': ‹(K i ?q) ∈ W›
    using assms(6) assms(7) c2 consequent_in_maximal apply blast
    using assms(4) assms(5) c2' c3 consequent_in_maximal by blast
  then have ‹(L i (K i ?p)) ∈ V› and c5: ‹(L i (K i ?q)) ∈ V› 
    using assms(2) assms(3) assms(6) assms(7) assms(9) exactly_one_in_maximal apply blast
    using assms(2) assms(3) assms(4) assms(5) assms(8) c4' exactly_one_in_maximal by blast
  then have ‹(K i (L i ?p)) ∈ V›
    by (meson Ax_2.intros assms(1) assms(2) assms(3) ax_in_maximal consequent_in_maximal)
  then have ‹((K i (L i ?p)) ❙∧ (L i (K i ?q))) ∈ V›
    using assms(2) assms(3) c5 mcs_conjunction by blast
  then have ‹(L i ((L i ?p) ❙∧ K i ?q)) ∈ V›
    by (meson K_thm assms(2) assms(3) consequent_in_maximal deriv_in_maximal)
  then have ‹(L i ((K i ?q) ❙∧ L i ?p)) ∈ V›
    by (smt (verit) ‹K i (L i (conjunct (filter (λp. p ∈ known U i) S'))) ∈ V› assms(2) assms(3) assms(4) assms(5) assms(8) c4' exactly_one_in_maximal mcs_conjunction mem_Collect_eq subset_iff)
  then obtain Z' where z1:‹(consistent A Z') ∧ (maximal A Z')› and z2:‹Z' ∈ (reach A i V)› 
                  and z3: ‹((K i ?q) ❙∧ L i ?p) ∈ Z'›
    using ‹K i (L i (conjunct (filter (λp. p ∈ known U i) S'))) ∈ V› assms(4) assms(5) assms(8) c4' mcs_conjunction by blast
  then have z4: ‹(L i (?q ❙∧ ?p)) ∈ Z'›
    by (metis K_thm consequent_in_maximal deriv_in_maximal)
  then have o2:‹(L i (L i (?q ❙∧ ?p))) ∈ V›
    using assms(2) assms(3) mcs_properties(2) z1 z2 by blast
  then have ‹A ⊢ K i (K i (((?p ❙∧ ?q) ❙⟶ ❙⊥)))› 
    by (metis R2 o1)
  then have o3:‹K i (K i (((?p ❙∧ ?q) ❙⟶ ❙⊥))) ∈ V›
    using assms(2) assms(3) deriv_in_maximal by blast
  then obtain X1 where x1:‹(consistent A X1) ∧ (maximal A X1)› and x2:‹X1 ∈ (reach A i V)› 
                  and x3: ‹(L i (?q ❙∧ ?p)) ∈ X1›
    using z1 z2 z4 by blast
  then have x4:‹(K i (((?p ❙∧ ?q) ❙⟶ ❙⊥))) ∈ X1›
    using o3 by blast
  then have t:‹∀x. ∀y. tautology (((x❙∧y)❙⟶❙⊥)❙⟶❙¬(y❙∧x))›
    by (metis eval.simps(4) eval.simps(5))
  then have ‹(((?p❙∧?q)❙⟶❙⊥)❙⟶❙¬(?q❙∧?p)) ∈ X1›
    using A1 deriv_in_maximal x1 by blast
  then have ‹K i (((?p❙∧?q)❙⟶❙⊥)❙⟶❙¬(?q❙∧?p)) ∈ X1›
    by (meson A1 R2 deriv_in_maximal t x1)
  then have ‹(K i ((?p❙∧?q)❙⟶❙⊥)❙⟶ K i (❙¬(?q❙∧?p))) ∈ X1›
    by (meson K_A2' consequent_in_maximal deriv_in_maximal x1)
  then have ‹(K i ((?p❙∧?q)❙⟶❙⊥)❙⟶ (❙¬ L i(?q❙∧?p))) ∈ X1›
    using consequent_in_maximal exactly_one_in_maximal x1 x3 x4 by blast
  then have ‹(❙¬ L i(?q❙∧?p)) ∈ X1 ∧ (L i(?q❙∧?p)) ∈ X1›
    using consequent_in_maximal x1 x4 x3 by blast
  then show False
    using exactly_one_in_maximal x1 by blast
qed

lemma mcs⇩_⇩2_weakly_directed:
  fixes A :: ‹'i fm ⇒ bool›
  assumes ‹∀p. Ax_2 p ⟶ A p›
  shows ‹weakly_directed ⦇𝒲 = mcss A, 𝒦 = reach A, π = pi⦈›
  unfolding weakly_directed_def
proof (intro allI ballI, auto)
  fix i V U W
  assume ‹consistent A V› ‹maximal A V› ‹consistent A U› ‹maximal A U› ‹consistent A W› 
      ‹maximal A W› ‹known V i ⊆ U› ‹known V i ⊆ W›
  then have ‹∃X. (consistent A X) ∧ (maximal A X) ∧ X ∈ (reach A i W) ∩ (reach A i U)›
    using Ax_2_weakly_directed [where A=A and V=V and W=W and U=U] assms IntD2 
      by simp
  then have ‹∃X. (consistent A X) ∧ (maximal A X) ∧ X ∈ (reach A i W) ∧ X ∈ (reach A i U)›
    by simp
  then show ‹∃X. (consistent A X) ∧ (maximal A X) ∧ known W i ⊆ X ∧ known U i ⊆ X›
    by auto
qed

lemma imply_completeness_K_2:
  assumes valid: ‹∀(M :: ('i, 'i fm set) kripke). ∀w ∈ 𝒲 M.
    weakly_directed M ⟶ (∀q ∈ G. M, w ⊨ q) ⟶ M, w ⊨ p›
  shows ‹∃qs. set qs ⊆ G ∧ (Ax_2 ⊢ imply qs p)›
proof (rule ccontr)
assume ‹∄qs. set qs ⊆ G ∧ Ax_2 ⊢ imply qs p›
  then have *: ‹∀qs. set qs ⊆ G ⟶ ¬ Ax_2 ⊢ imply ((❙¬ p) # qs) ❙⊥›
    using K_Boole by blast

  let ?S = ‹{❙¬ p} ∪ G›
  let ?V = ‹Extend Ax_2 ?S›
  let ?M = ‹⦇𝒲 = mcss Ax_2, 𝒦 = reach Ax_2, π = pi⦈›

  have ‹consistent Ax_2 ?S›
    using * by (metis K_imply_Cons consistent_def inconsistent_subset)
  then have ‹?M, ?V ⊨ (❙¬ p)› ‹∀q ∈ G. ?M, ?V ⊨ q› ‹consistent Ax_2 ?V› ‹maximal Ax_2 ?V›
    using canonical_model unfolding list_all_def by fastforce+
  moreover have ‹weakly_directed ?M›
    using mcs⇩_⇩2_weakly_directed [where A=Ax_2] by fast
  ultimately have ‹?M, ?V ⊨ p›
    using valid by auto
  then show False
    using ‹?M, ?V ⊨ (❙¬ p)› by simp
qed


section ‹System S4.2›

abbreviation SystemS4_2 :: ‹'i fm ⇒ bool› ("⊢⇩S⇩4⇩2 _" [50] 50) where
  ‹⊢⇩S⇩4⇩2 p ≡ AxT ⊕ Ax4 ⊕ Ax_2 ⊢ p›

abbreviation AxS4_2 :: ‹'i fm ⇒ bool› where
  ‹AxS4_2 ≡ AxT ⊕ Ax4 ⊕ Ax_2›

subsection ‹Soundness›

abbreviation w_directed_preorder :: ‹('i, 'w) kripke ⇒ bool› where
  ‹w_directed_preorder M ≡ reflexive M ∧ transitive M ∧ weakly_directed M›

lemma soundness_AxS4_2: ‹AxS4_2 p ⟹ w_directed_preorder M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  using soundness_AxT soundness_Ax4 soundness_Ax_2 by metis

lemma soundness⇩S⇩4⇩2: ‹⊢⇩S⇩4⇩2 p ⟹ w_directed_preorder M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  using soundness soundness_AxS4_2 .

subsection ‹Completeness›

lemma imply_completeness_S4_2:
  assumes valid: ‹∀(M :: ('i, 'i fm set) kripke). ∀w ∈ 𝒲 M.
    w_directed_preorder M ⟶ (∀q ∈ G. M, w ⊨ q) ⟶ M, w ⊨ p›
  shows ‹∃qs. set qs ⊆ G ∧ (AxS4_2 ⊢ imply qs p)›
proof (rule ccontr)
  assume ‹∄qs. set qs ⊆ G ∧ AxS4_2 ⊢ imply qs p›
  then have *: ‹∀qs. set qs ⊆ G ⟶ ¬ AxS4_2 ⊢ imply ((❙¬ p) # qs) ❙⊥›
    using K_Boole by blast

  let ?S = ‹{❙¬ p} ∪ G›
  let ?V = ‹Extend AxS4_2 ?S›
  let ?M = ‹⦇𝒲 = mcss AxS4_2, 𝒦 = reach AxS4_2, π = pi⦈›

  have ‹consistent AxS4_2 ?S›
    using * by (metis (no_types, lifting) K_imply_Cons consistent_def inconsistent_subset)
  then have
    ‹?M, ?V ⊨ (❙¬ p)› ‹∀q ∈ G. ?M, ?V ⊨ q›
    ‹consistent AxS4_2 ?V› ‹maximal AxS4_2 ?V›
    using canonical_model unfolding list_all_def by fastforce+
  moreover have ‹w_directed_preorder ?M›
    using reflexive⇩T[of AxS4_2] mcs⇩_⇩2_weakly_directed[of AxS4_2] transitive⇩K⇩4[of AxS4_2] by auto
  ultimately have ‹?M, ?V ⊨ p›
    using valid by auto
  then show False
    using ‹?M, ?V ⊨ (❙¬ p)› by simp
qed

lemma completeness⇩S⇩4⇩2:
  assumes ‹∀(M :: ('i, 'i fm set) kripke). ∀w ∈ 𝒲 M. w_directed_preorder M ⟶ M, w ⊨ p›
  shows ‹⊢⇩S⇩4⇩2 p›
  using assms imply_completeness_S4_2[where G=‹{}›] by auto

abbreviation ‹valid⇩S⇩4⇩2 p ≡ ∀(M :: (nat, nat fm set) kripke). ∀w ∈ 𝒲 M. w_directed_preorder M ⟶ M, w ⊨ p›

theorem main⇩S⇩4⇩2: ‹valid⇩S⇩4⇩2 p ⟷ ⊢⇩S⇩4⇩2 p›
  using soundness⇩S⇩4⇩2 completeness⇩S⇩4⇩2 by fast

corollary
  assumes ‹w_directed_preorder M› ‹w ∈ 𝒲 M›
  shows ‹valid⇩S⇩4⇩2 p ⟶ M, w ⊨ p›
  using assms soundness⇩S⇩4⇩2 completeness⇩S⇩4⇩2 by fast


section ‹Topological S4 axioms›

abbreviation DoubleImp (infixr "❙⟷" 25) where
  ‹(p❙⟷q) ≡ ((p ❙⟶ q) ❙∧ (q ❙⟶ p))›

inductive System_topoS4 :: ‹'i fm ⇒ bool› ("⊢⇩T⇩o⇩p _" [50] 50) where
  A1': ‹tautology p ⟹ ⊢⇩T⇩o⇩p p›
| AR: ‹⊢⇩T⇩o⇩p ((K i (p ❙∧ q)) ❙⟷ ((K i p) ❙∧ K i q))›
| AT': ‹⊢⇩T⇩o⇩p (K i p ❙⟶ p)›
| A4': ‹⊢⇩T⇩o⇩p (K i p ❙⟶ K i (K i p))›
| AN: ‹⊢⇩T⇩o⇩p K i ❙⊤›
| R1': ‹⊢⇩T⇩o⇩p p ⟹ ⊢⇩T⇩o⇩p (p ❙⟶ q) ⟹ ⊢⇩T⇩o⇩p q›
| RM: ‹⊢⇩T⇩o⇩p (p ❙⟶ q) ⟹ ⊢⇩T⇩o⇩p ((K i p) ❙⟶ K i q)›

lemma topoS4_trans: ‹⊢⇩T⇩o⇩p ((p ❙⟶ q) ❙⟶ (q ❙⟶ r) ❙⟶ p ❙⟶ r)›
  by (simp add: A1')

lemma topoS4_conjElim: ‹⊢⇩T⇩o⇩p (p ❙∧ q ❙⟶ q)›
  by (simp add: A1')

lemma topoS4_AxK: ‹⊢⇩T⇩o⇩p (K i p ❙∧ K i (p ❙⟶ q) ❙⟶ K i q)›
proof -
  have ‹⊢⇩T⇩o⇩p ((p ❙∧ (p ❙⟶ q)) ❙⟶ q)›
    using A1' by force
  then have *: ‹⊢⇩T⇩o⇩p (K i (p ❙∧ (p ❙⟶ q)) ❙⟶ K i q)›
    using RM by fastforce
  then have ‹⊢⇩T⇩o⇩p (K i p ❙∧ K i (p ❙⟶ q) ❙⟶ K i (p ❙∧ (p ❙⟶ q)))›
    using AR topoS4_conjElim System_topoS4.simps by fast
  then show ?thesis
    by (meson "*" System_topoS4.R1' topoS4_trans)
qed

lemma topoS4_NecR:
  assumes ‹⊢⇩T⇩o⇩p p›
  shows‹⊢⇩T⇩o⇩p K i p›
proof -
  have ‹⊢⇩T⇩o⇩p (❙⊤ ❙⟶ p)›
    using assms by (metis System_topoS4.A1' System_topoS4.R1' conjunct.simps(1) imply.simps(1) imply_conjunct)
  then have ‹⊢⇩T⇩o⇩p (K i ❙⊤ ❙⟶ K i p)›
    using RM by force
  then show ?thesis
    by (meson AN System_topoS4.R1')
qed

lemma empty_S4: "{} ⊢⇩S⇩4 p ⟷ AxT ⊕ Ax4 ⊢ p"
  by simp

lemma S4_topoS4: ‹{} ⊢⇩S⇩4 p ⟹ ⊢⇩T⇩o⇩p p›
  unfolding empty_S4
proof (induct p rule: AK.induct)
  case (A2 i p q)
  then show ?case using topoS4_AxK .
next 
  case (Ax p)
    then show ?case 
      using AT' A4' by (metis AxT.cases Ax4.cases)
next
  case (R2 p)
  then show ?case 
    by (simp add: topoS4_NecR)
qed (meson System_topoS4.intros)+

lemma topoS4_S4:
  fixes p :: ‹'i fm›
  shows ‹⊢⇩T⇩o⇩p p ⟹ {} ⊢⇩S⇩4 p›
  unfolding empty_S4
proof (induct p rule: System_topoS4.induct)
  case (AT' i p)
  then show ?case
    by (simp add: Ax AxT.intros)
next
  case (A4' i p)
  then show ?case
    by (simp add: Ax Ax4.intros)
next
  case (AR i p q)
    then show ?case
      by (meson K_conj_imply_factor K_conjunction_in K_conjunction_out K_imp_trans' K_imply_multi R1)
next
  case (AN i) 
  then have *: ‹AxT ⊕ Ax4 ⊢ ❙⊤›
    by (simp add: A1)
  then show ?case 
    by (simp add: * R2)
next
  case (RM p q i)
  then have ‹AxT ⊕ Ax4 ⊢ K i (p ❙⟶ q)›
    by (simp add: R2)
  then show ?case
    by (simp add: K_map RM.hyps(2))
qed (meson AK.intros)+

theorem main⇩S⇩4': ‹{} ⊫⇩S⇩4 p ⟷ (⊢⇩T⇩o⇩p p)›
  using main⇩S⇩4[of "{}"] S4_topoS4 topoS4_S4 by fast

end