theory Corres_C

lemma ccorres_split_nothrow_call_novcg:
  assumes ac: "ccorres r' xf'' P P' [] a (Call f)"
  and     gg: "\<And>x y s. globals (g x y s) = globals s"
  and   xfxf: "\<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t"
  and     gi: "\<And>s. globals (i s) = globals s"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'} \<inter>
             {s'. (\<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))})
            hs (a >>= (\<lambda>rv. b rv))
         (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) ;; d)" (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?P (?Q1 \<inter> ?Q2) hs ?A ?B") apply (rule ccorres_master_split_nohs) apply (rule ccorres_call [OF ac]) apply (rule gg) apply (rule xfxf) apply (rule gi) apply (rule ccorres_abstract[OF ceqv]) apply (rule ccorres_gen_asm2) apply (erule bd) apply (simp add: valid) apply (rule exec_handlers_Hoare_call_Basic) apply (clarsimp simp: ccHoarePost_def xfxf) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)}) hs (a >>= b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y));;
d) proof (prove)
goal (4 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> ?r' ?xf' ?arrel' ?axf' P {s. i s \<in> P'} [] a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)))
 2. \<And>rv. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 3. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost ?r' ?xf' (\<lambda>a b. ?R' a)) UNIV proof (prove)
goal (6 subgoals):
 1. \<And>x y s. globals (g x y s) = globals s
 2. \<And>a s t. ?xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 3. \<And>s. globals (i s) = globals s
 4. \<And>rv. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 5. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 6. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' ?xf' (\<lambda>a b. ?R' a)) UNIV proof (prove)
goal (5 subgoals):
 1. \<And>a s t. ?xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 2. \<And>s. globals (i s) = globals s
 3. \<And>rv. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 4. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 5. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' ?xf' (\<lambda>a b. ?R' a)) UNIV proof (prove)
goal (4 subgoals):
 1. \<And>s. globals (i s) = globals s
 2. \<And>rv. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 3. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' xf' (\<lambda>a b. ?R' a)) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' xf' (\<lambda>a b. ?R' a)) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?R rv) (?G'15 rv rv') hs (b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> ?G'15 a (xf' s)})) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. ?P19 rv rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?R rv) (?G'19 rv rv') hs (b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> ?G'19 a (xf' s) \<inter> \<lbrace>?P19 a (xf' s)\<rbrace>})) UNIV proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>
 2. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})) UNIV proof (prove)
goal (1 subgoal):
 1. exec_handlers_Hoare \<Gamma> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})) UNIV proof (prove)
goal (2 subgoals):
 1. \<forall>s' t x. s' \<in> {s'. \<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t)} \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})
 2. UNIV \<subseteq> UNIV proof (prove)
goal (1 subgoal):
 1. UNIV \<subseteq> UNIV proof (prove)
goal:
No subgoals!