theory Corres_UL

lemma corres_splitEE_prod:
  assumes x: "corres_underlying sr nf nf' (f \<oplus> r') P P' a c"
  assumes y: "\<And>x y x' y'. r' (x, y) (x', y')
              \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R x y) (R' x' y') (b x y) (d x' y')"
  assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>\<lambda>(x, y). R x y \<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>(x, y). R' x y\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>"
  shows      "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>(x, y). b x y)) (c >>=E (\<lambda>(x, y). d x y))" using assms apply (unfold bindE_def validE_def) apply (rule corres_split[rotated 2], assumption+) apply (fastforce simp: lift_def y split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (doE (x, y) <- a;
b x y
odE) (doE (x, y) <- c;
d x y
odE) proof (prove)
using this:
corres_underlying sr nf nf' (f \<oplus> r') P P' a c
r' (?x, ?y) (?x', ?y') \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R ?x ?y) (R' ?x' ?y') (b ?x ?y) (d ?x' ?y')
\<lbrace>Q\<rbrace> a \<lbrace>\<lambda>(x, y). R x y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
\<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>(x, y). R' x y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>

goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (doE (x, y) <- a;
b x y
odE) (doE (x, y) <- c;
d x y
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>x y x' y'. r' (x, y) (x', y') \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R x y) (R' x' y') (b x y) (d x' y'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (case r of (x, xa) \<Rightarrow> R x xa) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (case r of (x, xa) \<Rightarrow> R' x xa) s\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>= lift (\<lambda>(x, y). b x y)) (c >>= lift (\<lambda>(x, y). d x y)) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> r') P P' a c; \<And>x y x' y'. r' (x, y) (x', y') \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R x y) (R' x' y') (b x y) (d x' y'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (case r of (x, xa) \<Rightarrow> R x xa) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (case r of (x, xa) \<Rightarrow> R' x xa) s\<rbrace>; (f \<oplus> r') rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (case r of (x, xa) \<Rightarrow> R x xa) s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> (case r of (x, xa) \<Rightarrow> R' x xa) s) (lift (\<lambda>(x, y). b x y) rv) (lift (\<lambda>(x, y). d x y) rv') proof (prove)
goal:
No subgoals!