theory Corres_UL

lemma corres_initial_splitE:
"\<lbrakk> corres_underlying sr nf nf' (f \<oplus> r') P P' a c;
   \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv');
   \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>;
   \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>\<rbrakk>
\<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) P P' (a >>=E b) (c >>=E d)" apply corres_pre apply (erule corres_splitEE) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) P P' (a >>=E b) (c >>=E d) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) ?Q ?Q' (a >>=E b) (c >>=E d)
 2. \<And>s s'. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; r' rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (?R1 rv) (?R'1 rv') (b rv) (d rv')
 2. \<lbrakk>\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q1\<rbrace> a \<lbrace>?R1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'1\<rbrace> c \<lbrace>?R'1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and ?Q1) s
 5. \<And>s s'. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' and ?Q'1) s' proof (prove)
goal:
No subgoals!