theory Bisim_UL

lemma bisim_split_reflE:
  assumes ab: "\<And>r. bisim (f \<oplus> R) (Q r) (Q' r) (a r) (b r)"
  and     v1: "\<lbrace>S\<rbrace> m \<lbrace>Q\<rbrace>, -"
  and     v2: "\<lbrace>S'\<rbrace> m \<lbrace>Q'\<rbrace>, -"
  and  refls: "\<And>e. f e e" "\<And>r. R r r"
  shows "bisim (f \<oplus> R) S S' (m >>=E a) (m >>=E b)" using refls apply - apply (rule bisim_guard_imp) apply (rule bisim_splitE [where R' = "(=)", OF _ _ v1 v2]) apply (rule bisim_refl) apply (case_tac r, simp_all)[1] apply simp apply (rule ab) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> R) S S' (m >>=E a) (m >>=E b) proof (prove)
using this:
f ?e ?e
R ?r ?r

goal (1 subgoal):
 1. bisim (f \<oplus> R) S S' (m >>=E a) (m >>=E b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>e. f e e; \<And>r. R r r\<rbrakk> \<Longrightarrow> bisim (f \<oplus> R) S S' (m >>=E a) (m >>=E b) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>e. f e e; \<And>r. R r r\<rbrakk> \<Longrightarrow> bisim (f \<oplus> R) ?Q4 ?Q'4 (m >>=E a) (m >>=E b)
 2. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S' s\<rbrakk> \<Longrightarrow> ?Q'4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>e. f e e; \<And>r. R r r\<rbrakk> \<Longrightarrow> bisim (f \<oplus> (=)) ?P8 ?P'8 m m
 2. \<And>r r'. \<lbrakk>\<And>e. f e e; \<And>r. R r r; r = r'\<rbrakk> \<Longrightarrow> bisim (f \<oplus> R) (Q r) (Q' r') (a r) (b r')
 3. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S s\<rbrakk> \<Longrightarrow> (?P8 and S) s
 4. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S' s\<rbrakk> \<Longrightarrow> (?P'8 and S') s proof (prove)
goal (4 subgoals):
 1. \<And>r. \<lbrakk>\<And>e. f e e; \<And>r. R r r\<rbrakk> \<Longrightarrow> (f \<oplus> (=)) r r
 2. \<And>r r'. \<lbrakk>\<And>e. f e e; \<And>r. R r r; r = r'\<rbrakk> \<Longrightarrow> bisim (f \<oplus> R) (Q r) (Q' r') (a r) (b r')
 3. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S s\<rbrakk> \<Longrightarrow> (?P8 and S) s
 4. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S' s\<rbrakk> \<Longrightarrow> (?P'8 and S') s proof (prove)
goal (3 subgoals):
 1. \<And>r r'. \<lbrakk>\<And>e. f e e; \<And>r. R r r; r = r'\<rbrakk> \<Longrightarrow> bisim (f \<oplus> R) (Q r) (Q' r') (a r) (b r')
 2. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S s\<rbrakk> \<Longrightarrow> (?P8 and S) s
 3. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S' s\<rbrakk> \<Longrightarrow> (?P'8 and S') s proof (prove)
goal (3 subgoals):
 1. \<And>r r'. \<lbrakk>\<And>e. f e e; \<And>r. R r r; r = r'\<rbrakk> \<Longrightarrow> bisim (f \<oplus> R) (Q r') (Q' r') (a r') (b r')
 2. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S s\<rbrakk> \<Longrightarrow> (?P8 and S) s
 3. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S' s\<rbrakk> \<Longrightarrow> (?P'8 and S') s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S s\<rbrakk> \<Longrightarrow> (?P8 and S) s
 2. \<And>s. \<lbrakk>\<And>e. f e e; \<And>r. R r r; S' s\<rbrakk> \<Longrightarrow> (?P'8 and S') s proof (prove)
goal:
No subgoals!