theory CorresK_Lemmas

lemma mapME_x_corresK_inv:
  assumes x: "\<And>x. corres_underlyingK sr nf nf' (F x) (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>,-"
  shows      "corres_underlyingK sr nf nf' (xs = ys \<and> (\<forall>x \<in> set xs. F x)) (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 (rule corresK_use_guard, elim conjE) subgoal premises prems unfolding \<open>xs = ys\<close> proof (induct ys) case Nil show ?case by (simp add: mapME_x_def sequenceE_x_def returnOk_def corres_underlyingK_def) next case (Cons z zs) from Cons have IH:
      "corres_underlyingK sr nf nf' (\<forall>x\<in>set zs. F x) (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)" by (auto simp add:  dc_def) show ?case apply (simp add: mapME_x_def sequenceE_x_def) apply (fold mapME_x_def sequenceE_x_def dc_def) apply (corresKsimp corresK: x IH wp: y) done qed done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' (xs = ys \<and> (\<forall>x\<in>set xs. F x)) (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. \<lbrakk>xs = ys; \<forall>x\<in>set xs. F x\<rbrakk> \<Longrightarrow> corres_underlyingK sr nf nf' (xs = ys \<and> (\<forall>x\<in>set xs. F x)) (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_underlyingK sr nf nf' (xs = ys \<and> (\<forall>x\<in>set xs. F x)) (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_underlyingK sr nf nf' (ys = ys \<and> (\<forall>x\<in>set ys. F x)) (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_underlyingK sr nf nf' ([] = [] \<and> (\<forall>x\<in>set []. F x)) (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_underlyingK sr nf nf' (ys = ys \<and> (\<forall>x\<in>set ys. F x)) (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_underlyingK sr nf nf' (a # ys = a # ys \<and> (\<forall>x\<in>set (a # ys). F x)) (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_underlyingK sr nf nf' ([] = [] \<and> (\<forall>x\<in>set []. F x)) (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_underlyingK sr nf nf' (ys = ys \<and> (\<forall>x\<in>set ys. F x)) (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_underlyingK sr nf nf' (a # ys = a # ys \<and> (\<forall>x\<in>set (a # ys). F x)) (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_underlyingK sr nf nf' ([] = [] \<and> (\<forall>x\<in>set []. F x)) (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_underlyingK sr nf nf' ([] = [] \<and> (\<forall>x\<in>set []. F x)) (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_underlyingK sr nf nf' (ys = ys \<and> (\<forall>x\<in>set ys. F x)) (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_underlyingK sr nf nf' (a # ys = a # ys \<and> (\<forall>x\<in>set (a # ys). F x)) (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_underlyingK sr nf nf' (ys = ys \<and> (\<forall>x\<in>set ys. F x)) (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_underlyingK sr nf nf' (a # ys = a # ys \<and> (\<forall>x\<in>set (a # ys). F x)) (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_underlyingK sr nf nf' (zs = zs \<and> (\<forall>x\<in>set zs. F x)) (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_underlyingK sr nf nf' (ys = ys \<and> (\<forall>x\<in>set ys. F x)) (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_underlyingK sr nf nf' (a # ys = a # ys \<and> (\<forall>x\<in>set (a # ys). F x)) (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_underlyingK sr nf nf' (zs = zs \<and> (\<forall>x\<in>set zs. F x)) (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_underlyingK sr nf nf' (zs = zs \<and> (\<forall>x\<in>set zs. F x)) (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_underlyingK sr nf nf' (\<forall>x\<in>set zs. F x) (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_underlyingK sr nf nf' (\<forall>x\<in>set zs. F x) (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_underlyingK sr nf nf' (ys = ys \<and> (\<forall>x\<in>set ys. F x)) (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_underlyingK sr nf nf' (a # ys = a # ys \<and> (\<forall>x\<in>set (a # ys). F x)) (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_underlyingK sr nf nf' (z # zs = z # zs \<and> (\<forall>x\<in>set (z # zs). F x)) (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_underlyingK sr nf nf' (F z \<and> Ball (set zs) F) (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_underlyingK sr nf nf' (F z \<and> Ball (set zs) F) (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:
No subgoals! proof (state)
this:
corres_underlyingK sr nf nf' (z # zs = z # zs \<and> (\<forall>x\<in>set (z # zs). F x)) (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! proof (prove)
goal:
No subgoals!