theory Corres_C

lemma ccorres_split_nothrow_call_record:
  assumes ac: "ccorres r' xf'' P P' [] a (Call f)"
  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' (xfru (\<lambda>_. rv') oldv))"
  and      ggl: "\<And>f s. globals (xfu' f s) = globals s"
  and    xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v"
  and  xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v"
  and      igl: "\<And>s. globals (i s) = globals s"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>"
  and  valid': "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> R' call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv)))
       {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>rv. r' rv ((xfr \<circ> xf') s) \<longrightarrow> s \<in> Q' rv ((xfr \<circ> xf') s))}"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> R') hs (a >>= (\<lambda>rv. b rv)) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
                (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) ;; d)" using ac ggl xfxfu xfrxfru igl ceqv apply (rule  ccorres_split_nothrow_record [OF ccorres_call_record]) apply (erule bd) apply (rule valid) apply (rule valid') 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> R') hs (a >>= b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv)));;
d) proof (prove)
using this:
ccorres r' xf'' P P' [] a (Call f)
globals (xfu' ?f1 ?s1) = globals ?s1
xf' (xfu' (\<lambda>_. ?v1) ?s1) = ?v1
xfr (xfru (\<lambda>_. ?v1) ?s1) = ?v1
globals (i ?s1) = globals ?s1
ceqv \<Gamma> xf' ?rv'1 ?t1 ?t'1 d (d' ?rv'1)

goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> R') hs (a >>= b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv)));;
d) proof (prove)
goal (3 subgoals):
 1. \<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' (?xfru (\<lambda>_. rv') ?oldv))
 2. \<lbrace>R\<rbrace> a \<lbrace>?Q\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F\<^esub> R' call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = ?xfru (\<lambda>_. (xfr \<circ> xf') s) ?oldv \<and> (\<forall>rv. r' rv ((xfr \<circ> xf') s) \<longrightarrow> s \<in> ?Q' rv ((xfr \<circ> xf') s))} proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F\<^esub> R' call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>rv. r' rv ((xfr \<circ> xf') s) \<longrightarrow> s \<in> Q' rv ((xfr \<circ> xf') s))} proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/?F\<^esub> R' call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>rv. r' rv ((xfr \<circ> xf') s) \<longrightarrow> s \<in> Q' rv ((xfr \<circ> xf') s))} proof (prove)
goal:
No subgoals!