theory Invariants_H

lemma obj_range'_disjoint:
  "\<lbrakk> ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s;
     pspace_aligned' s; a \<noteq> b \<rbrakk>
   \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {}" apply (frule_tac x=a in pspace_alignedD') apply assumption apply (frule_tac x=b in pspace_alignedD') apply assumption apply (frule_tac p=a and p'=b in aligned_mask_range_cases) apply assumption apply (metis add_mask_fold distinct_obj_range'_not_subset obj_range'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b\<rbrakk> \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj)\<rbrakk> \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj)\<rbrakk> \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj)\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj')\<rbrakk> \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj')\<rbrakk> \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj')\<rbrakk> \<Longrightarrow> is_aligned b ?n'4
 2. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj'); mask_range a (objBitsKO obj) \<inter> mask_range b ?n'4 = {} \<or> mask_range a (objBitsKO obj) \<subseteq> mask_range b ?n'4 \<or> mask_range b ?n'4 \<subseteq> mask_range a (objBitsKO obj)\<rbrakk> \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj'); mask_range a (objBitsKO obj) \<inter> mask_range b (objBitsKO obj') = {} \<or> mask_range a (objBitsKO obj) \<subseteq> mask_range b (objBitsKO obj') \<or> mask_range b (objBitsKO obj') \<subseteq> mask_range a (objBitsKO obj)\<rbrakk> \<Longrightarrow> obj_range' a obj \<inter> obj_range' b obj' = {} proof (prove)
goal:
No subgoals!