theory Ctac

lemma ccorres_lift_rhs_Basic_record:
  fixes xf' :: "cstate \<Rightarrow> 'a" and xfu' :: "('a \<Rightarrow> 'a) \<Rightarrow> cstate \<Rightarrow> cstate" and xfru :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' (xfru (\<lambda>_. v) oldv))"
  and  xfxfu: "\<And>v s. xf' (xfu' (\<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"
  (* 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. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} hs a (Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) 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 _ ceqv]) show "ccorres dc ((\<lambda>_. v) \<circ> xf') \<top> UNIV hs (return ()) ?c" apply (rule ccorres_noop) apply (vcg spec=modifies) done next fix rv' show "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> {s. rv' = v}) hs a (d' (xfru (\<lambda>_. rv') oldv))" apply (rule ccorres_gen_asm2) apply (erule ssubst) apply (rule cc) done next show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp next show "\<Gamma>\<turnstile> ?G' ?c {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and>
           (\<forall>uu. dc uu (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}" apply (rule conseqPre) apply vcg apply (clarsimp simp add: xfxfu) done qed simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} hs a (Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv));;
d) proof (state)
goal (6 subgoals):
 1. ccorres ?r'1 (?xfr1 \<circ> xf') ?P1 ?P'1 hs (return ()) (Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)))
 2. \<And>uu_ rv'. ?r'1 uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' (xfru (\<lambda>_. rv') ?oldv1))
 3. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. (?xfr1 \<circ> xf') s) ?oldv1 \<and> (\<forall>uu_. ?r'1 uu_ ((?xfr1 \<circ> xf') s) \<longrightarrow> s \<in> ?Q'1 uu_ ((?xfr1 \<circ> xf') s))}
 5. \<And>s. G s \<Longrightarrow> (?P1 and ?R1) s
 6. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> ?P'1 \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. ccorres dc ((\<lambda>_. v) \<circ> xf') (\<lambda>_. True) UNIV hs (return ()) (Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv))) proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {t. t may_not_modify_globals s} proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc ((\<lambda>_. v) \<circ> xf') (\<lambda>_. True) UNIV hs (return ()) (Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)))

goal (5 subgoals):
 1. \<And>uu_ rv'. dc uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' (xfru (\<lambda>_. rv') ?oldv1))
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) ?oldv1 \<and> (\<forall>uu_. dc uu_ (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> ?Q'1 uu_ (((\<lambda>_. v) \<circ> xf') s))}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (state)
goal (5 subgoals):
 1. \<And>uu_ rv'. dc uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' (xfru (\<lambda>_. rv') ?oldv1))
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) ?oldv1 \<and> (\<forall>uu_. dc uu_ (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> ?Q'1 uu_ (((\<lambda>_. v) \<circ> xf') s))}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (state)
goal (5 subgoals):
 1. \<And>uu_ rv'. dc uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' (xfru (\<lambda>_. rv') ?oldv1))
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) ?oldv1 \<and> (\<forall>uu_. dc uu_ (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> ?Q'1 uu_ (((\<lambda>_. v) \<circ> xf') s))}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> \<lbrace>rv' = v\<rbrace>) hs a (d' (xfru (\<lambda>_. rv') oldv)) proof (prove)
goal (1 subgoal):
 1. rv' = v \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' (xfru (\<lambda>_. rv') oldv)) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' (xfru (\<lambda>_. v) oldv)) proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> \<lbrace>rv' = v\<rbrace>) hs a (d' (xfru (\<lambda>_. rv') oldv))

goal (4 subgoals):
 1. \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}
 3. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 4. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<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 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}
 3. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 4. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<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 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}
 2. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 3. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (state)
goal (3 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> (\<forall>uu_. dc uu_ (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}
 2. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 3. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)} proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> ?P' Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}
 2. {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<subseteq> ?P' proof (prove)
goal (1 subgoal):
 1. {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<subseteq> {s. xf' (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s) = xfru (\<lambda>_. v) oldv \<and> (\<forall>uu. dc uu v \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G' \<and> v = v)} proof (prove)
goal:
No subgoals! proof (state)
this:
\<Gamma>\<turnstile> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> (\<forall>uu. dc uu (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}

goal (2 subgoals):
 1. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 2. \<And>s. s \<in> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'}