theory CSpace_R

lemma dest_no_parent_n:
  "n \<turnstile> dest \<rightarrow> p = False" using src simple safe_parent apply clarsimp apply (erule subtree.induct) prefer 2 apply simp apply (clarsimp simp: parentOf_def mdb_next_unfold n_dest new_dest_def n) apply (cases "mdbNext src_node = dest") apply (subgoal_tac "m \<turnstile> src \<leadsto> dest") apply simp apply (subst mdb_next_unfold) apply (simp add: src) apply (clarsimp simp: isMDBParentOf_CTE) apply (clarsimp simp: is_simple_cap'_def revokable'_def) apply (cases c', auto simp: isCap_simps) apply (clarsimp simp add: sameRegionAs_def2) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: safe_parent_for'_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> dest \<rightarrow> p = False proof (prove)
using this:
m src = Some (CTE src_cap src_node)
is_simple_cap' c'
safe_parent_for' m src c'

goal (1 subgoal):
 1. n \<turnstile> dest \<rightarrow> p = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; n \<turnstile> dest \<rightarrow> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'a. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; n \<turnstile> dest \<leadsto> c'a; c'a \<noteq> 0; n \<turnstile> dest parentOf c'a\<rbrakk> \<Longrightarrow> False
 2. \<And>c'a c''. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; n \<turnstile> dest \<rightarrow> c'a; False; n \<turnstile> c'a \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'a c''. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; n \<turnstile> dest \<rightarrow> c'a; False; n \<turnstile> c'a \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> dest parentOf c''\<rbrakk> \<Longrightarrow> False
 2. \<And>c'a. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; n \<turnstile> dest \<leadsto> c'a; c'a \<noteq> 0; n \<turnstile> dest parentOf c'a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c'a. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; n \<turnstile> dest \<leadsto> c'a; c'a \<noteq> 0; n \<turnstile> dest parentOf c'a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest; m \<turnstile> src \<leadsto> dest\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> dest
 3. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> dest
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> \<exists>z. m src = Some z \<and> dest = mdbNext (cteMDBNode z)
 2. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; (if mdbNext src_node = dest then Some (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) else m (mdbNext src_node)) = Some cte; isMDBParentOf (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))) cte; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); is_simple_cap' c'; safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; global.sameRegionAs c' cap'; revokable' src_cap c'; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' node'. \<lbrakk>m src = Some (CTE src_cap src_node); safe_parent_for' m src c'; mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; global.sameRegionAs c' cap'; case c' of capability.NotificationCap x xa xb xc \<Rightarrow> capNtfnBadge c' \<noteq> capNtfnBadge src_cap | capability.IRQHandlerCap x \<Rightarrow> isIRQControlCap src_cap | capability.EndpointCap x xa xb xc xd xe \<Rightarrow> capEPBadge c' \<noteq> capEPBadge src_cap | capability.ArchObjectCap x \<Rightarrow> Arch.isCapRevocable c' src_cap | capability.UntypedCap x xa xb xc \<Rightarrow> True | _ \<Rightarrow> False; (capBadge c', capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isUntypedCap c'; \<not> isReplyCap c'; \<not> isEndpointCap c'; \<not> isNotificationCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' node' x4. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); safe_parent_for' m src (capability.IRQHandlerCap x4); mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; global.sameRegionAs (capability.IRQHandlerCap x4) cap'; src_cap = capability.IRQControlCap; c' = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' node' x4. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); safe_parent_for' m src (capability.IRQHandlerCap x4); mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE cap' node'); mdbNext src_node \<noteq> dest; capability.IRQHandlerCap x4 = capMasterCap cap' \<and> \<not> isZombie (capability.IRQHandlerCap x4) \<and> \<not> isArchPageCap (capability.IRQHandlerCap x4) \<and> capMasterCap cap' \<noteq> capability.NullCap \<and> \<not> isZombie (capMasterCap cap') \<and> \<not> isUntypedCap (capMasterCap cap') \<and> \<not> isArchPageCap (capMasterCap cap') \<or> capRange (capMasterCap cap') \<noteq> {} \<and> capRange (capMasterCap cap') \<subseteq> capRange (capability.IRQHandlerCap x4) \<and> isArchPageCap (capability.IRQHandlerCap x4) \<and> isArchPageCap (capMasterCap cap') \<or> isIRQControlCap (capability.IRQHandlerCap x4) \<and> isIRQHandlerCap (capMasterCap cap'); src_cap = capability.IRQControlCap; c' = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>node' x4. \<lbrakk>m src = Some (CTE capability.IRQControlCap src_node); safe_parent_for' m src (capability.IRQHandlerCap x4); mdbNext src_node \<noteq> 0; m (mdbNext src_node) = Some (CTE (capability.IRQHandlerCap x4) node'); mdbNext src_node \<noteq> dest; src_cap = capability.IRQControlCap; c' = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!