Theory Kripke

(*<*)
(*
 * 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}

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

The syntax includes one knowledge modality per agent, and one for
\emph{common knowledge} amongst a set of agents. It is parameterised
by 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‹

A Kripke structure consists of a set of \emph{worlds} of type @{typ
"'w"}, one \emph{accessibility relation} between worlds for each agent
and a \emph{valuation function} that indicates the truth of a
proposition at a world. This is a very general story that we will
quickly 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 ‹

The standard semantics for knowledge is given by taking the
accessibility relations to be equivalence relations, yielding the
S$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‹

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

›

subsection‹Satisfaction›

text‹

A formula $\phi$ is satisfied at a world $w$ in Kripke structure $M$
in 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⇩a φ) = (∀w' ∈ relations M a `` {w}. M, w' ⊨ φ)"
| "M, w ⊨ (❙C⇘as⇙ φ) = (∀w' ∈ (⋃a ∈ set as. relations M a)⇧+ `` {w}. M, w' ⊨ φ)"

text‹

The first three clauses are standard.

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

The clause for @{term "Kcknows as φ"} captures what it means for the
set of agents @{term "as"} to commonly know @{term "φ"}; roughly,
everyone knows @{term "φ"} and knows that everyone knows it, and so
forth. Note that the transitive closure and the reflexive-transitive
closure generate the same relation due to the reflexivity of the
agents' accessibility relations; we use the former as it has a more
pleasant 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‹

A key property of the semantics for common knowledge is that it forms
an 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)
  from E is_nempty show "refl_on A ((⋃i∈is. f i)⇧+)"
    unfolding equiv_def
    apply -
    apply (rule refl_onI)
    apply (rule trancl_Int_subset)
    apply (auto dest: refl_onD refl_onD1 refl_onD2)
    done
  from E show "sym ((⋃i∈is. f i)⇧+)"
    apply -
    apply (rule sym_trancl)
    unfolding equiv_def sym_def by blast
  show "trans  ((⋃i∈is. f i)⇧+)" by (rule 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)⇧+ `` {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‹

The relation between knowledge and common knowledge can be understood
as follows, following \<^citet>‹‹\S2.4› in "FHMV:1995"›. Firstly, that $\phi$
is common knowledge to a set of agents $as$ can be seen as asserting
that everyone in $as$ knows $\phi$ and moreover knows that it is
common 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‹

Secondly we can provide an induction schema for the introduction of
common knowledge: from everyone in $as$ knows that $\phi$ implies
$\phi \land \psi$, and that $\phi$ is satisfied at world $w$, infer
that $\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⇩a (Kand φ ψ)"
  assumes p: "M, w ⊨ φ"
  shows "M, w ⊨ ❙C⇘as⇙ ψ"
(*<*)
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}

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

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

Given 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‹

where we take the image of @{term "w"} under the reflexive transitive
closure of the agents' relations, we can show that the satisfaction of
a formula @{term "φ"} at a world @{term "w'"} is preserved, provided
@{term "w'"} is relevant to the world @{term "w"} that the sub-model
is 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‹

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

›
(*<*)

lemma gen_model_S5n:
  assumes S5n: "S5n M"
  shows "S5n (gen_model M w)"
proof(intro S5nI equivI)
  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‹

If two models generate the same sub-model for a world, they satisfy
the 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 ‹

Our final lemma in this section is technical: it allows us to move
between 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)⇧* `` {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)⇧* `` {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)⇧* `` {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)⇧* `` {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)⇧* `` {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)⇧* `` {t}"
        by blast }
    moreover
    { fix a x y
      assume XY: "(x, y) ∈ relations M' a ∩ (⋃x. relations M' x)⇧* `` {t} × (⋃x. relations M' x)⇧* `` {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)⇧* `` {t}"
        by blast }
    ultimately show "Restr (relations M a) ((⋃x. relations M x)⇧* `` {t}) =
      Restr (relations M' a) ((⋃x. relations M' x)⇧* `` {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}

A \emph{simulation}, or \emph{p-morphism}, is a mapping from the
worlds of one Kripke structure to another that preserves the truth of
all formulas at related worlds \<^citep>‹‹\S3.4, Ex. 3.60› in "Chellas:1980"›.
Such a function @{term "f"} must satisfy four properties. Firstly, the
image of the set of worlds of @{term "M"} under @{term "f"} should
equal 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
worlds:›

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‹

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

›

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‹

Conversely, if two worlds @{term "f u"} and @{term "v'"} are related
in @{term "M'"}, then there is a pair of related worlds @{term "u"}
and @{term "v"} in @{term "M"} where @{term "f v = v'"}. Intuitively
the 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‹

Due to the common knowledge modality, we need to show the simulation
properties lift through the transitive closure. In particular we can
show 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‹

Reverse 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)⇧* `` {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)
  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‹

Finally we establish the key property of simulations, that they
preserve 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‹

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

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

This is all we need to know about Kripke structures.

›

(*<*)
end
(*>*)