theory Untyped_R

lemma sameRegionAs_capRange_subset:
  "\<lbrakk> sameRegionAs c c'; capClass c = PhysicalClass \<rbrakk> \<Longrightarrow> capRange c' \<subseteq> capRange c" apply (erule sameRegionAsE) apply (rule equalityD1) apply (rule master_eqI, rule capRange_Master) apply simp apply assumption+ apply (clarsimp simp: isCap_simps) done

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