theory CNode_DR

lemma dcorres_get_object_special:
  fixes C   :: "'a \<Rightarrow> cdl_object"
  and   UN_C :: "cdl_object \<Rightarrow> 'a"
  and   AP :: "word32 \<Rightarrow> det_state \<Rightarrow> 'b option"
  and   AP_LIFT :: "'b \<Rightarrow> det_state \<Rightarrow> 'a"
  assumes unc: "\<And>obj. UN_C (C obj) = obj"
  and     ap_lift: "\<And>s obj. \<lbrakk>AP ptr s = Some obj; AP_Q s\<rbrakk>
                   \<Longrightarrow> cdl_objects (transform s) ptr = Some (C (AP_LIFT obj s))"
  and     c: "\<And>obj. dcorres r (R obj) (R' obj) (a (C obj)) c"
  \<comment> \<open>weak\<close>
  shows   "dcorres r (\<lambda>s. (\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s))
                     (\<lambda>s. (\<forall>obj'. AP ptr s = Some obj' \<longrightarrow> R' (AP_LIFT obj' s) s) \<and> AP ptr s \<noteq> None \<and> AP_Q s)
                     (KHeap_D.get_object ptr >>= a) c" apply (rule stronger_corres_guard_imp) apply (rule corres_gets_the_bind) apply (rule corres_underlying_gets_pre_lhs) apply (rule_tac  F = "\<exists>obj. x = C obj" in corres_gen_asm) apply clarsimp apply (rule_tac P = "\<lambda>s. R (UN_C (C obj)) s \<and> cdl_objects s ptr = Some (C obj)"
      and P' = "\<lambda>s. (\<forall>obj'. AP ptr s = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s))) s) \<and> AP ptr s \<noteq> None \<and> AP_Q s"
      in stronger_corres_guard_imp) apply (rule c) apply (simp add: unc) apply clarsimp apply (drule (1) ap_lift [symmetric]) apply (simp, simp add: unc) \<comment> \<open>yuck, first simp applies unc too early\<close> apply clarsimp apply (frule (1) ap_lift) apply (simp add: unc) apply fastforce apply (simp add: unc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r (\<lambda>s. \<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s) (\<lambda>s. (\<forall>obj'. AP ptr s = Some obj' \<longrightarrow> R' (AP_LIFT obj' s) s) \<and> AP ptr s \<noteq> None \<and> AP_Q s) (KHeap_D.get_object ptr >>= a) c proof (prove)
goal (3 subgoals):
 1. dcorres r ?Q ?Q' (KHeap_D.get_object ptr >>= a) c
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. dcorres r ?P4 ?Q' (gets (the \<circ> (\<lambda>s. cdl_objects s ptr)) >>= a) c
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P4 and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. \<And>x. dcorres r (?P6 x) ?Q' (a x) c
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ?P6 ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. \<And>x. \<exists>obj. x = C obj \<Longrightarrow> dcorres r (?P8 x) ?Q' (a x) c
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (?P8 ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. \<And>obj. dcorres r (?P8 (C obj)) ?Q' (a (C obj)) c
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (?P8 ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (5 subgoals):
 1. \<And>obj. dcorres r (?Q13 obj) (?Q'13 obj) (a (C obj)) c
 2. \<And>obj s s'. \<lbrakk>R (UN_C (C obj)) s \<and> cdl_objects s ptr = Some (C obj); (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q13 obj s
 3. \<And>obj s s'. \<lbrakk>R (UN_C (C obj)) s \<and> cdl_objects s ptr = Some (C obj); (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q'13 obj s'
 4. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (UN_C ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) a \<and> cdl_objects a ptr = Some ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 5. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (4 subgoals):
 1. \<And>obj s s'. \<lbrakk>R (UN_C (C obj)) s \<and> cdl_objects s ptr = Some (C obj); (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> R obj s
 2. \<And>obj s s'. \<lbrakk>R (UN_C (C obj)) s \<and> cdl_objects s ptr = Some (C obj); (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> R' obj s'
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (UN_C ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) a \<and> cdl_objects a ptr = Some ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 4. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (3 subgoals):
 1. \<And>obj s s'. \<lbrakk>R (UN_C (C obj)) s \<and> cdl_objects s ptr = Some (C obj); (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> R' obj s'
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (UN_C ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) a \<and> cdl_objects a ptr = Some ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (3 subgoals):
 1. \<And>obj s' y. \<lbrakk>R (UN_C (C obj)) (transform s'); cdl_objects (transform s') ptr = Some (C obj); R' (UN_C (C (AP_LIFT y s'))) s'; AP_Q s'; AP ptr s' = Some y\<rbrakk> \<Longrightarrow> R' obj s'
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (UN_C ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) a \<and> cdl_objects a ptr = Some ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (3 subgoals):
 1. \<And>obj s' y. \<lbrakk>R (UN_C (C obj)) (transform s'); cdl_objects (transform s') ptr = Some (C obj); R' (UN_C (C (AP_LIFT y s'))) s'; AP_Q s'; Some (C (AP_LIFT y s')) = cdl_objects (transform s') ptr\<rbrakk> \<Longrightarrow> R' obj s'
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (UN_C ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) a \<and> cdl_objects a ptr = Some ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (UN_C ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) a \<and> cdl_objects a ptr = Some ((the \<circ> (\<lambda>s. cdl_objects s ptr)) s)) and (\<lambda>sa. \<exists>obj. (the \<circ> (\<lambda>s. cdl_objects s ptr)) s = C obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (2 subgoals):
 1. \<And>s' y. \<lbrakk>\<forall>obj. cdl_objects (transform s') ptr = Some (C obj) \<longrightarrow> R obj (transform s'); R' (AP_LIFT y s') s'; AP_Q s'; AP ptr s' = Some y\<rbrakk> \<Longrightarrow> R (UN_C (the (cdl_objects (transform s') ptr))) (transform s') \<and> cdl_objects (transform s') ptr = Some (the (cdl_objects (transform s') ptr)) \<and> (\<exists>obj. the (cdl_objects (transform s') ptr) = C obj) \<and> (\<exists>y. cdl_objects (transform s') ptr = Some y)
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (2 subgoals):
 1. \<And>s' y. \<lbrakk>\<forall>obj. cdl_objects (transform s') ptr = Some (C obj) \<longrightarrow> R obj (transform s'); R' (AP_LIFT y s') s'; AP_Q s'; AP ptr s' = Some y; cdl_objects (transform s') ptr = Some (C (AP_LIFT y s'))\<rbrakk> \<Longrightarrow> R (UN_C (the (cdl_objects (transform s') ptr))) (transform s') \<and> cdl_objects (transform s') ptr = Some (the (cdl_objects (transform s') ptr)) \<and> (\<exists>obj. the (cdl_objects (transform s') ptr) = C obj) \<and> (\<exists>y. cdl_objects (transform s') ptr = Some y)
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (2 subgoals):
 1. \<And>s' y. \<lbrakk>\<forall>obj. C (AP_LIFT y s') = C obj \<longrightarrow> R obj (transform s'); R' (AP_LIFT y s') s'; AP_Q s'; AP ptr s' = Some y; cdl_objects (transform s') ptr = Some (C (AP_LIFT y s'))\<rbrakk> \<Longrightarrow> \<exists>obj. C (AP_LIFT y s') = C obj
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (C obj) \<longrightarrow> R obj s; (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (AP_LIFT obj' s') s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj'. AP ptr s' = Some obj' \<longrightarrow> R' (UN_C (C (AP_LIFT obj' s'))) s') \<and> AP ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal:
No subgoals!