# Theory Bisim

```section "Bisimilarity, abstractly"

theory Bisim
imports Interface
begin

type_synonym 'a rel = "('a * 'a) set"
type_synonym ('cmd,'state)config = "'cmd * 'state"

definition mono where
"mono Retr ≡
∀ theta theta'. theta ≤ theta' ⟶ Retr theta ≤ Retr theta'"

definition simul where
"simul Retr theta ≡ theta ≤ Retr theta"

definition bisim where
"bisim Retr theta ≡ sym theta ∧ simul Retr theta"

lemma mono_Union:
assumes "mono Retr"
shows "Union (Retr ` Theta) ≤ Retr (Union Theta)"
proof-
have "∀ theta' ∈ Retr ` Theta. theta' ⊆ Retr (Union Theta)"
using assms unfolding mono_def by blast
thus ?thesis by blast
qed

lemma mono_Un:
assumes "mono Retr"
shows "Retr theta Un Retr theta' ⊆ Retr (theta Un theta')"
using assms unfolding mono_def
by (metis Un_least Un_upper1 Un_upper2)

lemma sym_Union:
assumes "⋀theta. theta ∈ Theta ⟹ sym theta"
shows "sym (Union Theta)"
using assms unfolding sym_def by blast

lemma sym_Un:
assumes "sym theta1" and "sym theta2"
shows "sym (theta1 Un theta2)"
using assms sym_Union[of "{theta1,theta2}"] by auto

lemma simul_Union:
assumes "mono Retr"
and "⋀theta. theta ∈ Theta ⟹ simul Retr theta"
shows "simul Retr (Union Theta)"
proof-
have "∀ theta ∈ Theta. theta ⊆ Retr theta"
using assms unfolding simul_def by blast
hence "Union Theta ⊆ Union (Retr ` Theta)" by blast
also have "... ⊆ Retr (Union Theta)" using mono_Union assms unfolding mono_def by auto
finally have "Union Theta ⊆ Retr (Union Theta)" .
thus ?thesis unfolding simul_def by simp
qed

lemma simul_Un:
assumes "mono Retr" and "simul Retr theta1" and "simul Retr theta2"
shows "simul Retr (theta1 Un theta2)"
using assms simul_Union[of Retr "{theta1,theta2}"] by auto

lemma bisim_Union:
assumes "mono Retr" and "⋀theta. theta ∈ Theta ⟹ bisim Retr theta"
shows "bisim Retr (Union Theta)"
using assms unfolding bisim_def
using sym_Union simul_Union by blast

lemma bisim_Un:
assumes "mono Retr" and "bisim Retr theta1" and "bisim Retr theta2"
shows "bisim Retr (theta1 Un theta2)"
using assms bisim_Union[of Retr "{theta1,theta2}"] by auto

definition bis where
"bis Retr ≡ Union {theta. bisim Retr theta}"

lemma bisim_bis[simp]:
assumes "mono Retr"
shows "bisim Retr (bis Retr)"
using assms unfolding mono_def
by (metis CollectD assms bis_def bisim_Union)

corollary sym_bis[simp]: "mono Retr ⟹ sym (bis Retr)"
and simul_bis[simp]: "mono Retr ⟹ simul Retr (bis Retr)"
using bisim_bis unfolding bisim_def by auto

lemma bis_raw_coind:
assumes "mono Retr" and "sym theta" and "theta ⊆ Retr theta"
shows "theta ⊆ bis Retr"
using assms unfolding mono_def bis_def bisim_def simul_def by blast

lemma bis_prefix[simp]:
assumes "mono Retr"
shows "bis Retr ⊆ Retr (bis Retr)"
by (metis assms bisim_bis bisim_def simul_def)

lemma bis_coind:
assumes *: "mono Retr" and "sym theta" and **: "theta ⊆ Retr (theta Un (bis Retr))"
shows "theta ⊆ bis Retr"
proof-
let ?theta' = "theta Un (bis Retr)"
have "sym ?theta'" by (metis Bisim.sym_Un sym_bis assms)
moreover have "?theta' ⊆ Retr ?theta'"
by (metis assms mono_Un Un_least bis_prefix le_supI2 subset_trans)
ultimately show ?thesis using * bis_raw_coind by blast
qed

lemma bis_coind2:
assumes *: "mono Retr" and
**: "theta ⊆ Retr (theta Un (bis Retr))" and
***: "theta ^-1 ⊆ Retr ((theta ^-1) Un (bis Retr))"
shows "theta ⊆ bis Retr"
proof-
let ?th = "theta Un theta ^-1"
have "sym ?th" by (metis sym_Un_converse)
moreover
{have "?th ⊆ Retr (theta Un (bis Retr)) Un Retr (theta ^-1 Un (bis Retr))"
using ** *** Un_mono by blast
also have "... ⊆ Retr ((theta Un (bis Retr)) Un (theta ^-1 Un (bis Retr)))"
using * mono_Un by blast
also have "... = Retr (?th Un (bis Retr))" by (metis Un_assoc Un_commute Un_left_absorb)
finally have "?th ⊆ Retr (?th Un (bis Retr))" .
}
ultimately have "?th ⊆ bis Retr" using assms bis_coind by blast
thus ?thesis by blast
qed

lemma bis_raw_coind2:
assumes *: "mono Retr" and
**: "theta ⊆ Retr theta" and
***: "theta ^-1 ⊆ Retr (theta ^-1)"
shows "theta ⊆ bis Retr"
proof-
have "theta ⊆ Retr (theta Un (bis Retr))" and
"theta ^-1 ⊆ Retr ((theta ^-1) Un (bis Retr))"
using assms by(metis mono_Un le_supI1 subset_trans)+
thus ?thesis using * bis_coind2 by blast
qed

lemma mono_bis:
assumes "mono Retr1"  and "mono Retr2"
and "⋀ theta. Retr1 theta ⊆ Retr2 theta"
shows "bis Retr1 ⊆ bis Retr2"
by (metis assms bis_prefix bis_raw_coind subset_trans sym_bis)

end
```