kings-crown/FVELER_Isabelle huggingface dataset:
theory Aligned

lemma is_aligned_imp_not_bit:
  \<open>\<not> bit w m\<close> if \<open>is_aligned w n\<close> and \<open>m < n\<close>
  for w :: \<open>'a::len word\<close> proof - from \<open>is_aligned w n\<close> obtain q where \<open>w = push_bit n (word_of_nat q)\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close> .. moreover have \<open>\<not> bit (push_bit n (word_of_nat q :: 'a word)) m\<close> using \<open>m < n\<close> by (simp add: bit_simps) ultimately show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit w m proof (state)
goal (1 subgoal):
 1. \<not> bit w m proof (chain)
picking this:
is_aligned w n proof (prove)
using this:
is_aligned w n

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> bit w m proof (state)
this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> bit w m proof (prove)
goal (1 subgoal):
 1. \<not> bit (push_bit n (word_of_nat q)) m proof (prove)
using this:
m < n

goal (1 subgoal):
 1. \<not> bit (push_bit n (word_of_nat q)) m proof (state)
this:
\<not> bit (push_bit n (word_of_nat q)) m

goal (1 subgoal):
 1. \<not> bit w m proof (chain)
picking this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)
\<not> bit (push_bit n (word_of_nat q)) m proof (prove)
using this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)
\<not> bit (push_bit n (word_of_nat q)) m

goal (1 subgoal):
 1. \<not> bit w m proof (state)
this:
\<not> bit w m

goal:
No subgoals!
theory Aligned

lemma is_aligned_weaken:
  "\<lbrakk> is_aligned w x; x \<ge> y \<rbrakk> \<Longrightarrow> is_aligned w y" unfolding is_aligned_iff_dvd_nat by (erule dvd_trans [rotated]) (simp add: le_imp_power_dvd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w x; y \<le> x\<rbrakk> \<Longrightarrow> is_aligned w y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ x dvd unat w; y \<le> x\<rbrakk> \<Longrightarrow> 2 ^ y dvd unat w
theory Aligned

lemma is_alignedE_pre:
  fixes w::"'a::len word"
  assumes aligned: "is_aligned w n"
  shows        rl: "\<exists>q. w = 2 ^ n * (of_nat q) \<and> q < 2 ^ (LENGTH('a) - n)" using aligned is_alignedE by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>q. w = 2 ^ n * word_of_nat q \<and> q < 2 ^ (LENGTH('a) - n) proof (prove)
using this:
is_aligned w n
\<lbrakk>is_aligned ?w ?n; \<And>q. \<lbrakk>?w = 2 ^ ?n * word_of_nat q; q < 2 ^ (LENGTH(?'a) - ?n)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>q. w = 2 ^ n * word_of_nat q \<and> q < 2 ^ (LENGTH('a) - n)
theory Aligned

lemma aligned_mod_eq_0:
  fixes p::"'a::len word"
  assumes al: "is_aligned p sz"
  shows   "p mod 2 ^ sz = 0" proof cases assume szv: "sz < LENGTH('a)" with al show ?thesis unfolding is_aligned_iff_dvd_nat by (simp add: and_mask_dvd_nat p2_gt_0 word_mod_2p_is_mask) next assume "\<not> sz < LENGTH('a)" with al show ?thesis by (simp add: is_aligned_mask flip: take_bit_eq_mask take_bit_eq_mod) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p mod 2 ^ sz = 0 proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> p mod 2 ^ sz = 0
 2. \<not> ?P \<Longrightarrow> p mod 2 ^ sz = 0 proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> p mod 2 ^ sz = 0
 2. \<not> ?P \<Longrightarrow> p mod 2 ^ sz = 0 proof (chain)
picking this:
is_aligned p sz
sz < LENGTH('a) proof (prove)
using this:
is_aligned p sz
sz < LENGTH('a)

goal (1 subgoal):
 1. p mod 2 ^ sz = 0 proof (prove)
using this:
2 ^ sz dvd unat p
sz < LENGTH('a)

goal (1 subgoal):
 1. p mod 2 ^ sz = 0 proof (state)
this:
p mod 2 ^ sz = 0

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> p mod 2 ^ sz = 0 proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> p mod 2 ^ sz = 0 proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> p mod 2 ^ sz = 0 proof (chain)
picking this:
is_aligned p sz
\<not> sz < LENGTH('a) proof (prove)
using this:
is_aligned p sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. p mod 2 ^ sz = 0 proof (state)
this:
p mod 2 ^ sz = 0

goal:
No subgoals!
theory Aligned

lemma is_aligned_triv: "is_aligned (2 ^ n ::'a::len word) n" by (rule is_alignedI [where k = 1], simp)

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

lemma is_aligned_mult_triv1: "is_aligned (2 ^ n * x  ::'a::len word) n" by (rule is_alignedI [OF refl])

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

lemma is_aligned_mult_triv2: "is_aligned (x * 2 ^ n ::'a::len word) n" by (subst mult.commute, simp add: is_aligned_mult_triv1)

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

lemma is_aligned_no_overflow':
  fixes p :: "'a::len word"
  assumes al: "is_aligned p n"
  shows "p \<le> p + (2 ^ n - 1)" proof cases assume "n<LENGTH('a)" with al have "2^n - (1::'a::len word) < 2^n" by (simp add: word_less_nat_alt unat_sub_if_size) with al show ?thesis by (rule is_aligned_no_wrap') next assume "\<not> n<LENGTH('a)" with al show ?thesis by (simp add: not_less power_overflow is_aligned_mask mask_2pm1) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<le> p + (2 ^ n - 1) proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<not> ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1) proof (state)
this:
n < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<not> ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1) proof (chain)
picking this:
is_aligned p n
n < LENGTH('a) proof (prove)
using this:
is_aligned p n
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n - 1 < 2 ^ n proof (state)
this:
2 ^ n - 1 < 2 ^ n

goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<not> ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1) proof (chain)
picking this:
is_aligned p n
2 ^ n - 1 < 2 ^ n proof (prove)
using this:
is_aligned p n
2 ^ n - 1 < 2 ^ n

goal (1 subgoal):
 1. p \<le> p + (2 ^ n - 1) proof (state)
this:
p \<le> p + (2 ^ n - 1)

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> p \<le> p + (2 ^ n - 1) proof (state)
goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> p \<le> p + (2 ^ n - 1) proof (state)
this:
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> p \<le> p + (2 ^ n - 1) proof (chain)
picking this:
is_aligned p n
\<not> n < LENGTH('a) proof (prove)
using this:
is_aligned p n
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. p \<le> p + (2 ^ n - 1) proof (state)
this:
p \<le> p + (2 ^ n - 1)

goal:
No subgoals!
theory Aligned

lemma is_aligned_no_overflow:
  "is_aligned ptr sz \<Longrightarrow> ptr \<le> ptr + 2^sz - 1" by (drule is_aligned_no_overflow') (simp add: field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> ptr \<le> ptr + 2 ^ sz - 1
theory Aligned

lemma replicate_not_True:
  "\<And>n. xs = replicate n False \<Longrightarrow> True \<notin> set xs" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>n. xs = replicate n False \<Longrightarrow> True \<notin> set xs
theory Aligned

lemma map_zip_replicate_False_xor:
  "n = length xs \<Longrightarrow> map (\<lambda>(x, y). x = (\<not> y)) (zip xs (replicate n False)) = xs" by (induct xs arbitrary: n, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> map2 (\<lambda>x y. x = (\<not> y)) xs (replicate n False) = xs
theory Aligned

lemma drop_minus:
  "\<lbrakk> n < length xs; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - Suc n) xs = rev xs ! n  # drop (n' - n) xs" apply (subst drop_minus_lem) apply simp apply simp apply simp apply simp apply (cases "length xs", simp) apply (simp add: Suc_diff_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - Suc n) xs = rev xs ! n # drop (n' - n) xs proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> Suc n \<le> length xs
 2. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> 0 < Suc n
 3. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> n' = length xs
 4. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> 0 < Suc n
 2. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> n' = length xs
 3. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> n' = length xs
 2. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> drop (Suc (length xs - Suc n)) xs = drop (length xs - n) xs proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>n < length xs; n' = length xs; length xs = Suc nat\<rbrakk> \<Longrightarrow> drop (Suc (length xs - Suc n)) xs = drop (length xs - n) xs proof (prove)
goal:
No subgoals!
theory Aligned

lemma aligned_add_xor:
  \<open>(x + 2 ^ n) XOR 2 ^ n = x\<close>
  if al: \<open>is_aligned (x::'a::len word) n'\<close> and le: \<open>n < n'\<close> proof - have \<open>\<not> bit x n\<close> using that by (rule is_aligned_imp_not_bit) then have \<open>x + 2 ^ n = x OR 2 ^ n\<close> by (subst disjunctive_add) (auto simp add: bit_simps disjunctive_add) moreover have \<open>(x OR 2 ^ n) XOR 2 ^ n = x\<close> by (rule bit_word_eqI) (auto simp add: bit_simps \<open>\<not> bit x n\<close>) ultimately show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x proof (state)
goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x proof (prove)
goal (1 subgoal):
 1. \<not> bit x n proof (prove)
using this:
is_aligned x n'
n < n'

goal (1 subgoal):
 1. \<not> bit x n proof (state)
this:
\<not> bit x n

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x proof (chain)
picking this:
\<not> bit x n proof (prove)
using this:
\<not> bit x n

goal (1 subgoal):
 1. x + 2 ^ n = x OR 2 ^ n proof (state)
this:
x + 2 ^ n = x OR 2 ^ n

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x proof (state)
this:
x + 2 ^ n = x OR 2 ^ n

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x proof (prove)
goal (1 subgoal):
 1. (x OR 2 ^ n) XOR 2 ^ n = x proof (state)
this:
(x OR 2 ^ n) XOR 2 ^ n = x

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x proof (chain)
picking this:
x + 2 ^ n = x OR 2 ^ n
(x OR 2 ^ n) XOR 2 ^ n = x proof (prove)
using this:
x + 2 ^ n = x OR 2 ^ n
(x OR 2 ^ n) XOR 2 ^ n = x

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x proof (state)
this:
x + 2 ^ n XOR 2 ^ n = x

goal:
No subgoals!
theory Aligned

lemma is_aligned_add_mult_multI:
  fixes p :: "'a::len word"
  shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n * z) n'" apply (erule aligned_add_aligned) apply (auto intro: is_alignedI [where k="x*z"]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n * z) n' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (x * 2 ^ n * z) n'
 2. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> n' \<le> m proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_add_multI:
  fixes p :: "'a::len word"
  shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n) n'" apply (erule aligned_add_aligned) apply (auto intro: is_alignedI [where k="x"]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n) n' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (x * 2 ^ n) n'
 2. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> n' \<le> m proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_no_wrap''':
  fixes ptr :: "'a::len word"
  shows"\<lbrakk> is_aligned ptr sz; sz < LENGTH('a); off < 2 ^ sz \<rbrakk>
         \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)" apply (drule is_aligned_no_wrap[where off="of_nat off"]) apply (simp add: word_less_nat_alt) apply (erule order_le_less_trans[rotated]) apply (simp add: take_bit_eq_mod unsigned_of_nat) apply (subst(asm) unat_of_nat_len) apply (erule order_less_trans) apply (erule power_strict_increasing) apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> word_of_nat off < 2 ^ sz
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (word_of_nat off) < 2 ^ sz
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (word_of_nat off) \<le> off
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> off < 2 ^ LENGTH('a)
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH('a)
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. 1 < 2
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_get_word_bits:
  fixes p :: "'a::len word"
  shows "\<lbrakk> is_aligned p n; \<lbrakk> is_aligned p n; n < LENGTH('a) \<rbrakk> \<Longrightarrow> P;
           \<lbrakk> p = 0; n \<ge> LENGTH('a) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" apply (cases "n < LENGTH('a)") apply simp apply simp apply (erule meta_mp) apply (simp add: is_aligned_mask power_add power_overflow not_less
    flip: take_bit_eq_mask) apply (metis take_bit_length_eq take_bit_of_0 take_bit_tightened) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; p = 0 \<Longrightarrow> P; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> p = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_bit n p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p = 0 proof (prove)
goal:
No subgoals!
theory Aligned

lemma aligned_small_is_0:
  "\<lbrakk> is_aligned x n; x < 2 ^ n \<rbrakk> \<Longrightarrow> x = 0" by (simp add: is_aligned_mask less_mask_eq)

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

lemma aligned_at_least_t2n_diff:
  "\<lbrakk>is_aligned x n; is_aligned y n; x < y\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n" apply (erule is_aligned_get_word_bits[where p=y]) apply (rule ccontr) apply (clarsimp simp: linorder_not_le) apply (subgoal_tac "y - x = 0") apply clarsimp apply (rule aligned_small_is_0) apply (erule(1) aligned_sub_aligned) apply simp apply unat_arith apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; x < y\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); \<not> x \<le> y - 2 ^ n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x; y - x = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x = 0
 3. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x = 0
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> is_aligned (y - x) ?n8
 2. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x < 2 ^ ?n8
 3. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> n \<le> n
 2. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x < 2 ^ n
 3. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x < 2 ^ n
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_aligned_no_overflow'':
  "\<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n" apply (frule is_aligned_no_overflow') apply (erule order_trans) apply (simp add: field_simps) apply (erule word_sub_1_le) done

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

lemma is_aligned_nth:
  "is_aligned p m = (\<forall>n < m. \<not> bit p n)" apply (auto intro: is_aligned_bitI simp add: is_aligned_mask bit_eq_iff) apply (auto simp: bit_simps) using bit_imp_le_length not_less apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p m = (\<forall>n<m. \<not> bit p n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n<LENGTH('a). \<not> bit (p AND mask m) n; n < m; bit p n\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>\<forall>n<m. \<not> bit p n; n < LENGTH('a); bit (p AND mask m) n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n<LENGTH('a). bit p n \<longrightarrow> \<not> n < m; n < m; bit p n\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
bit ?w ?n \<Longrightarrow> ?n < LENGTH(?'a)
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n<LENGTH('a). bit p n \<longrightarrow> \<not> n < m; n < m; bit p n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Aligned

lemma range_inter:
  "({a..b} \<inter> {c..d} = {}) = (\<forall>x. \<not>(a \<le> x \<and> x \<le> b \<and> c \<le> x \<and> x \<le> d))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({a..b} \<inter> {c..d} = {}) = (\<forall>x. \<not> (a \<le> x \<and> x \<le> b \<and> c \<le> x \<and> x \<le> d))