theory CorresK_Lemmas

lemma corresK_mapM:
  assumes S: "set (zip xs ys) \<subseteq> S"
  assumes z: "\<And>x y. corres_protect ((x, y) \<in> S) \<Longrightarrow> corres_underlyingK R nf nf' (F x y) 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      "corres_underlyingK R nf nf'
                  ((length xs = length ys) \<and>
                   (r [] []) \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and>
                  (\<forall>(x,y)\<in>S. F x y)) r P P' (mapM f xs) (mapM f' ys)" unfolding corres_underlyingK_def apply (rule impI, rule corres_mapM[of r r' S]) using assms unfolding corres_underlyingK_def by (auto simp: corres_protect_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK R nf nf' (length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y)) r P P' (mapM f xs) (mapM f' ys) proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<longrightarrow> corres_underlying R nf nf' r P P' (mapM f xs) (mapM f' ys) proof (prove)
goal (7 subgoals):
 1. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> r [] []
 2. \<And>x xsa y ysa. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); r xsa ysa; r' x y\<rbrakk> \<Longrightarrow> r (x # xsa) (y # ysa)
 3. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r' P P' (f x) (f' y)
 4. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>
 6. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> length xs = length ys
 7. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> set (zip xs ys) \<subseteq> S proof (prove)
using this:
set (zip xs ys) \<subseteq> S
corres_protect ((?x, ?y) \<in> S) \<Longrightarrow> corres_underlyingK R nf nf' (F ?x ?y) r' P P' (f ?x) (f' ?y)
(?x, ?y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>rv. P\<rbrace>
(?x, ?y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' ?y \<lbrace>\<lambda>rv. P'\<rbrace>

goal (7 subgoals):
 1. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> r [] []
 2. \<And>x xsa y ysa. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); r xsa ysa; r' x y\<rbrakk> \<Longrightarrow> r (x # xsa) (y # ysa)
 3. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r' P P' (f x) (f' y)
 4. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>
 6. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> length xs = length ys
 7. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> set (zip xs ys) \<subseteq> S proof (prove)
using this:
set (zip xs ys) \<subseteq> S
corres_protect ((?x, ?y) \<in> S) \<Longrightarrow> F ?x ?y \<longrightarrow> corres_underlying R nf nf' r' P P' (f ?x) (f' ?y)
(?x, ?y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>rv. P\<rbrace>
(?x, ?y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' ?y \<lbrace>\<lambda>rv. P'\<rbrace>

goal (7 subgoals):
 1. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> r [] []
 2. \<And>x xsa y ysa. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); r xsa ysa; r' x y\<rbrakk> \<Longrightarrow> r (x # xsa) (y # ysa)
 3. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> corres_underlying R nf nf' r' P P' (f x) (f' y)
 4. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>x y. \<lbrakk>length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y); (x, y) \<in> S\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>
 6. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> length xs = length ys
 7. length xs = length ys \<and> r [] [] \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> (\<forall>(x, y)\<in>S. F x y) \<Longrightarrow> set (zip xs ys) \<subseteq> S