theory ExtraCorres

lemma corres_mapME:
  assumes x: "r [] []"
  assumes y: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
  assumes z: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r') P P' (f x) (f' y)"
  assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
  shows      "\<lbrakk> length xs = length ys; set (zip xs ys) \<subseteq> S \<rbrakk> \<Longrightarrow>
                   corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys)" proof (induct xs ys rule: list_induct2) case Nil show ?case by (simp add: mapME_def sequenceE_def x returnOk_def) next case (Cons a as b bs) from Cons have P: "(a, b) \<in> S" by simp from Cons have Q: "corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)" by simp show ?case apply (simp add: mapME_Cons) apply (rule corres_guard_imp) apply (unfold bindE_def validE_def) apply (rule corres_underlying_split[OF z[OF P]]) apply (case_tac rv) apply (clarsimp simp: throwError_def) apply clarsimp apply (rule corres_split[OF Q]) apply (rule corres_trivial) apply (case_tac rv) apply (clarsimp simp add: lift_def throwError_def) apply (clarsimp simp add: y lift_def returnOk_def throwError_def) apply (wpsimp wp: w P)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys) proof (state)
goal (2 subgoals):
 1. set (zip [] []) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f []) (mapME f' [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (x # xs)) (mapME f' (y # ys)) proof (state)
this:
set (zip [] []) \<subseteq> S

goal (2 subgoals):
 1. set (zip [] []) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f []) (mapME f' [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (x # xs)) (mapME f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f []) (mapME f' []) proof (state)
this:
corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f []) (mapME f' [])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (x # xs)) (mapME f' (y # ys)) proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (x # xs)) (mapME f' (y # ys)) proof (state)
this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)
set (zip (a # as) (b # bs)) \<subseteq> S

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (x # xs)) (mapME f' (y # ys)) proof (chain)
picking this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)
set (zip (a # as) (b # bs)) \<subseteq> S proof (prove)
using this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)
set (zip (a # as) (b # bs)) \<subseteq> S

goal (1 subgoal):
 1. (a, b) \<in> S proof (state)
this:
(a, b) \<in> S

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (x # xs)) (mapME f' (y # ys)) proof (chain)
picking this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)
set (zip (a # as) (b # bs)) \<subseteq> S proof (prove)
using this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)
set (zip (a # as) (b # bs)) \<subseteq> S

goal (1 subgoal):
 1. corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs) proof (state)
this:
corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (x # xs)) (mapME f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (a # as)) (mapME f' (b # bs)) proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf nf' (F \<oplus> r) P P' (doE y <- f a;
ys <- mapME f as;
returnOk (y # ys)
odE) (doE y <- f' b;
ys <- mapME f' bs;
returnOk (y # ys)
odE) proof (prove)
goal (3 subgoals):
 1. corres_underlying R nf nf' (F \<oplus> r) ?Q ?Q' (doE y <- f a;
ys <- mapME f as;
returnOk (y # ys)
odE) (doE y <- f' b;
ys <- mapME f' bs;
returnOk (y # ys)
odE)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres_underlying R nf nf' (F \<oplus> r) ?Q ?Q' (f a >>= lift (\<lambda>y. mapME f as >>= lift (\<lambda>ys. returnOk (y # ys)))) (f' b >>= lift (\<lambda>y. mapME f' bs >>= lift (\<lambda>ys. returnOk (y # ys))))
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. (F \<oplus> r') rv rv' \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (?Q4 rv) (?Q'4 rv') (lift (\<lambda>y. mapME f as >>= lift (\<lambda>ys. returnOk (y # ys))) rv) (lift (\<lambda>y. mapME f' bs >>= lift (\<lambda>ys. returnOk (y # ys))) rv')
 2. \<lbrace>P\<rbrace> f a \<lbrace>?Q4\<rbrace>
 3. \<lbrace>P'\<rbrace> f' b \<lbrace>?Q'4\<rbrace>
 4. \<And>s. P s \<Longrightarrow> P s
 5. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' a. \<lbrakk>(F \<oplus> r') rv rv'; rv = Inl a\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (?Q4 rv) (?Q'4 rv') (lift (\<lambda>y. mapME f as >>= lift (\<lambda>ys. returnOk (y # ys))) rv) (lift (\<lambda>y. mapME f' bs >>= lift (\<lambda>ys. returnOk (y # ys))) rv')
 2. \<And>rv rv' b. \<lbrakk>(F \<oplus> r') rv rv'; rv = Inr b\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (?Q4 rv) (?Q'4 rv') (lift (\<lambda>y. mapME f as >>= lift (\<lambda>ys. returnOk (y # ys))) rv) (lift (\<lambda>y. mapME f' bs >>= lift (\<lambda>ys. returnOk (y # ys))) rv')
 3. \<lbrace>P\<rbrace> f a \<lbrace>?Q4\<rbrace>
 4. \<lbrace>P'\<rbrace> f' b \<lbrace>?Q'4\<rbrace>
 5. \<And>s. P s \<Longrightarrow> P s
 6. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' b. \<lbrakk>(F \<oplus> r') rv rv'; rv = Inr b\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (?Q4 rv) (?Q'4 rv') (lift (\<lambda>y. mapME f as >>= lift (\<lambda>ys. returnOk (y # ys))) rv) (lift (\<lambda>y. mapME f' bs >>= lift (\<lambda>ys. returnOk (y # ys))) rv')
 2. \<lbrace>P\<rbrace> f a \<lbrace>?Q4\<rbrace>
 3. \<lbrace>P'\<rbrace> f' b \<lbrace>?Q'4\<rbrace>
 4. \<And>s. P s \<Longrightarrow> P s
 5. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>b y'. r' b y' \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (?Q4 (Inr b)) (?Q'4 (Inr y')) (mapME f as >>= lift (\<lambda>ys. returnOk (b # ys))) (mapME f' bs >>= lift (\<lambda>ys. returnOk (y' # ys)))
 2. \<lbrace>P\<rbrace> f a \<lbrace>?Q4\<rbrace>
 3. \<lbrace>P'\<rbrace> f' b \<lbrace>?Q'4\<rbrace>
 4. \<And>s. P s \<Longrightarrow> P s
 5. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (7 subgoals):
 1. \<And>b y' rv rv'. \<lbrakk>r' b y'; (F \<oplus> r) rv rv'\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (?R22 b y' rv) (?R'22 b y' rv') (lift (\<lambda>ys. returnOk (b # ys)) rv) (lift (\<lambda>ys. returnOk (y' # ys)) rv')
 2. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q27 (Inr b)\<rbrace> mapME f as \<lbrace>?R22 b y'\<rbrace>
 3. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q'25 (Inr y')\<rbrace> mapME f' bs \<lbrace>?R'22 b y'\<rbrace>
 4. \<lbrace>P\<rbrace> f a \<lbrace>\<lambda>a. P and ?Q27 a\<rbrace>
 5. \<lbrace>P'\<rbrace> f' b \<lbrace>\<lambda>a. P' and ?Q'25 a\<rbrace>
 6. \<And>s. P s \<Longrightarrow> P s
 7. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (7 subgoals):
 1. \<And>b y' rv rv'. \<lbrakk>r' b y'; (F \<oplus> r) rv rv'\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (lift (\<lambda>ys. returnOk (b # ys)) rv) (lift (\<lambda>ys. returnOk (y' # ys)) rv')
 2. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q27 (Inr b)\<rbrace> mapME f as \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q'25 (Inr y')\<rbrace> mapME f' bs \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<lbrace>P\<rbrace> f a \<lbrace>\<lambda>a. P and ?Q27 a\<rbrace>
 5. \<lbrace>P'\<rbrace> f' b \<lbrace>\<lambda>a. P' and ?Q'25 a\<rbrace>
 6. \<And>s. P s \<Longrightarrow> P s
 7. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (8 subgoals):
 1. \<And>b y' rv rv' a. \<lbrakk>r' b y'; (F \<oplus> r) rv rv'; rv = Inl a\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (lift (\<lambda>ys. returnOk (b # ys)) rv) (lift (\<lambda>ys. returnOk (y' # ys)) rv')
 2. \<And>b y' rv rv' ba. \<lbrakk>r' b y'; (F \<oplus> r) rv rv'; rv = Inr ba\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (lift (\<lambda>ys. returnOk (b # ys)) rv) (lift (\<lambda>ys. returnOk (y' # ys)) rv')
 3. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q27 (Inr b)\<rbrace> mapME f as \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q'25 (Inr y')\<rbrace> mapME f' bs \<lbrace>\<lambda>rv' _. True\<rbrace>
 5. \<lbrace>P\<rbrace> f a \<lbrace>\<lambda>a. P and ?Q27 a\<rbrace>
 6. \<lbrace>P'\<rbrace> f' b \<lbrace>\<lambda>a. P' and ?Q'25 a\<rbrace>
 7. \<And>s. P s \<Longrightarrow> P s
 8. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (7 subgoals):
 1. \<And>b y' rv rv' ba. \<lbrakk>r' b y'; (F \<oplus> r) rv rv'; rv = Inr ba\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (lift (\<lambda>ys. returnOk (b # ys)) rv) (lift (\<lambda>ys. returnOk (y' # ys)) rv')
 2. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q27 (Inr b)\<rbrace> mapME f as \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q'25 (Inr y')\<rbrace> mapME f' bs \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<lbrace>P\<rbrace> f a \<lbrace>\<lambda>a. P and ?Q27 a\<rbrace>
 5. \<lbrace>P'\<rbrace> f' b \<lbrace>\<lambda>a. P' and ?Q'25 a\<rbrace>
 6. \<And>s. P s \<Longrightarrow> P s
 7. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q27 (Inr b)\<rbrace> mapME f as \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>b y'. r' b y' \<Longrightarrow> \<lbrace>?Q'25 (Inr y')\<rbrace> mapME f' bs \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<lbrace>P\<rbrace> f a \<lbrace>\<lambda>a. P and ?Q27 a\<rbrace>
 4. \<lbrace>P'\<rbrace> f' b \<lbrace>\<lambda>a. P' and ?Q'25 a\<rbrace>
 5. \<And>s. P s \<Longrightarrow> P s
 6. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f (a # as)) (mapME f' (b # bs))

goal:
No subgoals!