kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma capBadge_ordering_relation:
  "\<lbrakk> cap_relation c c'; cap_relation d d' \<rbrakk> \<Longrightarrow>
  ((capBadge c', capBadge d') \<in> capBadge_ordering f) =
  ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)" apply (cases c) apply (auto simp add: cap_badge_def capBadge_ordering_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.NullCap\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 3. \<And>x31 x32 x33. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 4. \<And>x41 x42 x43. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 5. \<And>x51 x52 x53. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 6. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 7. \<And>x7. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 8. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 9. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
 10. \<And>x10. \<lbrakk>cap_relation c c'; cap_relation d d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> ((capBadge c', capBadge d') \<in> capBadge_ordering f) = ((cap_badge c, cap_badge d) \<in> capBadge_ordering f)
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma is_reply_master_relation:
  "cap_relation c c' \<Longrightarrow>
   is_master_reply_cap c = (isReplyCap c' \<and> capReplyMaster c')" by (cases c, auto simp add: is_cap_simps isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> is_master_reply_cap c = (isReplyCap c' \<and> capReplyMaster c')
theory CSpace1_R

lemma cap_asid_cap_relation:
  "cap_relation c c' \<Longrightarrow> capASID c' = cap_asid c" by (auto simp: capASID_def cap_asid_def split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> capASID c' = cap_asid c
theory CSpace1_R

lemma isArchCapE[elim!]:
  "\<lbrakk> isArchCap P cap; \<And>arch_cap. cap = ArchObjectCap arch_cap \<Longrightarrow> P arch_cap \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" by (cases cap, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isArchCap P cap; \<And>arch_cap. \<lbrakk>cap = capability.ArchObjectCap arch_cap; P arch_cap\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
theory CSpace1_R

lemma isZombie [simp]:
  "isZombie cap' = isZombie cap" using master by (simp add: capMasterCap_def isZombie_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isZombie cap' = isZombie cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isZombie cap' = isZombie cap
theory CSpace1_R

lemma isUntypedCap [simp]:
  "isUntypedCap cap' = isUntypedCap cap" using master by (simp add: capMasterCap_def isUntypedCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap cap' = isUntypedCap cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isUntypedCap cap' = isUntypedCap cap
theory CSpace1_R

lemma isArchPageCap [simp]:
  "isArchPageCap cap' = isArchPageCap cap" using master by (simp add: capMasterCap_def isArchPageCap_def
           split: capability.splits arch_capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isArchPageCap cap' = isArchPageCap cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isArchPageCap cap' = isArchPageCap cap
theory CSpace1_R

lemma isIRQHandlerCap [simp]:
  "isIRQHandlerCap cap' = isIRQHandlerCap cap" using master by (simp add: capMasterCap_def isIRQHandlerCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isIRQHandlerCap cap' = isIRQHandlerCap cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isIRQHandlerCap cap' = isIRQHandlerCap cap
theory CSpace1_R

lemma isEndpointCap [simp]:
  "isEndpointCap cap' = isEndpointCap cap" using master by (simp add: capMasterCap_def isEndpointCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isEndpointCap cap' = isEndpointCap cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isEndpointCap cap' = isEndpointCap cap
theory CSpace1_R

lemma isNotificationCap [simp]:
  "isNotificationCap cap' = isNotificationCap cap" using master by (simp add: capMasterCap_def isNotificationCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isNotificationCap cap' = isNotificationCap cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isNotificationCap cap' = isNotificationCap cap
theory CSpace1_R

lemma isIRQControlCap [simp]:
  "isIRQControlCap cap' = isIRQControlCap cap" using master by (simp add: capMasterCap_def isIRQControlCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isIRQControlCap cap' = isIRQControlCap cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isIRQControlCap cap' = isIRQControlCap cap
theory CSpace1_R

lemma isReplyCap [simp]:
  "isReplyCap cap' = isReplyCap cap" using master by (simp add: capMasterCap_def isReplyCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isReplyCap cap' = isReplyCap cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. isReplyCap cap' = isReplyCap cap
theory CSpace1_R

lemma capRange [simp]:
  "capRange cap' = capRange cap" using master by (simp add: capRange_def capMasterCap_def split: capability.splits arch_capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange cap' = capRange cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. capRange cap' = capRange cap
theory CSpace1_R

lemma isDomain1:
  "(cap' = DomainCap) = (cap = DomainCap)" using master by (simp add: capMasterCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap' = capability.DomainCap) = (cap = capability.DomainCap) proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. (cap' = capability.DomainCap) = (cap = capability.DomainCap)
theory CSpace1_R

lemma isDomain2:
  "(DomainCap = cap') = (DomainCap = cap)" using master by (simp add: capMasterCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (capability.DomainCap = cap') = (capability.DomainCap = cap) proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. (capability.DomainCap = cap') = (capability.DomainCap = cap)
theory CSpace1_R

lemma isNull1:
  "(cap' = NullCap) = (cap = NullCap)" using master by (simp add: capMasterCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap' = capability.NullCap) = (cap = capability.NullCap) proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. (cap' = capability.NullCap) = (cap = capability.NullCap)
theory CSpace1_R

lemma isNull2:
  "(NullCap = cap') = (NullCap = cap)" using master by (simp add: capMasterCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (capability.NullCap = cap') = (capability.NullCap = cap) proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. (capability.NullCap = cap') = (capability.NullCap = cap)
theory CSpace1_R

lemma sameRegionAs1:
  "sameRegionAs c cap' = sameRegionAs c cap" using master by (simp add: sameRegionAs_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs c cap' = global.sameRegionAs c cap proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. global.sameRegionAs c cap' = global.sameRegionAs c cap
theory CSpace1_R

lemma sameRegionAs2:
  "sameRegionAs cap' c = sameRegionAs cap c" using master by (simp add: sameRegionAs_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap' c = global.sameRegionAs cap c proof (prove)
using this:
capMasterCap cap = capMasterCap cap'

goal (1 subgoal):
 1. global.sameRegionAs cap' c = global.sameRegionAs cap c
theory CSpace1_R

lemma isMDBParentOf2:
  assumes "\<not>isReplyCap cap"
  assumes "\<not>isEndpointCap cap"
  assumes "\<not>isNotificationCap cap"
  shows "isMDBParentOf (CTE cap' m) c = isMDBParentOf (CTE cap m) c" proof - from assms have c':
    "\<not>isReplyCap cap'" "\<not>isEndpointCap cap'"
    "\<not>isNotificationCap cap'" by auto note isReplyCap [simp del] isEndpointCap [simp del] isNotificationCap [simp del] from c' assms show ?thesis apply (cases c, clarsimp) apply (simp add: isMDBParentOf_CTE) apply (auto simp: capBadge_ordering_def capBadge_def isCap_simps sameRegionAs_def3
                  split: if_split_asm)[1] done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (CTE cap' m) c = isMDBParentOf (CTE cap m) c proof (state)
goal (1 subgoal):
 1. isMDBParentOf (CTE cap' m) c = isMDBParentOf (CTE cap m) c proof (chain)
picking this:
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap proof (prove)
using this:
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap

goal (1 subgoal):
 1. \<not> isReplyCap cap' &&& \<not> isEndpointCap cap' &&& \<not> isNotificationCap cap' proof (state)
this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap'

goal (1 subgoal):
 1. isMDBParentOf (CTE cap' m) c = isMDBParentOf (CTE cap m) c proof (state)
this:
isReplyCap cap' = isReplyCap cap
isEndpointCap cap' = isEndpointCap cap
isNotificationCap cap' = isNotificationCap cap

goal (1 subgoal):
 1. isMDBParentOf (CTE cap' m) c = isMDBParentOf (CTE cap m) c proof (chain)
picking this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap'
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap proof (prove)
using this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap'
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap

goal (1 subgoal):
 1. isMDBParentOf (CTE cap' m) c = isMDBParentOf (CTE cap m) c proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE cap' m) (CTE x1 x2) = isMDBParentOf (CTE cap m) (CTE x1 x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap\<rbrakk> \<Longrightarrow> (global.sameRegionAs cap x1 \<and> mdbRevocable m \<and> (capBadge cap', capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2)) = (global.sameRegionAs cap x1 \<and> mdbRevocable m \<and> (capBadge cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2)) proof (prove)
goal:
No subgoals! proof (state)
this:
isMDBParentOf (CTE cap' m) c = isMDBParentOf (CTE cap m) c

goal:
No subgoals!
theory CSpace1_R

lemma is_ep_cap_relation:
  "cap_relation c c' \<Longrightarrow> isEndpointCap c' = is_ep_cap c" apply (simp add: isCap_simps is_cap_simps) apply (cases c, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> isEndpointCap c' = is_ep_cap c proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> (\<exists>v0 v1 v2 v3 v4 v5. c' = capability.EndpointCap v0 v1 v2 v3 v4 v5) = (\<exists>r b R. c = cap.EndpointCap r b R) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma is_ntfn_cap_relation:
  "cap_relation c c' \<Longrightarrow> isNotificationCap c' = is_ntfn_cap c" apply (simp add: isCap_simps is_cap_simps) apply (cases c, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> isNotificationCap c' = is_ntfn_cap c proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> (\<exists>v0 v1 v2 v3. c' = capability.NotificationCap v0 v1 v2 v3) = (\<exists>r b R. c = cap.NotificationCap r b R) proof (prove)
goal:
No subgoals!
theory CSpace1_R

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

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

lemma n: "n = m (dest \<mapsto> new_dest, src \<mapsto> new_src)" using src dest by (simp add: n_def modify_map_apply new_dest_def new_src_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = m(dest \<mapsto> new_dest, src \<mapsto> new_src) proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. n = m(dest \<mapsto> new_dest, src \<mapsto> new_src)
theory CSpace1_R

lemma dest_no_parent [iff]:
  "m \<turnstile> dest \<rightarrow> x = False" using dest dest_next 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 dest_cap dest_node)
mdbNext dest_node = 0

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

lemma dest_no_child [iff]:
  "m \<turnstile> x \<rightarrow> dest = False" using dest 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 dest_cap dest_node)
mdbPrev dest_node = 0

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

lemma dest_no_descendants: "descendants_of' dest m = {}" by (simp add: descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' dest m = {}
theory CSpace1_R

lemma descendants_not_dest: "dest \<in> descendants_of' p m \<Longrightarrow> False" by (simp add: descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dest \<in> descendants_of' p m \<Longrightarrow> False
theory CSpace1_R

lemma src_next: "m \<turnstile> src \<leadsto> mdbNext src_node" by (simp add: src mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> mdbNext src_node
theory CSpace1_R

lemma src_next_rtrancl_conv [simp]:
  "m \<turnstile> mdbNext src_node \<leadsto>\<^sup>* dest = m \<turnstile> src \<leadsto>\<^sup>+ dest" apply (rule iffI) apply (insert src_next) apply (erule (1) rtrancl_into_trancl2) apply (drule tranclD) apply (clarsimp simp: mdb_next_unfold) done

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

lemma dest_no_next [iff]:
  "m \<turnstile> x \<leadsto> dest = False" using dest dest_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> dest = False proof (prove)
using this:
m dest = Some (CTE dest_cap dest_node)
mdbPrev dest_node = 0
valid_dlist m

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto> dest = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; m \<turnstile> x \<leadsto> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; \<exists>z. m x = Some z \<and> dest = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; m x = Some z; dest = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; m x = Some z; dest = 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 dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; m x = Some (CTE x1 x2); dest = 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 dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; m x = Some (CTE x1 x2); dest = 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 dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; m x = Some (CTE x1 x2); dest = 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 dest_cap dest_node); mdbPrev dest_node = 0; valid_dlist m; m x = Some (CTE x1 x2); dest = 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 CSpace1_R

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

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

lemma dest_no_prev [iff]:
  "m \<turnstile> dest \<leadsto> p = (p = 0)" using dest dest_next by (simp add: mdb_next_unfold)

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

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

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

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

lemma no_loops_n: "no_loops n" using chain_n no_0_n by (rule mdb_chain_0_no_loops)

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

goal (1 subgoal):
 1. no_loops n
theory CSpace1_R

lemma n_direct_eq:
  "n \<turnstile> p \<leadsto> p' = (if p = src then p' = dest else
                 if p = dest then m \<turnstile> src \<leadsto> p'
                 else m \<turnstile> p \<leadsto> p')" using src dest dest_prev by (auto simp: mdb_next_update n new_src_def new_dest_def
                 src_next mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> p' = (if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p') proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)
mdbPrev dest_node = 0

goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> p' = (if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p')
theory CSpace1_R

lemma n_dest:
  "n dest = Some new_dest" by (simp add: n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n dest = Some new_dest