theory TcbAcc_R

lemma zipWithM_x_corres:
  assumes x: "\<And>x x' y y'. ((x, y), (x', y')) \<in> S \<Longrightarrow> corres dc P P' (f x y) (f' x' y')"
  assumes y: "\<And>x x' y y'. ((x, y), (x', y')) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x y \<lbrace>\<lambda>rv. P\<rbrace>"
      and z: "\<And>x x' y y'. ((x, y), (x', y')) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' x' y' \<lbrace>\<lambda>rv. P'\<rbrace>"
      and a: "set (zip (zip xs ys) (zip xs' ys')) \<subseteq> S"
      and b: "length (zip xs ys) = length (zip xs' ys')"
  shows      "corres dc P P' (zipWithM_x f xs ys) (zipWithM_x f' xs' ys')" apply (simp add: zipWithM_x_mapM) apply (rule corres_underlying_split) apply (rule corres_mapM) apply (rule dc_simp)+ apply clarsimp apply (rule x) apply assumption apply (clarsimp simp: y) apply (clarsimp simp: z) apply (rule b) apply (rule a) apply (rule corres_trivial, simp) apply (rule hoare_post_taut)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc P P' (zipWithM_x f xs ys) (zipWithM_x f' xs' ys') proof (prove)
goal (1 subgoal):
 1. corres dc P P' (do _ <- mapM (\<lambda>(x, y). f x y) (zip xs ys);
return ()
od) (do _ <- mapM (\<lambda>(x, y). f' x y) (zip xs' ys');
return ()
od) proof (prove)
goal (4 subgoals):
 1. corres ?r' P P' (mapM (\<lambda>(x, y). f x y) (zip xs ys)) (mapM (\<lambda>(x, y). f' x y) (zip xs' ys'))
 2. \<And>uu_ uua_. ?r' uu_ uua_ \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 3. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 4. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (10 subgoals):
 1. ?r' [] []
 2. \<And>x xs y ys. \<lbrakk>?r' xs ys; ?r'5 x y\<rbrakk> \<Longrightarrow> ?r' (x # xs) (y # ys)
 3. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> corres ?r'5 P P' (case x of (x, xa) \<Rightarrow> f x xa) (case y of (x, xa) \<Rightarrow> f' x xa)
 4. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P\<rbrace> case x of (x, xa) \<Rightarrow> f x xa \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P'\<rbrace> case y of (x, xa) \<Rightarrow> f' x xa \<lbrace>\<lambda>rv. P'\<rbrace>
 6. length (zip xs ys) = length (zip xs' ys')
 7. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> ?S5
 8. \<And>uu_ uua_. ?r' uu_ uua_ \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 9. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 10. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> corres ?r'5 P P' (case x of (x, xa) \<Rightarrow> f x xa) (case y of (x, xa) \<Rightarrow> f' x xa)
 2. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P\<rbrace> case x of (x, xa) \<Rightarrow> f x xa \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P'\<rbrace> case y of (x, xa) \<Rightarrow> f' x xa \<lbrace>\<lambda>rv. P'\<rbrace>
 4. length (zip xs ys) = length (zip xs' ys')
 5. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> ?S5
 6. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 7. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 8. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> ?S5 \<Longrightarrow> corres ?r'5 P P' (f a b) (f' aa ba)
 2. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P\<rbrace> case x of (x, xa) \<Rightarrow> f x xa \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P'\<rbrace> case y of (x, xa) \<Rightarrow> f' x xa \<lbrace>\<lambda>rv. P'\<rbrace>
 4. length (zip xs ys) = length (zip xs' ys')
 5. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> ?S5
 6. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 7. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 8. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> ?S5 \<Longrightarrow> ((a, b), aa, ba) \<in> S
 2. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P\<rbrace> case x of (x, xa) \<Rightarrow> f x xa \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x y. (x, y) \<in> ?S5 \<Longrightarrow> \<lbrace>P'\<rbrace> case y of (x, xa) \<Rightarrow> f' x xa \<lbrace>\<lambda>rv. P'\<rbrace>
 4. length (zip xs ys) = length (zip xs' ys')
 5. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> ?S5
 6. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 7. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 8. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> case x of (x, xa) \<Rightarrow> f x xa \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> case y of (x, xa) \<Rightarrow> f' x xa \<lbrace>\<lambda>rv. P'\<rbrace>
 3. length (zip xs ys) = length (zip xs' ys')
 4. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> S
 5. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 6. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 7. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> case y of (x, xa) \<Rightarrow> f' x xa \<lbrace>\<lambda>rv. P'\<rbrace>
 2. length (zip xs ys) = length (zip xs' ys')
 3. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> S
 4. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 5. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 6. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (5 subgoals):
 1. length (zip xs ys) = length (zip xs' ys')
 2. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> S
 3. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 4. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 5. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (4 subgoals):
 1. set (zip (zip xs ys) (zip xs' ys')) \<subseteq> S
 2. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 3. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 4. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>uu_ uua_. dc (?a15 uu_ uua_) (?b14 uu_ uua_) \<Longrightarrow> corres dc (?Q uu_) (?Q' uua_) (return ()) (return ())
 2. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>?Q\<rbrace>
 3. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>?Q'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> mapM (\<lambda>(x, y). f x y) (zip xs ys) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>P'\<rbrace> mapM (\<lambda>(x, y). f' x y) (zip xs' ys') \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!