kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

lemma ucast_or_distrib:
  fixes x :: "'a::len word"
  fixes y :: "'a::len word"
  shows "(ucast (x OR y) :: ('b::len) word) = ucast x OR ucast y" by (fact unsigned_or_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ucast (x OR y) = ucast x OR ucast y
theory More_Word

lemma word_exists_nth:
  "(w::'a::len word) \<noteq> 0 \<Longrightarrow> \<exists>i. bit w i" by (auto simp add: bit_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> \<exists>i. bit w i
theory More_Word

lemma max_word_not_0 [simp]:
  "- 1 \<noteq> (0 :: 'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 \<noteq> 0
theory More_Word

lemma unat_max_word_pos[simp]: "0 < unat (- 1 :: 'a::len word)" using unat_gt_0 [of \<open>- 1 :: 'a::len word\<close>] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < unat (- 1) proof (prove)
using this:
(0 < unat (- 1)) = (- 1 \<noteq> 0)

goal (1 subgoal):
 1. 0 < unat (- 1)
theory More_Word

lemma word_of_nat_inj:
  assumes bounded: "x < 2 ^ LENGTH('a)" "y < 2 ^ LENGTH('a)"
  assumes of_nats: "of_nat x = (of_nat y :: 'a::len word)"
  shows "x = y" by (rule contrapos_pp[OF of_nats]; cases "x < y"; cases "y < x")
     (auto dest: bounded[THEN of_nat_mono_maybe])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y
theory More_Word

lemma word_of_int_bin_cat_eq_iff:
  "(word_of_int (concat_bit LENGTH('b) (uint b) (uint a))::'c::len word) =
  word_of_int (concat_bit LENGTH('b) (uint d) (uint c)) \<longleftrightarrow> b = d \<and> a = c"
  if "LENGTH('a) + LENGTH('b) \<le> LENGTH('c)"
  for a::"'a::len word" and b::"'b::len word" proof - from that show ?thesis using that concat_bit_eq_iff [of \<open>LENGTH('b)\<close> \<open>uint b\<close> \<open>uint a\<close> \<open>uint d\<close> \<open>uint c\<close>] apply (simp add: word_of_int_eq_iff take_bit_int_eq_self flip: word_eq_iff_unsigned) apply (simp add: concat_bit_def take_bit_int_eq_self bintr_uint take_bit_push_bit) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (word_of_int (concat_bit LENGTH('b) (uint b) (uint a)) = word_of_int (concat_bit LENGTH('b) (uint d) (uint c))) = (b = d \<and> a = c) proof (state)
goal (1 subgoal):
 1. (word_of_int (concat_bit LENGTH('b) (uint b) (uint a)) = word_of_int (concat_bit LENGTH('b) (uint d) (uint c))) = (b = d \<and> a = c) proof (chain)
picking this:
LENGTH('a) + LENGTH('b) \<le> LENGTH('c) proof (prove)
using this:
LENGTH('a) + LENGTH('b) \<le> LENGTH('c)

goal (1 subgoal):
 1. (word_of_int (concat_bit LENGTH('b) (uint b) (uint a)) = word_of_int (concat_bit LENGTH('b) (uint d) (uint c))) = (b = d \<and> a = c) proof (prove)
using this:
LENGTH('a) + LENGTH('b) \<le> LENGTH('c)
LENGTH('a) + LENGTH('b) \<le> LENGTH('c)
(concat_bit LENGTH('b) (uint b) (uint a) = concat_bit LENGTH('b) (uint d) (uint c)) = (take_bit LENGTH('b) (uint b) = take_bit LENGTH('b) (uint d) \<and> uint a = uint c)

goal (1 subgoal):
 1. (word_of_int (concat_bit LENGTH('b) (uint b) (uint a)) = word_of_int (concat_bit LENGTH('b) (uint d) (uint c))) = (b = d \<and> a = c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('a) + LENGTH('b) \<le> LENGTH('c); (concat_bit LENGTH('b) (uint b) (uint a) = concat_bit LENGTH('b) (uint d) (uint c)) = (b = d \<and> a = c)\<rbrakk> \<Longrightarrow> (take_bit LENGTH('c) (concat_bit LENGTH('b) (uint b) (uint a)) = take_bit LENGTH('c) (concat_bit LENGTH('b) (uint d) (uint c))) = (b = d \<and> a = c) proof (prove)
goal:
No subgoals! proof (state)
this:
(word_of_int (concat_bit LENGTH('b) (uint b) (uint a)) = word_of_int (concat_bit LENGTH('b) (uint d) (uint c))) = (b = d \<and> a = c)

goal:
No subgoals!
theory More_Word

lemma word_cat_inj: "(word_cat a b::'c::len word) = word_cat c d \<longleftrightarrow> a = c \<and> b = d"
  if "LENGTH('a) + LENGTH('b) \<le> LENGTH('c)"
  for a::"'a::len word" and b::"'b::len word" using word_of_int_bin_cat_eq_iff [OF that, of b a d c] by (simp add: word_cat_eq' ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (word_cat a b = word_cat c d) = (a = c \<and> b = d) proof (prove)
using this:
(word_of_int (concat_bit LENGTH('b) (uint b) (uint a)) = word_of_int (concat_bit LENGTH('b) (uint d) (uint c))) = (b = d \<and> a = c)

goal (1 subgoal):
 1. (word_cat a b = word_cat c d) = (a = c \<and> b = d)
theory More_Word

lemma p2_eq_1: "2 ^ n = (1::'a::len word) \<longleftrightarrow> n = 0" proof - have "2 ^ n = (1::'a word) \<Longrightarrow> n = 0" by (metis One_nat_def not_less one_less_numeral_iff p2_eq_0 p2_gt_0 power_0 power_0
        power_inject_exp semiring_norm(76) unat_power_lower zero_neq_one) then show ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 ^ n = 1) = (n = 0) proof (state)
goal (1 subgoal):
 1. (2 ^ n = 1) = (n = 0) proof (prove)
goal (1 subgoal):
 1. 2 ^ n = 1 \<Longrightarrow> n = 0 proof (state)
this:
2 ^ n = 1 \<Longrightarrow> n = 0

goal (1 subgoal):
 1. (2 ^ n = 1) = (n = 0) proof (chain)
picking this:
2 ^ n = 1 \<Longrightarrow> n = 0 proof (prove)
using this:
2 ^ n = 1 \<Longrightarrow> n = 0

goal (1 subgoal):
 1. (2 ^ n = 1) = (n = 0) proof (state)
this:
(2 ^ n = 1) = (n = 0)

goal:
No subgoals!
theory More_Word

lemma bin_nth_minus_Bit0[simp]:
  "0 < n \<Longrightarrow> bit (numeral (num.Bit0 w) :: int) n = bit (numeral w :: int) (n - 1)" by (cases n; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bit (numeral (num.Bit0 w)) n = bit (numeral w) (n - 1)
theory More_Word

lemma bin_nth_minus_Bit1[simp]:
  "0 < n \<Longrightarrow> bit (numeral (num.Bit1 w) :: int) n = bit (numeral w :: int) (n - 1)" by (cases n; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bit (numeral (num.Bit1 w)) n = bit (numeral w) (n - 1)
theory More_Word

lemma word_mod_by_0: "k mod (0::'a::len word) = k" by (simp add: word_arith_nat_mod)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k mod 0 = k
theory Bit_Shifts_Infix_Syntax

lemma bit_shiftl_iff [bit_simps]:
  \<open>bit (a << m) n \<longleftrightarrow> m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m)\<close> by (simp add: shiftl_def bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (a << m) n = (m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m))
theory Bit_Shifts_Infix_Syntax

lemma bit_sshiftr_iff [bit_simps]:
  \<open>bit (w >>> m) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
  for w :: \<open>'a::len word\<close> by (simp add: sshiftr_def bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (w >>> m) n = bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)
theory Bit_Shifts_Infix_Syntax

lemma shiftl_word_transfer [transfer_rule]:
  \<open>(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. push_bit n k) (<<)\<close> apply (unfold shiftl_def) apply transfer_prover done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. push_bit n k) (<<) proof (prove)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. push_bit n k) (\<lambda>a n. push_bit n a) proof (prove)
goal:
No subgoals!
theory Bit_Shifts_Infix_Syntax

lemma shiftr_word_transfer [transfer_rule]:
  \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
    (\<lambda>k n. drop_bit n (take_bit LENGTH('a) k))
    (>>)\<close> proof - have \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
    (\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k)
    (>>)\<close> by (unfold shiftr_def) transfer_prover then show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)) (>>) proof (state)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)) (>>) proof (prove)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k) (>>) proof (state)
this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k) (>>)

goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)) (>>) proof (chain)
picking this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k) (>>) proof (prove)
using this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k) (>>)

goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)) (>>) proof (state)
this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)) (>>)

goal:
No subgoals!
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_transfer [transfer_rule]:
  \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
    (\<lambda>k n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))
    (>>>)\<close> proof - have \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
    (\<lambda>k n. (drop_bit n \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k)
    (>>>)\<close> by (unfold sshiftr_def) transfer_prover then show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k)) (>>>) proof (state)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k)) (>>>) proof (prove)
goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k) (>>>) proof (state)
this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k) (>>>)

goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k)) (>>>) proof (chain)
picking this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k) (>>>) proof (prove)
using this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k) (>>>)

goal (1 subgoal):
 1. (pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k)) (>>>) proof (state)
this:
(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k)) (>>>)

goal:
No subgoals!
theory Bit_Shifts_Infix_Syntax

lemma shiftl_0 [simp]:
  \<open>0 << n = 0\<close> by (simp add: shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0::'a) << n = (0::'a)
theory Bit_Shifts_Infix_Syntax

lemma shiftl_of_0 [simp]:
  \<open>a << 0 = a\<close> by (simp add: shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a << 0 = a
theory Bit_Shifts_Infix_Syntax

lemma shiftl_of_Suc [simp]:
  \<open>a << Suc n = (a * 2) << n\<close> by (simp add: shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a << Suc n = a * (2::'a) << n
theory Bit_Shifts_Infix_Syntax

lemma shiftl_1 [simp]:
  \<open>1 << n = 2 ^ n\<close> by (simp add: shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (1::'a) << n = (2::'a) ^ n
theory Bit_Shifts_Infix_Syntax

lemma shiftl_numeral_numeral [simp]:
  \<open>numeral m << numeral n = push_bit (numeral n) (numeral m)\<close> by (fact shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral m << numeral n = push_bit (numeral n) (numeral m)
theory Bit_Shifts_Infix_Syntax

lemma shiftr_0 [simp]:
  \<open>0 >> n = 0\<close> by (simp add: shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0::'a) >> n = (0::'a)
theory Bit_Shifts_Infix_Syntax

lemma shiftr_of_0 [simp]:
  \<open>a >> 0 = a\<close> by (simp add: shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a >> 0 = a
theory Bit_Shifts_Infix_Syntax

lemma shiftr_numeral_Suc [simp]:
  \<open>numeral m >> Suc n = drop_bit (Suc n) (numeral m)\<close> by (fact shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral m >> Suc n = drop_bit (Suc n) (numeral m)
theory Bit_Shifts_Infix_Syntax

lemma shiftr_numeral_numeral [simp]:
  \<open>numeral m >> numeral n = drop_bit (numeral n) (numeral m)\<close> by (fact shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral m >> numeral n = drop_bit (numeral n) (numeral m)
theory Bit_Shifts_Infix_Syntax

lemma shiftl_eq_mult:
  \<open>x << n = x * 2 ^ n\<close> unfolding shiftl_def by (fact push_bit_eq_mult)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x << n = x * (2::'a) ^ n proof (prove)
goal (1 subgoal):
 1. push_bit n x = x * (2::'a) ^ n
theory Bit_Shifts_Infix_Syntax

lemma shiftr_eq_div:
  \<open>x >> n = x div 2 ^ n\<close> unfolding shiftr_def by (fact drop_bit_eq_div)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >> n = x div (2::'a) ^ n proof (prove)
goal (1 subgoal):
 1. drop_bit n x = x div (2::'a) ^ n
theory Bit_Shifts_Infix_Syntax

lemma shiftl_minus_1_numeral [simp]:
  \<open>- 1 << numeral n = NOT (mask (numeral n))\<close> by (simp add: shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (1::'a) << numeral n = NOT (mask (numeral n))
theory Bit_Shifts_Infix_Syntax

lemma shiftr_Suc_0 [simp]:
  \<open>Suc 0 >> n = of_bool (n = 0)\<close> by (simp add: shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc 0 >> n = of_bool (n = 0)
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_numeral_Suc [simp]:
  \<open>numeral m >>> Suc n = signed_drop_bit (Suc n) (numeral m)\<close> by (fact sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral m >>> Suc n = signed_drop_bit (Suc n) (numeral m)
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_numeral_numeral [simp]:
  \<open>numeral m >>> numeral n = signed_drop_bit (numeral n) (numeral m)\<close> by (fact sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. numeral m >>> numeral n = signed_drop_bit (numeral n) (numeral m)
theory Bit_Shifts_Infix_Syntax

lemma shiftl_minus_numeral_Suc [simp]:
  \<open>- numeral m << Suc n = push_bit (Suc n) (- numeral m)\<close> by (fact shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral m << Suc n = push_bit (Suc n) (- numeral m)
theory Bit_Shifts_Infix_Syntax

lemma shiftl_minus_numeral_numeral [simp]:
  \<open>- numeral m << numeral n = push_bit (numeral n) (- numeral m)\<close> by (fact shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral m << numeral n = push_bit (numeral n) (- numeral m)
theory Bit_Shifts_Infix_Syntax

lemma shiftr_minus_numeral_Suc [simp]:
  \<open>- numeral m >> Suc n = drop_bit (Suc n) (- numeral m)\<close> by (fact shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral m >> Suc n = drop_bit (Suc n) (- numeral m)
theory Bit_Shifts_Infix_Syntax

lemma shiftr_minus_numeral_numeral [simp]:
  \<open>- numeral m >> numeral n = drop_bit (numeral n) (- numeral m)\<close> by (fact shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral m >> numeral n = drop_bit (numeral n) (- numeral m)
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_0 [simp]:
  \<open>0 >>> n = 0\<close> by (simp add: sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 >>> n = 0
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_of_0 [simp]:
  \<open>w >>> 0 = w\<close> by (simp add: sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w >>> 0 = w
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_1 [simp]:
  \<open>(1 :: 'a::len word) >>> n = of_bool (LENGTH('a) = 1 \<or> n = 0)\<close> by (simp add: sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 >>> n = of_bool (LENGTH('a) = 1 \<or> n = 0)
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_minus_numeral_Suc [simp]:
  \<open>- numeral m >>> Suc n = signed_drop_bit (Suc n) (- numeral m)\<close> by (fact sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral m >>> Suc n = signed_drop_bit (Suc n) (- numeral m)
theory Bit_Shifts_Infix_Syntax

lemma sshiftr_minus_numeral_numeral [simp]:
  \<open>- numeral m >>> numeral n = signed_drop_bit (numeral n) (- numeral m)\<close> by (fact sshiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral m >>> numeral n = signed_drop_bit (numeral n) (- numeral m)
theory Aligned

lemma is_aligned_iff_udvd:
  \<open>is_aligned w n \<longleftrightarrow> 2 ^ n udvd w\<close> by transfer (simp flip: take_bit_eq_0_iff add: min_def)

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

lemma is_aligned_iff_take_bit_eq_0:
  \<open>is_aligned w n \<longleftrightarrow> take_bit n w = 0\<close> by (simp add: is_aligned_iff_udvd take_bit_eq_0_iff exp_dvd_iff_exp_udvd)

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

lemma is_aligned_iff_dvd_int:
  \<open>is_aligned ptr n \<longleftrightarrow> 2 ^ n dvd uint ptr\<close> by transfer simp

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

lemma is_aligned_iff_dvd_nat:
  \<open>is_aligned ptr n \<longleftrightarrow> 2 ^ n dvd unat ptr\<close> proof - have \<open>unat ptr = nat \<bar>uint ptr\<bar>\<close> by transfer simp then have \<open>2 ^ n dvd unat ptr \<longleftrightarrow> 2 ^ n dvd uint ptr\<close> by (simp only: dvd_nat_abs_iff) simp then show ?thesis by (simp add: is_aligned_iff_dvd_int) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr) proof (state)
goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr) proof (prove)
goal (1 subgoal):
 1. unat ptr = nat \<bar>uint ptr\<bar> proof (state)
this:
unat ptr = nat \<bar>uint ptr\<bar>

goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr) proof (chain)
picking this:
unat ptr = nat \<bar>uint ptr\<bar> proof (prove)
using this:
unat ptr = nat \<bar>uint ptr\<bar>

goal (1 subgoal):
 1. (2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr) proof (state)
this:
(2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr)

goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr) proof (chain)
picking this:
(2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr) proof (prove)
using this:
(2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr)

goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr) proof (state)
this:
is_aligned ptr n = (2 ^ n dvd unat ptr)

goal:
No subgoals!
theory Aligned

lemma is_aligned_0 [simp]:
  \<open>is_aligned 0 n\<close> by transfer simp

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

lemma is_aligned_at_0 [simp]:
  \<open>is_aligned w 0\<close> by transfer simp

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

lemma is_aligned_beyond_length:
  \<open>is_aligned w n \<longleftrightarrow> w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close> using that apply (simp add: is_aligned_iff_udvd) apply transfer apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned w n = (w = 0) proof (prove)
using this:
LENGTH('a) \<le> n

goal (1 subgoal):
 1. is_aligned w n = (w = 0) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> (2 ^ n udvd w) = (w = 0) proof (prove)
goal (1 subgoal):
 1. \<And>n w. LENGTH('a) \<le> n \<Longrightarrow> (take_bit LENGTH('a) (2 ^ n) dvd take_bit LENGTH('a) w) = (take_bit LENGTH('a) w = take_bit LENGTH('a) 0) proof (prove)
goal:
No subgoals!
theory Aligned

lemma is_alignedI [intro?]:
  \<open>is_aligned x n\<close> if \<open>x = 2 ^ n * k\<close> for x :: \<open>'a::len word\<close> proof (unfold is_aligned_iff_udvd) from that show \<open>2 ^ n udvd x\<close> using dvd_triv_left exp_dvd_iff_exp_udvd by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x n proof (state)
goal (1 subgoal):
 1. 2 ^ n udvd x proof (chain)
picking this:
x = 2 ^ n * k proof (prove)
using this:
x = 2 ^ n * k

goal (1 subgoal):
 1. 2 ^ n udvd x proof (prove)
using this:
x = 2 ^ n * k
?a dvd ?a * ?b
(2 ^ ?n dvd ?w) = (2 ^ ?n udvd ?w)

goal (1 subgoal):
 1. 2 ^ n udvd x proof (state)
this:
2 ^ n udvd x

goal:
No subgoals!
theory Aligned

lemma is_alignedE' [elim?]:
  fixes w :: \<open>'a::len word\<close>
  assumes \<open>is_aligned w n\<close>
  obtains q where \<open>w = push_bit n (word_of_nat q)\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close> proof - from assms obtain q where \<open>w = 2 ^ n * word_of_nat q\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close> by (rule is_alignedE) then have \<open>w = push_bit n (word_of_nat q)\<close> by (simp add: push_bit_eq_mult) with that show thesis using \<open>q < 2 ^ (LENGTH('a) - n)\<close> . qed

(* Proof state trace *)
proof (prove)
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)
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 (chain)
picking this:
is_aligned w n proof (prove)
using this:
is_aligned w n

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - 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 (chain)
picking this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n) proof (prove)
using this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. w = push_bit n (word_of_nat q) proof (state)
this:
w = push_bit n (word_of_nat q)

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 (chain)
picking this:
\<lbrakk>w = push_bit n (word_of_nat ?q); ?q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = push_bit n (word_of_nat q) proof (prove)
using this:
\<lbrakk>w = push_bit n (word_of_nat ?q); ?q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = push_bit n (word_of_nat q)

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

goal (1 subgoal):
 1. thesis proof (state)
this:
thesis

goal:
No subgoals!
theory Aligned

lemma is_aligned_mask:
  \<open>is_aligned w n \<longleftrightarrow> w AND mask n = 0\<close> by (simp add: is_aligned_iff_take_bit_eq_0 take_bit_eq_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned w n = (w AND mask n = 0)