theory CNode_DR

lemma dcorres_opt_parent_set_parent_helper:
  "dcorres dc \<top> P
  (gets (opt_parent (transform_cslot_ptr src)) >>=
  case_option (return ())
  (\<lambda>parent. 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)
  (gets (opt_parent (transform_cslot_ptr src)) >>=
  case_option (return ()) (set_parent (transform_cslot_ptr child)))
  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 (intro conjI impI) apply clarsimp apply clarsimp 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 (gets (opt_parent (transform_cslot_ptr src)) >>= case_option (return ()) (\<lambda>parent. 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) (gets (opt_parent (transform_cslot_ptr src)) >>= case_option (return ()) (set_parent (transform_cslot_ptr child))) g proof (prove)
goal (1 subgoal):
 1. \<And>b. \<forall>b. (P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))) \<Longrightarrow> (cdl_cdt (transform b) (transform_cslot_ptr child) = None \<longrightarrow> opt_parent (transform_cslot_ptr src) (transform b) = None \<longrightarrow> cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> ((\<exists>a ba. cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba)) \<longrightarrow> (opt_parent (transform_cslot_ptr src) (transform b) = None \<longrightarrow> cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> ((\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<longrightarrow> cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b \<longrightarrow> (\<forall>a ba. (a, ba) \<notin> fst (g b)))) proof (prove)
goal (1 subgoal):
 1. \<And>b. (P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))) \<Longrightarrow> (cdl_cdt (transform b) (transform_cslot_ptr child) = None \<longrightarrow> opt_parent (transform_cslot_ptr src) (transform b) = None \<longrightarrow> cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> ((\<exists>a ba. cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba)) \<longrightarrow> (opt_parent (transform_cslot_ptr src) (transform b) = None \<longrightarrow> cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> ((\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<longrightarrow> cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b \<longrightarrow> (\<forall>a ba. (a, ba) \<notin> fst (g b)))) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>(P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))); cdl_cdt (transform b) (transform_cslot_ptr child) = None; opt_parent (transform_cslot_ptr src) (transform b) = None; cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b
 2. \<And>b. \<lbrakk>(P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))); \<exists>a ba. cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba); opt_parent (transform_cslot_ptr src) (transform b) = None; cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b
 3. \<And>b. \<lbrakk>(P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))); \<exists>a ba. cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba); \<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba); cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b\<rbrakk> \<Longrightarrow> \<forall>a ba. (a, ba) \<notin> fst (g b) proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>(P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))); \<exists>a ba. cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba); opt_parent (transform_cslot_ptr src) (transform b) = None; cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b
 2. \<And>b. \<lbrakk>(P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))); \<exists>a ba. cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba); \<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba); cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b\<rbrakk> \<Longrightarrow> \<forall>a ba. (a, ba) \<notin> fst (g b) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(P b \<longrightarrow> (\<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba)) \<or> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> transform t' = transform b)) \<and> (P b \<longrightarrow> (\<forall>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba) \<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> (a, ba))\<rparr>))); \<exists>a ba. cdl_cdt (transform b) (transform_cslot_ptr child) = Some (a, ba); \<exists>a ba. opt_parent (transform_cslot_ptr src) (transform b) = Some (a, ba); cdt b child = None \<and> cte_wp_at (\<lambda>_. True) child b \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b) \<and> P b\<rbrakk> \<Longrightarrow> \<forall>a ba. (a, ba) \<notin> fst (g b) proof (prove)
goal (1 subgoal):
 1. \<And>b a aa ba bb ab bc. \<lbrakk>\<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> (aa, bb))\<rparr>; transform_cdt b (transform_cslot_ptr child) = Some (a, ba); opt_parent (transform_cslot_ptr src) (transform b) = Some (aa, bb); 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; (ab, bc) \<in> fst (g b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a aa ba bb ab bc. \<lbrakk>\<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> (aa, bb))\<rparr>; transform_cdt b (transform_cslot_ptr child) = Some (a, ba); opt_parent (transform_cslot_ptr src) (transform b) = Some (aa, bb); cdt b child = None; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b); P b; (ab, bc) \<in> fst (g b); transform_cdt b (transform_cslot_ptr child) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!