theory Corres_C

lemma ccorres_call:
  assumes  cul: "ccorres_underlying rf_sr \<Gamma> r xf'' r xf'' A C' [] a (Call f)"
  and      ggl: "\<And>x y s. globals (g x y s) = globals s"
  and      xfg: "\<And>a s t. (xf' (g a t (s\<lparr>globals := globals t\<rparr>))) = xf'' t"
  and      igl: "\<And>s. globals (i s) = globals s"
  shows "ccorres_underlying rf_sr \<Gamma> r xf' arrel axf
          A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)))" using cul unfolding rf_sr_def apply - apply (rule ccorres_call) apply (erule ccorres_guard_imp) apply simp apply clarsimp apply (simp add: ggl) apply (simp add: xfg) apply (clarsimp simp: igl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf' arrel axf A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y))) proof (prove)
using this:
ccorres r xf'' A C' [] a (Call f)

goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf' arrel axf A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y))) proof (prove)
using this:
ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f)

goal (1 subgoal):
 1. ccorres_underlying {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf' arrel axf A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y))) proof (prove)
goal (1 subgoal):
 1. ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f) \<Longrightarrow> ccorres_underlying {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf' arrel axf A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y))) proof (prove)
goal (4 subgoals):
 1. ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f) \<Longrightarrow> ccorres_underlying {(s, s'). cstate_relation s (globals s')} \<Gamma> r ?xf'1 ?rrel1 ?xf'1 A (i ` {s. i s \<in> C'}) [] a (Call f)
 2. \<And>aa b x s t. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, t) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, g aa b (s\<lparr>globals := globals t\<rparr>)) \<in> {(s, s'). cstate_relation s (globals s')}
 3. \<And>aa s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); r rv (?xf'1 t)\<rbrakk> \<Longrightarrow> r rv (xf' (g aa t (s\<lparr>globals := globals t\<rparr>)))
 4. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, s) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, i s) \<in> {(s, s'). cstate_relation s (globals s')} proof (prove)
goal (5 subgoals):
 1. \<And>s. A s \<Longrightarrow> A s
 2. \<And>s. s \<in> i ` {s. i s \<in> C'} \<Longrightarrow> s \<in> C'
 3. \<And>aa b x s t. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, t) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, g aa b (s\<lparr>globals := globals t\<rparr>)) \<in> {(s, s'). cstate_relation s (globals s')}
 4. \<And>aa s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); r rv (xf'' t)\<rbrakk> \<Longrightarrow> r rv (xf' (g aa t (s\<lparr>globals := globals t\<rparr>)))
 5. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, s) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, i s) \<in> {(s, s'). cstate_relation s (globals s')} proof (prove)
goal (4 subgoals):
 1. \<And>s. s \<in> i ` {s. i s \<in> C'} \<Longrightarrow> s \<in> C'
 2. \<And>aa b x s t. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, t) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, g aa b (s\<lparr>globals := globals t\<rparr>)) \<in> {(s, s'). cstate_relation s (globals s')}
 3. \<And>aa s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); r rv (xf'' t)\<rbrakk> \<Longrightarrow> r rv (xf' (g aa t (s\<lparr>globals := globals t\<rparr>)))
 4. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, s) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, i s) \<in> {(s, s'). cstate_relation s (globals s')} proof (prove)
goal (3 subgoals):
 1. \<And>aa b x s t. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, t) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, g aa b (s\<lparr>globals := globals t\<rparr>)) \<in> {(s, s'). cstate_relation s (globals s')}
 2. \<And>aa s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); r rv (xf'' t)\<rbrakk> \<Longrightarrow> r rv (xf' (g aa t (s\<lparr>globals := globals t\<rparr>)))
 3. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, s) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, i s) \<in> {(s, s'). cstate_relation s (globals s')} proof (prove)
goal (2 subgoals):
 1. \<And>aa s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); r rv (xf'' t)\<rbrakk> \<Longrightarrow> r rv (xf' (g aa t (s\<lparr>globals := globals t\<rparr>)))
 2. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, s) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, i s) \<in> {(s, s'). cstate_relation s (globals s')} proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xf'' A C' [] a (Call f); (x, s) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, i s) \<in> {(s, s'). cstate_relation s (globals s')} proof (prove)
goal:
No subgoals!