theory Untyped_R

lemma pspace_no_overlap_valid_untyped':
  "\<lbrakk>  pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits;
      pspace_aligned' s \<rbrakk>
  \<Longrightarrow> valid_untyped' d ptr bits idx s" apply (clarsimp simp: valid_untyped'_def ko_wp_at'_def split del: if_split) apply (frule(1) pspace_no_overlapD') apply (simp add: obj_range'_def[symmetric] Int_commute) apply (erule disjE) apply (drule base_member_set[simplified field_simps]) apply (simp add: word_bits_def) apply blast apply (simp split: if_split_asm) apply (erule notE, erule disjoint_subset2[rotated]) apply (clarsimp simp: is_aligned_no_wrap'[OF _ word_of_nat_less]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s\<rbrakk> \<Longrightarrow> valid_untyped' d ptr bits idx s proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}; ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}; ps_clear ptr' (objBitsKO ko) s; {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 2. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; ptr \<in> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; ptr \<in> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; idx < 2 ^ bits; obj_range' ptr' ko \<inter> {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>pspace_no_overlap' ptr bits s; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; ps_clear ptr' (objBitsKO ko) s; idx < 2 ^ bits\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal:
No subgoals!