(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Kripke
imports Main
begin
(*>*)

section ‹A modal logic of knowledge›

text‹

 label{sec:kbps-logic-of-knowledge}

  begin with the standard syntax and semantics of the propositional
  of knowledge based on \emph{Kripke structures}. More extensive
  can be found in 🚫‹"Lenzen:1978"›, 🚫‹"Chellas:1980"›,
 🚫‹"Hintikka:1962"› and 🚫‹‹Chapter~2› in "FHMV:1995"›.

  syntax includes one knowledge modality per agent, and one for
 emph{common knowledge} amongst a set of agents. It is parameterised
  the type @{typ "'a"} of agents and @{typ "'p"} of propositions.

 ›

datatype ('a, 'p) Kform
  = Kprop "'p"
  | Knot "('a, 'p) Kform"
  | Kand "('a, 'p) Kform" "('a, 'p) Kform"
  | Kknows "'a" "('a, 'p) Kform"  (‹K _›)
  | Kcknows "'a list" "('a, 'p) Kform" (‹C _›)

text‹

  Kripke structure consists of a set of \emph{worlds} of type @{typ
 'w"}, one \emph{accessibility relation} between worlds for each agent
  a \emph{valuation function} that indicates the truth of a
  at a world. This is a very general story that we will
  specialise.

 ›

type_synonym 'w Relation = "('w × 'w) set"

record ('a, 'p, 'w) KripkeStructure =
  worlds :: "'w set"
  relations :: "'a → 'w Relation"
  valuation :: "'w → 'p → bool"

definition kripke :: "('a, 'p, 'w) KripkeStructure → bool" where
  "kripke M ≡ ∀a. relations M a ⊆ worlds M × worlds M"

definition
  mkKripke :: "'w set → ('a → 'w Relation) → ('w → 'p → bool)
            → ('a, 'p, 'w) KripkeStructure"
where
  "mkKripke ws rels val ≡
     ( worlds = ws, relations = λa. rels a ∩ ws × ws, valuation = val )"
(*<*)

lemma kripkeI[intro]:
  assumes "∧a. relations M a ⊆ worlds M × worlds M"
  shows "kripke M"
  using assms unfolding kripke_def by simp

lemma kripke_rels_worlds[dest]:
  assumes "(w, w') ∈ relations M a"
  assumes M: "kripke M"
  shows "w ∈ worlds M ∧ w' ∈ worlds M"
  using assms unfolding kripke_def by auto

lemma kripke_tc_rels_worlds[dest]:
  assumes R: "(w, w') ∈ (∪a ∈ as. relations M a)⁺"
  assumes M: "kripke M"
  shows "w ∈ worlds M ∧ w' ∈ worlds M"
  using assms by (induct rule: trancl_induct) auto

lemma kripke_rels_trc_worlds:
  assumes R: "(w, w') ∈ (∪a. relations M a)^*"
  assumes w: "w ∈ worlds M"
  assumes M: "kripke M"
  assumes W: "W = worlds M"
  shows "w' ∈ W"
  using assms by (induct rule: rtrancl_induct) auto

lemma mkKripke_kripke[intro, simp]:
  "kripke (mkKripke ws rels val)"
  unfolding kripke_def mkKripke_def by clarsimp

lemma mkKripke_simps[simp]:
  "worlds (mkKripke ws rels val) = ws"
  "relations (mkKripke ws rels val) = (λa. rels a ∩ ws × ws)"
  "valuation (mkKripke ws rels val) = val"
  unfolding mkKripke_def by simp_all
(*>*)

text ‹

  standard semantics for knowledge is given by taking the
  relations to be equivalence relations, yielding the
 $5_n$ structures, so-called due to their axiomatisation.

 ›

definition S5n :: "('a, 'p, 'w) KripkeStructure → bool" where
  "S5n M ≡ ∀a. equiv (worlds M) (relations M a)"
(*<*)

lemma S5nI[intro]: "[ ∧a. equiv (worlds M) (relations M a) ] ==> S5n M"
  by (simp add: S5n_def)

lemma S5nD[dest]: "S5n M ==> equiv (worlds M) (relations M a)"
  by (simp add: S5n_def)

lemma S5n_kripke[intro]: "S5n M ==> kripke M"
  by (rule kripkeI, erule equivE[OF S5nD], auto simp add: refl_on_def)

lemma S5n_rels_closed:
  "S5n M ==> relations M a `` (relations M a `` X) ⊆ relations M a `` X"
  apply (drule S5nD[where a=a])
  apply (erule equivE)
  apply (auto dest: refl_onD symD transD)
  done

(*>*)

text‹

  an agent considers two worlds to be equivalent if it
  distinguish between them.

 ›

subsection‹Satisfaction›

text‹

  formula $\phi$ is satisfied at a world $w$ in Kripke structure $M$
  the following way:›

fun models :: "('a, 'p, 'w) KripkeStructure → 'w → ('a, 'p) Kform
           → bool" (‹(_, _ ⊨ _)› [80,0,80] 80) where
  "M, w ⊨ (Kprop p) = valuation M w p"
| "M, w ⊨ (Knot φ) = (¬ M, w ⊨ φ)"
| "M, w ⊨ (Kand φ ψ) = (M, w ⊨ φ ∧ M, w ⊨ ψ)"
| "M, w ⊨ (K φ) = (∀w' ∈ relations M a `` {w}. M, w' ⊨ φ)"
| "M, w ⊨ (C φ) = (∀w' ∈ (∪a ∈ set as. relations M a)<sup>+</sup> `` {w}. M, w' ⊨ φ)"

text‹

  first three clauses are standard.

  clause for @{term "Kknows a φ"} expresses the idea that an agent
  @{term "φ"} at world @{term "w"} in structure @{term "M"} iff
 {term "φ"} is true at all worlds it considers possible.

  clause for @{term "Kcknows as φ"} captures what it means for the
  of agents @{term "as"} to commonly know @{term "φ"}; roughly,
  knows @{term "φ"} and knows that everyone knows it, and so
 . Note that the transitive closure and the reflexive-transitive
  generate the same relation due to the reflexivity of the
 ' accessibility relations; we use the former as it has a more
  induction principle.

 ›
(*<*)

lemma S5n_rels_eq:
  assumes S5n: "S5n M"
      and ww': "(w, w') ∈ relations M a"
  shows "relations M a `` {w} = relations M a `` {w'}"
  using S5nD[OF S5n] ww' by - (rule equiv_class_eq, blast+)

text‹

  key property of the semantics for common knowledge is that it forms
  equivalence class itself.

 ›

lemma tc_equiv:
  assumes E: "∧i. i ∈ is ==> equiv A (f i)"
      and is_nempty: "is ≠ {}"
  shows "equiv A ((∪i∈is. f i)⁺)"
proof(rule equivI)
  show "(∪ (f ` is))<sup>+</sup> ⊆ A × A"
  proof (rule trancl_Int_subset)
    show "∪ (f ` is) ⊆ A × A"
      by (simp add: E UN_least equiv_type)
  next
    show "Restr ((∪ (f ` is))<sup>+</sup>) A O ∪ (f ` is) ⊆ A × A"
      using E equiv_def by fastforce
  qed
next
  show "refl_on A ((∪i∈is. f i)⁺)"
    using E is_nempty
    by (smt (verit, ccfv_threshold) UN_iff equals0I equiv_def
        refl_on_def trancl.r_into_trancl)
next
  show "sym ((∪i∈is. f i)⁺)"
    using E
    by (simp add: equiv_def sym_UNION sym_trancl)
next
  show "trans ((∪i∈is. f i)⁺)"
    using trans_trancl .
qed

lemma S5n_tc_rels_eq:
  assumes S5n: "S5n M"
      and ww': "(w, w') ∈ (∪a ∈ as. relations M a)⁺"
  shows "(∪a ∈ as. relations M a)⁺ `` {w} = (∪a ∈ as. relations M a)<sup>+</sup> `` {w'}"
  apply (cases "as = {}")
   apply fastforce
  apply (rule equiv_class_eq[OF _ ww'])
  apply (erule tc_equiv[OF S5nD[OF S5n]])
  done

text‹We can show that the standard S5 properties hold of this semantics:›

lemma S5n_knowledge_generalisation:
  "[ S5n M; ∀w ∈ worlds M. M, w ⊨ φ ] ==> M, w ⊨ Kknows a φ"
  unfolding S5n_def equiv_def refl_on_def by auto

lemma S5n_knowledge:
  "[ S5n M; w ∈ worlds M; M, w ⊨ Kknows a φ ] ==> M, w ⊨ φ"
  unfolding S5n_def equiv_def refl_on_def by auto

lemma S5n_positive_introspection:
  "[ S5n M; w ∈ worlds M; M, w ⊨ Kknows a φ ] ==> M, w ⊨ Kknows a (Kknows a φ)"
  unfolding S5n_def equiv_def by simp (blast dest: transD)

lemma S5n_negative_introspection:
  "[ S5n M; w ∈ worlds M; M, w ⊨ Knot (Kknows a φ) ]
     ==> M, w ⊨ Kknows a (Knot (Kknows a φ))"
  unfolding S5n_def equiv_def by simp (blast dest: symD transD)
(*>*)

text‹

  relation between knowledge and common knowledge can be understood
  follows, following 🚫‹‹\S2.4› in "FHMV:1995"›. Firstly, that $\phi$
  common knowledge to a set of agents $as$ can be seen as asserting
  everyone in $as$ knows $\phi$ and moreover knows that it is
  knowledge amongst $as$.

 ›

lemma S5n_common_knowledge_fixed_point:
  assumes S5n: "S5n M"
  assumes w: "w ∈ worlds M"
  assumes a: "a ∈ set as"
  shows "M, w ⊨ Kcknows as φ
     ⟷ M, w ⊨ Kand (Kknows a φ) (Kknows a (Kcknows as φ))"
(*<*)
proof
  assume CK: "M, w ⊨ Kcknows as φ"
  from S5n a w CK
  have "M, w ⊨ Kknows a φ"
   and "M, w ⊨ Kknows a (Kcknows as φ)"
    by (auto intro: trancl_into_trancl2)
  then show "M, w ⊨ Kand (Kknows a φ) (Kknows a (Kcknows as φ))"
    by simp
next
  assume "M, w ⊨ Kand (Kknows a φ) (Kknows a (Kcknows as φ))"
  hence "M, w ⊨ (Kknows a (Kcknows as φ))" by simp
  with S5n w show "M, w ⊨ (Kcknows as φ)" by (rule S5n_knowledge)
qed

(*>*)
text‹

  we can provide an induction schema for the introduction of
  knowledge: from everyone in $as$ knows that $\phi$ implies
 \phi \land \psi$, and that $\phi$ is satisfied at world $w$, infer
  $\psi$ is common knowledge amongst $as$ at $w$.

 ›

lemma S5n_common_knowledge_induct:
  assumes S5n: "S5n M"
  assumes w: "w ∈ worlds M"
  assumes E: "∀a ∈ set as. ∀w ∈ worlds M.
                 M, w ⊨ φ ⟶ M, w ⊨ K (Kand φ ψ)"
  assumes p: "M, w ⊨ φ"
  shows "M, w ⊨ C ψ"
(*<*)
proof -
  { fix w' assume ww': "(w, w') ∈ (∪x∈set as. relations M x)⁺"
    from ww' S5n E p w have "M, w' ⊨ Kand φ ψ"
      by ( induct rule: trancl_induct
         , simp_all, blast+) }
  thus ?thesis by simp
qed

(* We actually use a simpler variant. *)

lemma S5n_common_knowledge_fixed_point_simpler:
  assumes S5n: "S5n M"
      and w: "w ∈ worlds M"
      and a: "a ∈ set as"
  shows "M, w ⊨ Kcknows as φ ⟷ M, w ⊨ Kknows a (Kcknows as φ)"
proof
  assume CK: "M, w ⊨ Kcknows as φ"
  from S5n a w CK show "M, w ⊨ Kknows a (Kcknows as φ)"
    by (auto intro: trancl_into_trancl2)
next
  assume "M, w ⊨ Kknows a (Kcknows as φ)"
  with S5n w show "M, w ⊨ (Kcknows as φ)" by (rule S5n_knowledge)
qed

(*>*)

(* **************************************** *)

subsection ‹Generated models›

text‹

 label{sec:generated_models}

  rest of this section introduces the technical machinery we use to
  Kripke structures.

  the truth of a formula at a world depends only on the
  that are reachable from it in zero or more steps, using any of
  accessibility relations at each step. Traditionally this result is
  the \emph{generated model property}
 🚫‹‹\S3.4› in "Chellas:1980"›.

  the model generated by @{term "w"} in @{term "M"}:

 ›

definition
  gen_model :: "('a, 'p, 'w) KripkeStructure → 'w → ('a, 'p, 'w) KripkeStructure"
where
  "gen_model M w ≡
    let ws' = worlds M ∩ (∪a. relations M a)^* `` {w}
     in ( worlds = ws',
          relations = λa. relations M a ∩ (ws' × ws'),
          valuation = valuation M )"
(*<*)

lemma gen_model_worldsD[dest]:
  "w' ∈ worlds (gen_model M w) ==> w' ∈ worlds M"
  unfolding gen_model_def by simp

lemma gen_model_world_refl:
  "w ∈ worlds M ==> w ∈ worlds (gen_model M w)"
  unfolding gen_model_def by simp

lemma gen_model_rels_worlds[dest]:
  assumes "(w', w'') ∈ relations (gen_model M w) a"
  shows "w' ∈ worlds (gen_model M w) ∧ w'' ∈ worlds (gen_model M w)"
  using assms unfolding gen_model_def by simp

lemma gen_model_rels_tc_worlds[dest]:
  assumes "(w', w'') ∈ (∪a ∈ as. relations (gen_model M w) a)⁺"
  shows "w'' ∈ worlds (gen_model M w)"
  using assms by (induct rule: trancl_induct) auto

lemma gen_model_rels[dest]:
  assumes "(w', w'') ∈ relations (gen_model M w) a"
  shows "(w', w'') ∈ relations M a"
  using assms unfolding gen_model_def by simp

lemma gen_model_worlds:
  "worlds (gen_model M w) = worlds M ∩ (∪a. relations M a)^* `` {w}"
  unfolding gen_model_def by simp

lemma gen_model_tc_rels[dest]:
  assumes M: "kripke M"
      and R: "(w', w'') ∈ (∪a ∈ as. relations (gen_model M w) a)⁺"
  shows "(w', w'') ∈ (∪a ∈ as. relations M a)⁺"
using R
proof(induct rule: trancl_induct)
  case (base y) with M show ?case by auto
next
  case (step y z)
  with M have "y ∈ worlds (gen_model M w)"
          and "z ∈ worlds (gen_model M w)" by auto
  with M step show ?case by (auto intro: trancl_into_trancl)
qed

lemma gen_model_rels_rev[dest]:
  assumes M: "kripke M"
      and "w' ∈ worlds (gen_model M w)"
      and "(w', w'') ∈ relations M a"
  shows "(w', w'') ∈ relations (gen_model M w) a"
  using assms
  unfolding gen_model_def by (auto intro: rtrancl_into_rtrancl)

lemma gen_model_tc_rels_rev[dest]:
  assumes M: "kripke M"
      and R: "(w', w'') ∈ (∪a ∈ as. relations M a)⁺"
      and W: "w' ∈ worlds (gen_model M w)"
  shows "(w', w'') ∈ (∪a ∈ as. relations (gen_model M w) a)⁺"
using R W
proof(induct rule: trancl_induct)
  case (base y) with M show ?case by auto
next
  case (step y z)
  with M have "y ∈ worlds (gen_model M w)"
          and "z ∈ worlds (gen_model M w)" by auto
  with M step show ?case by (auto intro: trancl_into_trancl)
qed

lemma gen_model_kripke:
  shows "kripke (gen_model M w)"
  unfolding gen_model_def by auto

(*>*)

text‹

  we take the image of @{term "w"} under the reflexive transitive
  of the agents' relations, we can show that the satisfaction of
  formula @{term "φ"} at a world @{term "w'"} is preserved, provided
 {term "w'"} is relevant to the world @{term "w"} that the sub-model
  based upon:

 ›

lemma gen_model_semantic_equivalence:
  assumes M: "kripke M"
  assumes w': "w' ∈ worlds (gen_model M w)"
  shows "M, w' ⊨ φ ⟷ (gen_model M w), w' ⊨ φ"
(*<*)
proof -
  { fix w w' assume "w' ∈ worlds (gen_model M w)"
    hence "M, w' ⊨ φ ⟷ (gen_model M w), w' ⊨ φ"
    proof(induct φ arbitrary: w')
      case (Kknows a f w') show ?case
      proof
        assume lhs: "M, w' ⊨ Kknows a f"
        with Kknows show "gen_model M w, w' ⊨ Kknows a f" by auto
      next
        assume rhs: "gen_model M w, w' ⊨ Kknows a f"
        with M Kknows show "M, w' ⊨ Kknows a f"
          by (simp, blast)
      qed
    next
      case (Kcknows as f w') show ?case
      proof
        assume lhs: "M, w' ⊨ Kcknows as f"
        with M Kcknows show "gen_model M w, w' ⊨ Kcknows as f"
          by (simp, blast)
      next
        assume rhs: "gen_model M w, w' ⊨ Kcknows as f"
        with M Kcknows show "M, w' ⊨ Kcknows as f"
          by (simp, blast)
      qed
    qed (simp_all add: gen_model_def) }
  with w' show ?thesis by simp
qed
(*>*)

text‹

  is shown by a straightforward structural induction over the
  @{term "φ"}.

 ›
(*<*)

lemma gen_model_S5n:
  assumes S5n: "S5n M"
  shows "S5n (gen_model M w)"
proof(intro S5nI equivI)
  show "∧n. relations (gen_model M w) n ⊆ worlds (gen_model M w) × worlds (gen_model M w)"
    by (simp add: gen_model_rels_worlds subrelI)
  show "∧n. refl_on (worlds (gen_model M w)) (relations (gen_model M w) n)"
    apply (rule equivE[OF S5nD[OF S5n]])
    by - (rule refl_onI, auto simp add: refl_on_def gen_model_def)
  show "∧n. sym (relations (gen_model M w) n)"
    apply (rule equivE[OF S5nD[OF S5n]])
    by (unfold gen_model_def sym_def, auto)
  show "∧n. trans (relations (gen_model M w) n)"
    apply (rule equivE[OF S5nD[OF S5n]])
    by - (rule transI, simp add: gen_model_def, unfold trans_def, blast)
qed

text‹

  two models generate the same sub-model for a world, they satisfy
  same formulas at that world.

 ›

lemma gen_model_eq:
  assumes M: "kripke M"
      and M': "kripke M'"
      and "gen_model M w = gen_model M' w"
      and "w' ∈ worlds (gen_model M' w)"
  shows "M, w' ⊨ φ ⟷ M', w' ⊨ φ"
  using assms gen_model_semantic_equivalence[OF M, where w=w]
              gen_model_semantic_equivalence[OF M', where w=w]
  by auto

text ‹

  final lemma in this section is technical: it allows us to move
  two Kripke structures that have the same relevant worlds.

 ›

lemma gen_model_subset_aux:
  assumes R: "∧a. relations M a ∩ T × T = relations M' a ∩ T × T"
      and T: "(∪a. relations M a)^* `` {t} ⊆ T"
  shows "(∪x. relations M x)<sup>*</sup> `` {t} ⊆ (∪x. relations M' x)^* `` {t}"
proof -
  { fix x assume "(t, x) ∈ (∪x. relations M x)^*"
    hence "(t, x) ∈ (∪x. relations M' x)^*"
    proof(induct rule: rtrancl_induct)
      case (step y z)
      with R T have "(y, z) ∈ (∪a. relations M' a)"
        by auto (blast dest: rtrancl_trans)
      with step show ?case by (blast intro: rtrancl_trans)
    qed simp }
  thus ?thesis by blast
qed

lemma gen_model_subset:
  assumes M: "kripke M"
      and M': "kripke M'"
      and R: "∧a. relations M a ∩ T × T = relations M' a ∩ T × T"
      and tMT: "(∪a. relations M a)^* `` {t} ⊆ T"
      and tM'T: "(∪a. relations M' a)<sup>*</sup> `` {t} ⊆ T"
      and tM: "t ∈ worlds M"
      and tM': "t ∈ worlds M'"
      and V: "valuation M = valuation M'"
  shows "gen_model M t = gen_model M' t"
proof -
  from tMT tM'T gen_model_subset_aux[OF R] gen_model_subset_aux[OF R[symmetric]]
  have F: "(∪a. relations M a)^* `` {t} = (∪a. relations M' a)<sup>*</sup> `` {t}"
    by - (rule, simp_all)

  from M tMT tM have G: "(∪a. relations M a)^* `` {t} ⊆ worlds M"
    by (auto dest: kripke_rels_trc_worlds)
  from M' tM'T tM' have H: "(∪a. relations M' a)<sup>*</sup> `` {t} ⊆ worlds M'"
    by (auto dest: kripke_rels_trc_worlds)

  from F G H have WORLDS: "worlds (gen_model M t) = worlds (gen_model M' t)"
    unfolding gen_model_def by (auto iff: Int_absorb1)

  have RELATIONS: "∧a. relations (gen_model M t) a = relations (gen_model M' t) a"
  proof (simp add: Int_absorb1 G H gen_model_def)
    fix a
    { fix a x y
      assume XY: "(x, y) ∈ relations M a ∩ (∪x. relations M x)^* `` {t} × (∪x. relations M x)<sup>*</sup> `` {t}"
      from XY tMT
      have "(x, y) ∈ relations M a ∩ T × T" by blast
      with R
      have "(x, y) ∈ relations M' a ∩ T × T" by blast
      with F XY tM'T
      have "(x, y) ∈ relations M' a ∩ (∪x. relations M' x)^* `` {t} × (∪x. relations M' x)<sup>*</sup> `` {t}"
        by blast }
    moreover
    { fix a x y
      assume XY: "(x, y) ∈ relations M' a ∩ (∪x. relations M' x)^* `` {t} × (∪x. relations M' x)<sup>*</sup> `` {t}"
      from XY tM'T
      have "(x, y) ∈ relations M' a ∩ T × T" by blast
      with R
      have "(x, y) ∈ relations M a ∩ T × T" by blast
      with F XY tMT
      have "(x, y) ∈ relations M a ∩ (∪x. relations M x)^* `` {t} × (∪x. relations M x)<sup>*</sup> `` {t}"
        by blast }
    ultimately show "Restr (relations M a) ((∪x. relations M x)^* `` {t}) =
      Restr (relations M' a) ((∪x. relations M' x)<sup>*</sup> `` {t})"
    apply -
    apply rule
     apply rule
     apply auto[1]
    apply rule
    apply (case_tac x)
    apply (simp (no_asm_use))
    apply (metis Image_singleton_iff mem_Sigma_iff)
    done
  qed
  from WORLDS RELATIONS V show ?thesis
    unfolding gen_model_def by simp
qed

(*>*)

subsection ‹Simulations›

text‹

 label{sec:kripke-theory-simulations}

  \emph{simulation}, or \emph{p-morphism}, is a mapping from the
  of one Kripke structure to another that preserves the truth of
  formulas at related worlds 🚫‹‹\S3.4, Ex. 3.60› in "Chellas:1980"›.
  a function @{term "f"} must satisfy four properties. Firstly, the
  of the set of worlds of @{term "M"} under @{term "f"} should
  the set of worlds of @{term "M'"}.

 ›

definition
  sim_range :: "('a, 'p, 'w1) KripkeStructure
              → ('a, 'p, 'w2) KripkeStructure → ('w1 → 'w2) → bool"
where
  "sim_range M M' f ≡ worlds M' = f ` worlds M
                    ∧ (∀a. relations M' a ⊆ worlds M' × worlds M')"

text‹The value of a proposition should be the same at corresponding
 :›

definition
  sim_val :: "('a, 'p, 'w1) KripkeStructure
           → ('a, 'p, 'w2) KripkeStructure → ('w1 → 'w2) → bool"
where
  "sim_val M M' f ≡ ∀u ∈ worlds M. valuation M u = valuation M' (f u)"

text‹

  two worlds are related in @{term "M"}, then the simulation
  them to related worlds in @{term "M'"}; intuitively the
  relates enough worlds. We term this the \emph{forward}
 .

 ›

definition
  sim_f :: "('a, 'p, 'w1) KripkeStructure
         → ('a, 'p, 'w2) KripkeStructure → ('w1 → 'w2) → bool"
where
  "sim_f M M' f ≡
     ∀a u v. (u, v) ∈ relations M a ⟶ (f u, f v) ∈ relations M' a"

text‹

 , if two worlds @{term "f u"} and @{term "v'"} are related
  @{term "M'"}, then there is a pair of related worlds @{term "u"}
  @{term "v"} in @{term "M"} where @{term "f v = v'"}. Intuitively
  simulation makes enough distinctions. We term this the
 emph{reverse} property.

 ›

definition
  sim_r :: "('a, 'p, 'w1) KripkeStructure
         → ('a, 'p, 'w2) KripkeStructure → ('w1 → 'w2) → bool"
where
  "sim_r M M' f ≡ ∀a. ∀u ∈ worlds M. ∀v'.
              (f u, v') ∈ relations M' a
           ⟶ (∃v. (u, v) ∈ relations M a ∧ f v = v')"

definition "sim M M' f ≡ sim_range M M' f ∧ sim_val M M' f
                       ∧ sim_f M M' f ∧ sim_r M M' f"
(*<*)

lemma sim_rangeI[intro]:
  "[ worlds M' = f ` worlds M; (∧a. relations M' a ⊆ worlds M' × worlds M') ]
     ==> sim_range M M' f"
  unfolding sim_range_def by simp

lemma sim_valI[intro]:
  "(∧u. u ∈ worlds M ==> valuation M u = valuation M' (f u))
   ==> sim_val M M' f"
  unfolding sim_val_def by simp

lemma sim_fI[intro]:
  "(∧a u v. (u, v) ∈ relations M a ==> (f u, f v) ∈ relations M' a)
   ==> sim_f M M' f"
  unfolding sim_f_def by simp

lemma sim_fD:
  "[ (u, v) ∈ relations M a; sim M M' f ]
     ==> (f u, f v) ∈ relations M' a"
  unfolding sim_def sim_f_def by blast

lemma sim_rI[intro]:
  "(∧a u v'.
    [u ∈ worlds M; (f u, v') ∈ relations M' a]
    ==> (∃v. (u, v) ∈ relations M a ∧ f v = v'))
  ==> sim_r M M' f"
  unfolding sim_r_def by simp

lemma sim_rD:
  "[ (f u, v') ∈ relations M' a; sim M M' f; u ∈ worlds M ]
     ==> (∃v. (u, v) ∈ relations M a ∧ f v = v')"
  unfolding sim_def sim_r_def by blast

lemma simI[intro]:
  "[ sim_range M M' f; sim_val M M' f; sim_f M M' f; sim_r M M' f ]
     ==> sim M M' f"
  unfolding sim_def by simp

text‹The identity is a simulation:›

lemma sim_id: "kripke M ==> sim M M id"
(*<*)
  unfolding sim_def sim_r_def sim_f_def sim_range_def sim_val_def
  by auto
(*>*)

(*>*)

text‹

  to the common knowledge modality, we need to show the simulation
  lift through the transitive closure. In particular we can
  that forward simulation is preserved:

 ›

lemma sim_f_tc:
  assumes s: "sim M M' f"
  assumes uv': "(u, v) ∈ (∪a∈as. relations M a)⁺"
  shows "(f u, f v) ∈ (∪a∈as. relations M' a)⁺"
(*<*)
  using assms
  by - ( induct rule: trancl_induct[OF uv']
       , auto dest: sim_fD intro: trancl_into_trancl )
(*>*)
text‹

  simulation also:

 ›

lemma sim_r_tc:
  assumes M: "kripke M"
  assumes s: "sim M M' f"
  assumes u: "u ∈ worlds M"
  assumes fuv': "(f u, v') ∈ (∪a∈as. relations M' a)⁺"
  obtains v where "f v = v'" and "(u, v) ∈ (∪a∈as. relations M a)⁺"
(*<*)
proof -
  assume E: "∧v. [f v = v'; (u, v) ∈ (∪a∈as. relations M a)⁺] ==> thesis"

  from fuv' have as_nempty: "as ≠ {}" by auto
  from fuv' have "∃v. f v = v' ∧ (u, v) ∈ (∪a∈as. relations M a)⁺"
  proof(induct rule: trancl_induct)
    case (base v') with u s as_nempty show ?case
      by (blast dest: sim_rD)
  next
    case (step v' w')
    hence fuv': "(f u, v') ∈ (∪a∈as. relations M' a)⁺"
      and v'w': "(v', w') ∈ (∪a∈as. relations M' a)" by fast+
    from step
    obtain v where vv': "f v = v'"
               and uv: "(u, v) ∈ (∪a∈as. relations M a)⁺"
      by blast
    from s v'w' vv' kripke_tc_rels_worlds[OF uv M]
    obtain w where ww': "f w = w'"
               and vw: "(v, w) ∈ (∪a∈as. relations M a)"
      by (blast dest: sim_rD)
    from uv vw ww' show ?case by (blast intro: trancl_trans)
  qed
  with E show thesis by blast
qed

lemma sim_f_trc:
  assumes uv': "(u, v) ∈ (∪a. relations M a)^*"
      and s: "sim M M' f"
  shows "(f u, f v) ∈ (∪a. relations M' a)^*"
  using assms
  by - ( induct rule: rtrancl_induct[OF uv']
       , auto dest: sim_fD intro: rtrancl_into_rtrancl )

lemma sim_r_trc:
  assumes s: "sim M M' f"
      and fuv': "(f u, v') ∈ (∪a. relations M' a)^*"
      and M: "kripke M"
      and u: "u ∈ worlds M"
  obtains v
    where "f v = v'"
      and "(u, v) ∈ (∪a. relations M a)^*"
proof -
  assume E: "∧v. [f v = v'; (u, v) ∈ (∪a. relations M a)^*] ==> thesis"
  from fuv' have "∃v. f v = v' ∧ (u, v) ∈ (∪a. relations M a)^*"
  proof(induct rule: rtrancl_induct)
    case base show ?case by blast
  next
    case (step v' w')
    hence fuv': "(f u, v') ∈ (∪a. relations M' a)^*"
      and v'w': "(v', w') ∈ (∪a. relations M' a)" by fast+
    from step
    obtain v where vv': "f v = v'"
               and uv: "(u, v) ∈ (∪a. relations M a)^*"
      by blast
    from s v'w' vv' kripke_rels_trc_worlds[OF uv u M]
    obtain w where ww': "f w = w'"
               and vw: "(v, w) ∈ (∪a. relations M a)"
      by (blast dest: sim_rD)
    from uv vw ww' show ?case by (blast intro: rtrancl_trans)
  qed
  with E show thesis by blast
qed

lemma sim_trc_commute:
  assumes M: "kripke M"
      and s: "sim M M' f"
      and t: "t ∈ worlds M"
  shows "f ` ((∪a. relations M a)^* `` {t})
       = (∪a. relations M' a)<sup>*</sup> `` {f t}" (is "?lhs = ?rhs")
proof
  from M s show "?lhs ⊆ ?rhs" by (auto intro: sim_f_trc)
next
  from M s t show "?rhs ⊆ ?lhs" by (auto elim: sim_r_trc)
qed

lemma sim_kripke: "[ sim M M' f; kripke M ] ==> kripke M'"
  unfolding sim_def sim_range_def by (rule kripkeI, blast)

lemma sim_S5n:
  assumes S5n: "S5n M"
      and sim: "sim M M' f"
  shows "S5n M'"
proof(intro S5nI equivI)
  show "∧a. relations M' a ⊆ worlds M' × worlds M'"
    by (metis S5n S5n_kripke kripke_def sim sim_kripke)
next
  fix a from S5n sim show "refl_on (worlds M') (relations M' a)"
     using sim_kripke S5n_kripke
     unfolding S5n_def equiv_def sim_def sim_f_def sim_range_def
     by - (rule refl_onI, (simp, blast dest: refl_onD)+)
next
  fix a
  { fix u v assume uv: "(u, v) ∈ relations M' a"
    from sim uv
    obtain u' where uw: "u' ∈ worlds M"
                and fu: "u = f u'"
      unfolding sim_def sim_range_def by bestsimp
    from sim uv fu uw
    obtain v' where u'v': "(u', v') ∈ relations M a"
                and fv: "v = f v'"
      unfolding sim_def sim_r_def sim_range_def by best
    from S5n u'v' have "(v', u') ∈ relations M a"
      unfolding S5n_def equiv_def by (blast dest: symD)
    with sim fu fv have "(v, u) ∈ relations M' a"
      unfolding sim_def sim_f_def by simp }
  thus "sym (relations M' a)" by (blast intro: symI)
next
  fix a
  { fix x y z
    assume xy: "(x, y) ∈ relations M' a"
       and yz: "(y, z) ∈ relations M' a"
    from sim xy
    obtain x' where xw: "x' ∈ worlds M"
                and fx: "x = f x'"
      unfolding sim_def sim_range_def by bestsimp
    from sim xy fx xw
    obtain y' where x'y': "(x', y') ∈ relations M a"
                and fy: "y = f y'"
      unfolding sim_def sim_r_def sim_range_def by best
    from S5n sim yz fy x'y'
    obtain z' where y'z': "(y', z') ∈ relations M a"
                and fz: "z = f z'"
      unfolding sim_def sim_r_def sim_range_def by best
    from S5n x'y' y'z' have "(x', z') ∈ relations M a"
      unfolding S5n_def equiv_def by (blast dest: transD)
    with sim fx fy fz have "(x, z) ∈ relations M' a"
      unfolding sim_def sim_f_def by simp }
  thus "trans (relations M' a)" by (blast intro: transI)
qed

(*>*)
text‹

  we establish the key property of simulations, that they
  the satisfaction of all formulas in the following way:

 ›

lemma sim_semantic_equivalence:
  assumes M: "kripke M"
  assumes s: "sim M M' f"
  assumes u: "u ∈ worlds M"
  shows "M, u ⊨ φ ⟷ M', f u ⊨ φ"
(*<*)
using u
proof(induct φ arbitrary: u)
  case (Kknows a ψ u)
  hence u: "u ∈ worlds M" by fast
  show ?case
  proof
    assume lhs: "M, u ⊨ Kknows a ψ"
    { fix v' assume "(f u, v') ∈ relations M' a"
      with s u obtain v where uv:  "(u, v) ∈ relations M a"
                          and vv': "f v = v'"
        by (blast dest: sim_rD)
      from lhs uv have "M, v ⊨ ψ" by simp
      with kripke_rels_worlds[OF uv M] vv' Kknows
      have "M', v' ⊨ ψ" by auto }
    thus "M', f u ⊨ Kknows a ψ" by simp
  next
    assume rhs: "M', f u ⊨ Kknows a ψ"
    { fix v assume uv: "(u, v) ∈ relations M a"
      with s have "(f u, f v) ∈ relations M' a"
        by (blast dest: sim_fD)
      with rhs have "M', f v ⊨ ψ" by simp
      with kripke_rels_worlds[OF uv M] Kknows s
      have "M, v ⊨ ψ" by auto }
    thus "M, u ⊨ Kknows a ψ" by simp
  qed
next
  case (Kcknows as ψ)
  hence u: "u ∈ worlds M" by fast
  show ?case
  proof
    assume lhs: "M, u ⊨ Kcknows as ψ"
    { fix v' assume "(f u, v') ∈ (∪x∈set as. relations M' x)⁺"
      with M s u
      obtain v where uv:  "(u, v) ∈ (∪x∈set as. relations M x)⁺"
                and vv': "f v = v'"
        by (blast intro: sim_r_tc)
      from uv lhs have "M, v ⊨ ψ" by simp
      with kripke_tc_rels_worlds[OF uv M] vv' Kcknows
      have "M', v' ⊨ ψ" by auto }
    thus "M', f u ⊨ Kcknows as ψ" by simp
  next
    assume rhs: "M', f u ⊨ Kcknows as ψ"
    { fix v assume uv: "(u, v) ∈ (∪x∈set as. relations M x)⁺"
      with s have "(f u, f v) ∈ (∪x∈set as. relations M' x)⁺"
        by (blast dest: sim_f_tc)
      with rhs have "M', f v ⊨ ψ" by simp
      with kripke_tc_rels_worlds[OF uv M] Kcknows s
      have "M, v ⊨ ψ" by auto }
    thus "M, u ⊨ Kcknows as ψ" by simp
  qed
qed (insert s,
     auto simp add: sim_range_def sim_def sim_val_def)
(*>*)

text‹

  proof is by structural induction over the formula @{term "φ"}. The
  cases appeal to our two simulation preservation lemmas.

 🚫‹"DBLP:journals/toplas/Sangiorgi09"› surveys the history of
 -morphisms and the related concept of \emph{bisimulation}.

  is all we need to know about Kripke structures.

 ›

(*<*)
end
(*>*)