kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_R

lemma cap_case_CNodeCap_True_throw:
  "(case cap of CNodeCap a b c d \<Rightarrow> returnOk ()
         |  _ \<Rightarrow> throw $ e)
          = (whenE (\<not>isCNodeCap cap) (throwError e))" by (simp split: capability.split bool.split
             add: whenE_def isCNodeCap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.CNodeCap a b c d \<Rightarrow> returnOk () | _ \<Rightarrow> throw $ e) = whenE (\<not> isCNodeCap cap) (throwError e)
theory Untyped_R

lemma empty_descendants_range_in':
  "\<lbrakk>descendants_of' slot m = {}\<rbrakk> \<Longrightarrow> descendants_range_in' S slot m " by (clarsimp simp:descendants_range_in'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' slot m = {} \<Longrightarrow> descendants_range_in' S slot m
theory Untyped_R

lemma liftE_validE_R:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,-" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>, -
theory Untyped_R

lemma getCTE_known_cap:
  "\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = cap) p\<rbrace> getCTE p \<lbrace>\<lambda>rv s. cteCap rv = cap\<rbrace>" by (rule getCTE_get)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = cap) p\<rbrace> getCTE p \<lbrace>\<lambda>rv s. cteCap rv = cap\<rbrace>
theory Untyped_R

lemma valid_mdbD3':
  "\<lbrakk> ctes_of s p = Some cte; valid_mdb' s \<rbrakk> \<Longrightarrow> p \<noteq> 0" by (clarsimp simp add: valid_mdb'_def valid_mdb_ctes_def no_0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; valid_mdb' s\<rbrakk> \<Longrightarrow> p \<noteq> 0
theory Untyped_R

lemma no_0_helper: "no_0 m \<Longrightarrow> no_0 n" by (simp add: n_def, simp add: no_0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 m \<Longrightarrow> no_0 n
theory Untyped_R

lemma no_0_n [intro!]: "no_0 n" by (auto intro: no_0_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 n
theory Untyped_R

lemma n: "n = m (site \<mapsto> new_site, parent \<mapsto> new_parent)" using parent site by (simp add: n_def modify_map_apply new_site_def new_parent_def
                fun_upd_def[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = m(site \<mapsto> new_site, parent \<mapsto> new_parent) proof (prove)
using this:
m parent = Some (CTE parent_cap parent_node)
m site = Some (CTE site_cap site_node)

goal (1 subgoal):
 1. n = m(site \<mapsto> new_site, parent \<mapsto> new_parent)
theory Untyped_R

lemma site_no_child [iff]:
  "m \<turnstile> x \<rightarrow> site = False" using site site_prev by (auto dest: subtree_prev_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<rightarrow> site = False proof (prove)
using this:
m site = Some (CTE site_cap site_node)
mdbPrev site_node = 0

goal (1 subgoal):
 1. m \<turnstile> x \<rightarrow> site = False
theory Untyped_R

lemma parent_next: "m \<turnstile> parent \<leadsto> mdbNext parent_node" by (simp add: parent mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> parent \<leadsto> mdbNext parent_node
theory Untyped_R

lemma parent_next_rtrancl_conv [simp]:
  "m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site = m \<turnstile> parent \<leadsto>\<^sup>+ site" apply (rule iffI) apply (insert parent_next) apply (fastforce dest: rtranclD) apply (drule tranclD) apply (clarsimp simp: mdb_next_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site = m \<turnstile> parent \<leadsto>\<^sup>+ site proof (prove)
goal (2 subgoals):
 1. m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ site
 2. m \<turnstile> parent \<leadsto>\<^sup>+ site \<Longrightarrow> m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site; m \<turnstile> parent \<leadsto> mdbNext parent_node\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto>\<^sup>+ site
 2. \<lbrakk>m \<turnstile> parent \<leadsto>\<^sup>+ site; m \<turnstile> parent \<leadsto> mdbNext parent_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> parent \<leadsto>\<^sup>+ site; m \<turnstile> parent \<leadsto> mdbNext parent_node\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> mdbNext parent_node; \<exists>z. m \<turnstile> parent \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* site\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext parent_node \<leadsto>\<^sup>* site proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma site_no_next [iff]:
  "m \<turnstile> x \<leadsto> site = False" using site site_prev dlist apply clarsimp apply (simp add: mdb_next_unfold) apply (elim exE conjE) apply (case_tac z) apply simp apply (rule dlistEn [where p=x], assumption) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto> site = False proof (prove)
using this:
m site = Some (CTE site_cap site_node)
mdbPrev site_node = 0
valid_dlist m

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto> site = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; m \<turnstile> x \<leadsto> site\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; \<exists>z. m x = Some z \<and> site = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; m x = Some z; site = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m site = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; m x = Some z; site = mdbNext (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m (mdbNext x2) = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; m x = Some (CTE x1 x2); site = mdbNext x2; z = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>z x1 x2. \<lbrakk>m (mdbNext x2) = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; m x = Some (CTE x1 x2); site = mdbNext x2; z = CTE x1 x2\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (CTE x1 x2)) \<noteq> 0
 2. \<And>z x1 x2 cte'. \<lbrakk>m (mdbNext x2) = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; m x = Some (CTE x1 x2); site = mdbNext x2; z = CTE x1 x2; m (mdbNext (cteMDBNode (CTE x1 x2))) = Some cte'; mdbPrev (cteMDBNode cte') = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2 cte'. \<lbrakk>m (mdbNext x2) = Some (CTE site_cap site_node); mdbPrev site_node = 0; valid_dlist m; m x = Some (CTE x1 x2); site = mdbNext x2; z = CTE x1 x2; m (mdbNext (cteMDBNode (CTE x1 x2))) = Some cte'; mdbPrev (cteMDBNode cte') = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma site_no_next_trans [iff]:
  "m \<turnstile> x \<leadsto>\<^sup>+ site = False" by (clarsimp dest!: tranclD2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ site = False
theory Untyped_R

lemma site_no_prev [iff]:
  "m \<turnstile> site \<leadsto> p = (p = 0)" using site site_next by (simp add: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> site \<leadsto> p = (p = 0) proof (prove)
using this:
m site = Some (CTE site_cap site_node)
mdbNext site_node = 0

goal (1 subgoal):
 1. m \<turnstile> site \<leadsto> p = (p = 0)
theory Untyped_R

lemma site_no_prev_trancl [iff]:
  "m \<turnstile> site \<leadsto>\<^sup>+ p = (p = 0)" apply (rule iffI) apply (drule tranclD) apply clarsimp apply simp apply (insert chain site) apply (simp add: mdb_chain_0_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> site \<leadsto>\<^sup>+ p = (p = 0) proof (prove)
goal (2 subgoals):
 1. m \<turnstile> site \<leadsto>\<^sup>+ p \<Longrightarrow> p = 0
 2. p = 0 \<Longrightarrow> m \<turnstile> site \<leadsto>\<^sup>+ p proof (prove)
goal (2 subgoals):
 1. \<exists>z. m \<turnstile> site \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* p \<Longrightarrow> p = 0
 2. p = 0 \<Longrightarrow> m \<turnstile> site \<leadsto>\<^sup>+ p proof (prove)
goal (1 subgoal):
 1. p = 0 \<Longrightarrow> m \<turnstile> site \<leadsto>\<^sup>+ p proof (prove)
goal (1 subgoal):
 1. p = 0 \<Longrightarrow> m \<turnstile> site \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = 0; mdb_chain_0 m; m site = Some (CTE site_cap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> site \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = 0; \<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; m site = Some (CTE site_cap site_node)\<rbrakk> \<Longrightarrow> m \<turnstile> site \<leadsto>\<^sup>+ 0 proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma n_direct_eq:
  "n \<turnstile> p \<leadsto> p' = (if p = parent then p' = site else
                 if p = site then m \<turnstile> parent \<leadsto> p'
                 else m \<turnstile> p \<leadsto> p')" using parent site site_prev by (auto simp: mdb_next_update n new_parent_def new_site_def
                 parent_next mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> p' = (if p = parent then p' = site else if p = site then m \<turnstile> parent \<leadsto> p' else m \<turnstile> p \<leadsto> p') proof (prove)
using this:
m parent = Some (CTE parent_cap parent_node)
m site = Some (CTE site_cap site_node)
mdbPrev site_node = 0

goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> p' = (if p = parent then p' = site else if p = site then m \<turnstile> parent \<leadsto> p' else m \<turnstile> p \<leadsto> p')
theory Untyped_R

lemma next_not_parent:
  "\<lbrakk> mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some cte \<rbrakk>
      \<Longrightarrow> \<not> isMDBParentOf new_site cte" apply (drule(1) next_wont_bite) apply (cases cte) apply (simp add: isMDBParentOf_def new_site_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some cte\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf new_site cte proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbNext parent_node) = Some cte; \<not> global.sameRegionAs c' (cteCap cte)\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf new_site cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>m (mdbNext parent_node) = Some cte; \<not> global.sameRegionAs c' (cteCap cte); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf new_site cte proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma new_child [simp]:
  "isMDBParentOf new_parent new_site" by (simp add: new_parent_def new_site_def) (rule child)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf new_parent new_site
theory Untyped_R

lemma n_site_child:
  "n \<turnstile> parent \<rightarrow> site" apply (rule subtree.direct_parent) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def parent site n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> parent \<rightarrow> site proof (prove)
goal (3 subgoals):
 1. n \<turnstile> parent \<leadsto> site
 2. site \<noteq> 0
 3. n \<turnstile> parent parentOf site proof (prove)
goal (2 subgoals):
 1. site \<noteq> 0
 2. n \<turnstile> parent parentOf site proof (prove)
goal (1 subgoal):
 1. n \<turnstile> parent parentOf site proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma n_to_site [simp]:
  "n \<turnstile> p \<leadsto> site = (p = parent)" by (simp add: n_direct_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> site = (p = parent)
theory Untyped_R

lemma descendants:
  "descendants_of' p n =
   (if parent \<in> descendants_of' p m \<or> p = parent
   then descendants_of' p m \<union> {site} else descendants_of' p m)" apply (rule set_eqI) apply (simp add: descendants_of'_def) apply (fastforce dest!: parent_n_m dest: parent_m_n simp: n_site_child split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p n = (if parent \<in> descendants_of' p m \<or> p = parent then descendants_of' p m \<union> {site} else descendants_of' p m) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of' p n) = (x \<in> (if parent \<in> descendants_of' p m \<or> p = parent then descendants_of' p m \<union> {site} else descendants_of' p m)) proof (prove)
goal (1 subgoal):
 1. \<And>x. (m \<turnstile> p \<rightarrow> parent \<longrightarrow> n \<turnstile> p \<rightarrow> x = (x = site \<or> m \<turnstile> p \<rightarrow> x)) \<and> (p = parent \<longrightarrow> n \<turnstile> parent \<rightarrow> x = (x = site \<or> m \<turnstile> parent \<rightarrow> x)) \<and> (\<not> m \<turnstile> p \<rightarrow> parent \<and> p \<noteq> parent \<longrightarrow> n \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma blarg_descendants_of':
  "descendants_of' x (modify_map m p (if P then id else cteMDBNode_update (mdbPrev_update f)))
     = descendants_of' x m" by (simp add: descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' x (modify_map m p (if P then id else cteMDBNode_update (mdbPrev_update f))) = descendants_of' x m
theory Untyped_R

lemma mdb_relation_simp:
  "\<lbrakk> (s, s') \<in> state_relation; cte_at p s \<rbrakk>
    \<Longrightarrow> descendants_of' (cte_map p) (ctes_of s') = cte_map ` descendants_of p (cdt s)" by (cases p, clarsimp simp: state_relation_def cdt_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at (\<lambda>_. True) p s\<rbrakk> \<Longrightarrow> descendants_of' (cte_map p) (ctes_of s') = cte_map ` descendants_of p (cdt s)
theory Untyped_R

lemma in_getCTE2:
  "((cte, s') \<in> fst (getCTE p s)) = (s' = s \<and> cte_wp_at' ((=) cte) p s)" apply (safe dest!: in_getCTE) apply (clarsimp simp: cte_wp_at'_def getCTE_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((cte, s') \<in> fst (getCTE p s)) = (s' = s \<and> cte_wp_at' ((=) cte) p s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' ((=) cte) p s; s' = s\<rbrakk> \<Longrightarrow> (cte, s) \<in> fst (getCTE p s) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma do_ext_op_update_cdt_list_symb_exec_l':
  "corres_underlying {(s::det_state, s'). f (kheap s) (ekheap s) s'} nf nf' dc P P' (create_cap_ext p z a) (return x)" apply (simp add: corres_underlying_def create_cap_ext_def
  update_cdt_list_def set_cdt_list_def bind_def put_def get_def gets_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). f (kheap s) (ekheap s) s'} nf nf' dc P P' (create_cap_ext p z a) (return x) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma state_relation_schact[elim!]:
  "(s,s') \<in> state_relation \<Longrightarrow> sched_act_relation (scheduler_action s) (ksSchedulerAction s')" apply (simp add: state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> sched_act_relation (scheduler_action s) (ksSchedulerAction s') proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma state_relation_queues[elim!]: "(s,s') \<in> state_relation \<Longrightarrow> ready_queues_relation (ready_queues s) (ksReadyQueues s')" apply (simp add: state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> ready_queues_relation (ready_queues s) (ksReadyQueues s') proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma set_cdt_symb_exec_l:
  "corres_underlying {(s, s'). f (kheap s) (exst s) s'} nf nf' dc P P' (set_cdt g) (return x)" by (simp add: corres_underlying_def return_def set_cdt_def in_monad Bex_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). f (kheap s) (exst s) s'} nf nf' dc P P' (set_cdt g) (return x)
theory Untyped_R

lemma setCTE_cteCaps_of[wp]:
  "\<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> cteCap cte))\<rbrace>
      setCTE p cte
   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" apply (simp add: cteCaps_of_def) apply wp apply (clarsimp elim!: rsubst[where P=P] intro!: ext) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> cteCap cte))\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((map_option cteCap \<circ> ctes_of s)(p \<mapsto> cteCap cte))\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (map_option cteCap \<circ> ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((map_option cteCap \<circ> ctes_of s)(p \<mapsto> cteCap cte)) \<Longrightarrow> P (map_option cteCap \<circ> (ctes_of s)(p \<mapsto> cte)) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_wps[wp]:
  "\<lbrace>pspace_aligned'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
  "\<lbrace>pspace_distinct'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>"
  "\<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> cap))\<rbrace>
      insertNewCap parent slot cap
   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" apply (simp_all add: insertNewCap_def) apply (wp hoare_drop_imps
            | simp add: o_def)+ apply (clarsimp elim!: rsubst[where P=P] intro!: ext) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> &&& \<lbrace>pspace_distinct'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace> &&& \<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> cap))\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>pspace_aligned'\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
 2. \<lbrace>pspace_distinct'\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 3. \<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> cap))\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((cteCaps_of s)(slot \<mapsto> cap)) \<Longrightarrow> P (\<lambda>a. if a = slot then Some cap else cteCaps_of s a) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma cte_wp_at_cteCaps_of:
  "cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s
    = (\<exists>cap. cteCaps_of s p = Some cap \<and> P cap)" apply (subst tree_cte_cteCap_eq[unfolded o_def]) apply (clarsimp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s = (\<exists>cap. cteCaps_of s p = Some cap \<and> P cap) proof (prove)
goal (1 subgoal):
 1. (case cteCaps_of s p of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (\<exists>cap. cteCaps_of s p = Some cap \<and> P cap) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma caps_contained_modify_mdb_helper[simp]:
  "(\<exists>n. modify_map m p (cteMDBNode_update f) x = Some (CTE c n))
    = (\<exists>n. m x = Some (CTE c n))" apply (cases "m p", simp_all add: modify_map_def) apply (case_tac a, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>n. modify_map m p (cteMDBNode_update f) x = Some (CTE c n)) = (\<exists>n. m x = Some (CTE c n)) proof (prove)
goal (1 subgoal):
 1. \<And>a. m p = Some a \<Longrightarrow> x = p \<longrightarrow> (\<exists>n. cteMDBNode_update f a = CTE c n) = (\<exists>n. a = CTE c n) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma mdb_chain_0_n' [simp]: "mdb_chain_0 n'" using chain_n apply (simp add: mdb_chain_0_def) apply (simp add: n'_def  trancl_prev_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 n' proof (prove)
using this:
mdb_chain_0 n

goal (1 subgoal):
 1. mdb_chain_0 n' proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom n. n \<turnstile> x \<leadsto>\<^sup>+ 0 \<Longrightarrow> \<forall>x\<in>dom n. n' \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma parency_n':
  "n' \<turnstile> p \<rightarrow> p' = (if m \<turnstile> p \<rightarrow> parent \<or> p = parent
                 then m \<turnstile> p \<rightarrow> p' \<or> p' = site
                  else m \<turnstile> p \<rightarrow> p')" using descendants [of p] unfolding descendants_of'_def by (auto simp add: set_eq_iff n'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<rightarrow> p' = (if m \<turnstile> p \<rightarrow> parent \<or> p = parent then m \<turnstile> p \<rightarrow> p' \<or> p' = site else m \<turnstile> p \<rightarrow> p') proof (prove)
using this:
descendants_of' p n = (if parent \<in> descendants_of' p m \<or> p = parent then descendants_of' p m \<union> {site} else descendants_of' p m)

goal (1 subgoal):
 1. n' \<turnstile> p \<rightarrow> p' = (if m \<turnstile> p \<rightarrow> parent \<or> p = parent then m \<turnstile> p \<rightarrow> p' \<or> p' = site else m \<turnstile> p \<rightarrow> p') proof (prove)
using this:
{c'. n \<turnstile> p \<rightarrow> c'} = (if parent \<in> {c'. m \<turnstile> p \<rightarrow> c'} \<or> p = parent then {c'. m \<turnstile> p \<rightarrow> c'} \<union> {site} else {c'. m \<turnstile> p \<rightarrow> c'})

goal (1 subgoal):
 1. n' \<turnstile> p \<rightarrow> p' = (if m \<turnstile> p \<rightarrow> parent \<or> p = parent then m \<turnstile> p \<rightarrow> p' \<or> p' = site else m \<turnstile> p \<rightarrow> p')