theory CSpace_I

lemma caps_no_overlap'_no_region:
  "\<lbrakk> caps_no_overlap' m (capRange cap); valid_objs' s;
    m = ctes_of s; s \<turnstile>' cap; fresh_virt_cap_class (capClass cap) m \<rbrakk> \<Longrightarrow>
  \<forall>c n p. m p = Some (CTE c n) \<longrightarrow>
         \<not> sameRegionAs c cap \<and> \<not> sameRegionAs cap c" apply (clarsimp simp add: caps_no_overlap'_def) apply (erule allE)+ apply (erule impE, erule exI) apply (frule (1) ctes_of_valid_cap') apply (drule valid_capAligned)+ apply (case_tac "capClass cap = PhysicalClass") apply (auto dest: sameRegionAs_capRange_Int)[1] apply (drule(1) fresh_virt_cap_classD) apply (auto dest: sameRegionAs_classes) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_no_overlap' m (capRange cap); valid_objs' s; m = ctes_of s; valid_cap' cap s; fresh_virt_cap_class (capClass cap) m\<rbrakk> \<Longrightarrow> \<forall>c n p. m p = Some (CTE c n) \<longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (1 subgoal):
 1. \<And>c n p. \<lbrakk>\<forall>p c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange cap = {}; valid_objs' s; m = ctes_of s; valid_cap' cap s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n)\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (1 subgoal):
 1. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; valid_cap' cap s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n); (\<exists>na. ctes_of s (?p11 c n p) = Some (CTE (?c13 c n p) na)) \<longrightarrow> capRange (?c13 c n p) \<inter> capRange cap = {}\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (1 subgoal):
 1. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; valid_cap' cap s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n); capRange c \<inter> capRange cap = {}\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (1 subgoal):
 1. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; valid_cap' cap s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n); capRange c \<inter> capRange cap = {}; valid_cap' c s\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (1 subgoal):
 1. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n); capRange c \<inter> capRange cap = {}; capAligned cap; capAligned c\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (2 subgoals):
 1. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n); capRange c \<inter> capRange cap = {}; capAligned cap; capAligned c; capClass cap = PhysicalClass\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c
 2. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n); capRange c \<inter> capRange cap = {}; capAligned cap; capAligned c; capClass cap \<noteq> PhysicalClass\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (1 subgoal):
 1. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; fresh_virt_cap_class (capClass cap) (ctes_of s); ctes_of s p = Some (CTE c n); capRange c \<inter> capRange cap = {}; capAligned cap; capAligned c; capClass cap \<noteq> PhysicalClass\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal (1 subgoal):
 1. \<And>c n p. \<lbrakk>valid_objs' s; m = ctes_of s; fresh_virt_cap_class (capClass cap) (ctes_of s); capRange c \<inter> capRange cap = {}; capAligned cap; capAligned c; capClass cap \<noteq> PhysicalClass; capClass cap \<noteq> PhysicalClass \<longrightarrow> capClass (cteCap (CTE c n)) \<noteq> capClass cap\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c cap \<and> \<not> global.sameRegionAs cap c proof (prove)
goal:
No subgoals!