kings-crown/FVELER_Isabelle huggingface dataset:
theory Aligned

lemma aligned_inter_non_empty:
  "\<lbrakk> {p..p + (2 ^ n - 1)} \<inter> {p..p + 2 ^ m - 1} = {};
     is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False" apply (clarsimp simp only: range_inter) apply (erule_tac x=p in allE) apply simp apply (erule impE) apply (erule is_aligned_no_overflow') apply (erule notE) apply (erule is_aligned_no_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{p..p + (2 ^ n - 1)} \<inter> {p..p + 2 ^ m - 1} = {}; is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. \<not> (p \<le> x \<and> x \<le> p + (2 ^ n - 1) \<and> p \<le> x \<and> x \<le> p + 2 ^ m - 1); is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m; \<not> (p \<le> p \<and> p \<le> p + (2 ^ n - 1) \<and> p \<le> p \<and> p \<le> p + 2 ^ m - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m; p \<le> p + (2 ^ n - 1) \<longrightarrow> \<not> p \<le> p + 2 ^ m - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<lbrakk>is_aligned p n; is_aligned p m; \<not> p \<le> p + 2 ^ m - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m; \<not> p \<le> p + 2 ^ m - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> p \<le> p + 2 ^ m - 1 proof (prove)
goal:
No subgoals!
theory Aligned

lemma not_aligned_mod_nz:
  assumes al: "\<not> is_aligned a n"
  shows "a mod 2 ^ n \<noteq> 0" apply (rule ccontr) using al apply (rule notE) apply simp apply (rule is_alignedI [of _ _ \<open>a div 2 ^ n\<close>]) apply (metis add.right_neutral mult.commute word_mod_div_equality) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<not> a mod 2 ^ n \<noteq> 0 \<Longrightarrow> False proof (prove)
using this:
\<not> is_aligned a n

goal (1 subgoal):
 1. \<not> a mod 2 ^ n \<noteq> 0 \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<not> a mod 2 ^ n \<noteq> 0 \<Longrightarrow> is_aligned a n proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n = 0 \<Longrightarrow> is_aligned a n proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n = 0 \<Longrightarrow> a = 2 ^ n * (a div 2 ^ n) proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_neg_mask:
  "m \<le> n \<Longrightarrow> is_aligned (x AND NOT (mask n)) m" by (rule is_aligned_bitI) (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> is_aligned (x AND NOT (mask n)) m
theory Aligned

lemma unat_minus:
  "unat (- (x :: 'a :: len word)) = (if x = 0 then 0 else 2 ^ size x - unat x)" using unat_sub_if_size[where x="2 ^ size x" and y=x] by (simp add: unat_eq_0 word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (- x) = (if x = 0 then 0 else 2 ^ size x - unat x) proof (prove)
using this:
unat (2 ^ size x - x) = (if unat x \<le> unat (2 ^ size x) then unat (2 ^ size x) - unat x else unat (2 ^ size x) + 2 ^ size (2 ^ size x) - unat x)

goal (1 subgoal):
 1. unat (- x) = (if x = 0 then 0 else 2 ^ size x - unat x)
theory Aligned

lemma is_aligned_minus:
  \<open>is_aligned (- p) n\<close> if \<open>is_aligned p n\<close> for p :: \<open>'a::len word\<close> using that apply (cases \<open>n < LENGTH('a)\<close>) apply (simp_all add: not_less is_aligned_beyond_length) apply transfer apply (simp flip: take_bit_eq_0_iff) apply (subst take_bit_minus [symmetric]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (- p) n proof (prove)
using this:
is_aligned p n

goal (1 subgoal):
 1. is_aligned (- p) n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (- p) n
 2. \<lbrakk>is_aligned p n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (- p) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (- p) n proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>2 ^ n dvd take_bit LENGTH('a) p; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n dvd take_bit LENGTH('a) (- p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>take_bit n p = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n (- p) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>take_bit n p = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n (- take_bit n p) = 0 proof (prove)
goal:
No subgoals!
theory Aligned

lemma add_mask_lower_bits:
  "\<lbrakk>is_aligned (x :: 'a :: len word) n;
    \<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x" apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_size is_aligned_nth) apply (erule_tac x=na in allE)+ apply (simp add: bit_simps) apply (rule bit_word_eqI) apply (auto simp add: bit_simps not_less word_size) apply (metis is_aligned_nth not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x AND p = 0
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> na < size (x AND p) \<longrightarrow> bit (x AND p) na = bit 0 na
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit x na; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'; na < LENGTH('a); bit (x AND p) na\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>na < LENGTH('a); bit (x AND p) na; na < n \<longrightarrow> \<not> bit x na; n \<le> na \<longrightarrow> na < LENGTH('a) \<longrightarrow> \<not> bit p na\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit ((x OR p) AND NOT (mask n)) na = bit x na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'; na < LENGTH('a); bit x na\<rbrakk> \<Longrightarrow> n \<le> na proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_andI1:
  "is_aligned x n \<Longrightarrow> is_aligned (x AND y) n" by (simp add: is_aligned_nth bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x n \<Longrightarrow> is_aligned (x AND y) n
theory Aligned

lemma is_aligned_andI2:
  "is_aligned y n \<Longrightarrow> is_aligned (x AND y) n" by (simp add: is_aligned_nth bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned y n \<Longrightarrow> is_aligned (x AND y) n
theory Aligned

lemma is_aligned_shiftr:
  "is_aligned w (n + m) \<Longrightarrow> is_aligned (w >> m) n" by (simp add: is_aligned_nth bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned w (n + m) \<Longrightarrow> is_aligned (w >> m) n
theory Aligned

lemma is_aligned_shiftl_self:
  "is_aligned (p << n) n" by (rule is_aligned_shift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (p << n) n
theory Aligned

lemma is_aligned_neg_mask_eq:
  "is_aligned p n \<Longrightarrow> p AND NOT (mask n) = p" apply (rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p n \<Longrightarrow> p AND NOT (mask n) = p proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned p n; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (p AND NOT (mask n)) na = bit p na proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_shiftr_shiftl:
  "is_aligned w n \<Longrightarrow> w >> n << n = w" apply (rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth intro: ccontr) apply (subst add_diff_inverse_nat) apply (auto intro: ccontr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned w n \<Longrightarrow> w >> n << n = w proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned w n; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (w >> n << n) na = bit w na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit w na; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> bit w (n + (na - n)) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit w na; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> \<not> na < n
 2. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit w na; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> bit w na proof (prove)
goal:
No subgoals!
theory Aligned

lemma aligned_shiftr_mask_shiftl:
  "is_aligned x n \<Longrightarrow> ((x >> n) AND mask v) << n = x AND mask (v + n)" apply (rule word_eqI) apply (simp add: word_size bit_simps) apply (subgoal_tac "\<forall>m. bit x m \<longrightarrow> m \<ge> n") apply auto[1] apply (clarsimp simp: is_aligned_mask) apply (drule_tac x=m in word_eqD) apply (frule test_bit_size) apply (simp add: word_size bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x n \<Longrightarrow> (x >> n) AND mask v << n = x AND mask (v + n) proof (prove)
goal (1 subgoal):
 1. \<And>na. is_aligned x n \<Longrightarrow> na < size ((x >> n) AND mask v << n) \<longrightarrow> bit ((x >> n) AND mask v << n) na = bit (x AND mask (v + n)) na proof (prove)
goal (1 subgoal):
 1. \<And>na. is_aligned x n \<Longrightarrow> na < LENGTH('a) \<longrightarrow> (n \<le> na \<and> bit x (n + (na - n)) \<and> na - n < LENGTH('a) \<and> na - n < v) = (bit x na \<and> na < v + n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>m. bit x m \<longrightarrow> n \<le> m\<rbrakk> \<Longrightarrow> na < LENGTH('a) \<longrightarrow> (n \<le> na \<and> bit x (n + (na - n)) \<and> na - n < LENGTH('a) \<and> na - n < v) = (bit x na \<and> na < v + n)
 2. \<And>na. is_aligned x n \<Longrightarrow> \<forall>m. bit x m \<longrightarrow> n \<le> m proof (prove)
goal (1 subgoal):
 1. \<And>na. is_aligned x n \<Longrightarrow> \<forall>m. bit x m \<longrightarrow> n \<le> m proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>x AND mask n = 0; bit x m\<rbrakk> \<Longrightarrow> n \<le> m proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>bit x m; bit (x AND mask n) m = bit 0 m\<rbrakk> \<Longrightarrow> n \<le> m proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>bit x m; bit (x AND mask n) m = bit 0 m; m < size x\<rbrakk> \<Longrightarrow> n \<le> m proof (prove)
goal:
No subgoals!
theory Aligned

lemma mask_zero:
  "is_aligned x a \<Longrightarrow> x AND mask a = 0" by (metis is_aligned_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x a \<Longrightarrow> x AND mask a = 0
theory Aligned

lemma is_aligned_and_not_zero:
  "\<lbrakk> is_aligned n k; n \<noteq> 0 \<rbrakk> \<Longrightarrow> 2 ^ k \<le> n" using is_aligned_less_sz leI by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned n k; n \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ k \<le> n proof (prove)
using this:
\<lbrakk>is_aligned ?a ?sz; ?a \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> ?a < 2 ^ ?sz
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x

goal (1 subgoal):
 1. \<lbrakk>is_aligned n k; n \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ k \<le> n
theory Aligned

lemma is_aligned_and_2_to_k:
  "(n AND 2 ^ k - 1) = 0 \<Longrightarrow> is_aligned (n :: 'a :: len word) k" by (simp add: is_aligned_mask mask_eq_decr_exp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n AND 2 ^ k - 1 = 0 \<Longrightarrow> is_aligned n k
theory Aligned

lemma is_aligned_power2:
  "b \<le> a \<Longrightarrow> is_aligned (2 ^ a) b" by (metis is_aligned_triv is_aligned_weaken)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> is_aligned (2 ^ a) b
theory Aligned

lemma aligned_sub_aligned':
  "\<lbrakk> is_aligned (a :: 'a :: len word) n; is_aligned b n; n < LENGTH('a) \<rbrakk>
   \<Longrightarrow> is_aligned (a - b) n" by (simp add: aligned_sub_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (a - b) n
theory Aligned

lemma is_aligned_neg_mask_weaken:
  "\<lbrakk> is_aligned p n; m \<le> n \<rbrakk> \<Longrightarrow> p AND NOT (mask m) = p" using is_aligned_neg_mask_eq is_aligned_weaken by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; m \<le> n\<rbrakk> \<Longrightarrow> p AND NOT (mask m) = p proof (prove)
using this:
is_aligned ?p ?n \<Longrightarrow> ?p AND NOT (mask ?n) = ?p
\<lbrakk>is_aligned ?w ?x; ?y \<le> ?x\<rbrakk> \<Longrightarrow> is_aligned ?w ?y

goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; m \<le> n\<rbrakk> \<Longrightarrow> p AND NOT (mask m) = p
theory Aligned

lemma is_aligned_neg_mask2 [simp]:
  "is_aligned (a AND NOT (mask n)) n" by (rule is_aligned_bitI) (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (a AND NOT (mask n)) n
theory Aligned

lemma is_aligned_0':
  "is_aligned 0 n" by (fact is_aligned_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned 0 n
theory Aligned

lemma is_aligned_add_helper:
  "\<lbrakk> is_aligned p n; d < 2 ^ n \<rbrakk>
     \<Longrightarrow> (p + d AND mask n = d) \<and> (p + d AND (NOT (mask n)) = p)" apply (subst (asm) is_aligned_mask) apply (drule less_mask_eq) apply (rule context_conjI) apply (subst word_plus_and_or_coroll) apply (simp_all flip: take_bit_eq_mask) apply (metis take_bit_eq_mask word_bw_lcs(1) word_log_esimps(1)) apply (metis add.commute add_left_imp_eq take_bit_eq_mask word_plus_and_or_coroll2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d AND mask n = d \<and> p + d AND NOT (mask n) = p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p AND mask n = 0; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d AND mask n = d \<and> p + d AND NOT (mask n) = p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND mask n = d \<and> p + d AND NOT (mask n) = p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND mask n = d
 2. \<lbrakk>p AND mask n = 0; d AND mask n = d; p + d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> p AND d = 0
 2. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> (p OR d) AND mask n = d
 3. \<lbrakk>p AND mask n = 0; d AND mask n = d; p + d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>take_bit n p = 0; take_bit n d = d\<rbrakk> \<Longrightarrow> p AND d = 0
 2. \<lbrakk>take_bit n p = 0; take_bit n d = d; take_bit n (p + d) = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_bit n p = 0; take_bit n d = d; take_bit n (p + d) = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p proof (prove)
goal:
No subgoals!
theory Aligned

lemma mask_add_aligned:
  "is_aligned p n \<Longrightarrow> (p + q) AND mask n = q AND mask n" apply (simp add: is_aligned_mask) apply (subst mask_inner_mask [symmetric]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p n \<Longrightarrow> p + q AND mask n = q AND mask n proof (prove)
goal (1 subgoal):
 1. p AND mask n = 0 \<Longrightarrow> p + q AND mask n = q AND mask n proof (prove)
goal (1 subgoal):
 1. p AND mask n = 0 \<Longrightarrow> (p AND mask n) + q AND mask n = q AND mask n proof (prove)
goal:
No subgoals!
theory Aligned

lemma mask_out_add_aligned:
  assumes al: "is_aligned p n"
  shows "p + (q AND NOT (mask n)) = (p + q) AND NOT (mask n)" using mask_add_aligned [OF al] by (simp add: mask_out_sub_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p + (q AND NOT (mask n)) = p + q AND NOT (mask n) proof (prove)
using this:
p + ?q AND mask n = ?q AND mask n

goal (1 subgoal):
 1. p + (q AND NOT (mask n)) = p + q AND NOT (mask n)
theory Aligned

lemma is_aligned_add_or:
  "\<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d = p OR d" apply (subst disjunctive_add, simp_all) apply (clarsimp simp: is_aligned_nth less_2p_is_upper_bits_unset) subgoal for m apply (cases \<open>m < n\<close>) apply (auto simp add: not_less dest: bit_imp_possible_bit) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d = p OR d proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> bit p na \<longrightarrow> \<not> bit d na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p na; bit d na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p m; bit d m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p m; bit d m; m < n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p m; bit d m; \<not> m < n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Aligned

lemma not_greatest_aligned:
  "\<lbrakk> x < y; is_aligned x n; is_aligned y n \<rbrakk> \<Longrightarrow> x + 2 ^ n \<noteq> 0" by (metis NOT_mask add_diff_cancel_right' diff_0 is_aligned_neg_mask_eq not_le word_and_le1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < y; is_aligned x n; is_aligned y n\<rbrakk> \<Longrightarrow> x + 2 ^ n \<noteq> 0
theory Aligned

lemma and_neg_mask_eq_iff_not_mask_le:
  "w AND NOT(mask n) = NOT(mask n) \<longleftrightarrow> NOT(mask n) \<le> w"
  for w :: \<open>'a::len word\<close> by (metis eq_iff neg_mask_mono_le word_and_le1 word_and_le2 word_bw_same(1))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w AND NOT (mask n) = NOT (mask n)) = (NOT (mask n) \<le> w)
theory Aligned

lemma is_aligned_add_less_t2n:
  "\<lbrakk>is_aligned (p::'a::len word) n; d < 2^n; n \<le> m; p < 2^m\<rbrakk> \<Longrightarrow> p + d < 2^m" apply (case_tac "m < LENGTH('a)") apply (subst mask_eq_iff_w2p[symmetric]) apply (simp add: word_size) apply (simp add: is_aligned_add_or word_ao_dist less_mask_eq) apply (subst less_mask_eq) apply (erule order_less_le_trans) apply (erule(1) two_power_increasing) apply simp apply (simp add: power_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> m < size (p + d)
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d AND mask m = p + d
 3. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d AND mask m = p + d
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d AND mask m = p OR d
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> d < 2 ^ m
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d = p OR d
 3. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n \<le> 2 ^ m
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d = p OR d
 3. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d = p OR d
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_no_overflow_mask:
  "is_aligned x n \<Longrightarrow> x \<le> x + mask n" by (simp add: mask_eq_decr_exp) (erule is_aligned_no_overflow')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x n \<Longrightarrow> x \<le> x + mask n