theory Untyped_AI

lemma usable_range_disjoint:
  "usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz
   (unat ((ptr && mask sz) + of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter>
   {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}" proof - have idx_compare''[simp]:
   "unat ((ptr && mask sz) + (of_nat (length slots) * (2::machine_word) ^ obj_bits_api tp us)) < 2 ^ sz
    \<Longrightarrow> ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1
    < ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us" apply (rule word_leq_le_minus_one,simp) apply (rule neq_0_no_wrap) apply (rule machine_word_plus_mono_right_split) apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps) apply (simp add:range_cover.sz[where 'a=machine_word_len, folded word_bits_def, OF cover])+ done show ?thesis apply (clarsimp simp:mask_out_sub_mask blah) apply (drule idx_compare'') apply (simp add:not_le[symmetric]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (state)
goal (1 subgoal):
 1. usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> unat (ptr && mask ?sz6) + unat (word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ ?sz6
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ?sz6 < word_bits
 3. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> sz < word_bits
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us

goal (1 subgoal):
 1. usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz; ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; ptr \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; ptr \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1; ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}

goal:
No subgoals!