theory CorresK_Lemmas

lemma corresK_mapM_list_all2:
  assumes x: "\<And>x y xs ys. corres_underlyingK sr nf nf' (F x y xs ys) r' (I (x#xs)) (I' (y#ys)) (f x) (f' y)"
  assumes "\<And>x y xs. \<lbrakk> S x y; suffix (x#xs) as \<rbrakk> \<Longrightarrow> \<lbrace> I  (x#xs) \<rbrace> f  x \<lbrace> \<lambda>rv. I  xs \<rbrace>"
  assumes "\<And>x y ys. \<lbrakk> S x y; suffix (y#ys) cs \<rbrakk> \<Longrightarrow> \<lbrace> I' (y#ys) \<rbrace> f' y \<lbrace> \<lambda>rv. I' ys \<rbrace>"
  shows "corres_underlyingK sr nf nf'
          (r [] [] \<and> (\<forall> x y xs ys. r' x y \<longrightarrow> r xs ys \<longrightarrow> r (x # xs) (y # ys)) \<and>
            list_all2 S as cs \<and> F_all2 F as cs)
                            r (I as) (I' cs) (mapM f as) (mapM f' cs)" unfolding corres_underlyingK_def apply (clarsimp simp: F_all2_def) subgoal for F' apply (rule corres_mapM_list_all2[of r r' "\<lambda>x y. S x y \<and> F' x y"]; (rule assms | assumption | clarsimp)?) apply (rule x[THEN corresK_unlift]) apply (drule list_all2_conjD) apply (clarsimp simp: assms | assumption)+ apply (rule list_all2_conj; simp) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' (r [] [] \<and> (\<forall>x y xs ys. r' x y \<longrightarrow> r xs ys \<longrightarrow> r (x # xs) (y # ys)) \<and> list_all2 S as cs \<and> F_all2 F as cs) r (I as) (I' cs) (mapM f as) (mapM f' cs) proof (prove)
goal (1 subgoal):
 1. r [] [] \<and> (\<forall>x y xs ys. r' x y \<longrightarrow> r xs ys \<longrightarrow> r (x # xs) (y # ys)) \<and> list_all2 S as cs \<and> F_all2 F as cs \<longrightarrow> corres_underlying sr nf nf' r (I as) (I' cs) (mapM f as) (mapM f' cs) proof (prove)
goal (1 subgoal):
 1. \<And>F'. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (I as) (I' cs) (mapM f as) (mapM f' cs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (I as) (I' cs) (mapM f as) (mapM f' cs) proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; list_all2 (\<lambda>x y. S x y \<and> F' x y) xs ys; S x y; F' x y\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r' (I (x # xs)) (I' (y # ys)) (f x) (f' y)
 2. \<And>x xs y. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (x # xs) as\<rbrakk> \<Longrightarrow> S x (?y17 x xs y)
 3. \<And>x xs y. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (x # xs) as\<rbrakk> \<Longrightarrow> suffix (x # xs) as
 4. \<And>x y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> S (?x12 x y ys) y
 5. \<And>x y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> suffix (y # ys) cs
 6. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. S x y \<and> F' x y) as cs proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; list_all2 (\<lambda>x y. S x y \<and> F' x y) xs ys; S x y; F' x y\<rbrakk> \<Longrightarrow> F x y xs ys
 2. \<And>x xs y. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (x # xs) as\<rbrakk> \<Longrightarrow> S x (?y17 x xs y)
 3. \<And>x xs y. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (x # xs) as\<rbrakk> \<Longrightarrow> suffix (x # xs) as
 4. \<And>x y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> S (?x12 x y ys) y
 5. \<And>x y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> suffix (y # ys) cs
 6. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. S x y \<and> F' x y) as cs proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y; F' x y; list_all2 S xs ys \<and> list_all2 F' xs ys\<rbrakk> \<Longrightarrow> F x y xs ys
 2. \<And>x xs y. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (x # xs) as\<rbrakk> \<Longrightarrow> S x (?y17 x xs y)
 3. \<And>x xs y. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (x # xs) as\<rbrakk> \<Longrightarrow> suffix (x # xs) as
 4. \<And>x y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> S (?x12 x y ys) y
 5. \<And>x y ys. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs; S x y \<and> F' x y; suffix (y # ys) cs\<rbrakk> \<Longrightarrow> suffix (y # ys) cs
 6. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. S x y \<and> F' x y) as cs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r [] []; \<forall>x y. r' x y \<longrightarrow> (\<forall>xs ys. r xs ys \<longrightarrow> r (x # xs) (y # ys)); list_all2 S as cs; \<forall>x y. F' x y \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> F x y xs ys); list_all2 F' as cs\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. S x y \<and> F' x y) as cs proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!