[STATEMENT]
lemma neg_mask_in_mask_range:
  "is_aligned ptr bits \<Longrightarrow> (ptr' AND NOT(mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr bits \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (erule is_aligned_get_word_bits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a)\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> ptr' \<in> mask_range ptr bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr = ptr' AND NOT (mask bits)\<rbrakk> \<Longrightarrow> ptr' \<in> mask_range ptr bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (simp add: word_and_le2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits < LENGTH('a); ptr = ptr' AND NOT (mask bits)\<rbrakk> \<Longrightarrow> ptr' \<le> (ptr' AND NOT (mask bits)) + mask bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (subst word_plus_and_or_coroll, word_eqI_solve)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits < LENGTH('a); ptr = ptr' AND NOT (mask bits)\<rbrakk> \<Longrightarrow> ptr' \<le> ptr' AND NOT (mask bits) OR mask bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (metis bit.disj_ac(2) bit.disj_conj_distrib2 le_word_or2 word_and_max word_or_not)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr'; ptr' \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (smt add.right_neutral eq_iff is_aligned_neg_mask_eq mask_out_add_aligned neg_mask_mono_le
              word_and_not)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
[PROOF STEP]
apply (simp add: power_overflow mask_eq_decr_exp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_offset_in_range:
  "\<lbrakk> is_aligned (x :: 'a :: len word) m; y < 2 ^ m; is_aligned p n; n \<ge> m; n < LENGTH('a) \<rbrakk>
   \<Longrightarrow> (x + y \<in> {p .. p + mask n}) = (x \<in> mask_range p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x + y \<in> mask_range p n) = (x \<in> mask_range p n)
[PROOF STEP]
apply (subst disjunctive_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> bit x na \<or> \<not> bit y na
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n)
[PROOF STEP]
apply (simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit x na \<longrightarrow> \<not> bit y na
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n)
[PROOF STEP]
apply (erule is_alignedE')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na q. \<lbrakk>y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a); x = push_bit m (word_of_nat q); q < 2 ^ (LENGTH('a) - m)\<rbrakk> \<Longrightarrow> bit x na \<longrightarrow> \<not> bit y na
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n)
[PROOF STEP]
apply (auto simp add: bit_simps not_le)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na q. \<lbrakk>y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a); x = push_bit m (word_of_nat q); q < 2 ^ (LENGTH('a) - m); m \<le> na; na < LENGTH('a); na - m < LENGTH('a); bit q (na - m); bit y na\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n)
[PROOF STEP]
apply (metis less_2p_is_upper_bits_unset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n)
[PROOF STEP]
apply (simp only: is_aligned_add_or word_ao_dist flip: neg_mask_in_mask_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x AND NOT (mask n) OR y AND NOT (mask n) = p) = (x AND NOT (mask n) = p)
[PROOF STEP]
apply (subgoal_tac \<open>y AND NOT (mask n) = 0\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a); y AND NOT (mask n) = 0\<rbrakk> \<Longrightarrow> (x AND NOT (mask n) OR y AND NOT (mask n) = p) = (x AND NOT (mask n) = p)
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> y AND NOT (mask n) = 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> y AND NOT (mask n) = 0
[PROOF STEP]
apply (metis (full_types) is_aligned_mask is_aligned_neg_mask less_mask_eq word_bw_comms(1) word_bw_lcs(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
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)}"
[PROOF STATE]
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 STEP]
apply (rule set_eqI, rule iffI)
[PROOF STATE]
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 STEP]
apply clarsimp
[PROOF STATE]
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 STEP]
apply (subgoal_tac "\<exists>y. x = ptr + y \<and> y < 2 ^ bits")
[PROOF STATE]
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 STEP]
apply clarsimp
[PROOF STATE]
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 STEP]
apply (subst is_aligned_add_conv)
[PROOF STATE]
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 STEP]
apply assumption
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (rule_tac x="x - ptr" in exI)
[PROOF STATE]
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 STEP]
apply (simp add: add_diff_eq[symmetric])
[PROOF STATE]
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 STEP]
apply (simp only: word_less_sub_le[symmetric])
[PROOF STATE]
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 STEP]
apply (rule word_diff_ls')
[PROOF STATE]
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 STEP]
apply (simp add: field_simps mask_eq_decr_exp)
[PROOF STATE]
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 STEP]
apply assumption
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (subgoal_tac "\<exists>y. y < 2 ^ bits \<and> to_bl (ptr + y) = to_bl x")
[PROOF STATE]
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 STEP]
apply clarsimp
[PROOF STATE]
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 STEP]
apply (rule conjI)
[PROOF STATE]
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 STEP]
apply (erule(1) is_aligned_no_wrap')
[PROOF STATE]
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 STEP]
apply (simp only: add_diff_eq[symmetric] mask_eq_decr_exp)
[PROOF STATE]
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 STEP]
apply (rule word_plus_mono_right)
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (erule is_aligned_no_wrap')
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (rule_tac x="of_bl (drop (LENGTH('a) - bits) (to_bl x))" in exI)
[PROOF STATE]
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 STEP]
apply (rule context_conjI)
[PROOF STATE]
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 STEP]
apply (rule order_less_le_trans [OF of_bl_length])
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (subst is_aligned_add_conv)
[PROOF STATE]
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 STEP]
apply assumption
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (drule sym)
[PROOF STATE]
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 STEP]
apply (simp add: word_rep_drop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mask_range_to_bl:
  "is_aligned (ptr :: 'a :: len word) bits
   \<Longrightarrow> mask_range ptr bits
        = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr bits \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}
[PROOF STEP]
apply (erule is_aligned_get_word_bits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 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)}
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}
[PROOF STEP]
apply (erule(1) mask_range_to_bl')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> mask_range ptr bits = {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)}
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (x \<in> mask_range ptr bits) = (x \<in> {x. take (LENGTH('a) - bits) (to_bl x) = take (LENGTH('a) - bits) (to_bl ptr)})
[PROOF STEP]
apply (simp add: power_overflow mask_eq_decr_exp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_mask_range_cases:
  "\<lbrakk> is_aligned (p :: 'a :: len word) n; is_aligned (p' :: 'a :: len word) n' \<rbrakk>
   \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {} \<or>
       mask_range p n \<subseteq> mask_range p' n' \<or>
       mask_range p n \<supseteq> mask_range p' n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {} \<or> mask_range p n \<subseteq> mask_range p' n' \<or> mask_range p' n' \<subseteq> mask_range p n
[PROOF STEP]
apply (simp add: mask_range_to_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<inter> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} = {} \<or> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<subseteq> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<or> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<subseteq> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)}
[PROOF STEP]
apply (rule Meson.disj_comm, rule disjCI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'; {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<inter> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<noteq> {}\<rbrakk> \<Longrightarrow> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<subseteq> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<or> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<subseteq> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "(\<exists>n''. LENGTH('a) - n = (LENGTH('a) - n') + n'')
                    \<or> (\<exists>n''. LENGTH('a) - n' = (LENGTH('a) - n) + n'')")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p'); (\<exists>n''. LENGTH('a) - n = LENGTH('a) - n' + n'') \<or> (\<exists>n''. LENGTH('a) - n' = LENGTH('a) - n + n'')\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p')\<rbrakk> \<Longrightarrow> (\<exists>n''. LENGTH('a) - n = LENGTH('a) - n' + n'') \<or> (\<exists>n''. LENGTH('a) - n' = LENGTH('a) - n + n'')
[PROOF STEP]
apply (fastforce simp: take_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p')\<rbrakk> \<Longrightarrow> (\<exists>n''. LENGTH('a) - n = LENGTH('a) - n' + n'') \<or> (\<exists>n''. LENGTH('a) - n' = LENGTH('a) - n + n'')
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_mask_range_offset_subset:
  assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'"
  and szv: "sz' \<le> sz"
  and xsz: "x < 2 ^ sz"
  shows "mask_range (ptr+x) sz' \<subseteq> mask_range ptr sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
using al
[PROOF STATE]
proof (prove)
using this:
is_aligned ptr sz

goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
proof (rule is_aligned_get_word_bits)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> sz\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
assume p0: "ptr = 0" and szv': "LENGTH ('a) \<le> sz"
[PROOF STATE]
proof (state)
this:
ptr = 0
LENGTH('a) \<le> sz

goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> sz\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ptr = 0
LENGTH('a) \<le> sz
[PROOF STEP]
have "(2 ::'a word) ^ sz = 0"
[PROOF STATE]
proof (prove)
using this:
ptr = 0
LENGTH('a) \<le> sz

goal (1 subgoal):
 1. 2 ^ sz = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ sz = 0

goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> sz\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
using p0
[PROOF STATE]
proof (prove)
using this:
ptr = 0

goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
by (simp add: \<open>2 ^ sz = 0\<close> mask_eq_decr_exp)
[PROOF STATE]
proof (state)
this:
mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
assume szv': "sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
sz < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
hence blah: "2 ^ (sz - sz') < (2 :: nat) ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ (sz - sz') < 2 ^ LENGTH('a)
[PROOF STEP]
using szv
[PROOF STATE]
proof (prove)
using this:
sz < LENGTH('a)
sz' \<le> sz

goal (1 subgoal):
 1. 2 ^ (sz - sz') < 2 ^ LENGTH('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 ^ (sz - sz') < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
using szv szv'
[PROOF STATE]
proof (prove)
using this:
sz' \<le> sz
sz < LENGTH('a)

goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr \<le> ptr + x
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr + x + mask sz' \<le> ptr + mask sz
[PROOF STEP]
using al assms(4) is_aligned_no_wrap'
[PROOF STATE]
proof (prove)
using this:
is_aligned ptr sz
x < 2 ^ sz
\<lbrakk>is_aligned ?ptr ?sz; ?off < 2 ^ ?sz\<rbrakk> \<Longrightarrow> ?ptr \<le> ?ptr + ?off

goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr \<le> ptr + x
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr + x + mask sz' \<le> ptr + mask sz
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr + x + mask sz' \<le> ptr + mask sz
[PROOF STEP]
apply (simp only: flip: add_diff_eq add_mask_fold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr + x + (2 ^ sz' - 1) \<le> ptr + (2 ^ sz - 1)
[PROOF STEP]
apply (subst add.assoc, rule word_plus_mono_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> x + (2 ^ sz' - 1) \<le> 2 ^ sz - 1
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ sz - 1)
[PROOF STEP]
using al' is_aligned_add_less_t2n xsz
[PROOF STATE]
proof (prove)
using this:
is_aligned x sz'
\<lbrakk>is_aligned ?p ?n; ?d < 2 ^ ?n; ?n \<le> ?m; ?p < 2 ^ ?m\<rbrakk> \<Longrightarrow> ?p + ?d < 2 ^ ?m
x < 2 ^ sz

goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> x + (2 ^ sz' - 1) \<le> 2 ^ sz - 1
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ sz - 1)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ sz - 1)
[PROOF STEP]
apply (simp add: field_simps szv al is_aligned_no_overflow)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aligned_mask_ranges_disjoint:
  "\<lbrakk> is_aligned (p :: 'a :: len word) n; is_aligned (p' :: 'a :: len word) n';
     p AND NOT(mask n') \<noteq> p'; p' AND NOT(mask n) \<noteq> p \<rbrakk>
   \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'; p AND NOT (mask n') \<noteq> p'; p' AND NOT (mask n) \<noteq> p\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {}
[PROOF STEP]
using aligned_mask_range_cases
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_aligned ?p ?n; is_aligned ?p' ?n'\<rbrakk> \<Longrightarrow> mask_range ?p ?n \<inter> mask_range ?p' ?n' = {} \<or> mask_range ?p ?n \<subseteq> mask_range ?p' ?n' \<or> mask_range ?p' ?n' \<subseteq> mask_range ?p ?n

goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'; p AND NOT (mask n') \<noteq> p'; p' AND NOT (mask n) \<noteq> p\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {}
[PROOF STEP]
by (auto simp: neg_mask_in_mask_range)


[STATEMENT]
lemma aligned_mask_ranges_disjoint2:
  "\<lbrakk> is_aligned p n; is_aligned ptr bits; n \<ge> m; n < size p; m \<le> bits;
     (\<forall>y < 2 ^ (n - m). p + (y << m) \<notin> mask_range ptr bits) \<rbrakk>
   \<Longrightarrow> mask_range p n \<inter> mask_range ptr bits = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; \<forall>y<2 ^ (n - m). p + (y << m) \<notin> mask_range ptr bits\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range ptr bits = {}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; \<forall>y<2 ^ (n - m). p + (y << m) \<notin> mask_range ptr bits; x \<in> mask_range p n; x \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> x \<in> {}
[PROOF STEP]
apply (simp only: flip: neg_mask_in_mask_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; \<forall>y<2 ^ (n - m). p + (y << m) AND NOT (mask bits) \<noteq> ptr; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> x \<in> {}
[PROOF STEP]
apply (drule_tac x="x AND mask n >> m" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr; x AND mask n >> m < 2 ^ (n - m) \<longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) \<noteq> ptr\<rbrakk> \<Longrightarrow> x \<in> {}
[PROOF STEP]
apply (erule notE[OF mp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> x AND mask n >> m < 2 ^ (n - m)
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr
[PROOF STEP]
apply (simp flip: take_bit_eq_mask add: shiftr_def drop_bit_take_bit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> take_bit (n - m) (drop_bit m x) < 2 ^ (n - m)
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p n ptr bits m. \<lbrakk>2 ^ n dvd take_bit LENGTH('a) p; 2 ^ bits dvd take_bit LENGTH('a) ptr; m \<le> n; n < LENGTH('a); m \<le> bits; take_bit LENGTH('a) (x AND NOT (mask n)) = take_bit LENGTH('a) p; take_bit LENGTH('a) (x AND NOT (mask bits)) = take_bit LENGTH('a) ptr\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (take_bit (min LENGTH('a) (n - m)) ((drop_bit m \<circ> take_bit LENGTH('a)) x)) < take_bit LENGTH('a) (2 ^ (n - m))
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr
[PROOF STEP]
apply (simp add: word_size and_mask_less_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < LENGTH('a); m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr
[PROOF STEP]
apply (subst disjunctive_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x na. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < LENGTH('a); m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> \<not> bit p na \<or> \<not> bit (x AND mask n >> m << m) na
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < LENGTH('a); m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> (p OR (x AND mask n >> m << m)) AND NOT (mask bits) = ptr
[PROOF STEP]
apply (auto simp add: bit_simps word_size intro!: bit_eqI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_clz_sint_upper[simp]:
  "LENGTH('a) \<ge> 3 \<Longrightarrow> sint (of_nat (word_clz (w :: 'a :: len word)) :: 'a sword) \<le> int (LENGTH('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> sint (word_of_nat (word_clz w)) \<le> int LENGTH('a)
[PROOF STEP]
using word_clz_max [of w]
[PROOF STATE]
proof (prove)
using this:
word_clz w \<le> size w

goal (1 subgoal):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> sint (word_of_nat (word_clz w)) \<le> int LENGTH('a)
[PROOF STEP]
apply (simp add: word_size signed_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) (int (word_clz w)) \<le> int LENGTH('a)
[PROOF STEP]
apply (subst signed_take_bit_int_eq_self)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> - (2 ^ (LENGTH('a) - Suc 0)) \<le> int (word_clz w)
 2. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> int (word_clz w) < 2 ^ (LENGTH('a) - Suc 0)
 3. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> int (word_clz w) \<le> int LENGTH('a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> - (2 ^ (LENGTH('a) - Suc 0)) \<le> int (word_clz w)
 2. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (metis negative_zle of_nat_numeral semiring_1_class.of_nat_power)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (drule small_powers_of_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_clz w \<le> LENGTH('a); LENGTH('a) < 2 ^ (LENGTH('a) - 1)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (erule le_less_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_clz_sint_lower[simp]:
  "LENGTH('a) \<ge> 3
   \<Longrightarrow> - sint (of_nat (word_clz (w :: 'a :: len word)) :: 'a signed word) \<le> int (LENGTH('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> - sint (word_of_nat (word_clz w)) \<le> int LENGTH('a)
[PROOF STEP]
apply (subst sint_eq_uint)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> \<not> msb (word_of_nat (word_clz w))
 2. 3 \<le> LENGTH('a) \<Longrightarrow> - uint (word_of_nat (word_clz w)) \<le> int LENGTH('a)
[PROOF STEP]
using word_clz_max [of w]
[PROOF STATE]
proof (prove)
using this:
word_clz w \<le> size w

goal (2 subgoals):
 1. 3 \<le> LENGTH('a) \<Longrightarrow> \<not> msb (word_of_nat (word_clz w))
 2. 3 \<le> LENGTH('a) \<Longrightarrow> - uint (word_of_nat (word_clz w)) \<le> int LENGTH('a)
[PROOF STEP]
apply (simp_all add: word_size unsigned_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> msb (word_of_nat (word_clz w))
[PROOF STEP]
apply (rule not_msb_from_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat (word_clz w) < 2 ^ (LENGTH('a signed) - 1)
[PROOF STEP]
apply (simp add: word_less_nat_alt unsigned_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (word_clz w) < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (subst take_bit_nat_eq_self)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ LENGTH('a)
 2. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (simp add: le_less_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 \<le> LENGTH('a); word_clz w \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (drule small_powers_of_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_clz w \<le> LENGTH('a); LENGTH('a) < 2 ^ (LENGTH('a) - 1)\<rbrakk> \<Longrightarrow> word_clz w < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (erule le_less_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mask_range_subsetD:
  "\<lbrakk> p' \<in> mask_range p n; x' \<in> mask_range p' n'; n' \<le> n; is_aligned p n; is_aligned p' n' \<rbrakk> \<Longrightarrow>
   x' \<in> mask_range p n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<in> mask_range p n; x' \<in> mask_range p' n'; n' \<le> n; is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> x' \<in> mask_range p n
[PROOF STEP]
using aligned_mask_step
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n' \<le> ?n; ?p' \<le> ?p + mask ?n; is_aligned ?p ?n; is_aligned ?p' ?n'\<rbrakk> \<Longrightarrow> ?p' + mask ?n' \<le> ?p + mask ?n

goal (1 subgoal):
 1. \<lbrakk>p' \<in> mask_range p n; x' \<in> mask_range p' n'; n' \<le> n; is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> x' \<in> mask_range p n
[PROOF STEP]
by fastforce


[STATEMENT]
lemma add_mult_in_mask_range:
  "\<lbrakk> is_aligned (base :: 'a :: len word) n; n < LENGTH('a); bits \<le> n; x < 2 ^ (n - bits) \<rbrakk>
   \<Longrightarrow> base + x * 2^bits \<in> mask_range base n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned base n; n < LENGTH('a); bits \<le> n; x < 2 ^ (n - bits)\<rbrakk> \<Longrightarrow> base + x * 2 ^ bits \<in> mask_range base n
[PROOF STEP]
by (simp add: is_aligned_no_wrap' mask_2pm1 nasty_split_lt word_less_power_trans2
                word_plus_mono_right)


[STATEMENT]
lemma from_to_bool_last_bit:
  "from_bool (to_bool (x AND 1)) = x AND 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_bool (to_bool (x AND 1)) = x AND 1
[PROOF STEP]
by (metis from_bool_to_bool_iff word_and_1)


[STATEMENT]
lemma sint_ctz:
  \<open>0 \<le> sint (of_nat (word_ctz (x :: 'a :: len word)) :: 'a signed word)
     \<and> sint (of_nat (word_ctz x) :: 'a signed word) \<le> int (LENGTH('a))\<close> (is \<open>?P \<and> ?Q\<close>)
  if \<open>LENGTH('a) > 2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sint (word_of_nat (word_ctz x)) \<and> sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> sint (word_of_nat (word_ctz x))
 2. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)
[PROOF STEP]
have *: \<open>word_ctz x < 2 ^ (LENGTH('a) - Suc 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_ctz x < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
using word_ctz_le
[PROOF STATE]
proof (prove)
using this:
word_ctz ?w \<le> LENGTH(?'a)

goal (1 subgoal):
 1. word_ctz x < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (rule le_less_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
using that small_powers_of_2 [of \<open>LENGTH('a)\<close>]
[PROOF STATE]
proof (prove)
using this:
2 < LENGTH('a)
3 \<le> LENGTH('a) \<Longrightarrow> LENGTH('a) < 2 ^ (LENGTH('a) - 1)

goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
word_ctz x < 2 ^ (LENGTH('a) - Suc 0)

goal (2 subgoals):
 1. 0 \<le> sint (word_of_nat (word_ctz x))
 2. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)
[PROOF STEP]
have \<open>int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0
[PROOF STEP]
apply (rule div_pos_pos_trivial)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> int (word_ctz x)
 2. int (word_ctz x) < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (simp_all add: *)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0

goal (2 subgoals):
 1. 0 \<le> sint (word_of_nat (word_ctz x))
 2. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
using this:
int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0

goal (1 subgoal):
 1. 0 \<le> sint (word_of_nat (word_ctz x))
[PROOF STEP]
by (simp add: signed_of_nat bit_iff_odd)
[PROOF STATE]
proof (state)
this:
0 \<le> sint (word_of_nat (word_ctz x))

goal (1 subgoal):
 1. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)
[PROOF STEP]
show ?Q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)
[PROOF STEP]
apply (auto simp add: signed_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit (LENGTH('a) - Suc 0) (int (word_ctz x)) \<le> int LENGTH('a)
[PROOF STEP]
apply (subst signed_take_bit_int_eq_self)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. - (2 ^ (LENGTH('a) - Suc 0)) \<le> int (word_ctz x)
 2. int (word_ctz x) < 2 ^ (LENGTH('a) - Suc 0)
 3. int (word_ctz x) \<le> int LENGTH('a)
[PROOF STEP]
apply (auto simp add: word_ctz_le * minus_le_iff [of _ \<open>int (word_ctz x)\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - int (word_ctz x) \<le> 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (rule order.trans [of _ 0])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. - int (word_ctz x) \<le> 0
 2. 0 \<le> 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unat_of_nat_word_log2:
  "LENGTH('a) < 2 ^ LENGTH('b)
   \<Longrightarrow> unat (of_nat (word_log2 (n :: 'a :: len word)) :: 'b :: len word) = word_log2 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ LENGTH('b) \<Longrightarrow> unat (word_of_nat (word_log2 n)) = word_log2 n
[PROOF STEP]
by (metis less_trans unat_of_nat_eq word_log2_max word_size)


[STATEMENT]
lemma aligned_mask_diff:
  "\<lbrakk> is_aligned (dest :: 'a :: len word) bits; is_aligned (ptr :: 'a :: len word) sz;
     bits \<le> sz; sz < LENGTH('a); dest < ptr \<rbrakk>
   \<Longrightarrow> mask bits + dest < ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
[PROOF STEP]
apply (frule_tac p' = ptr in aligned_mask_range_cases, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<inter> mask_range ptr sz = {} \<or> mask_range dest bits \<subseteq> mask_range ptr sz \<or> mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<inter> mask_range ptr sz = {}\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<subseteq> mask_range ptr sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 3. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
[PROOF STEP]
apply (drule_tac is_aligned_no_overflow_mask, simp)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits \<le> sz; sz < LENGTH('a); dest < ptr; \<not> ptr \<le> dest + mask bits; dest \<le> dest + mask bits; ptr \<le> ptr + mask sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<subseteq> mask_range ptr sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 3. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
[PROOF STEP]
apply (simp add: algebra_split_simps word_le_not_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<subseteq> mask_range ptr sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
[PROOF STEP]
apply (drule is_aligned_no_overflow_mask; fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
[PROOF STEP]
apply (simp add: is_aligned_weaken algebra_split_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; ptr \<le> ptr + mask sz \<longrightarrow> dest \<le> ptr \<and> ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
[PROOF STEP]
apply (auto simp add: not_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; ptr + mask sz < ptr\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; dest \<le> ptr; ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
[PROOF STEP]
using is_aligned_no_overflow_mask leD
[PROOF STATE]
proof (prove)
using this:
is_aligned ?x ?n \<Longrightarrow> ?x \<le> ?x + mask ?n
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (2 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; ptr + mask sz < ptr\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; dest \<le> ptr; ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; dest \<le> ptr; ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
[PROOF STEP]
apply (meson aligned_add_mask_less_eq is_aligned_weaken le_less_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma butlast_empty[iff]:
  "(butlast xs = []) = (case xs of [] \<Rightarrow> True | y#ys \<Rightarrow> ys=[])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (butlast xs = []) = (case xs of [] \<Rightarrow> True | y # ys \<Rightarrow> ys = [])
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma in_set_butlast_concatI:
 "x:set(butlast xs) \<Longrightarrow> xs:set xss \<Longrightarrow> x:set(butlast(concat xss))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set (butlast xs); xs \<in> set xss\<rbrakk> \<Longrightarrow> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply (induct "xss")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set (butlast xs); xs \<in> set []\<rbrakk> \<Longrightarrow> x \<in> set (butlast (concat []))
 2. \<And>a xss. \<lbrakk>\<lbrakk>x \<in> set (butlast xs); xs \<in> set xss\<rbrakk> \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs \<in> set (a # xss)\<rbrakk> \<Longrightarrow> x \<in> set (butlast (concat (a # xss)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>\<lbrakk>x \<in> set (butlast xs); xs \<in> set xss\<rbrakk> \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs \<in> set (a # xss)\<rbrakk> \<Longrightarrow> x \<in> set (butlast (concat (a # xss)))
[PROOF STEP]
apply (simp add: butlast_append del: ball_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> ((\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set (butlast a)) \<and> (\<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss)))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set (butlast a)
 2. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> \<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss; \<forall>xs\<in>set xss. xs = []\<rbrakk> \<Longrightarrow> x \<in> set (butlast a)
 2. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> \<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); \<forall>xs\<in>set xss. xs = []; xs = a\<rbrakk> \<Longrightarrow> x \<in> set (butlast a)
 2. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); \<forall>xs\<in>set xss. xs = []; xs \<in> set xss\<rbrakk> \<Longrightarrow> x \<in> set (butlast a)
 3. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> \<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply (blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); \<forall>xs\<in>set xss. xs = []; xs \<in> set xss\<rbrakk> \<Longrightarrow> x \<in> set (butlast a)
 2. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> \<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply (subgoal_tac "xs=[]")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); \<forall>xs\<in>set xss. xs = []; xs \<in> set xss; xs = []\<rbrakk> \<Longrightarrow> x \<in> set (butlast a)
 2. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); \<forall>xs\<in>set xss. xs = []; xs \<in> set xss\<rbrakk> \<Longrightarrow> xs = []
 3. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> \<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); \<forall>xs\<in>set xss. xs = []; xs \<in> set xss\<rbrakk> \<Longrightarrow> xs = []
 2. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> \<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply (blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>xs \<in> set xss \<Longrightarrow> x \<in> set (butlast (concat xss)); x \<in> set (butlast xs); xs = a \<or> xs \<in> set xss\<rbrakk> \<Longrightarrow> \<not> (\<forall>xs\<in>set xss. xs = []) \<longrightarrow> x \<in> set a \<or> x \<in> set (butlast (concat xss))
[PROOF STEP]
apply (blast dest: in_set_butlastD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done