theory Ctac

lemma ceqv_xpres_whileAnno:
  "\<lbrakk> ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S';
         xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S'';
         xpres_eq_If pres_norm pres_abr False pres_abr' \<rbrakk>
     \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (whileAnno S I V c) pres_norm pres_abr' False (whileAnno S'' I V c'')" unfolding whileAnno_def apply (cases pres_norm) apply (clarsimp simp add: ceqv_xpres_def xpres_eq_If_def) apply (intro conjI allI) apply (rule While_ceqv) apply (simp add: ceqv_xpres_rewrite_set_def) apply simp apply (erule xpres_ceqv) apply (rule ceqv_refl) apply (erule xpres_strong_while, rule xpres_eq_If_rules) apply (clarsimp simp: ceqv_xpres_def ceqv_def xpres_strong_def xpres_eq_If_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (whileAnno S I V c) pres_norm pres_abr' False (whileAnno S'' I V c'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'')
 2. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> (\<forall>s t. ceqv \<Gamma> xf v s t (While S c) (While S' c')) \<and> xpres_strong \<Gamma> xf v (While S c) True pres_abr False
 2. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s t (While S c) (While S' c')
 2. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (While S c) True pres_abr False
 3. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (5 subgoals):
 1. \<And>s t ta. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> S) = (ta \<in> S')
 2. \<And>s t ta t'. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v ta t' c c'
 3. \<And>s t. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v c True (?pabr9 s t) (?abnormal9 s t)
 4. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (While S c) True pres_abr False
 5. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (4 subgoals):
 1. \<And>s t ta t'. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v ta t' c c'
 2. \<And>s t. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v c True (?pabr9 s t) (?abnormal9 s t)
 3. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (While S c) True pres_abr False
 4. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v c True (?pabr9 s t) (?abnormal9 s t)
 2. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (While S c) True pres_abr False
 3. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (3 subgoals):
 1. \<And>s t ta t'. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v ta t' c c
 2. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (While S c) True pres_abr False
 3. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; c'' = c'; S'' = S'; pres_abr' = pres_abr; pres_norm; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c True pres_abr abnormal\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (While S c) True pres_abr False
 2. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'; ceqv_xpres_rewrite_set xf v S S'; xpres_eq_If pres_norm c' c c''; xpres_eq_If pres_norm S' S S''; xpres_eq_If pres_norm pres_abr False pres_abr'; \<not> pres_norm\<rbrakk> \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (While S c) pres_norm pres_abr' False (While S'' c'') proof (prove)
goal:
No subgoals!