theory Corres_C

lemma ccorres_trim_return:
  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_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c ;; return_C xfu axf)" using fg unfolding creturn_def apply - apply (rule ccorres_rhs_assoc2)+ apply (rule ccorres_trim_redundant_throw) apply (clarsimp split del: if_split) 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 (rule xfu) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c;;
return_C xfu axf) proof (prove)
using this:
xfu (\<lambda>_. axf ?s1) ?s1 = ?s1

goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c;;
return_C xfu axf) proof (prove)
using this:
xfu (\<lambda>_. axf ?s1) ?s1 = ?s1

goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel 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. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel 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. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c;;
Basic (\<lambda>s. xfu (\<lambda>_. axf s) s);;
\<acute>global_exn_var :== Return;;
THROW) proof (prove)
goal (2 subgoals):
 1. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> ccorres arrel axf G G' (SKIP # hs) a (c;;
Basic (\<lambda>s. xfu (\<lambda>_. axf s) s))
 2. \<And>s f. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> axf (global_exn_var_'_update f s) = axf s proof (prove)
goal (2 subgoals):
 1. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> ccorres arrel axf G G' (SKIP # hs) a (c;;
Basic (\<lambda>s. s))
 2. \<And>s f. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> axf (global_exn_var_'_update f s) = axf s proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<And>s. xfu (\<lambda>_. axf s) s = s; s \<in> G'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s s' (c;;
Basic (\<lambda>s. s)) c
 2. \<And>s f. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> axf (global_exn_var_'_update f s) = axf s proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<And>s. xfu (\<lambda>_. axf s) s = s; s \<in> G'\<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 f. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> axf (global_exn_var_'_update f s) = axf s proof (prove)
goal (5 subgoals):
 1. \<And>s s' x1. \<lbrakk>\<And>s. xfu (\<lambda>_. axf s) s = s; 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>\<And>s. xfu (\<lambda>_. axf s) s = s; 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>\<And>s. xfu (\<lambda>_. axf s) s = s; 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>\<And>s. xfu (\<lambda>_. axf s) s = s; 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 f. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> axf (global_exn_var_'_update f s) = axf s proof (prove)
goal (1 subgoal):
 1. \<And>s f. (\<And>s. xfu (\<lambda>_. axf s) s = s) \<Longrightarrow> axf (global_exn_var_'_update f s) = axf s proof (prove)
goal:
No subgoals!