theory Ctac

lemma ccorres_lift_rhs_call:
  assumes cc: "\<And>rv'. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' rv' \<inter> {s. P' rv' (i s)}) hs a (d' rv')"
  (* WARNING: the tactic csymbr relies on the outermost variable (v) being of the same type as the return type of xf' *)
  and  xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v"
  and f_spec: "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> P \<sigma> s} Call f {t. P' (xf'' t) s}"
  and f_modifies: "modifies_spec f"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     gg: "\<And>x f s. globals (xfu' f s) = globals s"
  and     gi: "\<And>s. globals (i s) = globals s"
  (* This is annoying, as simp doesn't always solve it *)
  and    Pig: "\<And>x (s :: cstate) v'. P' x (i s)
  \<Longrightarrow> P' x (i (xfu' (\<lambda>_. x) s))"
  (* The concrete guard here is stronger than required --- we really need xf'' t not v *)
  shows   "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G
  ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}}
  \<inter> {s. P (i s) (i s)}) hs a
            (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) ;; d)"
  (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric],
    rule ccorres_guard_imp [OF ccorres_split_nothrow, OF ccorres_call ceqv, OF _ gg xfxfu gi cc]) show "ccorres dc xf'' \<top> (Collect (\<lambda>s. P s s)) [] (return ()) (Call f)" apply (rule ccorres_guard_imp2) apply (rule ccorres_noop_spec [OF f_spec f_modifies]) apply simp done next show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp next show "\<Gamma>\<turnstile> ?G' ?c {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}" apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. s", OF _ _ f_modifies]) apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ f_spec]) defer apply vcg apply (clarsimp simp add: gi mex_def meq_def xfxfu) apply (clarsimp simp add: gi mex_def meq_def xfxfu Pig) done qed simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)}) hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t)));;
d) proof (state)
goal (5 subgoals):
 1. ccorres ?r'1 xf'' ?P1 ?C'4 [] (return ()) (Call f)
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu_. ?r'1 uu_ (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 4. \<And>s. G s \<Longrightarrow> (?P1 and ?R1) s
 5. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<Longrightarrow> s \<in> {s. i s \<in> ?C'4} \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. ccorres dc xf'' (\<lambda>_. True) {s. P s s} [] (return ()) (Call f) proof (prove)
goal (2 subgoals):
 1. ccorres dc xf'' ?Q ?Q' [] (return ()) (Call f)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. P s s}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. P s s}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. s \<in> {\<sigma>. s = \<sigma> \<and> P \<sigma> s}} proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xf'' (\<lambda>_. True) {s. P s s} [] (return ()) (Call f)

goal (4 subgoals):
 1. \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 3. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 4. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<Longrightarrow> s \<in> {s. i s \<in> {s. P s s}} \<inter> ?R'1 proof (state)
goal (4 subgoals):
 1. \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 3. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 4. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<Longrightarrow> s \<in> {s. i s \<in> {s. P s s}} \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. \<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace> proof (state)
this:
\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>

goal (3 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 2. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 3. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<Longrightarrow> s \<in> {s. i s \<in> {s. P s s}} \<inter> ?R'1 proof (state)
goal (3 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 2. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 3. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<Longrightarrow> s \<in> {s. i s \<in> {s. P s s}} \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)}) call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}} proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)}) call i f (\<lambda>s t. s) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 2. \<forall>s t. t \<in> {t. t may_not_modify_globals i s} \<longrightarrow> s = s\<lparr>globals := globals t\<rparr> proof (prove)
goal (3 subgoals):
 1. {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<subseteq> {s. \<exists>Z. i s \<in> {\<sigma>. Z = \<sigma> \<and> P \<sigma> Z} \<and> (\<forall>t. t \<in> {t. P' (xf'' t) Z} \<longrightarrow> s \<in> ?R5 s t)}
 2. \<forall>s t. \<Gamma>\<turnstile> (?R5 s t) Basic (xfu' (\<lambda>_. xf'' t)) {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 3. \<forall>s t. t \<in> {t. t may_not_modify_globals i s} \<longrightarrow> s = s\<lparr>globals := globals t\<rparr> proof (prove)
goal (3 subgoals):
 1. \<forall>s t. \<Gamma>\<turnstile> (?R5 s t) Basic (xfu' (\<lambda>_. xf'' t)) {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}
 2. \<forall>s t. t \<in> {t. t may_not_modify_globals i s} \<longrightarrow> s = s\<lparr>globals := globals t\<rparr>
 3. {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<subseteq> {s. \<exists>Z. i s \<in> {\<sigma>. Z = \<sigma> \<and> P \<sigma> Z} \<and> (\<forall>t. t \<in> {t. P' (xf'' t) Z} \<longrightarrow> s \<in> ?R5 s t)} proof (prove)
goal (2 subgoals):
 1. \<forall>s t. t \<in> {t. t may_not_modify_globals i s} \<longrightarrow> s = s\<lparr>globals := globals t\<rparr>
 2. {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<subseteq> {s. \<exists>Z. i s \<in> {\<sigma>. Z = \<sigma> \<and> P \<sigma> Z} \<and> (\<forall>t. t \<in> {t. P' (xf'' t) Z} \<longrightarrow> s \<in> {s. \<forall>uu. dc uu (xf' (xfu' (\<lambda>_. xf'' t) s)) \<longrightarrow> xfu' (\<lambda>_. xf'' t) s \<in> G' (xf' (xfu' (\<lambda>_. xf'' t) s)) \<and> P' (xf' (xfu' (\<lambda>_. xf'' t) s)) (i (xfu' (\<lambda>_. xf'' t) s))})} proof (prove)
goal (1 subgoal):
 1. {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<subseteq> {s. \<exists>Z. i s \<in> {\<sigma>. Z = \<sigma> \<and> P \<sigma> Z} \<and> (\<forall>t. t \<in> {t. P' (xf'' t) Z} \<longrightarrow> s \<in> {s. \<forall>uu. dc uu (xf' (xfu' (\<lambda>_. xf'' t) s)) \<longrightarrow> xfu' (\<lambda>_. xf'' t) s \<in> G' (xf' (xfu' (\<lambda>_. xf'' t) s)) \<and> P' (xf' (xfu' (\<lambda>_. xf'' t) s)) (i (xfu' (\<lambda>_. xf'' t) s))})} proof (prove)
goal:
No subgoals! proof (state)
this:
\<Gamma>\<turnstile> ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)}) call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}

goal (2 subgoals):
 1. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 2. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)} \<Longrightarrow> s \<in> {s. i s \<in> {s. P s s}} \<inter> ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)})