theory Bisim_UL

lemma bisim_split_bind_case_sum:
  "\<lbrakk>bisim_underlying sr (lr \<oplus> rr) P P' a d;
   \<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv');
   \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk>
  \<Longrightarrow> bisim_underlying sr r (P and Q) (P' and Q') (a >>= case_sum b c) (d >>= case_sum e f)" apply (erule bisim_split [where Q = "\<lambda>rv s. case_sum (\<lambda>l. R l s) (\<lambda>r. S r s) rv" and Q' = "\<lambda>rv s. case_sum (\<lambda>l. R' l s) (\<lambda>r. S' r s) rv", folded validE_def]) apply (case_tac r') apply clarsimp apply clarsimp apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bisim_underlying sr (lr \<oplus> rr) P P' a d; \<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> bisim_underlying sr r (P and Q) (P' and Q') (a >>= case_sum b c) (d >>= case_sum e f) proof (prove)
goal (3 subgoals):
 1. \<And>ra r'. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>; (lr \<oplus> rr) ra r'\<rbrakk> \<Longrightarrow> bisim_underlying sr r (\<lambda>s. case ra of Inl l \<Rightarrow> R l s | Inr r \<Rightarrow> S r s) (\<lambda>s. case r' of Inl l \<Rightarrow> R' l s | Inr r \<Rightarrow> S' r s) (case ra of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case r' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x)
 2. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>
 3. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ra r' aa. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>; (lr \<oplus> rr) ra r'; r' = Inl aa\<rbrakk> \<Longrightarrow> bisim_underlying sr r (\<lambda>s. case ra of Inl l \<Rightarrow> R l s | Inr r \<Rightarrow> S r s) (\<lambda>s. case r' of Inl l \<Rightarrow> R' l s | Inr r \<Rightarrow> S' r s) (case ra of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case r' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x)
 2. \<And>ra r' ba. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>; (lr \<oplus> rr) ra r'; r' = Inr ba\<rbrakk> \<Longrightarrow> bisim_underlying sr r (\<lambda>s. case ra of Inl l \<Rightarrow> R l s | Inr r \<Rightarrow> S r s) (\<lambda>s. case r' of Inl l \<Rightarrow> R' l s | Inr r \<Rightarrow> S' r s) (case ra of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case r' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x)
 3. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>
 4. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ra r' ba. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>; (lr \<oplus> rr) ra r'; r' = Inr ba\<rbrakk> \<Longrightarrow> bisim_underlying sr r (\<lambda>s. case ra of Inl l \<Rightarrow> R l s | Inr r \<Rightarrow> S r s) (\<lambda>s. case r' of Inl l \<Rightarrow> R' l s | Inr r \<Rightarrow> S' r s) (case ra of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case r' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x)
 2. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>
 3. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>
 2. \<lbrakk>\<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace> proof (prove)
goal:
No subgoals!