kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma revokable_n':
  "\<lbrakk> n' p = Some (CTE cap node) \<rbrakk> \<Longrightarrow>
   \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable node = mdbRevocable node'" by (fastforce simp add: n'_def elim!: modify_map_casesE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable node = mdbRevocable node'
theory CSpace1_R

lemma cteMDBNode_update_split_asm:
  "P (cteMDBNode_update f cte) = (\<not> (\<exists>cap mdb. cte = CTE cap mdb \<and> \<not> P (CTE cap (f mdb))))" by (cases cte, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (cteMDBNode_update f cte) = (\<nexists>cap mdb. cte = CTE cap mdb \<and> \<not> P (CTE cap (f mdb)))
theory CSpace1_R

lemma dest2_cap [simp]:
  "cteCap dest2 = scap" using dest2 by (cases dest2) (simp add: n'_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteCap dest2 = scap proof (prove)
using this:
n' dest = Some dest2

goal (1 subgoal):
 1. cteCap dest2 = scap
theory CSpace1_R

lemma dest2_next:
  "mdbNext (cteMDBNode dest2) =
  (if dest = mdbPrev src_node then dest else mdbNext dest_node)" using dest2 dest by (cases dest2) (clarsimp dest!: n'_next)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext (cteMDBNode dest2) = (if dest = mdbPrev src_node then dest else mdbNext dest_node) proof (prove)
using this:
n' dest = Some dest2
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbNext (cteMDBNode dest2) = (if dest = mdbPrev src_node then dest else mdbNext dest_node)
theory CSpace1_R

lemma dest2_prev:
  "mdbPrev (cteMDBNode dest2) =
  (if dest = mdbNext src_node then dest else mdbPrev dest_node)" using dest2 dest by (cases dest2) (clarsimp dest!: n'_prev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode dest2) = (if dest = mdbNext src_node then dest else mdbPrev dest_node) proof (prove)
using this:
n' dest = Some dest2
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev (cteMDBNode dest2) = (if dest = mdbNext src_node then dest else mdbPrev dest_node)
theory CSpace1_R

lemma dest2_rev [simp]:
  "mdbRevocable (cteMDBNode dest2) = mdbRevocable dest_node" using dest2 dest by (cases dest2) (clarsimp dest!: revokable_n')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbRevocable (cteMDBNode dest2) = mdbRevocable dest_node proof (prove)
using this:
n' dest = Some dest2
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbRevocable (cteMDBNode dest2) = mdbRevocable dest_node
theory CSpace1_R

lemma dest2_bdg [simp]:
  "mdbFirstBadged (cteMDBNode dest2) = mdbFirstBadged dest_node" using dest2 dest by (cases dest2) (clarsimp dest!: badge_n')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbFirstBadged (cteMDBNode dest2) = mdbFirstBadged dest_node proof (prove)
using this:
n' dest = Some dest2
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbFirstBadged (cteMDBNode dest2) = mdbFirstBadged dest_node
theory CSpace1_R

lemma dest2_parts [simp]:
  "dest2 = CTE scap dest2_node" unfolding dest2_node_def apply (subst dest2_prev [symmetric]) apply (subst dest2_next [symmetric]) apply (subst dest2_rev [symmetric]) apply (subst dest2_bdg [symmetric]) apply (subst dest2_cap [symmetric]) apply (cases dest2) apply (rename_tac mdbnode) apply (case_tac mdbnode) apply (simp del: dest2_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dest2 = CTE scap dest2_node proof (prove)
goal (1 subgoal):
 1. dest2 = CTE scap (MDB (if dest = mdbPrev src_node then dest else mdbNext dest_node) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)) proof (prove)
goal (1 subgoal):
 1. dest2 = CTE scap (MDB (if dest = mdbPrev src_node then dest else mdbNext dest_node) (mdbPrev (cteMDBNode dest2)) (mdbRevocable dest_node) (mdbFirstBadged dest_node)) proof (prove)
goal (1 subgoal):
 1. dest2 = CTE scap (MDB (mdbNext (cteMDBNode dest2)) (mdbPrev (cteMDBNode dest2)) (mdbRevocable dest_node) (mdbFirstBadged dest_node)) proof (prove)
goal (1 subgoal):
 1. dest2 = CTE scap (MDB (mdbNext (cteMDBNode dest2)) (mdbPrev (cteMDBNode dest2)) (mdbRevocable (cteMDBNode dest2)) (mdbFirstBadged dest_node)) proof (prove)
goal (1 subgoal):
 1. dest2 = CTE scap (MDB (mdbNext (cteMDBNode dest2)) (mdbPrev (cteMDBNode dest2)) (mdbRevocable (cteMDBNode dest2)) (mdbFirstBadged (cteMDBNode dest2))) proof (prove)
goal (1 subgoal):
 1. dest2 = CTE (cteCap dest2) (MDB (mdbNext (cteMDBNode dest2)) (mdbPrev (cteMDBNode dest2)) (mdbRevocable (cteMDBNode dest2)) (mdbFirstBadged (cteMDBNode dest2))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. dest2 = CTE x1 x2 \<Longrightarrow> dest2 = CTE (cteCap dest2) (MDB (mdbNext (cteMDBNode dest2)) (mdbPrev (cteMDBNode dest2)) (mdbRevocable (cteMDBNode dest2)) (mdbFirstBadged (cteMDBNode dest2))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 mdbnode. dest2 = CTE x1 mdbnode \<Longrightarrow> dest2 = CTE (cteCap dest2) (MDB (mdbNext (cteMDBNode dest2)) (mdbPrev (cteMDBNode dest2)) (mdbRevocable (cteMDBNode dest2)) (mdbFirstBadged (cteMDBNode dest2))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 mdbnode x1a x2 x3 x4. \<lbrakk>dest2 = CTE x1 mdbnode; mdbnode = MDB x1a x2 x3 x4\<rbrakk> \<Longrightarrow> dest2 = CTE (cteCap dest2) (MDB (mdbNext (cteMDBNode dest2)) (mdbPrev (cteMDBNode dest2)) (mdbRevocable (cteMDBNode dest2)) (mdbFirstBadged (cteMDBNode dest2))) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma prev_dest_src [simp]:
  "(mdbPrev dest_node = mdbPrev src_node) = (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0)" apply (subst mdb_ptr.p_prev_eq) apply (rule mdb_ptr_axioms) apply rule apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbPrev dest_node = mdbPrev src_node) = (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0) proof (prove)
goal (3 subgoals):
 1. mdb_ptr ?m ?p ?cap dest_node
 2. ?m ?p' = Some (CTE ?cap' src_node)
 3. (?p = ?p' \<or> mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0) = (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0) proof (prove)
goal (2 subgoals):
 1. m ?p' = Some (CTE ?cap' src_node)
 2. (dest = ?p' \<or> mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0) = (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0) proof (prove)
goal (1 subgoal):
 1. (dest = src \<or> mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0) = (mdbPrev dest_node = 0 \<and> mdbPrev src_node = 0) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma next_dest_src [simp]:
  "(mdbNext dest_node = mdbNext src_node) = (mdbNext dest_node = 0 \<and> mdbNext src_node = 0)" apply (subst mdb_ptr.p_next_eq) apply (rule mdb_ptr_axioms) apply rule apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext dest_node = mdbNext src_node) = (mdbNext dest_node = 0 \<and> mdbNext src_node = 0) proof (prove)
goal (3 subgoals):
 1. mdb_ptr ?m ?p ?cap dest_node
 2. ?m ?p' = Some (CTE ?cap' src_node)
 3. (?p = ?p' \<or> mdbNext dest_node = 0 \<and> mdbNext src_node = 0) = (mdbNext dest_node = 0 \<and> mdbNext src_node = 0) proof (prove)
goal (2 subgoals):
 1. m ?p' = Some (CTE ?cap' src_node)
 2. (dest = ?p' \<or> mdbNext dest_node = 0 \<and> mdbNext src_node = 0) = (mdbNext dest_node = 0 \<and> mdbNext src_node = 0) proof (prove)
goal (1 subgoal):
 1. (dest = src \<or> mdbNext dest_node = 0 \<and> mdbNext src_node = 0) = (mdbNext dest_node = 0 \<and> mdbNext src_node = 0) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma n_exists:
  "m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node')" apply (simp add: n_def n'_def) apply (intro modify_map_exists) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const dest2_node))) dest (cteMDBNode_update (const src_node))) (mdbPrev dest2_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext dest2_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap' node') proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma m_exists:
  "n p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node')" apply (simp add: n_def n'_def) apply (drule modify_map_exists_rev, clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const dest2_node))) dest (cteMDBNode_update (const src_node))) (mdbPrev dest2_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext dest2_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma next_src_node [simp]:
  "(m (mdbNext src_node) = Some (CTE cap src_node)) = False" apply clarsimp apply (subgoal_tac "m \<turnstile> mdbNext src_node \<leadsto> mdbNext src_node") apply simp apply (simp add: mdb_next_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m (mdbNext src_node) = Some (CTE cap src_node)) = False proof (prove)
goal (1 subgoal):
 1. m (mdbNext src_node) = Some (CTE cap src_node) \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbNext src_node) = Some (CTE cap src_node); m \<turnstile> mdbNext src_node \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> False
 2. m (mdbNext src_node) = Some (CTE cap src_node) \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto> mdbNext src_node proof (prove)
goal (1 subgoal):
 1. m (mdbNext src_node) = Some (CTE cap src_node) \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto> mdbNext src_node proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma mdbNext_update_self [simp]:
  "(mdbNext_update (\<lambda>_. x) node = node) = (mdbNext node = x)" by (cases node) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext_update (\<lambda>_. x) node = node) = (mdbNext node = x)
theory CSpace1_R

lemma parency:
  "n \<turnstile> p \<rightarrow> p' = m \<turnstile> s_d_swp p \<rightarrow> s_d_swp p'" apply (rule iffI) apply (erule parency_n_m) apply (drule parency_m_n) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<rightarrow> p' = m \<turnstile> s_d_swp p \<rightarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. n \<turnstile> p \<rightarrow> p' \<Longrightarrow> m \<turnstile> s_d_swp p \<rightarrow> s_d_swp p'
 2. m \<turnstile> s_d_swp p \<rightarrow> s_d_swp p' \<Longrightarrow> n \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. m \<turnstile> s_d_swp p \<rightarrow> s_d_swp p' \<Longrightarrow> n \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. n \<turnstile> s_d_swp (s_d_swp p) \<rightarrow> s_d_swp (s_d_swp p') \<Longrightarrow> n \<turnstile> p \<rightarrow> p' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma next_slot_eq:
  "\<lbrakk>next_slot p t' m' = x; t' = t; m' = m\<rbrakk> \<Longrightarrow> next_slot p t m = x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_slot p t' m' = x; t' = t; m' = m\<rbrakk> \<Longrightarrow> next_slot p t m = x
theory CSpace1_R

lemma inj_on_image_set_diff15 : (* for compatibility of assumptions *)
  "\<lbrakk>inj_on f C; A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> f ` (A - B) = f ` A - f ` B" by (rule inj_on_image_set_diff; auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f C; A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> f ` (A - B) = f ` A - f ` B
theory CSpace1_R

lemma subtree_no_parent:
  assumes "m \<turnstile> p \<rightarrow> x"
  assumes "mdbNext (cteMDBNode cte) \<noteq> 0"
  assumes "\<not> isMDBParentOf cte next"
  assumes "m p = Some cte"
  assumes "m (mdbNext (cteMDBNode cte)) = Some next"
  shows "False" using assms by induct (auto simp: parentOf_def mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> p \<rightarrow> x
mdbNext (cteMDBNode cte) \<noteq> 0
\<not> isMDBParentOf cte next
m p = Some cte
m (mdbNext (cteMDBNode cte)) = Some next

goal (1 subgoal):
 1. False
theory CSpace_R

lemma setCTE_pred_tcb_at':
  "\<lbrace>pred_tcb_at' proj P t\<rbrace>
     setCTE c cte
   \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>" unfolding pred_tcb_at'_def setCTE_def apply (rule setObject_cte_obj_at_tcb') apply (simp add: tcb_to_itcb'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> setCTE c cte \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setObject c cte \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tcb f. P (proj (tcb_to_itcb' (tcbCTable_update f tcb))) = P (proj (tcb_to_itcb' tcb))
 2. \<And>tcb f. P (proj (tcb_to_itcb' (tcbVTable_update f tcb))) = P (proj (tcb_to_itcb' tcb))
 3. \<And>tcb f. P (proj (tcb_to_itcb' (tcbReply_update f tcb))) = P (proj (tcb_to_itcb' tcb))
 4. \<And>tcb f. P (proj (tcb_to_itcb' (tcbCaller_update f tcb))) = P (proj (tcb_to_itcb' tcb))
 5. \<And>tcb f. P (proj (tcb_to_itcb' (tcbIPCBufferFrame_update f tcb))) = P (proj (tcb_to_itcb' tcb)) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma [intro?]:
  shows src_0: "src \<noteq> 0"
  and  dest_0: "dest \<noteq> 0" using no_0 src dest by (auto simp: no_0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. src \<noteq> 0 &&& dest \<noteq> 0 proof (prove)
using this:
no_0 m
m src = Some (CTE src_cap src_node)
m dest = Some (CTE capability.NullCap old_dest_node)

goal (1 subgoal):
 1. src \<noteq> 0 &&& dest \<noteq> 0
theory CSpace_R

lemma src_neq_next:
  "src \<noteq> mdbNext src_node" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. src \<noteq> mdbNext src_node
theory CSpace_R

lemma src_neq_prev:
  "src \<noteq> mdbPrev src_node" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. src \<noteq> mdbPrev src_node
theory CSpace_R

lemma n:
  "n = modify_map (m(dest \<mapsto> CTE cap' src_node,
                     src \<mapsto> CTE capability.NullCap nullMDBNode))
                  (mdbPrev src_node)
                  (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))" using neq src dest no_0 by (simp add: n_def modify_map_apply)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) proof (prove)
using this:
src \<noteq> dest
m src = Some (CTE src_cap src_node)
m dest = Some (CTE capability.NullCap old_dest_node)
no_0 m

goal (1 subgoal):
 1. n = modify_map (m(dest \<mapsto> CTE cap' src_node, src \<mapsto> CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))
theory CSpace_R

lemma dest_no_parent [iff]:
  "m \<turnstile> dest \<rightarrow> x = False" using dest nxt by (auto dest: subtree_next_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<rightarrow> x = False proof (prove)
using this:
m dest = Some (CTE capability.NullCap old_dest_node)
mdbNext old_dest_node = 0

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

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

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

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

lemma src_no_parent [iff]:
  "n \<turnstile> src \<rightarrow> x = False" apply clarsimp apply (erule subtree_next_0) apply (auto simp add: n modify_map_def nullPointer_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src \<rightarrow> x = False proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src \<rightarrow> x \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. n src = Some ?cte1
 2. mdbNext (cteMDBNode ?cte1) = 0 proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma no_0_n: "no_0 n" by (simp add: n_def no_0)

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

lemma prev_neq_dest [simp]:
  "mdbPrev src_node \<noteq> dest" using dlist src dest nxt dest_0 no_0 by (fastforce simp add: valid_dlist_def no_0_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev src_node \<noteq> dest proof (prove)
using this:
valid_dlist m
m src = Some (CTE src_cap src_node)
m dest = Some (CTE capability.NullCap old_dest_node)
mdbNext old_dest_node = 0
dest \<noteq> 0
no_0 m

goal (1 subgoal):
 1. mdbPrev src_node \<noteq> dest
theory CSpace_R

lemma src_no_child [iff]:
  "n \<turnstile> x \<rightarrow> src = False" proof - from src_neq_next have "m' src = Some (CTE capability.NullCap nullMDBNode)" by (simp add: m'_def n modify_map_def) hence "m' \<turnstile> x \<rightarrow> src = False" using dlist' no_0' by (auto elim!: subtree_prev_0 simp: nullPointer_def) thus ?thesis by (simp add: m'_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> x \<rightarrow> src = False proof (state)
goal (1 subgoal):
 1. n \<turnstile> x \<rightarrow> src = False proof (chain)
picking this:
src \<noteq> mdbNext src_node proof (prove)
using this:
src \<noteq> mdbNext src_node

goal (1 subgoal):
 1. m' src = Some (CTE capability.NullCap nullMDBNode) proof (state)
this:
m' src = Some (CTE capability.NullCap nullMDBNode)

goal (1 subgoal):
 1. n \<turnstile> x \<rightarrow> src = False proof (prove)
using this:
m' src = Some (CTE capability.NullCap nullMDBNode)

goal (1 subgoal):
 1. m' \<turnstile> x \<rightarrow> src = False proof (prove)
using this:
m' src = Some (CTE capability.NullCap nullMDBNode)
valid_dlist m'
no_0 m'

goal (1 subgoal):
 1. m' \<turnstile> x \<rightarrow> src = False proof (state)
this:
m' \<turnstile> x \<rightarrow> src = False

goal (1 subgoal):
 1. n \<turnstile> x \<rightarrow> src = False proof (prove)
using this:
m' \<turnstile> x \<rightarrow> src = False

goal (1 subgoal):
 1. n \<turnstile> x \<rightarrow> src = False proof (state)
this:
n \<turnstile> x \<rightarrow> src = False

goal:
No subgoals!
theory CSpace_R

lemma dest_not_parent [iff]:
  "m \<turnstile> dest parentOf c = False" using dest by (simp add: parentOf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest parentOf c = False proof (prove)
using this:
m dest = Some (CTE capability.NullCap old_dest_node)

goal (1 subgoal):
 1. m \<turnstile> dest parentOf c = False
theory CSpace_R

lemma dest_source [iff]:
  "(m \<turnstile> dest \<leadsto> x) = (x = 0)" using dest nxt by (simp add: next_unfold')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto> x = (x = 0) proof (prove)
using this:
m dest = Some (CTE capability.NullCap old_dest_node)
mdbNext old_dest_node = 0

goal (1 subgoal):
 1. m \<turnstile> dest \<leadsto> x = (x = 0)
theory CSpace_R

lemma dest_no_target [iff]:
  "m \<turnstile> p \<leadsto> dest = False" using dlist no_0 prev dest by (fastforce simp: valid_dlist_def Let_def no_0_def next_unfold')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> dest = False proof (prove)
using this:
valid_dlist m
no_0 m
mdbPrev old_dest_node = 0
m dest = Some (CTE capability.NullCap old_dest_node)

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> dest = False
theory CSpace_R

lemma parent_preserved:
  "isMDBParentOf cte' (CTE cap' src_node) =
   isMDBParentOf cte' (CTE src_cap src_node)" using parency unfolding weak_derived'_def apply (cases cte') apply (simp add: isMDBParentOf_CTE sameRegionAs_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf cte' (CTE cap' src_node) = isMDBParentOf cte' (CTE src_cap src_node) proof (prove)
using this:
weak_derived' src_cap cap'

goal (1 subgoal):
 1. isMDBParentOf cte' (CTE cap' src_node) = isMDBParentOf cte' (CTE src_cap src_node) proof (prove)
using this:
capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap')

goal (1 subgoal):
 1. isMDBParentOf cte' (CTE cap' src_node) = isMDBParentOf cte' (CTE src_cap src_node) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap'); cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte' (CTE cap' src_node) = isMDBParentOf cte' (CTE src_cap src_node) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma children_preserved:
  "isMDBParentOf (CTE cap' src_node) cte' =
   isMDBParentOf (CTE src_cap src_node) cte'" using parency unfolding weak_derived'_def apply (cases cte') apply (simp add: isMDBParentOf_CTE sameRegionAs_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (CTE cap' src_node) cte' = isMDBParentOf (CTE src_cap src_node) cte' proof (prove)
using this:
weak_derived' src_cap cap'

goal (1 subgoal):
 1. isMDBParentOf (CTE cap' src_node) cte' = isMDBParentOf (CTE src_cap src_node) cte' proof (prove)
using this:
capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap')

goal (1 subgoal):
 1. isMDBParentOf (CTE cap' src_node) cte' = isMDBParentOf (CTE src_cap src_node) cte' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap'); cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap' src_node) cte' = isMDBParentOf (CTE src_cap src_node) cte' proof (prove)
goal:
No subgoals!