theory Corres_C

lemma ccorres_sequence_while_gen':
  fixes i :: "nat" and xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes one: "\<And>n ys. \<lbrakk> n < length xs \<rbrakk> \<Longrightarrow>
                    ccorres (\<lambda>rv rv'. r' (ys @ [rv]) rv') xf'
                            (F (n * j)) {s. xf s = of_nat (i + n * j) \<and> r' ys (xf' s)} hs
                            (xs ! n) body"
  and      pn: "\<And>n. P n = (n < of_nat (i + length xs * j))"
  and   bodyi: "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}"
  and      hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace> F (n * j) \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>"
  and     lxs: "i + length xs * 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     xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)"
  and       j: "j > 0"
  shows  "ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (i + length xs * of_nat j))
                  (\<lambda>s. (xf s, xf' s))
                  (F 0) ({s. xf s = of_nat i \<and> r' [] (xf' s)}) hs
                  (sequence xs)
                  (While {s. P (xf s)}
                     (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))"
  (is "ccorres ?r' ?xf' ?G ?G' hs (sequence xs) ?body") using assms apply - apply (rule ccorres_guard_imp2) apply (rule ccorres_sequence_while_genQ [where Q=UNIV]) apply (assumption|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (F 0) {s. xf s = word_of_nat i \<and> r' [] (xf' s)} hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
using this:
?n1 < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (?ys1 @ [rv])) xf' (F (?n1 * j)) {s. xf s = word_of_nat (i + ?n1 * j) \<and> r' ?ys1 (xf' s)} hs (xs ! ?n1) body
P ?n1 = (?n1 < word_of_nat (i + length xs * j))
\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}
Suc ?n1 < length xs \<Longrightarrow> \<lbrace>F (?n1 * j)\<rbrace> xs ! ?n1 \<lbrace>\<lambda>_. F (Suc ?n1 * j)\<rbrace>
i + length xs * j < 2 ^ LENGTH('c)
\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s
\<forall>s f. xf' (xf_update f s) = xf' s
0 < j

goal (1 subgoal):
 1. ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (F 0) {s. xf s = word_of_nat i \<and> r' [] (xf' s)} hs (Nondet_Monad.sequence xs) (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. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (F 0) {s. xf s = word_of_nat i \<and> r' [] (xf' s)} hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) ?Q14 ?Q'14 hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>s s'. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j; (s, s') \<in> rf_sr; F 0 s; s' \<in> {s. xf s = word_of_nat i \<and> r' [] (xf' s)}\<rbrakk> \<Longrightarrow> ?Q14 s \<and> s' \<in> ?Q'14 proof (prove)
goal (9 subgoals):
 1. \<And>n ys. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j; n < length xs\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (?F17 (n * j)) ({s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} \<inter> UNIV) hs (xs ! n) body
 2. \<And>n. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> P n = (n < word_of_nat (i + length xs * j))
 3. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> \<forall>s. xf s < word_of_nat (i + length xs * j) \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> UNIV) body {t. xf t = xf s \<and> xf_update (\<lambda>_. xf t + word_of_nat j) t \<in> UNIV}
 4. \<And>n. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j; Suc n < length xs\<rbrakk> \<Longrightarrow> \<lbrace>?F17 (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. ?F17 (Suc n * j)\<rbrace>
 5. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> i + length xs * j < 2 ^ LENGTH('c)
 6. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> \<forall>s f. xf (xf_update (\<lambda>uu_. f (?xf_update18 f s uu_)) s) = f (xf s) \<and> globals (xf_update (\<lambda>uu_. f (?xf_update18 f s uu_)) s) = globals s
 7. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> \<forall>s f. xf' (xf_update (\<lambda>uu_. f (?xf_update18 f s uu_)) s) = xf' s
 8. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j\<rbrakk> \<Longrightarrow> 0 < j
 9. \<And>s s'. \<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres (\<lambda>rv. r' (ys @ [rv])) xf' (F (n * j)) {s. xf s = word_of_nat (i + n * j) \<and> r' ys (xf' s)} hs (xs ! n) body; \<And>n. P n = (n < word_of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ LENGTH('c); \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; \<forall>s f. xf' (xf_update f s) = xf' s; 0 < j; (s, s') \<in> rf_sr; F 0 s; s' \<in> {s. xf s = word_of_nat i \<and> r' [] (xf' s)}\<rbrakk> \<Longrightarrow> (P 0 \<longrightarrow> ?F17 0 s) \<and> s' \<in> {s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> UNIV proof (prove)
goal:
No subgoals!