theory ExtraCorres

lemma corres_mapM:
  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' 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' r P P' (mapM f xs) (mapM f' ys)" proof (induct xs ys rule: list_induct2) case Nil show ?case by (simp add: mapM_def sequence_def x) 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' r P P' (mapM f as) (mapM f' bs)" by simp show ?case apply (simp add: mapM_Cons) apply (rule corres_guard_imp) apply (rule corres_split[OF z[OF P] _ w[OF P]]) apply (rule corres_underlying_split[OF Q]) apply (rule corres_trivial, simp add: y) apply (wp | simp)+ 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' r P P' (mapM f xs) (mapM f' ys) proof (state)
goal (2 subgoals):
 1. set (zip [] []) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f []) (mapM f' [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f xs) (mapM f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f (x # xs)) (mapM f' (y # ys)) proof (state)
this:
set (zip [] []) \<subseteq> S

goal (2 subgoals):
 1. set (zip [] []) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f []) (mapM f' [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; set (zip xs ys) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f xs) (mapM f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f (x # xs)) (mapM f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf nf' r P P' (mapM f []) (mapM f' []) proof (state)
this:
corres_underlying R nf nf' r P P' (mapM f []) (mapM 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' r P P' (mapM f xs) (mapM f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f (x # xs)) (mapM 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' r P P' (mapM f xs) (mapM f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f (x # xs)) (mapM f' (y # ys)) proof (state)
this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f as) (mapM 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' r P P' (mapM f xs) (mapM f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f (x # xs)) (mapM f' (y # ys)) proof (chain)
picking this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f as) (mapM 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' r P P' (mapM f as) (mapM 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' r P P' (mapM f xs) (mapM f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f (x # xs)) (mapM f' (y # ys)) proof (chain)
picking this:
length as = length bs
set (zip as bs) \<subseteq> S \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f as) (mapM 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' r P P' (mapM f as) (mapM f' bs)
set (zip (a # as) (b # bs)) \<subseteq> S

goal (1 subgoal):
 1. corres_underlying R nf nf' r P P' (mapM f as) (mapM f' bs) proof (state)
this:
corres_underlying R nf nf' r P P' (mapM f as) (mapM 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' r P P' (mapM f xs) (mapM f' ys); set (zip (x # xs) (y # ys)) \<subseteq> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r P P' (mapM f (x # xs)) (mapM f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf nf' r P P' (mapM f (a # as)) (mapM f' (b # bs)) proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf nf' r P P' (do y <- f a;
ys <- mapM f as;
return (y # ys)
od) (do y <- f' b;
ys <- mapM f' bs;
return (y # ys)
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying R nf nf' r ?Q ?Q' (do y <- f a;
ys <- mapM f as;
return (y # ys)
od) (do y <- f' b;
ys <- mapM f' bs;
return (y # ys)
od)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying R nf nf' r P P' (do ys <- mapM f as;
return (rv # ys)
od) (do ys <- mapM f' bs;
return (rv' # ys)
od)
 2. \<And>s. P s \<Longrightarrow> (P and P) s
 3. \<And>s. P' s \<Longrightarrow> (P' and P') s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' ys ysa. \<lbrakk>r' rv rv'; r ys ysa\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r (?Q10 rv rv' ys) (?Q'10 rv rv' ysa) (return (rv # ys)) (return (rv' # ysa))
 2. \<And>rv rv'. r' rv rv' \<Longrightarrow> \<lbrace>P\<rbrace> mapM f as \<lbrace>?Q10 rv rv'\<rbrace>
 3. \<And>rv rv'. r' rv rv' \<Longrightarrow> \<lbrace>P'\<rbrace> mapM f' bs \<lbrace>?Q'10 rv rv'\<rbrace>
 4. \<And>s. P s \<Longrightarrow> (P and P) s
 5. \<And>s. P' s \<Longrightarrow> (P' and P') s proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> \<lbrace>P\<rbrace> mapM f as \<lbrace>\<lambda>ys _. True\<rbrace>
 2. \<And>rv rv'. r' rv rv' \<Longrightarrow> \<lbrace>P'\<rbrace> mapM f' bs \<lbrace>\<lambda>ysa _. True\<rbrace>
 3. \<And>s. P s \<Longrightarrow> (P and P) s
 4. \<And>s. P' s \<Longrightarrow> (P' and P') s proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying R nf nf' r P P' (mapM f (a # as)) (mapM f' (b # bs))

goal:
No subgoals!