theory CSpace_R

lemma ut_sameRegion_non_empty:
  "\<lbrakk> isUntypedCap src_cap; sameRegionAs c' cap \<rbrakk> \<Longrightarrow> capRange cap \<noteq> {}" using simple safe_parent src apply (clarsimp simp: is_simple_cap'_def sameRegionAs_def2 isCap_Master) apply (erule disjE) apply (clarsimp simp: ut_capRange_non_empty dest!: capMaster_capRange) apply clarsimp apply (clarsimp simp: safe_parent_for'_def) apply (erule disjE, clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps capRange_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} proof (prove)
using this:
is_simple_cap' c'
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> capRange cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; capMasterCap c' = capMasterCap cap \<and> capMasterCap c' \<noteq> capability.NullCap \<and> capMasterCap cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<or> isIRQControlCap c' \<and> isIRQHandlerCap cap; safe_parent_for' m src c'; m src = Some (CTE src_cap src_node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; capRange cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap src_cap; safe_parent_for' m src c'; m src = Some (CTE src_cap src_node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; capRange cap = {}; capMasterCap c' = capMasterCap cap \<and> capMasterCap c' \<noteq> capability.NullCap \<and> capMasterCap cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>isUntypedCap src_cap; safe_parent_for' m src c'; m src = Some (CTE src_cap src_node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; capRange cap = {}; isIRQControlCap c' \<and> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; safe_parent_for' m src c'; m src = Some (CTE src_cap src_node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; capRange cap = {}; isIRQControlCap c' \<and> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; safe_parent_for' m src c'; m src = Some (CTE src_cap src_node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; capRange cap = {}; isIRQControlCap c'; isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> src_cap = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap; m src = Some (CTE src_cap src_node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; capRange cap = {}; isIRQControlCap c'; isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; m src = Some (CTE src_cap src_node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; capRange cap = {}; isIRQControlCap c'; isIRQHandlerCap cap; descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!