theory Ctac

lemma ceqv_xpres_to_simpl_sequence:
  fixes v :: "'a :: ring_1"
  assumes c: "\<And>v. ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v)"
      and v: "\<And>v s. xf' (simpl_final_basic (c' v) s) - v = offs"
  shows "\<not> CP (v + of_nat n * offs)
    \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False
        (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0 ..< n])))"
  (is "_ \<Longrightarrow> ceqv_xpres _ _ _ _ (While ?S _) _ _ _ _") proof (induct n arbitrary: v) case 0 show ?case using c[where v=v] 0 apply (simp add: simpl_sequence_def) apply (simp add: ceqv_xpres_def ceqv_def xpres_strong_False_trivial) apply (auto elim!: exec_Normal_elim_cases intro: exec.Skip exec.WhileFalse) done next case (Suc n) have foo: "\<And>t t'. (\<Gamma> \<turnstile> \<langle>c' v, Normal t\<rangle> \<Rightarrow> Normal t') \<longrightarrow> xf' t' = v + offs" using v by (clarsimp simp: field_simps dest!: simpl_final_basic_exec) show ?case using c[where v=v] Suc.hyps[where v="v + offs"] Suc.prems apply (subst upt_conv_Cons, simp) apply (simp only: map_Suc_upt[symmetric] list.simps) apply (cases "CP v") apply (simp add: o_def field_simps simpl_sequence_Cons
                      ceqv_xpres_def xpres_strong_False_trivial) apply (clarsimp, rule ceqv_trans[where c'="c ;; While ?S c"]) apply (simp add: ceqv_def) apply (auto elim!: exec_Normal_elim_cases intro: exec.Seq exec.WhileTrue)[1] apply (rule ceqv_trans[where c'="c' v ;; While ?S c"]) apply (simp add: ceqv_def) apply (auto elim!: exec_Normal_elim_cases intro: exec.Seq)[1] apply (simp add: ceqv_def) apply (intro impI exec_Seq_cong refl) apply (simp add: foo) apply (simp add: simpl_sequence_def field_simps) apply (simp add: ceqv_xpres_def xpres_strong_False_trivial ceqv_def) apply (auto intro: exec.WhileFalse exec.Skip elim!: exec_Normal_elim_cases)[1] done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> CP (v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<n]))) proof (state)
goal (2 subgoals):
 1. \<And>v. \<not> CP (v + of_nat 0 * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<0])))
 2. \<And>n v. \<lbrakk>\<And>v. \<not> CP (v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (state)
this:
\<not> CP (v + of_nat 0 * offs)

goal (2 subgoals):
 1. \<And>v. \<not> CP (v + of_nat 0 * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<0])))
 2. \<And>n v. \<lbrakk>\<And>v. \<not> CP (v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<0]))) proof (prove)
using this:
ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v)
\<not> CP (v + of_nat 0 * offs)

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<0]))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False SKIP proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v,Normal s\<rangle> \<Rightarrow> t)) \<and> xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal; \<not> CP v\<rbrakk> \<Longrightarrow> \<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> t) proof (prove)
goal:
No subgoals! proof (state)
this:
ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<0])))

goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. \<not> CP (v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (state)
goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. \<not> CP (v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (state)
this:
\<not> CP (?v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' ?v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. ?v + of_nat x * offs) [0..<n])))
\<not> CP (v + of_nat (Suc n) * offs)

goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. \<not> CP (v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (prove)
goal (1 subgoal):
 1. \<And>t t'. \<Gamma>\<turnstile> \<langle>c' v,Normal t\<rangle> \<Rightarrow> Normal t' \<longrightarrow> xf' t' = v + offs proof (prove)
using this:
xf' (simpl_final_basic (c' ?v) ?s) - ?v = offs

goal (1 subgoal):
 1. \<And>t t'. \<Gamma>\<turnstile> \<langle>c' v,Normal t\<rangle> \<Rightarrow> Normal t' \<longrightarrow> xf' t' = v + offs proof (state)
this:
\<Gamma>\<turnstile> \<langle>c' v,Normal ?t\<rangle> \<Rightarrow> Normal ?t' \<longrightarrow> xf' ?t' = v + offs

goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. \<not> CP (v + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (prove)
using this:
ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v)
\<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n])))
\<not> CP (v + of_nat (Suc n) * offs)

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n]))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) (0 # [Suc 0..<Suc n])))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n]))))
 2. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>s t. ceqv \<Gamma> xf' v s t c (c' v)) \<and> xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal; \<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v\<rbrakk> \<Longrightarrow> \<forall>s t. ceqv \<Gamma> xf' v s t (While {s. CP (xf' s)} c) (c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])))
 2. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (While {s. CP (xf' s)} c) (c;;
While {s. CP (xf' s)} c)
 2. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (c;;
While {s. CP (xf' s)} c) (c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])))
 3. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s. xf' s = offs + v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])),Normal s\<rangle> \<Rightarrow> t); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v,Normal s\<rangle> \<Rightarrow> t); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> xf' s = v \<longrightarrow> \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c;;
While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t
 2. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (c;;
While {s. CP (xf' s)} c) (c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])))
 3. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (c;;
While {s. CP (xf' s)} c) (c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])))
 2. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (c;;
While {s. CP (xf' s)} c) (c' v;;
While {s. CP (xf' s)} c)
 2. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (c' v;;
While {s. CP (xf' s)} c) (c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])))
 3. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s. xf' s = offs + v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])),Normal s\<rangle> \<Rightarrow> t); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v,Normal s\<rangle> \<Rightarrow> t); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> xf' s = v \<longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v;;
While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t
 2. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (c' v;;
While {s. CP (xf' s)} c) (c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])))
 3. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s t. ceqv \<Gamma> xf' (offs + v) s t (While {s. CP (xf' s)} c) (simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s t. ceqv \<Gamma> xf' v s t c (c' v); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (c' v;;
While {s. CP (xf' s)} c) (c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])))
 2. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s. xf' s = offs + v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])),Normal s\<rangle> \<Rightarrow> t); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v,Normal s\<rangle> \<Rightarrow> t); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> xf' s = v \<longrightarrow> \<Gamma>\<turnstile> \<langle>c' v;;
While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v;;
simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])),Normal s\<rangle> \<Rightarrow> t
 2. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (2 subgoals):
 1. \<And>s t s''. \<lbrakk>\<forall>s. xf' s = offs + v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])),Normal s\<rangle> \<Rightarrow> t); \<not> CP (offs + (v + of_nat n * offs)); CP v; \<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v,Normal s\<rangle> \<Rightarrow> t); xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal; xf' s = v; \<Gamma>\<turnstile> \<langle>c' v,Normal s\<rangle> \<Rightarrow> Normal s''\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s''\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>simpl_sequence c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n])),Normal s''\<rangle> \<Rightarrow> t
 2. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); \<not> CP (v + offs + of_nat n * offs) \<Longrightarrow> ceqv_xpres \<Gamma> xf' (v + offs) True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + offs + of_nat x * offs) [0..<n]))); \<not> CP (v + of_nat (Suc n) * offs); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP ((v + of_nat 0 * offs) # map (\<lambda>x. v + of_nat x * offs) (map Suc [0..<n])))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf' v True c pres_norm pres_abr abnormal (c' v); ceqv_xpres \<Gamma> xf' (offs + v) True (While {s. CP (xf' s)} c) False False False (foldr Seq (map c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))) SKIP); \<not> CP (offs + (v + of_nat n * offs)); \<not> CP v\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False SKIP proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c' v,Normal s\<rangle> \<Rightarrow> t)) \<and> xpres_strong \<Gamma> xf' v c pres_norm pres_abr abnormal; \<forall>s. xf' s = offs + v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>foldr Seq (map c' (takeWhile CP (map (\<lambda>x. offs + (v + of_nat x * offs)) [0..<n]))) SKIP,Normal s\<rangle> \<Rightarrow> t); \<not> CP (offs + (v + of_nat n * offs)); \<not> CP v\<rbrakk> \<Longrightarrow> \<forall>s. xf' s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>While {s. CP (xf' s)} c,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> t) proof (prove)
goal:
No subgoals! proof (state)
this:
ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<Suc n])))

goal:
No subgoals!