theory Ctac

lemma ccorres_lift_rhs_call_record:
  fixes xf' :: "cstate \<Rightarrow> 'a" and xfu' :: "('a \<Rightarrow> 'a) \<Rightarrow> cstate \<Rightarrow> cstate"
  and  xf'' :: "cstate \<Rightarrow> 'b"  and xfr :: "'a \<Rightarrow> 'b" and xfru :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes cc: "\<And>rv' :: 'b. ccorres_underlying rf_sr \<Gamma> r xf arrel axf
                     G (G' rv' \<inter> {s. P' rv' (i s)}) hs a (d' (xfru (\<lambda>_. rv') oldv))"
  (* WARNING: the tactic csymbr relies on the outermost variable 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"
  (* WARNING: the tactic csymbr relies on the outermost variable being of the same type as the return type of xfr *)
  and  xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v"
  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"
  and Pig: "\<And>x (s :: cstate) v'. P' x (i s) \<Longrightarrow>
                P' x (i (xfu' (\<lambda>_. xfru (\<lambda>_. x) oldv) 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv))) ;; 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_record [where xfru = "xfru"], OF ccorres_call ceqv, OF _ gg _ 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 fix a s t show "(xfr \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t" by (simp add: xfxfu xfrxfru) next show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp next show "\<Gamma>\<turnstile> ?G' ?c {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and>
    (\<forall>uu. dc uu ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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 xfrxfru 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv)));;
d) proof (state)
goal (6 subgoals):
 1. ccorres ?r'1 ?xf''4 ?P1 ?C'4 [] (return ()) (Call f)
 2. \<And>a s t. (?xfr1 \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = ?xf''4 t
 3. \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 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>_. (?xfr1 \<circ> xf') s) oldv \<and> (\<forall>uu_. ?r'1 uu_ ((?xfr1 \<circ> xf') s) \<longrightarrow> s \<in> G' ((?xfr1 \<circ> xf') s) \<inter> {sa. P' ((?xfr1 \<circ> xf') s) (i sa)})}
 5. \<And>s. G s \<Longrightarrow> (?P1 and ?R1) s
 6. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) 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 (5 subgoals):
 1. \<And>a s t. (?xfr1 \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (?xfr1 \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ ((?xfr1 \<circ> xf') s) \<longrightarrow> s \<in> G' ((?xfr1 \<circ> xf') s) \<inter> {sa. P' ((?xfr1 \<circ> xf') s) (i sa)})}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) 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 (5 subgoals):
 1. \<And>a s t. (?xfr1 \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (?xfr1 \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ ((?xfr1 \<circ> xf') s) \<longrightarrow> s \<in> G' ((?xfr1 \<circ> xf') s) \<inter> {sa. P' ((?xfr1 \<circ> xf') s) (i sa)})}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) 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 (5 subgoals):
 1. \<And>a s t. (?xfr1 \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (?xfr1 \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ ((?xfr1 \<circ> xf') s) \<longrightarrow> s \<in> G' ((?xfr1 \<circ> xf') s) \<inter> {sa. P' ((?xfr1 \<circ> xf') s) (i sa)})}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) 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. (xfr \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t proof (state)
this:
(xfr \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t

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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> xf') s) (i sa)})} proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv)) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. xf'' t) oldv)) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. v) oldv) 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. xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s) = xfru (\<lambda>_. xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) oldv \<and> (\<forall>uu. dc uu (xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s \<in> G' (xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) \<and> P' (xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) (i (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s)))})} proof (prove)
goal (1 subgoal):
 1. {s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) 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. xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s) = xfru (\<lambda>_. xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) oldv \<and> (\<forall>uu. dc uu (xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s \<in> G' (xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) \<and> P' (xfr (xf' (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s))) (i (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) s)))})} proof (prove)
goal:
No subgoals! proof (state)
this:
\<Gamma>\<turnstile> ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. xf'' t) oldv))) {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> 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>_. xfru (\<lambda>_. v) oldv) 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>_. xfru (\<lambda>_. v) oldv) s \<in> {s. s \<in> G' v}} \<inter> {s. P (i s) (i s)})