# Theory Simulation

```section ‹Simulation›
theory Simulation
imports Automata
begin

lemma finite_ImageI:
assumes "finite A"
assumes "⋀a. a∈A ⟹ finite (R``{a})"
shows "finite (R``A)"
proof -
have "R``A = ⋃{R``{a} | a. a:A}"
by auto
also have "finite (⋃{R``{a} | a. a:A})"
apply (rule finite_Union)
apply (clarsimp simp: assms)
done
finally show ?thesis .
qed

section ‹Simulation›

subsection ‹Functional Relations›

definition "the_br_α R ≡ λ x. SOME y. (x, y) ∈ R"
abbreviation (input) "the_br_invar R ≡ λ x. x ∈ Domain R"

lemma the_br[simp]:
assumes "single_valued R"
shows "br (the_br_α R) (the_br_invar R) = R"
unfolding build_rel_def the_br_α_def
apply auto
apply (metis someI_ex)
apply (metis assms someI_ex single_valuedD)
done

lemma the_br_br[simp]:
"I x ⟹ the_br_α (br α I) x = α x"
"the_br_invar (br α I) = I"
unfolding the_br_α_def build_rel_def[abs_def]
by auto

subsection ‹Relation between Runs›

definition run_rel :: "('a × 'b) set ⇒ ('a word × 'b word) set" where
"run_rel R ≡ {(ra, rb). ∀ i. (ra i, rb i) ∈ R}"

lemma run_rel_converse[simp]: "(ra, rb) ∈ run_rel (R¯) ⟷ (rb, ra) ∈ run_rel R"
unfolding run_rel_def by auto

lemma run_rel_single_valued: "single_valued R
⟹ (ra, rb) ∈ run_rel R ⟷ ((∀i. the_br_invar R (ra i)) ∧ rb = the_br_α R o ra)"
unfolding run_rel_def the_br_α_def
apply (auto intro!: ext)
apply (metis single_valuedD someI_ex)
apply (metis DomainE someI_ex)
done

subsection ‹Simulation›
locale simulation =
a: graph A +
b: graph B
for R :: "('a × 'b) set"
and A :: "('a, _) graph_rec_scheme"
and B :: "('b, _) graph_rec_scheme"
+
assumes nodes_sim: "a ∈ a.V ⟹ (a, b) ∈ R ⟹ b ∈ b.V"
assumes init_sim: "a0 ∈ a.V0 ⟹ ∃ b0. b0 ∈ b.V0 ∧ (a0, b0) ∈ R"
assumes step_sim: "(a, a') ∈ a.E ⟹ (a, b) ∈ R ⟹ ∃ b'. (b, b') ∈ b.E ∧ (a', b') ∈ R"
begin

lemma simulation_this: "simulation R A B" by unfold_locales

lemma run_sim:
assumes arun: "a.is_run ra"
obtains rb where "b.is_run rb" "(ra, rb) ∈ run_rel R"
proof -
from arun have ainit: "ra 0 ∈ a.V0"
and astep: "∀i. (ra i, ra (Suc i)) ∈ a.E"
using a.run_V0 a.run_ipath ipathD by blast+
from init_sim obtain rb0 where rel0: "(ra 0, rb0) ∈ R" and binit: "rb0 ∈ b.V0"
by (auto intro: ainit)

define rb
where "rb = rec_nat rb0 (λi rbi. SOME rbsi. (rbi, rbsi) ∈ b.E ∧ (ra (Suc i), rbsi) ∈ R)"

have [simp]:
"rb 0 = rb0"
"⋀i. rb (Suc i) = (SOME rbsi. (rb i, rbsi) ∈ b.E ∧ (ra (Suc i), rbsi) ∈ R)"
unfolding rb_def by auto

{
fix i
have "(rb i, rb (Suc i)) ∈ b.E ∧ (ra (Suc i), rb (Suc i)) ∈ R"
proof (induction i)
case 0
from step_sim astep rel0 obtain rb1 where "(rb 0, rb1) ∈ b.E" and "(ra 1, rb1) ∈ R"
by fastforce
thus ?case by (auto intro!: someI)
next
case (Suc i)
with step_sim astep obtain rbss where "(rb (Suc i), rbss) ∈ b.E" and
"(ra (Suc (Suc i)), rbss) ∈ R"
by fastforce
thus ?case by (auto intro!: someI)
qed
} note aux=this

from aux binit have "b.is_run rb"
unfolding b.is_run_def ipath_def by simp
moreover from aux rel0 have "(ra, rb) ∈ run_rel R"
unfolding run_rel_def
apply safe
apply (case_tac i)
by auto
ultimately show ?thesis by rule
qed

lemma stuck_sim:
assumes "(a, b) ∈ R"
assumes "b ∉ Domain b.E"
shows "a ∉ Domain a.E"
using assms
by (auto dest: step_sim)

lemma run_Domain: "a.is_run r ⟹ r i ∈ Domain R"
by (erule run_sim) (auto simp: run_rel_def)

lemma br_run_sim:
assumes "R = br α I"
assumes "a.is_run r"
shows "b.is_run (α o r)"
using assms
apply -
apply (erule run_sim)
apply (auto simp: run_rel_def build_rel_def a.is_run_def b.is_run_def ipath_def)
done

lemma is_reachable_sim: "a ∈ a.E⇧* `` a.V0 ⟹ ∃ b. (a, b) ∈ R ∧ b ∈ b.E⇧* `` b.V0"
apply safe
apply (erule rtrancl_induct)
apply (metis ImageI init_sim rtrancl.rtrancl_refl)
done

lemma reachable_sim: "a.E⇧* `` a.V0 ⊆ R¯ `` b.E⇧* `` b.V0"
using is_reachable_sim by blast

lemma reachable_finite_sim:
assumes "finite (b.E⇧* `` b.V0)"
assumes "⋀b. b ∈ b.E⇧* `` b.V0 ⟹ finite (R¯ `` {b})"
shows "finite (a.E⇧* `` a.V0)"
apply (rule finite_subset[OF reachable_sim])
apply (rule finite_ImageI)
apply fact+
done

end

lemma simulation_trans[trans]:
assumes "simulation R1 A B"
assumes "simulation R2 B C"
shows "simulation (R1 O R2) A C"
proof -
interpret s1: simulation R1 A B by fact
interpret s2: simulation R2 B C by fact
show ?thesis
apply unfold_locales
using s1.nodes_sim s2.nodes_sim apply blast
using s1.init_sim s2.init_sim apply blast
using s1.step_sim s2.step_sim apply blast
done
qed

lemma (in graph) simulation_refl[simp]: "simulation Id G G" by unfold_locales auto

locale lsimulation =
a: sa A +
b: sa B +
simulation R A B
for R :: "('a × 'b) set"
and A :: "('a, 'l, _) sa_rec_scheme"
and B :: "('b, 'l, _) sa_rec_scheme"
+
assumes labeling_consistent: "(a, b) ∈ R ⟹ a.L a = b.L b"
begin

lemma lsimulation_this: "lsimulation R A B" by unfold_locales

lemma run_rel_consistent: "(ra, rb) ∈ run_rel R ⟹ a.L o ra = b.L o rb"
using labeling_consistent unfolding run_rel_def
by auto

lemma accept_sim: "a.accept w ⟹ b.accept w"
unfolding a.accept_def b.accept_def
apply clarsimp
apply (erule run_sim)
apply (auto simp: run_rel_consistent)
done

end

lemma lsimulation_trans[trans]:
assumes "lsimulation R1 A B"
assumes "lsimulation R2 B C"
shows "lsimulation (R1 O R2) A C"
proof -
interpret s1: lsimulation R1 A B by fact
interpret s2: lsimulation R2 B C by fact
interpret simulation "R1 O R2" A C
using simulation_trans s1.simulation_this s2.simulation_this by this
show ?thesis
apply unfold_locales
using s1.labeling_consistent s2.labeling_consistent
by auto
qed

lemma (in sa) lsimulation_refl[simp]: "lsimulation Id G G" by unfold_locales auto

subsection ‹Bisimulation›

locale bisimulation =
a: graph A +
b: graph B +
s1: simulation "R" A B +
s2: simulation "R¯" B A
for R :: "('a × 'b) set"
and A :: "('a, _) graph_rec_scheme"
and B :: "('b, _) graph_rec_scheme"
begin

lemma bisimulation_this: "bisimulation R A B" by unfold_locales

lemma converse: "bisimulation (R¯) B A"
proof -
interpret simulation "(R¯)¯" A B by simp unfold_locales
show ?thesis by unfold_locales
qed

lemma br_run_conv:
assumes "R = br α I"
shows "b.is_run rb ⟷ (∃ra. rb=α o ra ∧ a.is_run ra)"
using assms
apply safe
apply (erule s2.run_sim, auto
intro!: ext
simp: run_rel_def build_rel_def) []
apply (erule s1.br_run_sim, assumption)
done

lemma bri_run_conv:
assumes "R = (br γ I)¯"
shows "a.is_run ra ⟷ (∃rb. ra=γ o rb ∧ b.is_run rb)"
using assms
apply safe
apply (erule s1.run_sim, auto simp: run_rel_def build_rel_def intro!: ext) []

apply (erule s2.run_sim, auto simp: run_rel_def build_rel_def)
by (metis (no_types, opaque_lifting) fun_comp_eq_conv)

lemma inj_map_run_eq:
assumes "inj α"
assumes E: "α o r1 = α o r2"
shows "r1 = r2"
proof (rule ext)
fix i
from E have "α (r1 i) = α (r2 i)"
with ‹inj α› show "r1 i = r2 i"
by (auto dest: injD)
qed

lemma br_inj_run_conv:
assumes INJ: "inj α"
assumes [simp]: "R = br α I"
shows "b.is_run (α o ra) ⟷ a.is_run ra"
apply (subst br_run_conv[OF assms(2)])
apply (auto dest: inj_map_run_eq[OF INJ])
done

lemma single_valued_run_conv:
assumes "single_valued R"
shows "b.is_run rb
⟷ (∃ra. rb=the_br_α R o ra ∧ a.is_run ra)"
using assms
apply safe
apply (erule s2.run_sim)
apply (erule s1.run_sim)
done

lemma stuck_bisim:
assumes A: "(a, b) ∈ R"
shows "a ∈ Domain a.E ⟷ b ∈ Domain b.E"
using s1.stuck_sim[OF A]
using s2.stuck_sim[OF A[THEN converseI[of _ _ R]]]
by blast

end

lemma bisimulation_trans[trans]:
assumes "bisimulation R1 A B"
assumes "bisimulation R2 B C"
shows "bisimulation (R1 O R2) A C"
proof -
interpret s1: bisimulation R1 A B by fact
interpret s2: bisimulation R2 B C by fact
interpret t1: simulation "(R1 O R2)" A C
using simulation_trans s1.s1.simulation_this s2.s1.simulation_this by this
interpret t2: simulation "(R1 O R2)¯" C A
using simulation_trans s2.s2.simulation_this s1.s2.simulation_this
unfolding converse_relcomp
by this
show ?thesis by unfold_locales
qed

lemma (in graph) bisimulation_refl[simp]: "bisimulation Id G G" by unfold_locales auto

locale lbisimulation =
a: sa A +
b: sa B +
s1: lsimulation "R" A B +
s2: lsimulation "R¯" B A +
bisimulation R A B
for R :: "('a × 'b) set"
and A :: "('a, 'l, _) sa_rec_scheme"
and B :: "('b, 'l, _) sa_rec_scheme"
begin

lemma lbisimulation_this: "lbisimulation R A B" by unfold_locales

lemma accept_bisim: "a.accept = b.accept"
apply (rule ext)
using s1.accept_sim s2.accept_sim by blast

end

lemma lbisimulation_trans[trans]:
assumes "lbisimulation R1 A B"
assumes "lbisimulation R2 B C"
shows "lbisimulation (R1 O R2) A C"
proof -
interpret s1: lbisimulation R1 A B by fact
interpret s2: lbisimulation R2 B C by fact

from lsimulation_trans[OF s1.s1.lsimulation_this s2.s1.lsimulation_this]
interpret t1: lsimulation "(R1 O R2)" A C .

from lsimulation_trans[OF s2.s2.lsimulation_this s1.s2.lsimulation_this, folded converse_relcomp]
interpret t2: lsimulation "(R1 O R2)¯" C A .

show ?thesis by unfold_locales
qed

lemma (in sa) lbisimulation_refl[simp]: "lbisimulation Id G G" by unfold_locales auto

end
```