theory ExtraCorres

lemma corres_mapM_list_all2:
  assumes rn: "r [] []"
  and     rc: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
  and   corr: "\<And>x xs y ys. \<lbrakk> S x y; list_all2 S xs ys \<rbrakk>
               \<Longrightarrow> corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)"
  and     ha: "\<And>x xs y. \<lbrakk> S x y; suffix (x#xs) as \<rbrakk> \<Longrightarrow> \<lbrace>Q  (x # xs)\<rbrace> f x \<lbrace>\<lambda>r. Q xs\<rbrace>"
  and     hc: "\<And>x y ys. \<lbrakk> S x y; suffix (y#ys) cs \<rbrakk> \<Longrightarrow> \<lbrace>Q' (y # ys) \<rbrace> f' y \<lbrace>\<lambda>r. Q' ys\<rbrace>"
  and   lall: "list_all2 S as cs"
  shows       "corres_underlying sr nf nf' r (Q as) (Q' cs) (mapM f as) (mapM f' cs)" using lall proof (induct rule: list_all2_induct_suffixeq) case Nil thus ?case unfolding mapM_def sequence_def by (auto intro: rn) next case  (Cons x xs y ys) have corr': "corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)" proof (rule corr) show "list_all2 S xs ys" by (simp add: Cons) qed fact+ show ?case apply (simp add: mapM_Cons) apply (rule corres_underlying_split [OF corr' _ ha [OF Cons(2)] hc [OF Cons(2)]]) apply (rule corres_underlying_split [OF Cons(3) _ hoare_post_taut hoare_post_taut]) apply (simp add: rc) apply (rule Cons.hyps)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (Q as) (Q' cs) (mapM f as) (mapM f' cs) proof (prove)
using this:
list_all2 S as cs

goal (1 subgoal):
 1. corres_underlying sr nf nf' r (Q as) (Q' cs) (mapM f as) (mapM f' cs) proof (state)
goal (2 subgoals):
 1. corres_underlying sr nf nf' r (Q []) (Q' []) (mapM f []) (mapM f' [])
 2. \<And>x xs y ys. \<lbrakk>list_all2 S xs ys; S x y; corres_underlying sr nf nf' r (Q xs) (Q' ys) (mapM f xs) (mapM f' ys); suffix (x # xs) as; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys)) proof (state)
this:


goal (2 subgoals):
 1. corres_underlying sr nf nf' r (Q []) (Q' []) (mapM f []) (mapM f' [])
 2. \<And>x xs y ys. \<lbrakk>list_all2 S xs ys; S x y; corres_underlying sr nf nf' r (Q xs) (Q' ys) (mapM f xs) (mapM f' ys); suffix (x # xs) as; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (Q []) (Q' []) (mapM f []) (mapM f' []) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (Q []) (Q' []) (let mcons = \<lambda>p q. do x <- p;
y <- q;
return (x # y)
od in foldr mcons (map f []) (return [])) (let mcons = \<lambda>p q. do x <- p;
y <- q;
return (x # y)
od in foldr mcons (map f' []) (return [])) proof (state)
this:
corres_underlying sr nf nf' r (Q []) (Q' []) (mapM f []) (mapM f' [])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>list_all2 S xs ys; S x y; corres_underlying sr nf nf' r (Q xs) (Q' ys) (mapM f xs) (mapM f' ys); suffix (x # xs) as; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys)) proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>list_all2 S xs ys; S x y; corres_underlying sr nf nf' r (Q xs) (Q' ys) (mapM f xs) (mapM f' ys); suffix (x # xs) as; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys)) proof (state)
this:
list_all2 S xs ys
S x y
corres_underlying sr nf nf' r (Q xs) (Q' ys) (mapM f xs) (mapM f' ys)
suffix (x # xs) as
suffix (y # ys) cs

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>list_all2 S xs ys; S x y; corres_underlying sr nf nf' r (Q xs) (Q' ys) (mapM f xs) (mapM f' ys); suffix (x # xs) as; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y) proof (state)
goal (2 subgoals):
 1. S x y
 2. list_all2 S xs ys proof (prove)
goal (1 subgoal):
 1. list_all2 S xs ys proof (state)
this:
list_all2 S xs ys

goal (1 subgoal):
 1. S x y proof (state)
this:
corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>list_all2 S xs ys; S x y; corres_underlying sr nf nf' r (Q xs) (Q' ys) (mapM f xs) (mapM f' ys); suffix (x # xs) as; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (do y <- f x;
ys <- mapM f xs;
return (y # ys)
od) (do y <- f' y;
ys <- mapM f' ys;
return (y # ys)
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (Q xs) (Q' ys) (do ys <- mapM f xs;
return (rv # ys)
od) (do ys <- mapM f' ys;
return (rv' # ys)
od)
 2. suffix (x # xs) as
 3. suffix (y # ys) cs proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' ys ysa. \<lbrakk>r' rv rv'; r ys ysa\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (return (rv # ys)) (return (rv' # ysa))
 2. suffix (x # xs) as
 3. suffix (y # ys) cs proof (prove)
goal (2 subgoals):
 1. suffix (x # xs) as
 2. suffix (y # ys) cs proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' r (Q (x # xs)) (Q' (y # ys)) (mapM f (x # xs)) (mapM f' (y # ys))

goal:
No subgoals!