theory Retype_IF

lemma ptr_range_subset:
  fixes ptr :: obj_ref
  shows "\<lbrakk> is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits;
           x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<rbrakk>
           \<Longrightarrow> ptr_range x word_size_bits \<subseteq> ptr_range ptr bits" apply (frule is_aligned_word_size_bits_upto_enum_step_mem, assumption+) apply (rule subsetI) apply (clarsimp simp: word_size_size_bits_word[symmetric]) apply (subst (asm) upto_enum_step_shift_red; (fastforce simp: word_bits_def)?) apply (subst ptr_range_def) apply (clarsimp) apply (erule ptr_range_memE) apply (rule conjI) apply (erule order_trans[rotated]) apply (erule is_aligned_no_wrap') apply (rule word_less_power_trans2[where k=word_size_bits, simplified];
         fastforce elim: of_nat_power simp: word_bits_conv word_bits_def) apply (erule order_trans) apply (clarsimp simp: word_size_size_bits_word) apply (subgoal_tac "ptr + of_nat xaa * word_size + word_size - 1 =
                      ptr + ((2 ^ word_size_bits - 1) + of_nat xaa * word_size)") apply (subgoal_tac "ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)") apply (erule ssubst)+ apply (rule word_plus_mono_right) apply (drule is_aligned_addD1) apply (erule (1) is_aligned_weaken) prefer 2 apply (erule is_aligned_no_wrap') apply simp apply (simp_all add: word_size_size_bits_word) apply (drule (1) word_less_power_trans_ofnat[where 'a=machine_word_len], simp add: word_bits_def) apply (subst add.commute) apply (erule is_aligned_add_less_t2n) apply (simp_all add: word_size_size_bits_word) using zero_less_word_size gt0_iff_gem1 by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]\<rbrakk> \<Longrightarrow> ptr_range x word_size_bits \<subseteq> ptr_range ptr bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]; is_aligned x word_size_bits\<rbrakk> \<Longrightarrow> ptr_range x word_size_bits \<subseteq> ptr_range ptr bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]; is_aligned x word_size_bits; xa \<in> ptr_range x word_size_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range ptr bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set [ptr , ptr + 2 ^ word_size_bits .e. ptr + 2 ^ bits - 1]; is_aligned x word_size_bits; xa \<in> ptr_range x word_size_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range ptr bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set (map (\<lambda>x. ptr + word_of_nat x * 2 ^ word_size_bits) [0..<2 ^ (bits - word_size_bits)]); is_aligned x word_size_bits; xa \<in> ptr_range x word_size_bits\<rbrakk> \<Longrightarrow> xa \<in> ptr_range ptr bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set (map (\<lambda>x. ptr + word_of_nat x * 2 ^ word_size_bits) [0..<2 ^ (bits - word_size_bits)]); is_aligned x word_size_bits; xa \<in> ptr_range x word_size_bits\<rbrakk> \<Longrightarrow> xa \<in> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xa \<in> ptr_range (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; ptr + word_of_nat xaa * 2 ^ word_size_bits \<le> xa; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; ptr + word_of_nat xaa * 2 ^ word_size_bits \<le> xa; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> ptr \<le> xa
 2. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; ptr + word_of_nat xaa * 2 ^ word_size_bits \<le> xa; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> xa \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits
 2. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; ptr + word_of_nat xaa * 2 ^ word_size_bits \<le> xa; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> xa \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. \<lbrakk>word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> word_of_nat xaa * 2 ^ word_size_bits < 2 ^ bits
 2. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; ptr + word_of_nat xaa * 2 ^ word_size_bits \<le> xa; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> xa \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; ptr + word_of_nat xaa * 2 ^ word_size_bits \<le> xa; xa \<le> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1\<rbrakk> \<Longrightarrow> xa \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * 2 ^ word_size_bits) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * 2 ^ word_size_bits; ptr + word_of_nat xaa * 2 ^ word_size_bits \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * 2 ^ word_size_bits + 2 ^ word_size_bits - 1 \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 \<le> ptr + 2 ^ bits - 1
 2. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (3 subgoals):
 1. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size); ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 \<le> ptr + 2 ^ bits - 1
 2. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 3. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xa * word_size) word_size_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> ptr + (2 ^ word_size_bits - 1 + word_of_nat xa * word_size) \<le> ptr + (2 ^ bits - 1)
 2. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 3. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xa * word_size) word_size_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> 2 ^ word_size_bits - 1 + word_of_nat xa * word_size \<le> 2 ^ bits - 1
 2. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xa * word_size) word_size_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ bits - 1)
 3. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 4. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> is_aligned ptr word_size_bits
 2. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits\<rbrakk> \<Longrightarrow> 2 ^ word_size_bits - 1 + word_of_nat xa * word_size \<le> 2 ^ bits - 1
 3. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xa * word_size) word_size_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ bits - 1)
 4. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 5. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits\<rbrakk> \<Longrightarrow> 2 ^ word_size_bits - 1 + word_of_nat xa * word_size \<le> 2 ^ bits - 1
 2. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xa * word_size) word_size_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ bits - 1)
 3. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 4. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xa * word_size) word_size_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ bits - 1)
 2. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits\<rbrakk> \<Longrightarrow> 2 ^ word_size_bits - 1 + word_of_nat xa * word_size \<le> 2 ^ bits - 1
 3. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 4. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xa * word_size) word_size_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x\<rbrakk> \<Longrightarrow> 2 ^ bits - 1 < 2 ^ bits
 2. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits\<rbrakk> \<Longrightarrow> 2 ^ word_size_bits - 1 + word_of_nat xa * word_size \<le> 2 ^ bits - 1
 3. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 4. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits\<rbrakk> \<Longrightarrow> 2 ^ word_size_bits - 1 + word_of_nat xa * word_size \<le> 2 ^ bits - 1
 2. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa; ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size)\<rbrakk> \<Longrightarrow> ptr + 2 ^ bits - 1 = ptr + (2 ^ bits - 1)
 3. \<And>xa xaa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; is_aligned (ptr + word_of_nat xaa * word_size) word_size_bits; xaa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xaa * word_size; ptr + word_of_nat xaa * word_size \<le> xa\<rbrakk> \<Longrightarrow> ptr + word_of_nat xaa * word_size + word_size - 1 = ptr + (2 ^ word_size_bits - 1 + word_of_nat xaa * word_size) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits\<rbrakk> \<Longrightarrow> word_size - 1 + word_of_nat xa * word_size < 2 ^ bits proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits; word_of_nat xa * 2 ^ word_size_bits < 2 ^ bits\<rbrakk> \<Longrightarrow> word_size - 1 + word_of_nat xa * word_size < 2 ^ bits proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; ptr + word_of_nat xa * word_size \<le> x; is_aligned (word_of_nat xa * word_size) word_size_bits; word_of_nat xa * 2 ^ word_size_bits < 2 ^ bits\<rbrakk> \<Longrightarrow> word_of_nat xa * word_size + (word_size - 1) < 2 ^ bits proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; ptr + word_of_nat xa * word_size \<le> x; word_of_nat xa * 2 ^ word_size_bits < 2 ^ bits\<rbrakk> \<Longrightarrow> word_size - 1 < 2 ^ word_size_bits
 2. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; ptr + word_of_nat xa * word_size \<le> x; word_of_nat xa * 2 ^ word_size_bits < 2 ^ bits\<rbrakk> \<Longrightarrow> word_size_bits \<le> bits
 3. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; ptr + word_of_nat xa * word_size \<le> x; word_of_nat xa * 2 ^ word_size_bits < 2 ^ bits\<rbrakk> \<Longrightarrow> word_of_nat xa * word_size < 2 ^ bits proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; ptr + word_of_nat xa * word_size \<le> x; word_of_nat xa * word_size < 2 ^ bits\<rbrakk> \<Longrightarrow> word_size - 1 < word_size proof (prove)
using this:
0 < word_size
(0 < ?x) = (?x - 1 < ?x)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; ptr + word_of_nat xa * word_size \<le> x; word_of_nat xa * word_size < 2 ^ bits\<rbrakk> \<Longrightarrow> word_size - 1 < word_size