theory Corres_C

lemma ccorres_zipWithM_x_while_genQ:
  fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes rl: "\<forall>n. n < length xs \<and> n < length ys \<longrightarrow> ccorres dc xfdc (F (n * j)) ({s. xf s = of_nat n * of_nat j} \<inter> Q)
      hs (f (xs ! n) (ys ! n)) body"
  and  guard: "\<And>n. P n = (n < of_nat (min (length xs) (length ys)) * of_nat j)"
  and  bodyi: "\<forall>s. xf s < of_nat (min (length xs) (length ys)) * of_nat j
    \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>x. xf t + of_nat j) t \<in> Q}"
  and  hi: "\<And>n. Suc n < length xs \<and> Suc n < length ys \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> f (xs ! n) (ys ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>"
  and  wb: "min (length xs) (length ys) * j < 2 ^ len_of TYPE('c)"
  and  xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s"
  and   j: "0 < j"
  shows  "ccorres (\<lambda>rv rv'. rv' = of_nat (min (length xs) (length ys) * j)) xf
                  (F (0 :: nat)) {s. xf_update (\<lambda>_. 0) s \<in> Q} hs
                  (zipWithM_x f xs ys)
                  (Basic (\<lambda>s. xf_update (\<lambda>_. 0) s);;
          (While {s. P (xf s)}
              (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s))))" unfolding zipWithM_x_def apply (rule ccorres_guard_imp) apply (rule ccorres_rel_imp [OF ccorres_sequence_x_while_genQ[where F=F, OF _ _ _ _ _ xf j]];
           simp) apply (simp add: zipWith_nth) apply (rule rl) apply (rule guard) apply (rule bodyi) apply (simp add: zipWith_nth hi[simplified]) apply (rule wb) apply simp+ done

\<comment> \<open>Temporarily remove ccorres_weak_cong, so that the following lemmas can be constructed
    with simplified return relations.
    We do not use ccorres_all_cong due to it causing unexpected eta-expansion.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = word_of_nat (min (length xs) (length ys) * j)) xf (F 0) {s. xf_update (\<lambda>_. 0) s \<in> Q} hs (zipWithM_x f xs ys) (Basic (xf_update (\<lambda>_. 0));;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = word_of_nat (min (length xs) (length ys) * j)) xf (F 0) {s. xf_update (\<lambda>_. 0) s \<in> Q} hs (sequence_x (zipWith f xs ys)) (Basic (xf_update (\<lambda>_. 0));;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (3 subgoals):
 1. ccorres (\<lambda>rv rv'. rv' = word_of_nat (min (length xs) (length ys) * j)) xf ?Q ?Q' hs (sequence_x (zipWith f xs ys)) (Basic (xf_update (\<lambda>_. 0));;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>s. F 0 s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (7 subgoals):
 1. \<forall>n. n < length xs \<and> n < length ys \<longrightarrow> ccorres dc xfdc (F (n * j)) ({s. xf s = word_of_nat n * word_of_nat j} \<inter> ?Q6) hs (zipWith f xs ys ! n) body
 2. \<And>n. P n = (n < word_of_nat (min (length xs) (length ys)) * word_of_nat j)
 3. \<forall>s. xf s < word_of_nat (min (length xs) (length ys)) * word_of_nat j \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> ?Q6) body {t. xf t = xf s \<and> xf_update (\<lambda>a. xf t + word_of_nat j) t \<in> ?Q6}
 4. \<And>n. Suc n < length xs \<and> Suc n < length ys \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> zipWith f xs ys ! n \<lbrace>\<lambda>_. F (j + n * j)\<rbrace>
 5. min (length xs) (length ys) * j < 2 ^ LENGTH('c)
 6. \<And>s. F 0 s \<Longrightarrow> P 0 \<longrightarrow> F 0 s
 7. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> {s. xf_update (\<lambda>a. 0) s \<in> ?Q6} proof (prove)
goal (7 subgoals):
 1. \<forall>n. n < length xs \<and> n < length ys \<longrightarrow> ccorres dc xfdc (F (n * j)) ({s. xf s = word_of_nat n * word_of_nat j} \<inter> ?Q6) hs (f (xs ! n) (ys ! n)) body
 2. \<And>n. P n = (n < word_of_nat (min (length xs) (length ys)) * word_of_nat j)
 3. \<forall>s. xf s < word_of_nat (min (length xs) (length ys)) * word_of_nat j \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> ?Q6) body {t. xf t = xf s \<and> xf_update (\<lambda>a. xf t + word_of_nat j) t \<in> ?Q6}
 4. \<And>n. Suc n < length xs \<and> Suc n < length ys \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> zipWith f xs ys ! n \<lbrace>\<lambda>_. F (j + n * j)\<rbrace>
 5. min (length xs) (length ys) * j < 2 ^ LENGTH('c)
 6. \<And>s. F 0 s \<Longrightarrow> P 0 \<longrightarrow> F 0 s
 7. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> {s. xf_update (\<lambda>a. 0) s \<in> ?Q6} proof (prove)
goal (6 subgoals):
 1. \<And>n. P n = (n < word_of_nat (min (length xs) (length ys)) * word_of_nat j)
 2. \<forall>s. xf s < word_of_nat (min (length xs) (length ys)) * word_of_nat j \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>a. xf t + word_of_nat j) t \<in> Q}
 3. \<And>n. Suc n < length xs \<and> Suc n < length ys \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> zipWith f xs ys ! n \<lbrace>\<lambda>_. F (j + n * j)\<rbrace>
 4. min (length xs) (length ys) * j < 2 ^ LENGTH('c)
 5. \<And>s. F 0 s \<Longrightarrow> P 0 \<longrightarrow> F 0 s
 6. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> {s. xf_update (\<lambda>a. 0) s \<in> Q} proof (prove)
goal (5 subgoals):
 1. \<forall>s. xf s < word_of_nat (min (length xs) (length ys)) * word_of_nat j \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>a. xf t + word_of_nat j) t \<in> Q}
 2. \<And>n. Suc n < length xs \<and> Suc n < length ys \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> zipWith f xs ys ! n \<lbrace>\<lambda>_. F (j + n * j)\<rbrace>
 3. min (length xs) (length ys) * j < 2 ^ LENGTH('c)
 4. \<And>s. F 0 s \<Longrightarrow> P 0 \<longrightarrow> F 0 s
 5. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> {s. xf_update (\<lambda>a. 0) s \<in> Q} proof (prove)
goal (4 subgoals):
 1. \<And>n. Suc n < length xs \<and> Suc n < length ys \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> zipWith f xs ys ! n \<lbrace>\<lambda>_. F (j + n * j)\<rbrace>
 2. min (length xs) (length ys) * j < 2 ^ LENGTH('c)
 3. \<And>s. F 0 s \<Longrightarrow> P 0 \<longrightarrow> F 0 s
 4. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> {s. xf_update (\<lambda>a. 0) s \<in> Q} proof (prove)
goal (3 subgoals):
 1. min (length xs) (length ys) * j < 2 ^ LENGTH('c)
 2. \<And>s. F 0 s \<Longrightarrow> P 0 \<longrightarrow> F 0 s
 3. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> {s. xf_update (\<lambda>a. 0) s \<in> Q} proof (prove)
goal (2 subgoals):
 1. \<And>s. F 0 s \<Longrightarrow> P 0 \<longrightarrow> F 0 s
 2. \<And>s. s \<in> {s. xf_update (\<lambda>_. 0) s \<in> Q} \<Longrightarrow> s \<in> {s. xf_update (\<lambda>a. 0) s \<in> Q} proof (prove)
goal:
No subgoals!