kings-crown/FVELER_Isabelle huggingface dataset:
theory More_Word

lemma test_bit_wi:
  "bit (word_of_int x :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit x n" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (word_of_int x) n = (n < LENGTH('a) \<and> bit x n)
theory More_Word

lemma word_ao_nth:
  "bit (x OR y) n = (bit x n | bit y n) \<and>
    bit (x AND y) n = (bit x n \<and> bit y n)"
  for x :: "'a::len word" by transfer (auto simp add: bit_or_iff bit_and_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (x OR y) n = (bit x n \<or> bit y n) \<and> bit (x AND y) n = (bit x n \<and> bit y n)
theory More_Word

lemma nth_sint:
  fixes w :: "'a::len word"
  defines "l \<equiv> LENGTH('a)"
  shows "bit (sint w) n = (if n < l - 1 then bit w n else bit w (l - 1))" unfolding sint_uint l_def by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (sint w) n = (if n < l - 1 then bit w n else bit w (l - 1)) proof (prove)
goal (1 subgoal):
 1. bit (signed_take_bit (LENGTH('a) - Suc 0) (uint w)) n = (if n < LENGTH('a) - 1 then bit w n else bit w (LENGTH('a) - 1))
theory More_Word

lemma test_bit_2p: "bit (word_of_int (2 ^ n)::'a::len word) m \<longleftrightarrow> m = n \<and> m < LENGTH('a)" by transfer (auto simp add: bit_exp_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (word_of_int (2 ^ n)) m = (m = n \<and> m < LENGTH('a))
theory More_Word

lemma nth_w2p: "bit ((2::'a::len word) ^ n) m \<longleftrightarrow> m = n \<and> m < LENGTH('a::len)" by transfer (auto simp add: bit_exp_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (2 ^ n) m = (m = n \<and> m < LENGTH('a))
theory More_Word

lemma bang_is_le: "bit x m \<Longrightarrow> 2 ^ m \<le> x"
  for x :: "'a::len word" apply (rule xtrans(3)) apply (rule_tac [2] y = "x" in le_word_or2) apply (rule word_eqI) apply (auto simp add: word_ao_nth nth_w2p word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit x m \<Longrightarrow> 2 ^ m \<le> x proof (prove)
goal (2 subgoals):
 1. bit x m \<Longrightarrow> x = ?b
 2. bit x m \<Longrightarrow> 2 ^ m \<le> ?b proof (prove)
goal (1 subgoal):
 1. bit x m \<Longrightarrow> x = 2 ^ m OR x proof (prove)
goal (1 subgoal):
 1. \<And>n. bit x m \<Longrightarrow> n < size x \<longrightarrow> bit x n = bit (2 ^ m OR x) n proof (prove)
goal:
No subgoals!
theory More_Word

lemma test_bit_1 [iff]: "bit (1 :: 'a::len word) n \<longleftrightarrow> n = 0" by transfer (auto simp add: bit_1_iff)

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

lemma nth_0: "\<not> bit (0 :: 'a::len word) n" by transfer simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> bit 0 n
theory More_Word

lemma nth_ucast_weak:
  "bit (ucast w::'a::len word) n = (bit w n \<and> n < LENGTH('a))" by transfer (simp add: bit_take_bit_iff ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (ucast w) n = (bit w n \<and> n < LENGTH('a))
theory More_Word

lemma nth_ucast:
  "bit (ucast (w::'a::len word)::'b::len word) n =
   (bit w n \<and> n < min LENGTH('a) LENGTH('b))" by (auto simp: not_le nth_ucast_weak dest: bit_imp_le_length)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (ucast w) n = (bit w n \<and> n < min LENGTH('a) LENGTH('b))
theory More_Word

lemma nth_mask:
  \<open>bit (mask n :: 'a::len word) i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close> by (auto simp add: word_size Word.bit_mask_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (mask n) i = (i < n \<and> i < size (mask n))
theory More_Word

lemma nth_slice: "bit (slice n w :: 'a::len word) m = (bit w (m + n) \<and> m < LENGTH('a))" apply (auto simp add: bit_simps less_diff_conv dest: bit_imp_le_length) using bit_imp_le_length apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (slice n w) m = (bit w (m + n) \<and> m < LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bit w (m + n); m < LENGTH('a)\<rbrakk> \<Longrightarrow> bit w (m + LENGTH('b) - (LENGTH('b) - n)) proof (prove)
using this:
bit ?w ?n \<Longrightarrow> ?n < LENGTH(?'a)

goal (1 subgoal):
 1. \<lbrakk>bit w (m + n); m < LENGTH('a)\<rbrakk> \<Longrightarrow> bit w (m + LENGTH('b) - (LENGTH('b) - n)) proof (prove)
goal:
No subgoals!
theory More_Word

lemma test_bit_cat [OF refl]:
  "wc = word_cat a b \<Longrightarrow> bit wc n = (n < size wc \<and>
    (if n < size b then bit b n else bit a (n - size b)))" apply (simp add: word_size not_less; transfer) apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff) done

\<comment> \<open>keep quantifiers for use in simplification\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wc = word_cat a b \<Longrightarrow> bit wc n = (n < size wc \<and> (if n < size b then bit b n else bit a (n - size b))) proof (prove)
goal (1 subgoal):
 1. \<And>wc a b n. take_bit LENGTH('a) wc = take_bit LENGTH('a) (concat_bit LENGTH('c) b (take_bit LENGTH('b) a)) \<Longrightarrow> (n < LENGTH('c) \<longrightarrow> (n < LENGTH('a) \<and> bit (concat_bit LENGTH('c) b (take_bit LENGTH('b) a)) n) = (n < LENGTH('a) \<and> n < LENGTH('c) \<and> bit b n)) \<and> (LENGTH('c) \<le> n \<longrightarrow> (n < LENGTH('a) \<and> bit (concat_bit LENGTH('c) b (take_bit LENGTH('b) a)) n) = (n < LENGTH('a) \<and> n - LENGTH('c) < LENGTH('b) \<and> bit a (n - LENGTH('c)))) proof (prove)
goal:
No subgoals!
theory More_Word

lemma test_bit_split':
  "word_split c = (a, b) \<longrightarrow>
    (\<forall>n m.
      bit b n = (n < size b \<and> bit c n) \<and>
      bit a m = (m < size a \<and> bit c (m + size b)))" by (auto simp add: word_split_bin' bit_unsigned_iff word_size bit_drop_bit_eq ac_simps
           dest: bit_imp_le_length)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_split c = (a, b) \<longrightarrow> (\<forall>n m. bit b n = (n < size b \<and> bit c n) \<and> bit a m = (m < size a \<and> bit c (m + size b)))
theory More_Word

lemma test_bit_split:
  "word_split c = (a, b) \<Longrightarrow>
    (\<forall>n::nat. bit b n \<longleftrightarrow> n < size b \<and> bit c n) \<and>
    (\<forall>m::nat. bit a m \<longleftrightarrow> m < size a \<and> bit c (m + size b))" by (simp add: test_bit_split')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_split c = (a, b) \<Longrightarrow> (\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b)))
theory More_Word

lemma test_bit_split_eq:
  "word_split c = (a, b) \<longleftrightarrow>
    ((\<forall>n::nat. bit b n = (n < size b \<and> bit c n)) \<and>
     (\<forall>m::nat. bit a m = (m < size a \<and> bit c (m + size b))))" apply (rule_tac iffI) apply (rule_tac conjI) apply (erule test_bit_split [THEN conjunct1]) apply (erule test_bit_split [THEN conjunct2]) apply (case_tac "word_split c") apply (frule test_bit_split) apply (erule trans) apply (fastforce intro!: word_eqI simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (word_split c = (a, b)) = ((\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b)))) proof (prove)
goal (2 subgoals):
 1. word_split c = (a, b) \<Longrightarrow> (\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b)))
 2. (\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b))) \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (3 subgoals):
 1. word_split c = (a, b) \<Longrightarrow> \<forall>n. bit b n = (n < size b \<and> bit c n)
 2. word_split c = (a, b) \<Longrightarrow> \<forall>m. bit a m = (m < size a \<and> bit c (m + size b))
 3. (\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b))) \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (2 subgoals):
 1. word_split c = (a, b) \<Longrightarrow> \<forall>m. bit a m = (m < size a \<and> bit c (m + size b))
 2. (\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b))) \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (1 subgoal):
 1. (\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b))) \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b))); word_split c = (aa, ba)\<rbrakk> \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b))); word_split c = (aa, ba); (\<forall>n. bit ba n = (n < size ba \<and> bit c n)) \<and> (\<forall>m. bit aa m = (m < size aa \<and> bit c (m + size ba)))\<rbrakk> \<Longrightarrow> word_split c = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(\<forall>n. bit b n = (n < size b \<and> bit c n)) \<and> (\<forall>m. bit a m = (m < size a \<and> bit c (m + size b))); (\<forall>n. bit ba n = (n < size ba \<and> bit c n)) \<and> (\<forall>m. bit aa m = (m < size aa \<and> bit c (m + size ba)))\<rbrakk> \<Longrightarrow> (aa, ba) = (a, b) proof (prove)
goal:
No subgoals!
theory More_Word

lemma test_bit_rcat:
  "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> bit rc n =
    (n < size rc \<and> n div sw < size wl \<and> bit ((rev wl) ! (n div sw)) (n mod sw))"
  for wl :: "'a::len word list" by (simp add: word_size word_rcat_def rev_map bit_horner_sum_uint_exp_iff bit_simps not_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = size (hd wl); rc = word_rcat wl\<rbrakk> \<Longrightarrow> bit rc n = (n < size rc \<and> n div sw < length wl \<and> bit (rev wl ! (n div sw)) (n mod sw))
theory More_Word

lemma max_test_bit: "bit (- 1::'a::len word) n \<longleftrightarrow> n < LENGTH('a)" by (fact nth_minus1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (- 1) n = (n < LENGTH('a))
theory More_Word

lemma map_nth_0 [simp]: "map (bit (0::'a::len word)) xs = replicate (length xs) False" by (simp flip: map_replicate_const)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map (bit 0) xs = replicate (length xs) False
theory More_Word

lemma word_and_1:
  "n AND 1 = (if bit n 0 then 1 else 0)" for n :: "_ word" by (rule bit_word_eqI) (auto simp add: bit_and_iff bit_1_iff intro: gr0I)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n AND 1 = (if bit n 0 then 1 else 0)
theory More_Word

lemma test_bit_1':
  "bit (1 :: 'a :: len word) n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit 1 n = (0 < LENGTH('a) \<and> n = 0)
theory More_Word

lemma nth_w2p_same:
  "bit (2^n :: 'a :: len word) n = (n < LENGTH('a))" by (simp add: nth_w2p)

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

lemma word_leI:
  "(\<And>n.  \<lbrakk>n < size (u::'a::len word); bit u n \<rbrakk> \<Longrightarrow> bit (v::'a::len word) n) \<Longrightarrow> u <= v" apply (rule order_trans [of u \<open>u AND v\<close> v]) apply (rule eq_refl) apply (rule bit_word_eqI) apply (auto simp add: bit_simps word_and_le1 word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n < size u; bit u n\<rbrakk> \<Longrightarrow> bit v n) \<Longrightarrow> u \<le> v proof (prove)
goal (2 subgoals):
 1. (\<And>n. \<lbrakk>n < size u; bit u n\<rbrakk> \<Longrightarrow> bit v n) \<Longrightarrow> u \<le> u AND v
 2. (\<And>n. \<lbrakk>n < size u; bit u n\<rbrakk> \<Longrightarrow> bit v n) \<Longrightarrow> u AND v \<le> v proof (prove)
goal (2 subgoals):
 1. (\<And>n. \<lbrakk>n < size u; bit u n\<rbrakk> \<Longrightarrow> bit v n) \<Longrightarrow> u = u AND v
 2. (\<And>n. \<lbrakk>n < size u; bit u n\<rbrakk> \<Longrightarrow> bit v n) \<Longrightarrow> u AND v \<le> v proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<And>n. \<lbrakk>n < size u; bit u n\<rbrakk> \<Longrightarrow> bit v n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit u n = bit (u AND v) n
 2. (\<And>n. \<lbrakk>n < size u; bit u n\<rbrakk> \<Longrightarrow> bit v n) \<Longrightarrow> u AND v \<le> v proof (prove)
goal:
No subgoals!
theory More_Word

lemma bang_eq:
  fixes x :: "'a::len word"
  shows "(x = y) = (\<forall>n. bit x n = bit y n)" by (auto intro!: bit_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x = y) = (\<forall>n. bit x n = bit y n)
theory More_Word

lemma neg_mask_test_bit:
  "bit (NOT(mask n) :: 'a :: len word) m = (n \<le> m \<and> m < LENGTH('a))" by (auto simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (NOT (mask n)) m = (n \<le> m \<and> m < LENGTH('a))
theory More_Word

lemma test_bit_over:
  "n \<ge> size (x::'a::len word) \<Longrightarrow> (bit x n) = False" by transfer auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size x \<le> n \<Longrightarrow> bit x n = False
theory More_Word

lemma le_mask_high_bits:
  "w \<le> mask n \<longleftrightarrow> (\<forall>i \<in> {n ..< size w}. \<not> bit w i)"
  for w :: \<open>'a::len word\<close> apply (auto simp add: bit_simps word_size less_eq_mask_iff_take_bit_eq_self) apply (metis bit_take_bit_iff leD) apply (metis atLeastLessThan_iff leI take_bit_word_eq_self_iff upper_bits_unset_is_l2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w \<le> mask n) = (\<forall>i\<in>{n..<size w}. \<not> bit w i) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>take_bit n w = w; bit w i; n \<le> i; i < LENGTH('a)\<rbrakk> \<Longrightarrow> False
 2. \<forall>i\<in>{n..<LENGTH('a)}. \<not> bit w i \<Longrightarrow> take_bit n w = w proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{n..<LENGTH('a)}. \<not> bit w i \<Longrightarrow> take_bit n w = w proof (prove)
goal:
No subgoals!
theory More_Word

lemma test_bit_conj_lt:
  "(bit x m \<and> m < LENGTH('a)) = bit x m" for x :: "'a :: len word" using test_bit_bin by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (bit x m \<and> m < LENGTH('a)) = bit x m proof (prove)
using this:
bit ?w ?n = (?n < LENGTH(?'a) \<and> bit (uint ?w) ?n)

goal (1 subgoal):
 1. (bit x m \<and> m < LENGTH('a)) = bit x m
theory More_Word

lemma neg_test_bit:
  "bit (NOT x) n = (\<not> bit x n \<and> n < LENGTH('a))" for x :: "'a::len word" by (cases "n < LENGTH('a)") (auto simp add: test_bit_over word_ops_nth_size word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (NOT x) n = (\<not> bit x n \<and> n < LENGTH('a))
theory More_Word

lemma nth_bounded:
  "\<lbrakk>bit (x :: 'a :: len word) n; x < 2 ^ m; m \<le> len_of TYPE ('a)\<rbrakk> \<Longrightarrow> n < m" apply (rule ccontr) apply (auto simp add: not_less) apply (meson bit_imp_le_length bit_uint_iff less_2p_is_upper_bits_unset test_bit_bin) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bit x n; x < 2 ^ m; m \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> n < m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bit x n; x < 2 ^ m; m \<le> LENGTH('a); \<not> n < m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bit x n; x < 2 ^ m; m \<le> LENGTH('a); m \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory More_Word

lemma and_neq_0_is_nth:
  \<open>x AND y \<noteq> 0 \<longleftrightarrow> bit x n\<close> if \<open>y = 2 ^ n\<close> for x y :: \<open>'a::len word\<close> apply (simp add: bit_eq_iff bit_simps) using that apply (simp add: bit_simps not_le) apply transfer apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND y \<noteq> 0) = bit x n proof (prove)
goal (1 subgoal):
 1. (\<exists>n<LENGTH('a). bit x n \<and> bit y n) = bit x n proof (prove)
using this:
y = 2 ^ n

goal (1 subgoal):
 1. (\<exists>n<LENGTH('a). bit x n \<and> bit y n) = bit x n proof (prove)
goal (1 subgoal):
 1. y = 2 ^ n \<Longrightarrow> (n < LENGTH('a) \<and> bit x n \<and> n < LENGTH('a)) = bit x n proof (prove)
goal (1 subgoal):
 1. \<And>y n x. take_bit LENGTH('a) y = take_bit LENGTH('a) (2 ^ n) \<Longrightarrow> (n < LENGTH('a) \<and> (n < LENGTH('a) \<and> bit x n) \<and> n < LENGTH('a)) = (n < LENGTH('a) \<and> bit x n) proof (prove)
goal:
No subgoals!
theory More_Word

lemma nth_is_and_neq_0:
  "bit (x::'a::len word) n = (x AND 2 ^ n \<noteq> 0)" by (subst and_neq_0_is_nth; rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit x n = (x AND 2 ^ n \<noteq> 0)
theory More_Word

lemma max_word_not_less [simp]:
   "\<not> - 1 < x" for x :: \<open>'a::len word\<close> by (fact word_order.extremum_strict)

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

lemma bit_twiddle_max:
  "(x::'a::len word) XOR (((x::'a::len word) XOR y) AND (if x < y then -1 else 0)) = max x y" by (rule bit_eqI) (auto simp add: bit_simps max_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x XOR (x XOR y) AND (if x < y then - 1 else 0) = max x y
theory More_Word

lemma swap_with_xor:
  "\<lbrakk>(x::'a::len word) = a XOR b; y = b XOR x; z = x XOR y\<rbrakk> \<Longrightarrow> z = b \<and> y = a" by (auto intro: bit_word_eqI simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = a XOR b; y = b XOR x; z = x XOR y\<rbrakk> \<Longrightarrow> z = b \<and> y = a
theory More_Word

lemma le_mask_imp_and_mask:
  "(x::'a::len word) \<le> mask n \<Longrightarrow> x AND mask n = x" by (metis and_mask_eq_iff_le_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> mask n \<Longrightarrow> x AND mask n = x
theory More_Word

lemma or_not_mask_nop:
  "((x::'a::len word) OR NOT (mask n)) AND mask n = x AND mask n" by (metis word_and_not word_ao_dist2 word_bw_comms(1) word_log_esimps(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x OR NOT (mask n)) AND mask n = x AND mask n
theory More_Word

lemma mask_subsume:
  "\<lbrakk>n \<le> m\<rbrakk> \<Longrightarrow> ((x::'a::len word) OR y AND mask n) AND NOT (mask m) = x AND NOT (mask m)" by (rule bit_word_eqI) (auto simp add: bit_simps word_size)

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

lemma and_mask_0_iff_le_mask:
  fixes w :: "'a::len word"
  shows "(w AND NOT(mask n) = 0) = (w \<le> mask n)" by (simp add: mask_eq_0_eq_x le_mask_imp_and_mask and_mask_eq_iff_le_mask)

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

lemma mask_twice2:
  "n \<le> m \<Longrightarrow> ((x::'a::len word) AND mask m) AND mask n = x AND mask n" by (metis mask_twice min_def)

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

lemma uint_2_id:
  "LENGTH('a) \<ge> 2 \<Longrightarrow> uint (2::('a::len) word) = 2" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 \<le> LENGTH('a) \<Longrightarrow> uint 2 = 2
theory More_Word

lemma div_of_0_id[simp]:"(0::('a::len) word) div n = 0" by (simp add: word_div_def)

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

lemma degenerate_word:"LENGTH('a) = 1 \<Longrightarrow> (x::('a::len) word) = 0 \<or> x = 1" by (metis One_nat_def less_irrefl_nat sint_1_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) = 1 \<Longrightarrow> x = 0 \<or> x = 1
theory More_Word

lemma div_by_0_word: "(x::'a::len word) div 0 = 0" by (fact bits_div_by_0)

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

lemma div_less_dividend_word:"\<lbrakk>x \<noteq> 0; n \<noteq> 1\<rbrakk> \<Longrightarrow> (x::('a::len) word) div n < x" apply (cases \<open>n = 0\<close>) apply clarsimp apply (simp add:word_neq_0_conv) apply (subst word_arith_nat_div) apply (rule word_of_nat_less) apply (rule div_less_dividend) using unat_eq_zero word_unat_Rep_inject1 apply force apply (simp add:unat_gt_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1\<rbrakk> \<Longrightarrow> x div n < x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n = 0\<rbrakk> \<Longrightarrow> x div n < x
 2. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> x div n < x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 0; n = 0\<rbrakk> \<Longrightarrow> 0 < x
 2. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> x div n < x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> x div n < x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat (unat x div unat n) < x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> unat x div unat n < unat x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> 1 < unat n
 2. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < unat x proof (prove)
using this:
(unat ?x = 0) = (?x = 0)
(unat ?x = unat 1) = (?x = 1)

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> 1 < unat n
 2. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < unat x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; n \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < unat x proof (prove)
goal:
No subgoals!
theory More_Word

lemma word_less_div:
  fixes x :: "('a::len) word"
    and y :: "('a::len) word"
  shows "x div y = 0 \<Longrightarrow> y = 0 \<or> x < y" apply (case_tac "y = 0", clarsimp+) by (metis One_nat_def Suc_le_mono le0 le_div_geq not_less unat_0 unat_div unat_gt_0 word_less_nat_alt zero_less_one)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x div y = 0 \<Longrightarrow> y = 0 \<or> x < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x div y = 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x < y
theory More_Word

lemma not_degenerate_imp_2_neq_0:"LENGTH('a) > 1 \<Longrightarrow> (2::('a::len) word) \<noteq> 0" by (metis numerals(1) power_not_zero power_zero_numeral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < LENGTH('a) \<Longrightarrow> 2 \<noteq> 0
theory More_Word

lemma word_overflow:"(x::('a::len) word) + 1 > x \<or> x + 1 = 0" apply clarsimp by (metis diff_0 eq_diff_eq less_x_plus_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < x + 1 \<or> x + 1 = 0 proof (prove)
goal (1 subgoal):
 1. x + 1 \<noteq> 0 \<Longrightarrow> x < x + 1
theory More_Word

lemma word_overflow_unat:"unat ((x::('a::len) word) + 1) = unat x + 1 \<or> x + 1 = 0" by (metis Suc_eq_plus1 add.commute unatSuc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (x + 1) = unat x + 1 \<or> x + 1 = 0
theory More_Word

lemma even_word_imp_odd_next:"even (unat (x::('a::len) word)) \<Longrightarrow> x + 1 = 0 \<or> odd (unat (x + 1))" apply (cut_tac x=x in word_overflow_unat) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. even (unat x) \<Longrightarrow> x + 1 = 0 \<or> odd (unat (x + 1)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even (unat x); unat (x + 1) = unat x + 1 \<or> x + 1 = 0\<rbrakk> \<Longrightarrow> x + 1 = 0 \<or> odd (unat (x + 1)) proof (prove)
goal:
No subgoals!