theory Corres_C

lemma ccorres_sequence_x_while_genQ':
  fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  shows
  "\<lbrakk>\<And>n. n < length xs \<Longrightarrow> ccorres dc xfdc (F (n * j)) ({s. xf s = of_nat (i + n * j)} \<inter> Q) hs (xs ! n) body;
    \<And>n. P n = (n < of_nat (i + length xs * j));
    \<forall>s. xf s < of_nat (i + length xs * 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>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 ^ len_of TYPE('c);
    \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; j > 0 \<rbrakk>
    \<Longrightarrow> ccorres (\<lambda>rv i'. i' = of_nat (i + length xs * of_nat j)) xf (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = of_nat i} \<inter> Q) hs
       (Nondet_Monad.sequence_x xs)
       (While {s. P (xf s)} (body;;
                 Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" apply (simp add: sequence_x_sequence liftM_def[symmetric]
                   ccorres_liftM_simp) apply (rule ccorres_rel_imp) apply (rule ccorres_sequence_while_genQ
                   [where xf'=xfdc and r'=dc and xf_update=xf_update, simplified],
          (simp add: dc_def cong: ccorres_all_cong)+) done

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