theory Bisim_UL

lemma bisim_split:
  assumes ac: "bisim_underlying SR R' P P' a c"
  and     bd: "\<And>r r'. R' r r' \<Longrightarrow> bisim_underlying SR R (Q r) (Q' r') (b r) (d r')"
  and     v1: "\<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>"
  and     v2: "\<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>"
  shows "bisim_underlying SR R (P and S) (P' and S') (a >>= b) (c >>= d)" using ac apply - apply (rule bisim_underlyingI) apply (clarsimp simp: in_monad split_def) apply (erule (4) bisim_underlyingE1) apply (frule (1) use_valid [OF _ v1]) apply (frule (1) use_valid [OF _ v2]) apply (erule (4) bisim_underlyingE1 [OF bd]) apply (rename_tac r'' t'') apply (rule_tac x = "(r'', t'')" in bexI) apply clarsimp apply (fastforce simp: in_monad) apply (clarsimp simp: in_monad split_def) apply (erule (4) bisim_underlyingE2) apply (frule (1) use_valid [OF _ v1]) apply (frule (1) use_valid [OF _ v2]) apply (erule (4) bisim_underlyingE2 [OF bd]) apply (rename_tac r'' t'') apply (rule_tac x = "(r'', t'')" in bexI) apply clarsimp apply (fastforce simp: in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR R (P and S) (P' and S') (a >>= b) (c >>= d) proof (prove)
using this:
bisim_underlying SR R' P P' a c

goal (1 subgoal):
 1. bisim_underlying SR R (P and S) (P' and S') (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR R' P P' a c \<Longrightarrow> bisim_underlying SR R (P and S) (P' and S') (a >>= b) (c >>= d) proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r, t) \<in> fst ((a >>= b) s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst ((c >>= d) s'). R r r' \<and> SR t t'
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t s'' x. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> SR t (snd x)
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t s'' x r' t'. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); R' x r'; SR s'' t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> SR t (snd x)
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t s'' x r' t'. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); R' x r'; SR s'' t'; Q x s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> SR t (snd x)
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t s'' x r' t'. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); R' x r'; SR s'' t'; Q x s''; Q' r' t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> SR t (snd x)
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t s'' x r' t' r'a t'a. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); SR s'' t'; Q x s''; Q' r' t'; (r'a, t'a) \<in> fst (d r' t'); R r r'a; SR t t'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> SR t (snd x)
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t s'' x r' t' r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); SR s'' t'; Q x s''; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; SR t t''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((c >>= d) s'). R r (fst x) \<and> SR t (snd x)
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (3 subgoals):
 1. \<And>s s' r t s'' x r' t' r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); SR s'' t'; Q x s''; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; SR t t''\<rbrakk> \<Longrightarrow> R r (fst (r'', t'')) \<and> SR t (snd (r'', t''))
 2. \<And>s s' r t s'' x r' t' r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); SR s'' t'; Q x s''; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; SR t t''\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((c >>= d) s')
 3. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t s'' x r' t' r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (a s); (r, t) \<in> fst (b x s''); (r', t') \<in> fst (c s'); SR s'' t'; Q x s''; Q' r' t'; (r'', t'') \<in> fst (d r' t'); R r r''; SR t t''\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((c >>= d) s')
 2. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; (P and S) s; (P' and S') s'; (r', t') \<in> fst ((c >>= d) s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst ((a >>= b) s). R r r' \<and> SR t t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' s'' x. \<lbrakk>bisim_underlying SR R' P P' a c; SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s). R (fst x) r' \<and> SR (snd x) t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' s'' x r t. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); R' r x; SR t s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s). R (fst x) r' \<and> SR (snd x) t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' s'' x r t. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); R' r x; SR t s''; Q r t\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s). R (fst x) r' \<and> SR (snd x) t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' s'' x r t. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); R' r x; SR t s''; Q r t; Q' x s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s). R (fst x) r' \<and> SR (snd x) t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' s'' x r t ra ta. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); SR t s''; Q r t; Q' x s''; (ra, ta) \<in> fst (b r t); R ra r'; SR ta t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s). R (fst x) r' \<and> SR (snd x) t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' s'' x r t r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); SR t s''; Q r t; Q' x s''; (r'', t'') \<in> fst (b r t); R r'' r'; SR t'' t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((a >>= b) s). R (fst x) r' \<and> SR (snd x) t' proof (prove)
goal (2 subgoals):
 1. \<And>s s' r' t' s'' x r t r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); SR t s''; Q r t; Q' x s''; (r'', t'') \<in> fst (b r t); R r'' r'; SR t'' t'\<rbrakk> \<Longrightarrow> R (fst (r'', t'')) r' \<and> SR (snd (r'', t'')) t'
 2. \<And>s s' r' t' s'' x r t r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); SR t s''; Q r t; Q' x s''; (r'', t'') \<in> fst (b r t); R r'' r'; SR t'' t'\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((a >>= b) s) proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t' s'' x r t r'' t''. \<lbrakk>SR s s'; P s; S s; P' s'; S' s'; (x, s'') \<in> fst (c s'); (r', t') \<in> fst (d x s''); (r, t) \<in> fst (a s); SR t s''; Q r t; Q' x s''; (r'', t'') \<in> fst (b r t); R r'' r'; SR t'' t'\<rbrakk> \<Longrightarrow> (r'', t'') \<in> fst ((a >>= b) s) proof (prove)
goal:
No subgoals!