theory Corres_C

lemma ccorres_callE:
  "\<lbrakk> ccorres_underlying rf_sr \<Gamma> r (liftxf es sf vf xf'')
                               r (liftxf es sf vf xf'') A C' [] a (Call f);
     \<And>x y s. globals (g x y s) = globals s;
     \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t;
     \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t;
     \<And>s. globals (i s) = globals s
  \<rbrakk>
  \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r (liftxf es sf vf 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)))" apply (erule ccorres_call) apply assumption apply (simp add: liftxf_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres r (liftxf es sf vf xf'') A C' [] a (Call f); \<And>x y s. globals (g x y s) = globals s; \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; \<And>s. globals (i s) = globals s\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r (liftxf es sf vf 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 (3 subgoals):
 1. \<And>x y s. \<lbrakk>\<And>x y s. globals (g x y s) = globals s; \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; \<And>s. globals (i s) = globals s\<rbrakk> \<Longrightarrow> globals (g x y s) = globals s
 2. \<And>a s t. \<lbrakk>\<And>x y s. globals (g x y s) = globals s; \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; \<And>s. globals (i s) = globals s\<rbrakk> \<Longrightarrow> liftxf es sf vf xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = liftxf es sf vf xf'' t
 3. \<And>s. \<lbrakk>\<And>x y s. globals (g x y s) = globals s; \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; \<And>s. globals (i s) = globals s\<rbrakk> \<Longrightarrow> globals (i s) = globals s proof (prove)
goal (2 subgoals):
 1. \<And>a s t. \<lbrakk>\<And>x y s. globals (g x y s) = globals s; \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; \<And>s. globals (i s) = globals s\<rbrakk> \<Longrightarrow> liftxf es sf vf xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = liftxf es sf vf xf'' t
 2. \<And>s. \<lbrakk>\<And>x y s. globals (g x y s) = globals s; \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; \<And>s. globals (i s) = globals s\<rbrakk> \<Longrightarrow> globals (i s) = globals s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x y s. globals (g x y s) = globals s; \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; \<And>s. globals (i s) = globals s\<rbrakk> \<Longrightarrow> globals (i s) = globals s proof (prove)
goal:
No subgoals!