theory More_Word_Operations

lemma mask_range_to_bl':
  "\<lbrakk> is_aligned (ptr :: 'a :: len word) bits; bits < LENGTH('a) \<rbrakk>
   \<Longrightarrow> mask_range ptr bits
       = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}" apply (rule set_eqI, rule iffI) apply clarsimp apply (subgoal_tac "\<exists>y. x = ptr + y \<and> y < 2 ^ bits") apply clarsimp apply (subst is_aligned_add_conv) apply assumption apply simp apply simp apply (rule_tac x="x - ptr" in exI) apply (simp add: add_diff_eq[symmetric]) apply (simp only: word_less_sub_le[symmetric]) apply (rule word_diff_ls') apply (simp add: field_simps mask_eq_decr_exp) apply assumption apply simp apply (subgoal_tac "\<exists>y. y < 2 ^ bits \<and> to_bl (ptr + y) = to_bl x") apply clarsimp apply (rule conjI) apply (erule(1) is_aligned_no_wrap') apply (simp only: add_diff_eq[symmetric] mask_eq_decr_exp) apply (rule word_plus_mono_right) apply simp apply (erule is_aligned_no_wrap') apply simp apply (rule_tac x="of_bl (drop (LENGTH('a) - bits) (to_bl x))" in exI) apply (rule context_conjI) apply (rule order_less_le_trans [OF of_bl_length]) apply simp apply simp apply (subst is_aligned_add_conv) apply assumption apply simp apply (drule sym) apply (simp add: word_rep_drop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits; \<exists>y. x = ptr + y \<and> y < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + y \<and> y < 2 ^ bits
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr + y; ptr + y \<le> ptr + mask bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + y \<and> y < 2 ^ bits
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (5 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr + y; ptr + y \<le> ptr + mask bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> is_aligned ptr (?n15 y)
 2. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr + y; ptr + y \<le> ptr + mask bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> y < 2 ^ ?n15 y
 3. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr + y; ptr + y \<le> ptr + mask bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (take (LENGTH('a) - ?n15 y) (to_bl ptr) @ drop (LENGTH('a) - ?n15 y) (to_bl y)) = take (LENGTH('a) - bits) (to_bl ptr)
 4. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + y \<and> y < 2 ^ bits
 5. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr + y; ptr + y \<le> ptr + mask bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> y < 2 ^ bits
 2. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr + y; ptr + y \<le> ptr + mask bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (take (LENGTH('a) - bits) (to_bl ptr) @ drop (LENGTH('a) - bits) (to_bl y)) = take (LENGTH('a) - bits) (to_bl ptr)
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + y \<and> y < 2 ^ bits
 4. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr + y; ptr + y \<le> ptr + mask bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (take (LENGTH('a) - bits) (to_bl ptr) @ drop (LENGTH('a) - bits) (to_bl y)) = take (LENGTH('a) - bits) (to_bl ptr)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + y \<and> y < 2 ^ bits
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + y \<and> y < 2 ^ bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr) \<and> x - ptr < 2 ^ bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> x - ptr < 2 ^ bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> x - ptr \<le> 2 ^ bits - 1
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> x \<le> 2 ^ bits - 1 + ptr
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr \<le> x
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> x; x \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr \<le> x
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}\<rbrakk> \<Longrightarrow> x \<in> mask_range ptr bits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> ptr \<le> x \<and> x \<le> ptr + mask bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x\<rbrakk> \<Longrightarrow> ptr \<le> x \<and> x \<le> ptr + mask bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + y \<and> ptr + y \<le> ptr + mask bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + y
 2. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr + y \<le> ptr + mask bits
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr + y \<le> ptr + mask bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr + y \<le> ptr + (2 ^ bits - 1)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> y \<le> 2 ^ bits - 1
 2. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ bits - 1)
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ bits - 1)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl (ptr + y)) = take (LENGTH('a) - bits) (to_bl ptr); y < 2 ^ bits\<rbrakk> \<Longrightarrow> 2 ^ bits - 1 < 2 ^ bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> \<exists>y<2 ^ bits. to_bl (ptr + y) = to_bl x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits \<and> to_bl (ptr + of_bl (drop (LENGTH('a) - bits) (to_bl x))) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> to_bl (ptr + of_bl (drop (LENGTH('a) - bits) (to_bl x))) = to_bl x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> length (drop (LENGTH('a) - bits) (to_bl x)) < LENGTH('a)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> 2 ^ length (drop (LENGTH('a) - bits) (to_bl x)) \<le> 2 ^ bits
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> to_bl (ptr + of_bl (drop (LENGTH('a) - bits) (to_bl x))) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)\<rbrakk> \<Longrightarrow> 2 ^ length (drop (LENGTH('a) - bits) (to_bl x)) \<le> 2 ^ bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> to_bl (ptr + of_bl (drop (LENGTH('a) - bits) (to_bl x))) = to_bl x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> to_bl (ptr + of_bl (drop (LENGTH('a) - bits) (to_bl x))) = to_bl x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> is_aligned ptr (?n46 x)
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ ?n46 x
 3. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - ?n46 x) (to_bl ptr) @ drop (LENGTH('a) - ?n46 x) (to_bl (of_bl (drop (LENGTH('a) - bits) (to_bl x)))) = to_bl x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits
 2. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (to_bl ptr) @ drop (LENGTH('a) - bits) (to_bl (of_bl (drop (LENGTH('a) - bits) (to_bl x)))) = to_bl x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (to_bl ptr) @ drop (LENGTH('a) - bits) (to_bl (of_bl (drop (LENGTH('a) - bits) (to_bl x)))) = to_bl x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); of_bl (drop (LENGTH('a) - bits) (to_bl x)) < 2 ^ bits; take (LENGTH('a) - bits) (to_bl ptr) = take (LENGTH('a) - bits) (to_bl x)\<rbrakk> \<Longrightarrow> take (LENGTH('a) - bits) (to_bl ptr) @ drop (LENGTH('a) - bits) (to_bl (of_bl (drop (LENGTH('a) - bits) (to_bl x)))) = to_bl x proof (prove)
goal:
No subgoals!