theory Ctac

lemma creturn_ceqv_xf:
  fixes \<Gamma> :: "(('a globals_scheme, 'b) myvars_scheme) c_body"
  assumes xfg: "\<And>s f. xf (global_exn_var_'_update f s) = xf s"
  and   xfxfu: "\<And>v s. xf (xfu (\<lambda>_. v) s) = v"
  shows   "ceqv \<Gamma> xf v t t' (return_C xfu xf) (return_C xfu (\<lambda>_. v))" unfolding creturn_def apply (rule Seq_ceqv)+ apply (rule Basic_ceqv) apply (rule rewrite_xfI) apply simp apply (rule Seq_ceqv) apply (rule Basic_ceqv) apply (simp add: rewrite_xf_def) apply (rule Throw_ceqv) apply (rule xpres_basic) apply simp apply (simp add: xfg) apply (rule xpres_basic) apply (simp add: xfxfu) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (return_C xfu xf) (return_C xfu (\<lambda>_. v)) proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (Basic (\<lambda>s. xfu (\<lambda>_. xf s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) (Basic (xfu (\<lambda>_. v));;
(\<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>_. xf s) s)) (Basic (xfu (\<lambda>_. v)))
 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>_. xf s) s)) True ?pres_abr ?abnormal proof (prove)
goal (3 subgoals):
 1. \<And>t'. rewrite_xf xf t v (\<lambda>s. xfu (\<lambda>_. xf s) s) (xfu (\<lambda>_. v))
 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>_. xf s) s)) True ?pres_abr ?abnormal proof (prove)
goal (3 subgoals):
 1. \<And>t'. xf t = v \<Longrightarrow> xfu (\<lambda>_. xf t) t = xfu (\<lambda>_. v) 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>_. xf 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>_. xf 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>_. xf 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>_. xf 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>_. xf 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>_. xf 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>_. xf s) s)) True ?pres_abr ?abnormal proof (prove)
goal (2 subgoals):
 1. \<And>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>_. xf s) s)) True ?pres_abr ?abnormal proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu (\<lambda>_. xf s) s)) True ?pres_abr ?abnormal proof (prove)
goal (1 subgoal):
 1. \<And>s. xf s = v \<Longrightarrow> xf (xfu (\<lambda>_. xf s) s) = v proof (prove)
goal:
No subgoals!