theory CSpace_I

lemma sameRegionAs_capRange_Int:
  "\<lbrakk> sameRegionAs cap cap'; capClass cap = PhysicalClass \<or> capClass cap' = PhysicalClass;
     capAligned cap; capAligned cap' \<rbrakk>
     \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}" apply (frule sameRegionAs_classes, simp) apply (drule(1) capAligned_capUntypedPtr)+ apply (erule sameRegionAsE) apply (subgoal_tac "capRange (capMasterCap cap') \<inter> capRange (capMasterCap cap) \<noteq> {}") apply (simp(no_asm_use) add: capRange_Master) apply (clarsimp simp: capRange_Master) apply blast apply blast apply (clarsimp simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; capClass cap = PhysicalClass \<or> capClass cap' = PhysicalClass; capAligned cap; capAligned cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; capClass cap' = PhysicalClass; capAligned cap; capAligned cap'; capClass cap = PhysicalClass\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (4 subgoals):
 1. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 2. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 3. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 4. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (5 subgoals):
 1. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap; capRange (capMasterCap cap') \<inter> capRange (capMasterCap cap) \<noteq> {}\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 2. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> capRange (capMasterCap cap') \<inter> capRange (capMasterCap cap) \<noteq> {}
 3. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 4. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 5. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (4 subgoals):
 1. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> capRange (capMasterCap cap') \<inter> capRange (capMasterCap cap) \<noteq> {}
 2. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 3. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 4. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 2. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 3. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}
 2. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> capRange cap; global.capUntypedPtr cap' \<in> capRange cap'; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {} proof (prove)
goal:
No subgoals!