theory Corres_C

lemma ccorres_sequence_x_while_gen:
  fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes one: "\<forall>n < length xs. ccorres dc xfdc (F (n * j)) {s. xf s = of_nat n * of_nat j} hs (xs ! n) body"
  and      pn: "\<And>n. P n = (n < of_nat (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: "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 (length xs) * of_nat j) xf (F 0) UNIV hs
                  (sequence_x xs)
                  (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))))" apply (rule ccorres_symb_exec_r) apply (rule ccorres_rel_imp) apply (rule ccorres_sequence_x_while_gen' [where i=0 and xf_update=xf_update, simplified]) apply (simp add: assms hi[simplified])+ apply vcg apply (simp add: xf) apply vcg apply (simp add: xf rf_sr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = word_of_nat (length xs) * word_of_nat j) xf (F 0) UNIV hs (sequence_x xs) (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 (length xs) * word_of_nat j) xf (F 0) ?Q' hs (sequence_x xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<Gamma>\<turnstile> UNIV Basic (xf_update (\<lambda>_. 0)) ?Q'
 3. \<And>s. F 0 s \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) Basic (xf_update (\<lambda>_. 0)) {s'. (s, s') \<in> rf_sr} proof (prove)
goal (4 subgoals):
 1. ccorres ?r'4 ?xf'4 (F 0) ?Q' hs (sequence_x 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'4 x (?xf'4 y) \<Longrightarrow> xf y = word_of_nat (length xs) * word_of_nat j
 3. \<Gamma>\<turnstile> UNIV Basic (xf_update (\<lambda>_. 0)) ?Q'
 4. \<And>s. F 0 s \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) Basic (xf_update (\<lambda>_. 0)) {s'. (s, s') \<in> rf_sr} proof (prove)
goal (10 subgoals):
 1. \<And>n. n < length xs \<Longrightarrow> ccorres dc xfdc (F (n * j)) {s. xf s = word_of_nat n * word_of_nat j} hs (xs ! n) body
 2. \<And>n. P n = (n < word_of_nat (length xs) * word_of_nat j)
 3. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}
 4. \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (j + n * j)\<rbrace>
 5. length 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 (0 + length xs * of_nat j) \<Longrightarrow> xf y = word_of_nat (length xs) * word_of_nat j
 9. \<Gamma>\<turnstile> UNIV Basic (xf_update (\<lambda>_. 0)) {s. xf s = 0}
 10. \<And>s. F 0 s \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) Basic (xf_update (\<lambda>_. 0)) {s'. (s, s') \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> UNIV Basic (xf_update (\<lambda>_. 0)) {s. xf s = 0}
 2. \<And>s. F 0 s \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) Basic (xf_update (\<lambda>_. 0)) {s'. (s, s') \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. UNIV \<subseteq> {s. xf (xf_update (\<lambda>_. 0) s) = 0}
 2. \<And>s. F 0 s \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) Basic (xf_update (\<lambda>_. 0)) {s'. (s, s') \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>s. F 0 s \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) Basic (xf_update (\<lambda>_. 0)) {s'. (s, s') \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>s. F 0 s \<Longrightarrow> UNIV \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, xf_update (\<lambda>_. 0) sa) \<in> rf_sr} proof (prove)
goal:
No subgoals!