theory CNode_DR

lemma dcorres_get_object_special_2:
  fixes   AP_LIFT :: "tcb \<Rightarrow> etcb \<Rightarrow> det_state \<Rightarrow> cdl_tcb"
  assumes     ap_lift: "\<And>s obj etcb. \<lbrakk> get_tcb ptr s = Some obj; get_etcb ptr s = Some etcb; AP_Q s\<rbrakk>
                   \<Longrightarrow> cdl_objects (transform s) ptr = Some (Tcb (AP_LIFT obj etcb s))"
  and     c: "\<And>obj. dcorres r (R obj) (R' obj) (a (Tcb obj)) c"
  \<comment> \<open>weak\<close>
  shows   "dcorres r (\<lambda>s. (\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s))
                     (\<lambda>s. (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s) s) \<and>
                           get_tcb ptr s \<noteq> None \<and> get_etcb 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 = Tcb obj" in corres_gen_asm) apply clarsimp apply (rule_tac P = "\<lambda>s. R (obj_tcb (Tcb obj)) s \<and> cdl_objects s ptr = Some (Tcb obj)"
      and P' = "\<lambda>s. (\<forall>obj' etcb. get_tcb ptr s = Some obj'\<and> get_etcb ptr s = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> AP_Q s"
      in stronger_corres_guard_imp) apply (rule c) apply (simp add: obj_tcb_def) apply clarsimp apply (drule (2) ap_lift [symmetric]) apply (simp, simp add: obj_tcb_def) apply clarsimp apply (frule (1) ap_lift) apply (simp add: obj_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r (\<lambda>s. \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s) (\<lambda>s. (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 = Tcb obj \<Longrightarrow> dcorres r (?P8 x) ?Q' (a x) c
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 = Tcb obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj)) ?Q' (a (Tcb obj)) c
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 = Tcb obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj)) c
 2. \<And>obj s s'. \<lbrakk>R (obj_tcb (Tcb obj)) s \<and> cdl_objects s ptr = Some (Tcb obj); (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (obj_tcb (Tcb obj)) s \<and> cdl_objects s ptr = Some (Tcb obj); (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (obj_tcb ((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 = Tcb obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 5. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (4 subgoals):
 1. \<And>obj s s'. \<lbrakk>R (obj_tcb (Tcb obj)) s \<and> cdl_objects s ptr = Some (Tcb obj); (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (obj_tcb (Tcb obj)) s \<and> cdl_objects s ptr = Some (Tcb obj); (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (obj_tcb ((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 = Tcb obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 4. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (3 subgoals):
 1. \<And>obj s s'. \<lbrakk>R (obj_tcb (Tcb obj)) s \<and> cdl_objects s ptr = Some (Tcb obj); (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (obj_tcb ((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 = Tcb obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (3 subgoals):
 1. \<And>obj s' y ya. \<lbrakk>R (obj_tcb (Tcb obj)) (transform s'); cdl_objects (transform s') ptr = Some (Tcb obj); R' (AP_LIFT y ya s') s'; get_tcb ptr s' = Some y; AP_Q s'; get_etcb ptr s' = Some ya\<rbrakk> \<Longrightarrow> R' obj s'
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (obj_tcb ((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 = Tcb obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (3 subgoals):
 1. \<And>obj s' y ya. \<lbrakk>R (obj_tcb (Tcb obj)) (transform s'); cdl_objects (transform s') ptr = Some (Tcb obj); R' (AP_LIFT y ya s') s'; AP_Q s'; get_etcb ptr s' = Some ya; Some (Tcb (AP_LIFT y ya s')) = cdl_objects (transform s') ptr\<rbrakk> \<Longrightarrow> R' obj s'
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. R (obj_tcb ((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 = Tcb obj)) s) and (\<lambda>s. cdl_objects s ptr \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb 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 (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> (\<exists>y. get_tcb ptr s' = Some y) \<and> (\<exists>y. get_etcb ptr s' = Some y) \<and> AP_Q s'; transform s' = s\<rbrakk> \<Longrightarrow> R (case the (cdl_objects s ptr) of Tcb tcb \<Rightarrow> tcb) s \<and> cdl_objects s ptr = Some (the (cdl_objects s ptr)) \<and> (\<exists>obj. the (cdl_objects s ptr) = Tcb obj) \<and> (\<exists>y. cdl_objects s ptr = Some y)
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (2 subgoals):
 1. \<And>s' y ya. \<lbrakk>\<forall>obj. cdl_objects (transform s') ptr = Some (Tcb obj) \<longrightarrow> R obj (transform s'); R' (AP_LIFT y ya s') s'; get_tcb ptr s' = Some y; AP_Q s'; get_etcb ptr s' = Some ya\<rbrakk> \<Longrightarrow> R (case the (cdl_objects (transform s') ptr) of Tcb tcb \<Rightarrow> tcb) (transform s') \<and> cdl_objects (transform s') ptr = Some (the (cdl_objects (transform s') ptr)) \<and> (\<exists>obj. the (cdl_objects (transform s') ptr) = Tcb obj) \<and> (\<exists>y. cdl_objects (transform s') ptr = Some y)
 2. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal (3 subgoals):
 1. \<And>s' y ya. \<lbrakk>\<forall>obj. cdl_objects (transform s') ptr = Some (Tcb obj) \<longrightarrow> R obj (transform s'); R' (AP_LIFT y ya s') s'; get_tcb ptr s' = Some y; AP_Q s'; get_etcb ptr s' = Some ya\<rbrakk> \<Longrightarrow> AP_Q s'
 2. \<And>s' y ya. \<lbrakk>\<forall>obj. cdl_objects (transform s') ptr = Some (Tcb obj) \<longrightarrow> R obj (transform s'); R' (AP_LIFT y ya s') s'; get_tcb ptr s' = Some y; AP_Q s'; get_etcb ptr s' = Some ya; cdl_objects (transform s') ptr = Some (Tcb (AP_LIFT y ya s'))\<rbrakk> \<Longrightarrow> R (case the (cdl_objects (transform s') ptr) of Tcb tcb \<Rightarrow> tcb) (transform s') \<and> cdl_objects (transform s') ptr = Some (the (cdl_objects (transform s') ptr)) \<and> (\<exists>obj. the (cdl_objects (transform s') ptr) = Tcb obj) \<and> (\<exists>y. cdl_objects (transform s') ptr = Some y)
 3. \<And>s s'. \<lbrakk>\<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> R obj s; (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (\<forall>obj' etcb. get_tcb ptr s' = Some obj' \<and> get_etcb ptr s' = Some etcb \<longrightarrow> R' (AP_LIFT obj' etcb s') s') \<and> get_tcb ptr s' \<noteq> None \<and> get_etcb ptr s' \<noteq> None \<and> AP_Q s' proof (prove)
goal:
No subgoals!