theory Bisim_UL

lemma bisim_splitE:
  assumes ac: "bisim_underlying SR (f \<oplus> R') P P' a c"
  and     bd: "\<And>r r'. R' r r' \<Longrightarrow> bisim_underlying SR (f \<oplus> 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 (f \<oplus> R) (P and S) (P' and S') (a >>=E b) (c >>=E d)" apply (simp add: bindE_def lift_def[abs_def]) apply (rule bisim_split [where Q = "\<lambda>r s. case_sum  (\<lambda>_. True) (\<lambda>l. Q l s) r" and Q' = "\<lambda>r s. case_sum  (\<lambda>_. True) (\<lambda>l. Q' l s) r", OF ac, folded validE_def, folded validE_R_def]) apply (case_tac r') apply clarsimp apply (erule bisim_throwError') apply clarsimp apply (erule bd) apply (rule v1) apply (rule v2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR (f \<oplus> R) (P and S) (P' and S') (a >>=E b) (c >>=E d) proof (prove)
goal (1 subgoal):
 1. bisim_underlying SR (f \<oplus> R) (P and S) (P' and S') (do v <- a;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v'
od) (do v <- c;
case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v'
od) proof (prove)
goal (3 subgoals):
 1. \<And>r r'. (f \<oplus> R') r r' \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (\<lambda>s. case r of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q l s) (\<lambda>s. case r' of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q' l s) (case r of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') (case r' of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v')
 2. \<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>, -
 3. \<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>r r' a. \<lbrakk>(f \<oplus> R') r r'; r' = Inl a\<rbrakk> \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (\<lambda>s. case r of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q l s) (\<lambda>s. case r' of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q' l s) (case r of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') (case r' of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v')
 2. \<And>r r' ba. \<lbrakk>(f \<oplus> R') r r'; r' = Inr ba\<rbrakk> \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (\<lambda>s. case r of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q l s) (\<lambda>s. case r' of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q' l s) (case r of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') (case r' of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v')
 3. \<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>, -
 4. \<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>a x'. f x' a \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (\<lambda>s. True) (\<lambda>s. True) (throwError x') (throwError a)
 2. \<And>r r' ba. \<lbrakk>(f \<oplus> R') r r'; r' = Inr ba\<rbrakk> \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (\<lambda>s. case r of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q l s) (\<lambda>s. case r' of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q' l s) (case r of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') (case r' of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v')
 3. \<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>, -
 4. \<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>r r' ba. \<lbrakk>(f \<oplus> R') r r'; r' = Inr ba\<rbrakk> \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (\<lambda>s. case r of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q l s) (\<lambda>s. case r' of Inl uu_ \<Rightarrow> True | Inr l \<Rightarrow> Q' l s) (case r of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') (case r' of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> d v')
 2. \<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>, -
 3. \<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>ba x'. R' x' ba \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (Q x') (Q' ba) (b x') (d ba)
 2. \<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>, -
 3. \<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>, -
 2. \<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, - proof (prove)
goal:
No subgoals!