theory CSpace_R

lemma untyped_rangefree:
  "\<lbrakk> isUntypedCap src_cap; m x = Some cte; x \<noteq> src; \<not> isUntypedCap (cteCap cte) \<rbrakk>
          \<Longrightarrow> capRange (cteCap cte) \<noteq> capRange c'" apply (frule ut_descendants) apply (cases cte, clarsimp) apply (frule(2) untyped_mdbD' [OF src _ _ _ _ untyped_mdb]) apply (simp add: untypedCapRange[symmetric]) apply (frule ut_capRange_non_empty) apply (cut_tac capRange_c') apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; m x = Some cte; x \<noteq> src; \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> capRange (cteCap cte) \<noteq> capRange c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; m x = Some cte; x \<noteq> src; \<not> isUntypedCap (cteCap cte); descendants_of' src m = {}\<rbrakk> \<Longrightarrow> capRange (cteCap cte) \<noteq> capRange c' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'\<rbrakk> \<Longrightarrow> capRange x1 \<inter> untypedRange src_cap \<noteq> {}
 2. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'; x \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'\<rbrakk> \<Longrightarrow> capRange c' \<inter> capRange src_cap \<noteq> {}
 2. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'; x \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'; capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> capRange c' \<inter> capRange src_cap \<noteq> {}
 2. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'; x \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'; capRange c' \<noteq> {}; capRange c' \<subseteq> capRange src_cap\<rbrakk> \<Longrightarrow> capRange c' \<inter> capRange src_cap \<noteq> {}
 2. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'; x \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>isUntypedCap src_cap; m x = Some (CTE x1 x2); x \<noteq> src; \<not> isUntypedCap x1; descendants_of' src m = {}; cte = CTE x1 x2; capRange x1 = capRange c'; x \<in> descendants_of' src m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!