theory CSpace_R

lemma ut_c'_new:
  assumes ut_src: "isUntypedCap src_cap"
  shows "m p = Some (CTE cap node) \<Longrightarrow> \<not> sameRegionAs c' cap" using src simple apply clarsimp apply (drule untyped_mdbD', rule ut_src, assumption) apply (clarsimp simp: is_simple_cap'_def sameRegionAs_def2 isCap_Master capRange_Master) apply (fastforce simp: isCap_simps) apply (frule sameRegion_capRange_sub) apply (drule ut_sameRegion_non_empty [OF ut_src]) apply (insert utCapRange_c') apply blast apply (rule untyped_mdb) apply (simp add: ut_descendants [OF ut_src]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
using this:
m src = Some (CTE src_cap src_node)
is_simple_cap' c'

goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); m src = Some (CTE src_cap src_node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap cap
 2. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 3. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 4. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); c' \<noteq> capability.NullCap; c' \<noteq> capability.IRQControlCap; \<not> isReplyCap c'; \<not> isThreadCap c'; \<not> isCNodeCap c'; \<not> isZombie c'; \<not> isArchPageCap c'; isUntypedCap cap; isIRQControlCap c'; isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 3. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 4. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 2. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 3. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; capRange cap \<subseteq> capRange c'\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 2. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 3. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; capRange cap \<subseteq> capRange c'; capRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 2. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 3. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; capRange cap \<subseteq> capRange c'; capRange cap \<noteq> {}; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> untypedRange src_cap \<noteq> {}
 2. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 3. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> untyped_mdb' m
 2. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); is_simple_cap' c'; global.sameRegionAs c' cap; p \<in> descendants_of' src m; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!