theory Corres_UL

lemma mapME_x_corres_same_xs:
  assumes x: "\<And>x. x \<in> set xs
      \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (P x) (P' x) (m x) (m' x)"
  assumes y: "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y \<in> set xs. P y s\<rbrace> m x \<lbrace>\<lambda>_ s. \<forall>y \<in> set xs. P y s\<rbrace>,-"
             "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y \<in> set xs. P' y s\<rbrace> m' x \<lbrace>\<lambda>_ s. \<forall>y \<in> set xs. P' y s\<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)" apply (subgoal_tac "set ys \<subseteq> set xs
        \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x \<in> set xs. P x s) (\<lambda>s. \<forall>y \<in> set xs. P' y s)
                              (mapME_x m ys) (mapME_x m' ys)") apply (simp add: 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 xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s)
                       (mapME_x m zs) (mapME_x m' zs)" by (simp add: dc_def) from Cons have in_set:
      "z \<in> set xs" "set zs \<subseteq> set xs" by auto thus ?case apply (simp add: mapME_x_def sequenceE_x_def) apply (fold mapME_x_def sequenceE_x_def dc_def) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule x, simp) apply (rule IH) apply (wp y | 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 (2 subgoals):
 1. (set ys \<subseteq> set xs \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. 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 xs. P x s) (\<lambda>s. \<forall>y\<in>set ys. P' y s) (mapME_x m xs) (mapME_x m' ys)
 2. set ys \<subseteq> set xs \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m ys) (mapME_x m' ys) proof (prove)
goal (1 subgoal):
 1. set ys \<subseteq> set xs \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m ys) (mapME_x m' ys) proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> set xs \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m []) (mapME_x m' [])
 2. \<And>a ys. \<lbrakk>set ys \<subseteq> set xs \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m ys) (mapME_x m' ys); set (a # ys) \<subseteq> set xs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m (a # ys)) (mapME_x m' (a # ys)) proof (state)
this:
set [] \<subseteq> set xs

goal (2 subgoals):
 1. set [] \<subseteq> set xs \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m []) (mapME_x m' [])
 2. \<And>a ys. \<lbrakk>set ys \<subseteq> set xs \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m ys) (mapME_x m' ys); set (a # ys) \<subseteq> set xs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. 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 xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. 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 xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m []) (mapME_x m' [])

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

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

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 xs. 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 xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m zs) (mapME_x m' zs)

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

goal (1 subgoal):
 1. z \<in> set xs &&& set zs \<subseteq> set xs proof (state)
this:
z \<in> set xs
set zs \<subseteq> set xs

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

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 xs. P' y s) (mapME_x m (z # zs)) (mapME_x m' (z # zs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> (\<lambda>a b. True)) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. 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. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. 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. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) ?Q2 ?Q'2 (doE _ <- m z;
mapME_x m zs
odE) (doE _ <- m' z;
mapME_x m' zs
odE)
 2. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>x\<in>set xs. P x s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>y\<in>set xs. P' y s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> ?r'6) ?P6 ?P'6 (m z) (m' z)
 2. \<And>rv rv'. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; ?r'6 rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (?R6 rv) (?R'6 rv') (mapME_x m zs) (mapME_x m' zs)
 3. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> m z \<lbrace>?R6\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> m' z \<lbrace>?R'6\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>x\<in>set xs. P x s\<rbrakk> \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>y\<in>set xs. P' y s\<rbrakk> \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; dc rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (?R6 rv) (?R'6 rv') (mapME_x m zs) (mapME_x m' zs)
 2. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> m z \<lbrace>?R6\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> m' z \<lbrace>?R'6\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>x\<in>set xs. P x s\<rbrakk> \<Longrightarrow> (P z and ?Q6) s
 5. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>y\<in>set xs. P' y s\<rbrakk> \<Longrightarrow> (P' z and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> m z \<lbrace>\<lambda>rv s. \<forall>x\<in>set xs. P x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> m' z \<lbrace>\<lambda>rv' s. \<forall>y\<in>set xs. P' y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>x\<in>set xs. P x s\<rbrakk> \<Longrightarrow> (P z and ?Q6) s
 4. \<And>s. \<lbrakk>z \<in> set xs; set zs \<subseteq> set xs; \<forall>y\<in>set xs. P' y s\<rbrakk> \<Longrightarrow> (P' z and ?Q'6) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) (mapME_x m (z # zs)) (mapME_x m' (z # zs))

goal:
No subgoals!