theory CNode_DR

lemma dcorres_set_parent_helper:
  "dcorres dc \<top> P
  (modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr child \<mapsto> parent)\<rparr>))
  g \<Longrightarrow>
  dcorres dc \<top> (\<lambda>s. cdt s child = None \<and> cte_at child s \<and>
   mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> P s)
  (set_parent (transform_cslot_ptr child) parent)
  g" apply (clarsimp simp:gets_def set_parent_def bind_def
    return_def get_def assert_def corres_underlying_def
    fail_def
    simpler_modify_def split:option.splits) apply (drule_tac x = b in spec) apply (clarsimp simp:KHeap_DR.cdl_cdt_transform) apply (drule(2) transform_cdt_none) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) P (modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr child \<mapsto> parent)\<rparr>)) g \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. cdt s child = None \<and> cte_wp_at (\<lambda>_. True) child s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> P s) (set_parent (transform_cslot_ptr child) parent) g proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>\<forall>b. P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b\<lparr>cdl_cdt := (cdl_cdt (transform b))(transform_cslot_ptr child \<mapsto> parent)\<rparr>); cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba); cdt b child = None; cte_wp_at (\<lambda>_. True) child b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); P b; (aa, bb) \<in> fst (g b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba); cdt b child = None; cte_wp_at (\<lambda>_. True) child b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); P b; (aa, bb) \<in> fst (g b); P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b\<lparr>cdl_cdt := (cdl_cdt (transform b))(transform_cslot_ptr child \<mapsto> parent)\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>transform_cdt b (transform_cslot_ptr child) = Some (a, ba); cdt b child = None; cte_wp_at (\<lambda>_. True) child b; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); P b; (aa, bb) \<in> fst (g b); \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b\<lparr>cdl_cdt := (transform_cdt b)(transform_cslot_ptr child \<mapsto> parent)\<rparr>\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>transform_cdt b (transform_cslot_ptr child) = Some (a, ba); cdt b child = None; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); P b; (aa, bb) \<in> fst (g b); \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b\<lparr>cdl_cdt := (transform_cdt b)(transform_cslot_ptr child \<mapsto> parent)\<rparr>; transform_cdt b (transform_cslot_ptr child) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!