theory Retype_AI

lemma range_cover_subset:
  fixes ptr :: "'a :: len word"
  assumes cover:   "range_cover ptr sz sbit n"
  assumes pointer: "p<n"
  assumes not_0:   "n \<noteq> 0"
  shows  "{ptr + of_nat p * 2^sbit .. ptr + of_nat p * 2 ^ sbit + 2 ^ sbit - 1} \<subseteq> {ptr .. ptr + of_nat n * 2 ^ sbit - 1}" apply clarsimp apply (intro conjI) apply (rule word_plus_mono_right_split[OF range_cover.range_cover_compare[OF cover pointer]]) using cover apply (simp add:range_cover_def) proof - note n_less = range_cover.range_cover_n_less[OF cover] have unat_of_nat_m1: "unat (of_nat n - (1 :: 'a :: len word)) < n" using not_0 n_less by (simp add:unat_of_nat_minus_1) have decomp:"of_nat n * 2 ^ sbit = of_nat (n - 1) * 2 ^ sbit + (2 :: 'a :: len word) ^ sbit" apply (simp add:distrib_right[where b = "1::'a word",simplified,symmetric]) using not_0 n_less apply (simp add:unat_of_nat_minus_1) done show "ptr + of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + of_nat n * 2 ^ sbit - 1" using cover apply (subst decomp) apply (simp add:add.assoc[symmetric]) apply (simp add:p_assoc_help) apply (rule order_trans[OF word_plus_mono_left word_plus_mono_right]) apply (rule word_plus_mono_right) apply (rule word_mult_le_mono1[OF word_of_nat_le]) apply (insert n_less not_0 pointer) apply (simp add:unat_of_nat_minus_1) apply (rule p2_gt_0[THEN iffD2]) apply (simp add:word_bits_def range_cover_def) apply (simp only: word_bits_def[symmetric] unat_power_lower range_cover_def) apply (clarsimp simp: unat_of_nat_minus_1 ) apply (rule nat_less_power_trans2[OF range_cover.range_cover_le_n_less(2),OF cover]) apply (simp add:unat_of_nat_m1 less_imp_le) apply (simp add:range_cover_def) apply (rule word_plus_mono_right_split[where sz = sz]) using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1 :: 'a :: len word))"] apply (clarsimp simp:unat_of_nat_m1) apply (simp add:range_cover_def) apply (rule olen_add_eqv[THEN iffD2]) apply (subst add.commute[where a = "2^sbit - 1"]) apply (subst p_assoc_help[symmetric]) apply (rule is_aligned_no_overflow) apply (insert cover) apply (clarsimp simp:range_cover_def) apply (erule aligned_add_aligned[OF _  is_aligned_mult_triv2]) apply (simp add:range_cover_def)+ using is_aligned_add is_aligned_mult_triv2 is_aligned_no_overflow' by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {ptr + word_of_nat p * 2 ^ sbit..ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ sbit - 1} proof (prove)
goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr \<le> ptr + word_of_nat p * 2 ^ sbit \<and> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
goal (2 subgoals):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr \<le> ptr + word_of_nat p * 2 ^ sbit
 2. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
goal (2 subgoals):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> sz < LENGTH('a)
 2. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
using this:
range_cover ptr sz sbit n

goal (2 subgoals):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> sz < LENGTH('a)
 2. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (state)
goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (state)
this:
n < 2 ^ LENGTH('a)
n < 2 ^ (LENGTH('a) - sbit)

goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n - 1) < n proof (prove)
using this:
n \<noteq> 0
n < 2 ^ LENGTH('a)
n < 2 ^ (LENGTH('a) - sbit)

goal (1 subgoal):
 1. unat (word_of_nat n - 1) < n proof (state)
this:
unat (word_of_nat n - 1) < n

goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
goal (1 subgoal):
 1. word_of_nat n * 2 ^ sbit = word_of_nat (n - 1) * 2 ^ sbit + 2 ^ sbit proof (prove)
goal (1 subgoal):
 1. word_of_nat n * 2 ^ sbit = (word_of_nat (n - Suc 0) + 1) * 2 ^ sbit proof (prove)
using this:
n \<noteq> 0
n < 2 ^ LENGTH('a)
n < 2 ^ (LENGTH('a) - sbit)

goal (1 subgoal):
 1. word_of_nat n * 2 ^ sbit = (word_of_nat (n - Suc 0) + 1) * 2 ^ sbit proof (prove)
goal:
No subgoals! proof (state)
this:
word_of_nat n * 2 ^ sbit = word_of_nat (n - 1) * 2 ^ sbit + 2 ^ sbit

goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
using this:
range_cover ptr sz sbit n

goal (1 subgoal):
 1. ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1 proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sbit n \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + (word_of_nat (n - 1) * 2 ^ sbit + 2 ^ sbit) - 1 proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sbit n \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + 2 ^ sbit - 1 proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sbit n \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit + (2 ^ sbit - 1) \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (4 subgoals):
 1. range_cover ptr sz sbit n \<Longrightarrow> ptr + word_of_nat p * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 2. range_cover ptr sz sbit n \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 3. range_cover ptr sz sbit n \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 4. range_cover ptr sz sbit n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (5 subgoals):
 1. range_cover ptr sz sbit n \<Longrightarrow> word_of_nat p * 2 ^ sbit \<le> word_of_nat (n - Suc 0) * 2 ^ sbit
 2. range_cover ptr sz sbit n \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 3. range_cover ptr sz sbit n \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 4. range_cover ptr sz sbit n \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 5. range_cover ptr sz sbit n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (7 subgoals):
 1. range_cover ptr sz sbit n \<Longrightarrow> p \<le> unat (word_of_nat (n - Suc 0))
 2. range_cover ptr sz sbit n \<Longrightarrow> 0 < 2 ^ sbit
 3. range_cover ptr sz sbit n \<Longrightarrow> unat (word_of_nat (n - Suc 0)) * unat (2 ^ sbit) < 2 ^ LENGTH('a)
 4. range_cover ptr sz sbit n \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 5. range_cover ptr sz sbit n \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 6. range_cover ptr sz sbit n \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 7. range_cover ptr sz sbit n \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> p \<le> unat (word_of_nat (n - Suc 0))
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 0 < 2 ^ sbit
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat (n - Suc 0)) * unat (2 ^ sbit) < 2 ^ LENGTH('a)
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 6. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 7. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 0 < 2 ^ sbit
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat (n - Suc 0)) * unat (2 ^ sbit) < 2 ^ LENGTH('a)
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 6. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> sbit < LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat (n - Suc 0)) * unat (2 ^ sbit) < 2 ^ LENGTH('a)
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 6. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat (n - Suc 0)) * unat (2 ^ sbit) < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(is_aligned ptr sbit \<and> sz < LENGTH('a)) \<and> sbit \<le> sz \<and> n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat (n - Suc 0)) * unat (2 ^ sbit) < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> (n - Suc 0) * 2 ^ sbit < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> n - Suc 0 \<le> n
 2. \<lbrakk>n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> sbit \<le> LENGTH('a)
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 6. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> sbit \<le> LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat (n - Suc 0) * 2 ^ sbit) < 2 ^ sz
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
using this:
unat (word_of_nat n - 1) < n \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat (unat (word_of_nat n - 1)) * 2 ^ sbit) < 2 ^ sz

goal (5 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat (n - Suc 0) * 2 ^ sbit) < 2 ^ sz
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 5. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 4. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> 2 ^ sbit - 1 + (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1)
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + 2 ^ sbit - 1
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit) sbit
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat (n - Suc 0) * 2 ^ sbit) sbit
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat n - 1) * 2 ^ sbit) sbit
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> sbit \<le> sbit
 2. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 \<le> 2 ^ sbit - 1
 3. \<lbrakk>range_cover ptr sz sbit n; n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); n \<noteq> 0; p < n; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit \<le> ptr + word_of_nat (n - Suc 0) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit \<and> sz < LENGTH('a) \<and> sbit \<le> sz \<and> n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n - 1) * 2 ^ sbit \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit + (2 ^ sbit - 1) proof (prove)
using this:
\<lbrakk>is_aligned ?p ?n; is_aligned ?q ?n\<rbrakk> \<Longrightarrow> is_aligned (?p + ?q) ?n
is_aligned (?x * 2 ^ ?n) ?n
is_aligned ?p ?n \<Longrightarrow> ?p \<le> ?p + (2 ^ ?n - 1)

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit \<and> sz < LENGTH('a) \<and> sbit \<le> sz \<and> n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); n < 2 ^ LENGTH('a); n < 2 ^ (LENGTH('a) - sbit); p < n\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n - 1) * 2 ^ sbit \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit + (2 ^ sbit - 1) proof (state)
this:
ptr + word_of_nat p * 2 ^ sbit + 2 ^ sbit - 1 \<le> ptr + word_of_nat n * 2 ^ sbit - 1

goal:
No subgoals!