theory Ctac

lemma creturn_ceqv_not_xf:
  fixes \<Gamma> :: "(('a globals_scheme, 'b) myvars_scheme) c_body"
  assumes rl: "\<And>t. rewrite_xf xf t v rv rv'"
  and    xfu: "\<And>s f. xf (xfu' f s) = xf s" \<comment> \<open>i.e., xf is independent of xfu\<close>
  and    xfg: "\<And>s f. xf (global_exn_var_'_update f s) = xf s"
  shows   "ceqv \<Gamma> xf v t t' (return_C xfu' rv) (return_C xfu' rv')" unfolding creturn_def apply (rule Seq_ceqv)+ apply (rule Basic_ceqv) apply (rule rewrite_xfI) apply (simp add: rewrite_xfD [OF rl] xfu) apply (rule Seq_ceqv) apply (rule Basic_ceqv) apply (simp add: rewrite_xf_def) apply (rule Throw_ceqv) apply (rule xpres_basic) apply (simp add: xfg) apply (rule xpres_basic) apply (simp add: xfu) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (return_C xfu' rv) (return_C xfu' rv') proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) (Basic (\<lambda>s. xfu' (\<lambda>_. rv' s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) proof (prove)
goal (3 subgoals):
 1. \<And>t'. ceqv \<Gamma> xf v t t' (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) (Basic (\<lambda>s. xfu' (\<lambda>_. rv' s) s))
 2. \<And>t. ceqv \<Gamma> xf v t t' (\<acute>global_exn_var :== Return;;
THROW) (\<acute>global_exn_var :== Return;;
THROW)
 3. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (3 subgoals):
 1. \<And>t'. rewrite_xf xf t v (\<lambda>s. xfu' (\<lambda>_. rv s) s) (\<lambda>s. xfu' (\<lambda>_. rv' s) s)
 2. \<And>t. ceqv \<Gamma> xf v t t' (\<acute>global_exn_var :== Return;;
THROW) (\<acute>global_exn_var :== Return;;
THROW)
 3. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (3 subgoals):
 1. \<And>t'. xf t = v \<Longrightarrow> xfu' (\<lambda>_. rv t) t = xfu' (\<lambda>_. rv' t) t
 2. \<And>t. ceqv \<Gamma> xf v t t' (\<acute>global_exn_var :== Return;;
THROW) (\<acute>global_exn_var :== Return;;
THROW)
 3. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (2 subgoals):
 1. \<And>t. ceqv \<Gamma> xf v t t' (\<acute>global_exn_var :== Return;;
THROW) (\<acute>global_exn_var :== Return;;
THROW)
 2. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (4 subgoals):
 1. \<And>t t'. ceqv \<Gamma> xf v t t' (\<acute>global_exn_var :== Return) (\<acute>global_exn_var :== Return)
 2. \<And>t ta. ceqv \<Gamma> xf v ta t' THROW THROW
 3. \<And>t. xpres_strong \<Gamma> xf v (\<acute>global_exn_var :== Return) True (?pres_abr8 t) (?abnormal8 t)
 4. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (4 subgoals):
 1. \<And>t t'. rewrite_xf xf t v (global_exn_var_'_update (\<lambda>_. Return)) (global_exn_var_'_update (\<lambda>_. Return))
 2. \<And>t ta. ceqv \<Gamma> xf v ta t' THROW THROW
 3. \<And>t. xpres_strong \<Gamma> xf v (\<acute>global_exn_var :== Return) True (?pres_abr8 t) (?abnormal8 t)
 4. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (3 subgoals):
 1. \<And>t ta. ceqv \<Gamma> xf v ta t' THROW THROW
 2. \<And>t. xpres_strong \<Gamma> xf v (\<acute>global_exn_var :== Return) True (?pres_abr8 t) (?abnormal8 t)
 3. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (2 subgoals):
 1. \<And>t. xpres_strong \<Gamma> xf v (\<acute>global_exn_var :== Return) True (?pres_abr8 t) (?abnormal8 t)
 2. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (2 subgoals):
 1. \<And>t s. xf s = v \<Longrightarrow> xf (s\<lparr>global_exn_var_' := Return\<rparr>) = v
 2. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu' (\<lambda>_. rv s) s)) True ?pres_abr ?abnormal proof (prove)
goal (1 subgoal):
 1. \<And>s. xf s = v \<Longrightarrow> xf (xfu' (\<lambda>_. rv s) s) = v proof (prove)
goal:
No subgoals!