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