theory Corres_UL

lemma mapME_x_corres_inv:
  assumes x: "\<And>x. corres_underlying sr nf nf' (f \<oplus> dc) (P x) (P' x) (m x) (m' x)"
  assumes y: "\<And>x P. \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>x. P\<rbrace>,-" "\<And>x P'. \<lbrace>P'\<rbrace> m' x \<lbrace>\<lambda>x. P'\<rbrace>,-"
  assumes z: "xs = ys"
  shows      "corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x \<in> set xs. P x s) (\<lambda>s. \<forall>y \<in> set ys. P' y s)
                              (mapME_x m xs) (mapME_x m' ys)" unfolding z proof (induct ys) case Nil show ?case by (simp add: mapME_x_def sequenceE_x_def returnOk_def) next case (Cons z zs) from Cons have IH:
      "corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s)
                       (mapME_x m zs) (mapME_x m' zs)" . show ?case apply (simp add: mapME_x_def sequenceE_x_def) apply (fold mapME_x_def sequenceE_x_def dc_def) apply corres_pre apply (rule corres_splitEE) apply (rule x) apply (rule IH) apply (fold validE_R_def) apply (rule y)+ apply simp+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m xs) (mapME_x m' ys) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set ys. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m ys) (mapME_x m' ys) proof (state)
goal (2 subgoals):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set []. P x s) (\<lambda>s. \<forall>y\<in>set []. P' y s) (mapME_x m []) (mapME_x m' [])
 2. \<And>a ys. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set ys. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m ys) (mapME_x m' ys) \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (a # ys). P x s) (\<lambda>s. \<forall>y\<in>set (a # ys). P' y s) (mapME_x m (a # ys)) (mapME_x m' (a # ys)) proof (state)
this:


goal (2 subgoals):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set []. P x s) (\<lambda>s. \<forall>y\<in>set []. P' y s) (mapME_x m []) (mapME_x m' [])
 2. \<And>a ys. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set ys. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m ys) (mapME_x m' ys) \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (a # ys). P x s) (\<lambda>s. \<forall>y\<in>set (a # ys). P' y s) (mapME_x m (a # ys)) (mapME_x m' (a # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set []. P x s) (\<lambda>s. \<forall>y\<in>set []. P' y s) (mapME_x m []) (mapME_x m' []) proof (state)
this:
corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set []. P x s) (\<lambda>s. \<forall>y\<in>set []. P' y s) (mapME_x m []) (mapME_x m' [])

goal (1 subgoal):
 1. \<And>a ys. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set ys. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m ys) (mapME_x m' ys) \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (a # ys). P x s) (\<lambda>s. \<forall>y\<in>set (a # ys). P' y s) (mapME_x m (a # ys)) (mapME_x m' (a # ys)) proof (state)
goal (1 subgoal):
 1. \<And>a ys. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set ys. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m ys) (mapME_x m' ys) \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (a # ys). P x s) (\<lambda>s. \<forall>y\<in>set (a # ys). P' y s) (mapME_x m (a # ys)) (mapME_x m' (a # ys)) proof (state)
this:
corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s) (mapME_x m zs) (mapME_x m' zs)

goal (1 subgoal):
 1. \<And>a ys. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set ys. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m ys) (mapME_x m' ys) \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (a # ys). P x s) (\<lambda>s. \<forall>y\<in>set (a # ys). P' y s) (mapME_x m (a # ys)) (mapME_x m' (a # ys)) proof (chain)
picking this:
corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s) (mapME_x m zs) (mapME_x m' zs) proof (prove)
using this:
corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s) (mapME_x m zs) (mapME_x m' zs)

goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s) (mapME_x m zs) (mapME_x m' zs) proof (state)
this:
corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s) (mapME_x m zs) (mapME_x m' zs)

goal (1 subgoal):
 1. \<And>a ys. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set ys. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m ys) (mapME_x m' ys) \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (a # ys). P x s) (\<lambda>s. \<forall>y\<in>set (a # ys). P' y s) (mapME_x m (a # ys)) (mapME_x m' (a # ys)) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (z # zs). P x s) (\<lambda>s. \<forall>y\<in>set (z # zs). P' y s) (mapME_x m (z # zs)) (mapME_x m' (z # zs)) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> (\<lambda>a b. True)) (\<lambda>s. P z s \<and> (\<forall>x\<in>set zs. P x s)) (\<lambda>s. P' z s \<and> (\<forall>y\<in>set zs. P' y s)) (doE _ <- m z;
foldr (\<lambda>x y. doE _ <- x;
y
odE) (map m zs) (returnOk ())
odE) (doE _ <- m' z;
foldr (\<lambda>x y. doE _ <- x;
y
odE) (map m' zs) (returnOk ())
odE) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. P z s \<and> (\<forall>x\<in>set zs. P x s)) (\<lambda>s. P' z s \<and> (\<forall>y\<in>set zs. P' y s)) (doE _ <- m z;
mapME_x m zs
odE) (doE _ <- m' z;
mapME_x m' zs
odE) proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' (f \<oplus> dc) ?Q9 ?Q'9 (doE _ <- m z;
mapME_x m zs
odE) (doE _ <- m' z;
mapME_x m' zs
odE)
 2. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q9 s
 3. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q'9 s' proof (prove)
goal (6 subgoals):
 1. corres_underlying sr nf nf' (f \<oplus> ?r'10) ?P10 ?P'10 (m z) (m' z)
 2. \<And>rv rv'. ?r'10 rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (?R10 rv) (?R'10 rv') (mapME_x m zs) (mapME_x m' zs)
 3. \<lbrace>?Q10\<rbrace> m z \<lbrace>?R10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> m' z \<lbrace>?R'10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P10 and ?Q10) s
 6. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P'10 and ?Q'10) s' proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (?R10 rv) (?R'10 rv') (mapME_x m zs) (mapME_x m' zs)
 2. \<lbrace>?Q10\<rbrace> m z \<lbrace>?R10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'10\<rbrace> m' z \<lbrace>?R'10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P z and ?Q10) s
 5. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' z and ?Q'10) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q10\<rbrace> m z \<lbrace>\<lambda>rv s. \<forall>x\<in>set zs. P x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?Q'10\<rbrace> m' z \<lbrace>\<lambda>rv' s. \<forall>y\<in>set zs. P' y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P z and ?Q10) s
 4. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' z and ?Q'10) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q10\<rbrace> m z \<lbrace>\<lambda>rv s. \<forall>x\<in>set zs. P x s\<rbrace>, -
 2. \<lbrace>?Q'10\<rbrace> m' z \<lbrace>\<lambda>rv' s. \<forall>y\<in>set zs. P' y s\<rbrace>, -
 3. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P z and ?Q10) s
 4. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' z and ?Q'10) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P z and (\<lambda>s. \<forall>x\<in>set zs. P x s)) s
 2. \<And>s s'. \<lbrakk>P z s \<and> (\<forall>x\<in>set zs. P x s); P' z s' \<and> (\<forall>y\<in>set zs. P' y s'); (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P' z and (\<lambda>s. \<forall>y\<in>set zs. P' y s)) s' proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set (z # zs). P x s) (\<lambda>s. \<forall>y\<in>set (z # zs). P' y s) (mapME_x m (z # zs)) (mapME_x m' (z # zs))

goal:
No subgoals!