theory Corres_C

lemma ccorres_from_spec_modifies_heap:
  assumes spec: "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. P s\<rbrace> Call f {t. Q s t}"
  and      mod: "modifies_heap_spec f"
  and      xfg: "\<And>f s. xf (globals_update f s) = xf s"
  and    Pimp: "\<And>s s'. \<lbrakk> G s; s' \<in> G'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> P s'"
  and     rl: "\<And>s s' t'. \<lbrakk>G s; s' \<in> G'; (s, s') \<in> rf_sr; Q s' t'\<rbrakk>
            \<Longrightarrow> \<exists>(rv, t) \<in> fst (a s).
                  (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr
                       \<and> r rv (xf t')"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' [] a (Call f)" apply (rule ccorres_Call_call_for_vcg) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre) apply (rule HoarePartial.ProcModifyReturnNoAbr
                    [where return' = "\<lambda>s t. t\<lparr> globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t) \<rparr>\<rparr>"]) apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec]) apply (rule subset_refl) apply vcg prefer 2 apply (rule mod) apply (clarsimp simp: mex_def meq_def) apply (clarsimp simp: split_beta Pimp) apply (subst bex_cong [OF refl]) apply (rule arg_cong2 [where f = "(\<and>)"]) apply (rule_tac y = "t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>" in rf_sr_upd, simp_all) apply (drule (3) rl) apply (clarsimp simp: xfg elim!: bexI [rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' [] a (Call f) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' [] a (call id f (\<lambda>s t. t) (\<lambda>s t. Basic id)) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} call id f (\<lambda>s t. t) (\<lambda>s t. Basic id) {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'6 \<sigma>) call id f (\<lambda>s t. t) (\<lambda>s t. Basic id) {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 2. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'6 \<sigma> proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'6 \<sigma>) call id f (\<lambda>s t. t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) (\<lambda>s t. Basic id) {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 2. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 3. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 4. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'6 \<sigma> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma>. ?P'6 \<sigma> \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> ?R14 \<sigma> s t)}
 2. \<And>\<sigma>. \<forall>s t. \<Gamma>\<turnstile> (?R14 \<sigma> s t) Basic id {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 3. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 4. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 5. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'6 \<sigma> proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. \<forall>s t. \<Gamma>\<turnstile> (?R14 \<sigma> s t) Basic id {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> r rv (xf s)}
 2. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 3. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 4. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> ?R14 \<sigma> s t)} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 2. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 3. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> r rv (xf (id s))})} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 2. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 3. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> r rv (xf (id s))})} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<forall>s t. t \<in> {t. mex (\<lambda>t_hrs_'. t may_not_modify_globals globals (id s))} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 2. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> r rv (xf (id s))})} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. G \<sigma> \<and> s \<in> G' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> r rv (xf (id s))})} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t. \<lbrakk>G \<sigma>; x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (a \<sigma>). (snd xa, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> r (fst xa) (xf (t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t xa. \<lbrakk>G \<sigma>; x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t; xa \<in> fst (a \<sigma>)\<rbrakk> \<Longrightarrow> ((snd xa, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> r (fst xa) (xf (t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>))) = ?Q40 \<sigma> x t xa
 2. \<And>\<sigma> x t. \<lbrakk>G \<sigma>; x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t\<rbrakk> \<Longrightarrow> Bex (fst (a \<sigma>)) (?Q40 \<sigma> x t) proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x t xa. \<lbrakk>G \<sigma>; x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t; xa \<in> fst (a \<sigma>)\<rbrakk> \<Longrightarrow> ((snd xa, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr) = ?b41 \<sigma> x t xa
 2. \<And>\<sigma> x t xa. \<lbrakk>G \<sigma>; x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t; xa \<in> fst (a \<sigma>)\<rbrakk> \<Longrightarrow> r (fst xa) (xf (t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) = ?d41 \<sigma> x t xa
 3. \<And>\<sigma> x t. \<lbrakk>G \<sigma>; x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (a \<sigma>). ?b41 \<sigma> x t xa \<and> ?d41 \<sigma> x t xa proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t. \<lbrakk>G \<sigma>; x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (a \<sigma>). (snd xa, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> r (fst xa) (xf (t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t. \<lbrakk>x \<in> G'; (\<sigma>, x) \<in> rf_sr; Q x t; \<exists>(rv, ta)\<in>fst (a \<sigma>). (ta, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> r rv (xf t)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (a \<sigma>). (snd xa, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> r (fst xa) (xf (t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) proof (prove)
goal:
No subgoals!