theory Fastpath_C

lemma ccorres_call_hSkip:
  assumes  cul: "ccorres_underlying rf_sr \<Gamma> r xfdc r xfdc A C' [SKIP] a (Call f)"
  and      ggl: "\<And>x y s. globals (g x y s) = globals s"
  and      igl: "\<And>s. globals (i s) = globals s"
  shows "ccorres_underlying rf_sr \<Gamma> r xfdc r xfdc
          A {s. i s \<in> C'} [SKIP] 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_hSkip') apply (erule ccorres_guard_imp) apply (clarsimp simp: ggl igl xfdc_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xfdc A {s. i s \<in> C'} [SKIP] 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 xfdc A C' [SKIP] a (Call f)

goal (1 subgoal):
 1. ccorres r xfdc A {s. i s \<in> C'} [SKIP] 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 xfdc A C' [SKIP] a (Call f)

goal (1 subgoal):
 1. ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A {s. i s \<in> C'} [SKIP] 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 xfdc A C' [SKIP] a (Call f) \<Longrightarrow> ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A {s. i s \<in> C'} [SKIP] a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y))) proof (prove)
goal (6 subgoals):
 1. ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] a (Call f) \<Longrightarrow> ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r ?xf'1 A (i ` {s. i s \<in> C'}) [SKIP] a (Call f)
 2. \<And>aa b x s t. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] 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>x s t. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] a (Call f); (x, t) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, 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 xfdc A C' [SKIP] a (Call f); r rv (?xf'1 t)\<rbrakk> \<Longrightarrow> r rv (xfdc (g aa t (s\<lparr>globals := globals t\<rparr>)))
 5. \<And>s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] a (Call f); r rv (?xf'1 t)\<rbrakk> \<Longrightarrow> r rv (xfdc (s\<lparr>globals := globals t\<rparr>))
 6. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] 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 (7 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 xfdc A C' [SKIP] 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>x s t. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] a (Call f); (x, t) \<in> {(s, s'). cstate_relation s (globals s')}\<rbrakk> \<Longrightarrow> (x, s\<lparr>globals := globals t\<rparr>) \<in> {(s, s'). cstate_relation s (globals s')}
 5. \<And>aa s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] a (Call f); r rv (xfdc t)\<rbrakk> \<Longrightarrow> r rv (xfdc (g aa t (s\<lparr>globals := globals t\<rparr>)))
 6. \<And>s t rv. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] a (Call f); r rv (xfdc t)\<rbrakk> \<Longrightarrow> r rv (xfdc (s\<lparr>globals := globals t\<rparr>))
 7. \<And>x s. \<lbrakk>ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> r xfdc A C' [SKIP] 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!