theory CSpace_R

lemma usableUntypedRange_mono1:
  "is_aligned ptr sz \<Longrightarrow> idx \<le> 2 ^ sz \<Longrightarrow> idx' \<le> 2 ^ sz
    \<Longrightarrow> sz < word_bits
    \<Longrightarrow> idx \<ge> idx'
    \<Longrightarrow> usableUntypedRange (UntypedCap dev ptr sz idx)
      \<le> usableUntypedRange (UntypedCap dev' ptr sz idx')" apply clarsimp apply (rule word_plus_mono_right) apply (rule of_nat_mono_maybe_le[THEN iffD1]) apply (subst word_bits_def[symmetric]) apply (erule less_le_trans[OF _  power_increasing]) apply simp apply simp apply (subst word_bits_def[symmetric]) apply (erule le_less_trans) apply (erule less_le_trans[OF _ power_increasing]) apply simp+ apply (erule is_aligned_no_wrap') apply (rule word_of_nat_less) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; idx \<le> 2 ^ sz; idx' \<le> 2 ^ sz; sz < word_bits; idx' \<le> idx\<rbrakk> \<Longrightarrow> usableUntypedRange (capability.UntypedCap dev ptr sz idx) \<subseteq> usableUntypedRange (capability.UntypedCap dev' ptr sz idx') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat idx' \<le> ptr + word_of_nat idx proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx' \<le> word_of_nat idx
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx < 2 ^ LENGTH(32)
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' < 2 ^ LENGTH(32)
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 4. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx < 2 ^ word_bits
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' < 2 ^ LENGTH(32)
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 4. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (5 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> sz \<le> word_bits
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' < 2 ^ LENGTH(32)
 4. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 5. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' < 2 ^ LENGTH(32)
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 4. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' < 2 ^ LENGTH(32)
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' < 2 ^ word_bits
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx < 2 ^ word_bits
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> sz \<le> word_bits
 2. \<lbrakk>is_aligned ptr sz; sz < word_bits; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 3. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx' \<le> idx
 4. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < word_bits; idx' \<le> idx; idx < 2 ^ sz; ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx < unat (2 ^ sz) proof (prove)
goal:
No subgoals!