theory Ctac

lemma ccorres_lift_rhs_Spec_stateful:
  assumes cc: "\<And>v. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' v) hs a (d' v)"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  assumes gg: "\<And>v s. globals (upd (\<lambda>_. v) s) = globals s"
  assumes upd_acc: "\<And>s. upd (\<lambda>_. accessor s) s = s"
  shows   "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. \<forall>v. upd (\<lambda>_. v) s \<in> G' (xf' (upd (\<lambda>_. v) s))}  hs a (Spec {(s,t). \<exists>v. t = upd (\<lambda>_. v) s};; 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 _ ceqv]) show "ccorres dc xf' \<top> UNIV hs (return ()) ?c" apply (rule ccorres_noop) apply (vcg spec=modifies) apply clarsimp apply (drule arg_cong[where f=globals]) apply (simp add: gg) apply (rule_tac x=s in exI) apply (rule_tac x="accessor s" in exI) apply (rule upd_acc [symmetric]) done next fix rv' show "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' rv') hs a (d' rv')" by (rule cc) 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)}" apply (rule conseqPre) apply vcg apply clarsimp apply (rule conjI) apply clarsimp apply (rule_tac x=x in exI) apply (rule_tac x="accessor x" in exI) apply (rule upd_acc [symmetric]) 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. upd (\<lambda>_. v) s \<in> G' (xf' (upd (\<lambda>_. v) s))} hs a (Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s};;
d) proof (state)
goal (6 subgoals):
 1. ccorres ?r'1 xf' ?P1 ?P'1 hs (return ()) (Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s})
 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' rv')
 3. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s} {s. \<forall>uu_. ?r'1 uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 5. \<And>s. G s \<Longrightarrow> (?P1 and ?R1) s
 6. \<And>s. s \<in> {s. \<forall>v. upd (\<lambda>_. v) s \<in> G' (xf' (upd (\<lambda>_. v) s))} \<Longrightarrow> s \<in> ?P'1 \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. ccorres dc xf' (\<lambda>_. True) UNIV hs (return ()) (Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s}) proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s} {t. t may_not_modify_globals s} proof (prove)
goal (2 subgoals):
 1. \<And>s t_hrs phantom_machine_state ghost'state avail_reg ksNumCPUs ndks_boot active_irq rootserver ksCurDomain ksCurThread ksDomainTime ksIdleThread tlbLockCount armKSNextASID current_fault ksReadyQueues armKSASIDTable rootserver_mem armKSHWASIDTable intStateIRQTable ksDomScheduleIdx ksSchedulerAction current_extra_caps isFPUEnabledCached current_lookup_fault ksWorkUnitsCompleted current_syscall_error ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap more morea. \<exists>v. \<lparr>globals = \<lparr>t_hrs_' = t_hrs, phantom_machine_state_' = phantom_machine_state, ghost'state_' = ghost'state, avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap, \<dots> = more\<rparr>, \<dots> = morea\<rparr> = upd (\<lambda>_. v) s \<Longrightarrow> \<lparr>t_hrs_' = t_hrs, phantom_machine_state_' = phantom_machine_state, ghost'state_' = ghost'state, avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap, \<dots> = more\<rparr> = globals s
 2. \<And>s. \<exists>t v. t = upd (\<lambda>_. v) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b phantom_machine_state aa ab ba avail_reg ksNumCPUs ndks_boot active_irq rootserver ksCurDomain ksCurThread ksDomainTime ksIdleThread tlbLockCount armKSNextASID current_fault ksReadyQueues armKSASIDTable rootserver_mem armKSHWASIDTable intStateIRQTable ksDomScheduleIdx ksSchedulerAction current_extra_caps isFPUEnabledCached current_lookup_fault ksWorkUnitsCompleted current_syscall_error ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap more v. \<lparr>globals = \<lparr>t_hrs_' = (a, b), phantom_machine_state_' = phantom_machine_state, ghost'state_' = (aa, ab, ba), avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap\<rparr>, \<dots> = more\<rparr> = upd (\<lambda>_. v) s \<Longrightarrow> \<lparr>t_hrs_' = (a, b), phantom_machine_state_' = phantom_machine_state, ghost'state_' = (aa, ab, ba), avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap\<rparr> = globals s
 2. \<And>s. \<exists>t v. t = upd (\<lambda>_. v) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b phantom_machine_state aa ab ba avail_reg ksNumCPUs ndks_boot active_irq rootserver ksCurDomain ksCurThread ksDomainTime ksIdleThread tlbLockCount armKSNextASID current_fault ksReadyQueues armKSASIDTable rootserver_mem armKSHWASIDTable intStateIRQTable ksDomScheduleIdx ksSchedulerAction current_extra_caps isFPUEnabledCached current_lookup_fault ksWorkUnitsCompleted current_syscall_error ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap more v. globals \<lparr>globals = \<lparr>t_hrs_' = (a, b), phantom_machine_state_' = phantom_machine_state, ghost'state_' = (aa, ab, ba), avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap\<rparr>, \<dots> = more\<rparr> = globals (upd (\<lambda>_. v) s) \<Longrightarrow> \<lparr>t_hrs_' = (a, b), phantom_machine_state_' = phantom_machine_state, ghost'state_' = (aa, ab, ba), avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap\<rparr> = globals s
 2. \<And>s. \<exists>t v. t = upd (\<lambda>_. v) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>t v. t = upd (\<lambda>_. v) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>v. s = upd (\<lambda>_. v) s proof (prove)
goal (1 subgoal):
 1. \<And>s. s = upd (\<lambda>_. accessor s) s proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xf' (\<lambda>_. True) UNIV hs (return ()) (Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s})

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' rv')
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s} {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. \<forall>v. upd (\<lambda>_. v) s \<in> G' (xf' (upd (\<lambda>_. v) s))} \<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' rv')
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s} {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. \<forall>v. upd (\<lambda>_. v) s \<in> G' (xf' (upd (\<lambda>_. v) s))} \<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' rv')
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Spec {(s, t). \<exists>v. t = upd (\<lambda>_. v) s} {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. \<forall>v. upd (\<lambda>_. v) s \<in> G' (xf' (upd (\<lambda>_. v) s))} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' rv') hs a (d' rv') proof (state)
this:
ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' rv') hs a (d' rv')

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

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