theory Corres_C

lemma ccorres_return_void_C_Seq:
  "ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X return_void_C \<Longrightarrow>
      ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_void_C ;; Z)" apply (clarsimp simp: return_void_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 (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_void_C \<Longrightarrow> ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_void_C;;
Z) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (\<acute>global_exn_var :== Return;;
THROW) \<Longrightarrow> ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (\<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' (\<acute>global_exn_var :== Return;;
THROW) (\<acute>global_exn_var :== Return;;
THROW;;
Z) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> P' \<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 \<in> P' \<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>\<acute>global_exn_var :== Return,Normal s\<rangle> \<Rightarrow> Normal s''\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' s''. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>THROW,Normal s''\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''\<rangle> \<Rightarrow> s'
 2. \<And>s s' s''. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s''\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' s''. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>\<acute>global_exn_var :== Return,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>THROW;;
Z,Normal s''\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s''\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!