theory Corres_C

lemma ccorres_trim_returnE:
  assumes fg: "\<And>s. xfu (\<lambda>_. axf s) s = s"
  and    xfu: "\<And>f s. axf (global_exn_var_'_update f s) = axf s"
  and     cc: "ccorres r (liftxf errstate ef vf axf)
                    G G' (SKIP # hs) a c"
  shows "ccorres_underlying rf_sr \<Gamma> rvr rvxf r (liftxf errstate ef vf axf)
                    G G' (SKIP # hs) a (c ;; return_C xfu axf)" unfolding creturn_def apply (rule ccorres_rhs_assoc2)+ apply (rule ccorres_trim_redundant_throw') apply (simp add: fg) apply (rule iffD2 [OF ccorres_semantic_equiv, OF _ cc]) apply (rule semantic_equivI) apply (case_tac s') apply (auto elim!: exec_Normal_elim_cases exec_elim_cases intro!: exec.intros)[4] apply (simp add: liftxf_def xfu) apply (simp add: rf_sr_globals_exn_var) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> rvr rvxf r (liftxf errstate ef vf axf) G G' (SKIP # hs) a (c;;
return_C xfu axf) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> rvr rvxf r (liftxf errstate ef vf axf) G G' (SKIP # hs) a (c;;
(Basic (\<lambda>s. xfu (\<lambda>_. axf s) s);;
(\<acute>global_exn_var :== Return;;
THROW))) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> rvr rvxf r (liftxf errstate ef vf axf) G G' (SKIP # hs) a (c;;
Basic (\<lambda>s. xfu (\<lambda>_. axf s) s);;
\<acute>global_exn_var :== Return;;
THROW) proof (prove)
goal (3 subgoals):
 1. ccorres r (liftxf errstate ef vf axf) G G' (SKIP # hs) a (c;;
Basic (\<lambda>s. xfu (\<lambda>_. axf s) s))
 2. \<And>s. liftxf errstate ef vf axf (s\<lparr>global_exn_var_' := Return\<rparr>) = liftxf errstate ef vf axf s
 3. \<And>t t'. (t, t') \<in> rf_sr \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. ccorres r (liftxf errstate ef vf axf) G G' (SKIP # hs) a (c;;
Basic (\<lambda>s. s))
 2. \<And>s. liftxf errstate ef vf axf (s\<lparr>global_exn_var_' := Return\<rparr>) = liftxf errstate ef vf axf s
 3. \<And>t t'. (t, t') \<in> rf_sr \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (c;;
Basic (\<lambda>s. s)) c
 2. \<And>s. liftxf errstate ef vf axf (s\<lparr>global_exn_var_' := Return\<rparr>) = liftxf errstate ef vf axf s
 3. \<And>t t'. (t, t') \<in> rf_sr \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
Basic (\<lambda>s. s),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s. liftxf errstate ef vf axf (s\<lparr>global_exn_var_' := Return\<rparr>) = liftxf errstate ef vf axf s
 3. \<And>t t'. (t, t') \<in> rf_sr \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (6 subgoals):
 1. \<And>s s' x1. \<lbrakk>s \<in> G'; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
Basic (\<lambda>s. s),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s' x2. \<lbrakk>s \<in> G'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
Basic (\<lambda>s. s),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s' x3. \<lbrakk>s \<in> G'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
Basic (\<lambda>s. s),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
Basic (\<lambda>s. s),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
 5. \<And>s. liftxf errstate ef vf axf (s\<lparr>global_exn_var_' := Return\<rparr>) = liftxf errstate ef vf axf s
 6. \<And>t t'. (t, t') \<in> rf_sr \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>s. liftxf errstate ef vf axf (s\<lparr>global_exn_var_' := Return\<rparr>) = liftxf errstate ef vf axf s
 2. \<And>t t'. (t, t') \<in> rf_sr \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>t t'. (t, t') \<in> rf_sr \<Longrightarrow> (t, t'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr proof (prove)
goal:
No subgoals!