theory Tcb_R

lemma corres_splitEE':
  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>%(x, y). R x y \<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>%(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 split_def) apply (rule corres_split[rotated 2]) apply assumption+ apply (case_tac rv) apply (clarsimp simp: lift_def y)+ 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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>= lift (\<lambda>p. b (fst p) (snd p))) (c >>= lift (\<lambda>p. d (fst p) (snd p))) proof (prove)
goal (4 subgoals):
 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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>?R5\<rbrace>
 2. \<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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> c \<lbrace>?R'5\<rbrace>
 3. \<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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' ?r'5 P P' a c
 4. \<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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s\<rbrace>; ?r'5 rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (?R5 rv) (?R'5 rv') (lift (\<lambda>p. b (fst p) (snd p)) rv) (lift (\<lambda>p. d (fst p) (snd p)) rv') 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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) 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> R (fst r) (snd r) s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s) (lift (\<lambda>p. b (fst p) (snd p)) rv) (lift (\<lambda>p. d (fst p) (snd p)) rv') proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' aa. \<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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s\<rbrace>; (f \<oplus> r') rv rv'; rv = Inl aa\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R (fst r) (snd r) s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s) (lift (\<lambda>p. b (fst p) (snd p)) rv) (lift (\<lambda>p. d (fst p) (snd p)) rv')
 2. \<And>rv rv' ba. \<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> R (fst r) (snd r) s\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s\<rbrace>; (f \<oplus> r') rv rv'; rv = Inr ba\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R (fst r) (snd r) s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' (fst r) (snd r) s) (lift (\<lambda>p. b (fst p) (snd p)) rv) (lift (\<lambda>p. d (fst p) (snd p)) rv') proof (prove)
goal:
No subgoals!