theory Corres_C

lemma ccorres_mapM_x_while_gen':
  fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes rl: "\<forall>n. n < length xs \<longrightarrow>
                   ccorres dc xfdc (F (n * j)) {s. xf s = of_nat (i + n * j)} hs (f (xs ! n)) body"
  and  guard: "\<And>n. P n = (n < of_nat (i + length xs * j))"
  and  bodyi: "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {s'. xf s' = xf s}"
  and  hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n *j)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>"
  and  wb: "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   j: "0 < j"
  shows  "ccorres (\<lambda>rv rv'. rv' = of_nat (i + length xs * j)) xf
                  (F (0 :: nat)) {s. xf s = of_nat i} hs
                  (mapM_x f xs)
                  (While {s. P (xf s)}
                     (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" unfolding mapM_x_def apply (rule ccorres_rel_imp) apply (rule ccorres_sequence_x_while_gen'[where xf_update=xf_update]) apply (clarsimp simp only: length_map nth_map rl) apply (simp add: assms hi[simplified])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = word_of_nat (i + length xs * j)) xf (F 0) {s. xf s = word_of_nat i} hs (mapM_x f 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. ccorres (\<lambda>rv rv'. rv' = word_of_nat (i + length xs * j)) xf (F 0) {s. xf s = word_of_nat i} hs (sequence_x (map f 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. ccorres ?r' ?xf' (F 0) {s. xf s = word_of_nat i} hs (sequence_x (map f xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>x y. ?r' x (?xf' y) \<Longrightarrow> xf y = word_of_nat (i + length xs * j) proof (prove)
goal (8 subgoals):
 1. \<And>n ys. n < length (map f xs) \<Longrightarrow> ccorres dc xfdc (F (n * j)) {s. xf s = word_of_nat (i + n * j)} hs (map f xs ! n) body
 2. \<And>n. P n = (n < word_of_nat (i + length (map f xs) * j))
 3. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}
 4. \<And>n. Suc n < length (map f xs) \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> map f xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>
 5. i + length (map f xs) * j < 2 ^ LENGTH('c)
 6. \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s
 7. 0 < j
 8. \<And>x y. xf y = word_of_nat (i + length (map f xs) * of_nat j) \<Longrightarrow> xf y = word_of_nat (i + length xs * j) proof (prove)
goal (7 subgoals):
 1. \<And>n. P n = (n < word_of_nat (i + length (map f xs) * j))
 2. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}
 3. \<And>n. Suc n < length (map f xs) \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> map f xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>
 4. i + length (map f xs) * j < 2 ^ LENGTH('c)
 5. \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s
 6. 0 < j
 7. \<And>x y. xf y = word_of_nat (i + length (map f xs) * of_nat j) \<Longrightarrow> xf y = word_of_nat (i + length xs * j) proof (prove)
goal:
No subgoals!