theory Retype_C

lemma ccorres_return_C_Seq:
  "ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_C xfu v) \<Longrightarrow>
      ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_C xfu v ;; Z)" apply (clarsimp simp: return_C_def) apply (erule ccorres_semantic_equiv0[rotated]) apply (rule semantic_equivI) apply (clarsimp simp: exec_assoc[symmetric]) apply (rule exec_Seq_cong, simp) apply (clarsimp simp: exec_assoc[symmetric]) apply (rule exec_Seq_cong, simp) apply (rule iffI) apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw exec.Seq)[1] apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_C xfu v) \<Longrightarrow> ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_C xfu v;;
Z) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) \<Longrightarrow> ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW);;
Z) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> P' \<Longrightarrow> semantic_equiv \<Gamma> s s' (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW);;
Z) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> P' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW);;
Z,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> P' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW;;
Z),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' s''. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s),Normal s\<rangle> \<Rightarrow> Normal s''\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return;;
THROW,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return;;
THROW;;
Z,Normal s''\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' s''. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s),Normal s\<rangle> \<Rightarrow> Normal s''\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return;;
THROW,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return;;
(THROW;;
Z),Normal s''\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'' s''a. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s),Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s''\<rangle> \<Rightarrow> Normal s''a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s''a\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''a\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' s'' s''a. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s),Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s''\<rangle> \<Rightarrow> Normal s''a; \<Gamma>\<turnstile> \<langle>THROW,Normal s''a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''a\<rangle> \<Rightarrow> s'
 2. \<And>s s' s'' s''a. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s),Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s''\<rangle> \<Rightarrow> Normal s''a; \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s''a\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'' s''a. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s),Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s''\<rangle> \<Rightarrow> Normal s''a; \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s''a\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!