theory Ctac

lemma ceqv_xpres_While_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)"
  shows "ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False
        (if \<exists>n offs. (\<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs)) \<and> \<not> CP (v + of_nat n * offs)
          then simpl_sequence c' (map (\<lambda>x. v + of_nat x
                  * (THE offs. \<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs)))
              [0 ..< (LEAST n. \<not> CP (v + of_nat n
                  * (THE offs. \<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs))))])
          else While {s. CP (xf' s)} c)" apply (split if_split, clarsimp simp: ceqv_xpres_def xpres_strong_def ceqv_refl) apply (rule ceqv_trans) apply (rule_tac n="LEAST n. \<not> CP (v + of_nat n * offs)"
     in ceqv_xpres_to_simpl_sequence[simplified ceqv_xpres_eq_ceqv, rule_format]) apply (rule c) apply simp apply simp apply (rule LeastI_ex) apply blast apply (subst takeWhile_eq_all_conv[THEN iffD2]) apply (clarsimp dest!: not_less_Least) apply (simp add: ceqv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False False False (if \<exists>n offs. (\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs) \<and> \<not> CP (v + of_nat n * offs) then simpl_sequence c' (map (\<lambda>x. v + of_nat x * (THE offs. \<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs)) [0..<LEAST n. \<not> CP (v + of_nat n * (THE offs. \<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs))]) else While {s. CP (xf' s)} c) proof (prove)
goal (1 subgoal):
 1. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (While {s. CP (xf' s)} c) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (2 subgoals):
 1. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (While {s. CP (xf' s)} c) (?c'11 n offs s t)
 2. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (?c'11 n offs s t) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (4 subgoals):
 1. \<And>n offs s t va. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf' va True c (?pres_norm14 n offs s t) (?pres_abr14 n offs s t) (?abnormal14 n offs s t) (?c'14 n offs s t va)
 2. \<And>n offs s t va sa. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> xf' (simpl_final_basic (?c'14 n offs s t va) sa) - va = ?offs14 n offs s t
 3. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> \<not> CP (v + of_nat (LEAST n. \<not> CP (v + of_nat n * offs)) * ?offs14 n offs s t)
 4. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence (?c'14 n offs s t) (takeWhile CP (map (\<lambda>x. v + of_nat x * ?offs14 n offs s t) [0..<LEAST n. \<not> CP (v + of_nat n * offs)]))) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (3 subgoals):
 1. \<And>n offs s t va sa. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> xf' (simpl_final_basic (c' va) sa) - va = ?offs14 n offs s t
 2. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> \<not> CP (v + of_nat (LEAST n. \<not> CP (v + of_nat n * offs)) * ?offs14 n offs s t)
 3. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * ?offs14 n offs s t) [0..<LEAST n. \<not> CP (v + of_nat n * offs)]))) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (2 subgoals):
 1. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> \<not> CP (v + of_nat (LEAST n. \<not> CP (v + of_nat n * offs)) * offs)
 2. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)]))) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (2 subgoals):
 1. \<And>n offs. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> \<not> CP (v + of_nat (LEAST n. \<not> CP (v + of_nat n * offs)) * offs)
 2. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)]))) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (2 subgoals):
 1. \<And>n offs. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> \<exists>x. \<not> CP (v + of_nat x * offs)
 2. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)]))) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (1 subgoal):
 1. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)]))) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (2 subgoals):
 1. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> Ball (set (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) CP
 2. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal (1 subgoal):
 1. \<And>n offs s t. \<lbrakk>\<forall>s v. xf' (simpl_final_basic (c' v) s) - v = offs; \<not> CP (v + of_nat n * offs)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' v s t (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) (simpl_sequence c' (map (\<lambda>x. v + of_nat x * offs) [0..<LEAST n. \<not> CP (v + of_nat n * offs)])) proof (prove)
goal:
No subgoals!