kings-crown/FVELER_Isabelle huggingface dataset:
theory Bits_Int

lemma bin_nth_ops:
  "\<And>x y. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (x AND y) n \<longleftrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n"
  "\<And>x y. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (x OR y) n \<longleftrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n \<or> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n"
  "\<And>x y. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (x XOR y) n \<longleftrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n \<noteq> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n"
  "\<And>x. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (NOT x) n \<longleftrightarrow> \<not> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n" by (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x y. bit (x AND y) n = (bit x n \<and> bit y n)) &&& (\<And>x y. bit (x OR y) n = (bit x n \<or> bit y n))) &&& (\<And>x y. bit (x XOR y) n = (bit x n \<noteq> bit y n)) &&& (\<And>x. bit (NOT x) n = (\<not> bit x n))
theory Bits_Int

lemma int_xor_minus1 [simp]: "-1 XOR x = NOT x"
  for x :: int by (fact bit.xor_one_left)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 1 XOR x = NOT x
theory Bits_Int

lemma int_or_extra_simps [simp]:
  "w OR 0 = w"
  "w OR -1 = -1"
  for w :: int by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w OR 0 = w &&& w OR - 1 = - 1
theory Bits_Int

lemma int_and_extra_simps [simp]:
  "w AND 0 = 0"
  "w AND -1 = w"
  for w :: int by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w AND 0 = 0 &&& w AND - 1 = w
theory Bits_Int

lemma bin_ops_comm:
  fixes x y :: int
  shows int_and_comm: "x AND y = y AND x"
    and int_or_comm:  "x OR y = y OR x"
    and int_xor_comm: "x XOR y = y XOR x" by (simp_all add: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND y = y AND x &&& x OR y = y OR x &&& x XOR y = y XOR x
theory Bits_Int

lemma bin_ops_same [simp]:
  "x AND x = x"
  "x OR x = x"
  "x XOR x = 0"
  for x :: int by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND x = x &&& x OR x = x &&& x XOR x = 0
theory Bits_Int

lemma bbw_ao_absorb: "x AND (y OR x) = x \<and> x OR (y AND x) = x"
  for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops)

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

lemma bbw_ao_absorbs_other:
  "x AND (x OR y) = x \<and> (y AND x) OR x = x"
  "(y OR x) AND x = x \<and> x OR (x AND y) = x"
  "(x OR y) AND x = x \<and> (x AND y) OR x = x"
  for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND (x OR y) = x \<and> y AND x OR x = x &&& (y OR x) AND x = x \<and> x OR x AND y = x &&& (x OR y) AND x = x \<and> x AND y OR x = x
theory Bits_Int

lemma int_xor_not: "(NOT x) XOR y = NOT (x XOR y) \<and> x XOR (NOT y) = NOT (x XOR y)"
  for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT x XOR y = NOT (x XOR y) \<and> x XOR NOT y = NOT (x XOR y)
theory Bits_Int

lemma int_and_assoc: "(x AND y) AND z = x AND (y AND z)"
  for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops)

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

lemma int_or_assoc: "(x OR y) OR z = x OR (y OR z)"
  for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops)

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

lemma int_xor_assoc: "(x XOR y) XOR z = x XOR (y XOR z)"
  for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops)

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

lemma bbw_lcs [simp]:
  "y AND (x AND z) = x AND (y AND z)"
  "y OR (x OR z) = x OR (y OR z)"
  "y XOR (x XOR z) = x XOR (y XOR z)"
  for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y AND x AND z = x AND y AND z &&& y OR x OR z = x OR y OR z &&& y XOR x XOR z = x XOR y XOR z
theory Bits_Int

lemma bbw_not_dist:
  "NOT (x OR y) = (NOT x) AND (NOT y)"
  "NOT (x AND y) = (NOT x) OR (NOT y)"
  for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (x OR y) = NOT x AND NOT y &&& NOT (x AND y) = NOT x OR NOT y
theory Bits_Int

lemma bbw_oa_dist: "(x AND y) OR z = (x OR z) AND (y OR z)"
  for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND y OR z = (x OR z) AND (y OR z)
theory Bits_Int

lemma bbw_ao_dist: "(x OR y) AND z = (x AND z) OR (y AND z)"
  for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x OR y) AND z = x AND z OR y AND z
theory Bits_Int

lemma bin_last_neg_numeral_BitM [simp]:
  "(odd :: int \<Rightarrow> bool) (- numeral (Num.BitM w))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (- numeral (Num.BitM w))
theory Bits_Int

lemma le_int_or: "bin_sign y = 0 \<Longrightarrow> x \<le> x OR y"
  for x y :: int by (simp add: bin_sign_def or_greater_eq split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign y = 0 \<Longrightarrow> x \<le> x OR y
theory Bits_Int

lemma AND_mod: "x AND (2 ^ n - 1) = x mod 2 ^ n"
  for x :: int by (simp flip: take_bit_eq_mod add: take_bit_eq_mask mask_eq_exp_minus_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND 2 ^ n - 1 = x mod 2 ^ n
theory Bits_Int

lemma bin_trunc_ao:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x AND (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (x AND y)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x OR (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (x OR y)" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n x AND take_bit n y = take_bit n (x AND y) &&& take_bit n x OR take_bit n y = take_bit n (x OR y)
theory Bits_Int

lemma bin_trunc_xor: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x XOR (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (x XOR y)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n (take_bit n x XOR take_bit n y) = take_bit n (x XOR y)
theory Bits_Int

lemma bin_trunc_not: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (NOT ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x)) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (NOT x)" by (fact take_bit_not_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n (NOT (take_bit n x)) = take_bit n (NOT x)
theory Bits_Int

lemma bintr_bintr_i: "x = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = take_bit n y \<Longrightarrow> take_bit n x = take_bit n y
theory Bits_Int

lemma not_int_cmp_0 [simp]:
  fixes i :: int shows
  "0 < NOT i \<longleftrightarrow> i < -1"
  "0 \<le> NOT i \<longleftrightarrow> i < 0"
  "NOT i < 0 \<longleftrightarrow> i \<ge> 0"
  "NOT i \<le> 0 \<longleftrightarrow> i \<ge> -1" by(simp_all add: int_not_def) arith+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((0 < NOT i) = (i < - 1) &&& (0 \<le> NOT i) = (i < 0)) &&& (NOT i < 0) = (0 \<le> i) &&& (NOT i \<le> 0) = (- 1 \<le> i)
theory Bits_Int

lemma bbw_ao_dist2: "(x :: int) AND (y OR z) = x AND y OR x AND z" by (fact bit.conj_disj_distrib)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND (y OR z) = x AND y OR x AND z
theory Bits_Int

lemma int_nand_same [simp]: fixes x :: int shows "x AND NOT x = 0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND NOT x = 0
theory Bits_Int

lemma int_nand_same_middle: fixes x :: int shows "x AND y AND NOT x = 0" by (simp add: bit_eq_iff bit_and_iff bit_not_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND y AND NOT x = 0
theory Bits_Int

lemma and_xor_dist: fixes x :: int shows
  "x AND (y XOR z) = (x AND y) XOR (x AND z)" by (fact bit.conj_xor_distrib)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND (y XOR z) = x AND y XOR x AND z
theory Bits_Int

lemma int_and_lt0 [simp]:
  \<open>x AND y < 0 \<longleftrightarrow> x < 0 \<and> y < 0\<close> for x y :: int by (fact and_negative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x AND y < 0) = (x < 0 \<and> y < 0)
theory Bits_Int

lemma int_and_ge0 [simp]:
  \<open>x AND y \<ge> 0 \<longleftrightarrow> x \<ge> 0 \<or> y \<ge> 0\<close> for x y :: int by (fact and_nonnegative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<le> x AND y) = (0 \<le> x \<or> 0 \<le> y)
theory Bits_Int

lemma int_and_1: fixes x :: int shows "x AND 1 = x mod 2" by (fact and_one_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND 1 = x mod 2
theory Bits_Int

lemma int_1_and: fixes x :: int shows "1 AND x = x mod 2" by (fact one_and_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 AND x = x mod 2
theory Bits_Int

lemma int_or_lt0 [simp]:
  \<open>x OR y < 0 \<longleftrightarrow> x < 0 \<or> y < 0\<close> for x y :: int by (fact or_negative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x OR y < 0) = (x < 0 \<or> y < 0)
theory Bits_Int

lemma int_or_ge0 [simp]:
  \<open>x OR y \<ge> 0 \<longleftrightarrow> x \<ge> 0 \<and> y \<ge> 0\<close> for x y :: int by (fact or_nonnegative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<le> x OR y) = (0 \<le> x \<and> 0 \<le> y)
theory Bits_Int

lemma int_xor_ge0 [simp]:
  \<open>x XOR y \<ge> 0 \<longleftrightarrow> (x \<ge> 0 \<longleftrightarrow> y \<ge> 0)\<close> for x y :: int by (fact xor_nonnegative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<le> x XOR y) = ((0 \<le> x) = (0 \<le> y))
theory Bits_Int

lemma even_conv_AND:
  \<open>even i \<longleftrightarrow> i AND 1 = 0\<close> for i :: int by (simp add: and_one_eq mod2_eq_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. even i = (i AND 1 = 0)
theory Bits_Int

lemma bin_last_conv_AND:
  "(odd :: int \<Rightarrow> bool) i \<longleftrightarrow> i AND 1 \<noteq> 0" by (simp add: and_one_eq mod2_eq_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd i = (i AND 1 \<noteq> 0)
theory Bits_Int

lemma bitval_bin_last:
  "of_bool ((odd :: int \<Rightarrow> bool) i) = i AND 1" by (simp add: and_one_eq mod2_eq_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bool (odd i) = i AND 1
theory Bits_Int

lemma bin_sign_and:
  "bin_sign (i AND j) = - (bin_sign i * bin_sign j)" by(simp add: bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign (i AND j) = - (bin_sign i * bin_sign j)
theory Bits_Int

lemma int_not_neg_numeral: "NOT (- numeral n) = (Num.sub n num.One :: int)" by(simp add: int_not_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NOT (- numeral n) = neg_numeral_class.sub n num.One
theory Bits_Int

lemma int_neg_numeral_pOne_conv_not: "- numeral (n + num.One) = (NOT (numeral n) :: int)" by(simp add: int_not_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - numeral (n + num.One) = NOT (numeral n)
theory Bits_Int

lemma int_shiftl_BIT: fixes x :: int
  shows int_shiftl0: "x << 0 = x"
  and int_shiftl_Suc: "x << Suc n = 2 * x << n" by (auto simp add: shiftl_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x << 0 = x &&& x << Suc n = 2 * x << n
theory Bits_Int

lemma int_0_shiftl: "push_bit n 0 = (0 :: int)" by (fact push_bit_of_0)

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

lemma bin_last_shiftl: "odd (push_bit n x) \<longleftrightarrow> n = 0 \<and> (odd :: int \<Rightarrow> bool) x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (push_bit n x) = (n = 0 \<and> odd x)
theory Bits_Int

lemma bin_rest_shiftl: "(\<lambda>k::int. k div 2) (push_bit n x) = (if n > 0 then push_bit (n - 1) x else (\<lambda>k::int. k div 2) x)" by (cases n) (simp_all add: push_bit_eq_mult)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_bit n x div 2 = (if 0 < n then push_bit (n - 1) x else x div 2)
theory Bits_Int

lemma bin_nth_shiftl: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (push_bit n x) m \<longleftrightarrow> n \<le> m \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x (m - n)" by (fact bit_push_bit_iff_int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (push_bit n x) m = (n \<le> m \<and> bit x (m - n))
theory Bits_Int

lemma bin_last_shiftr: "odd (drop_bit n x) \<longleftrightarrow> bit x n" for x :: int by (simp add: bit_iff_odd_drop_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd (drop_bit n x) = bit x n
theory Bits_Int

lemma bin_rest_shiftr: "(\<lambda>k::int. k div 2) (drop_bit n x) = drop_bit (Suc n) x" by (simp add: drop_bit_Suc drop_bit_half)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_bit n x div 2 = drop_bit (Suc n) x
theory Bits_Int

lemma bin_nth_shiftr: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (drop_bit n x) m = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x (n + m)" by (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (drop_bit n x) m = bit x (n + m)
theory Bits_Int

lemma bin_nth_conv_AND:
  fixes x :: int shows
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n \<longleftrightarrow> x AND (push_bit n 1) \<noteq> 0" by (fact bit_iff_and_push_bit_not_eq_0)

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

lemma int_shiftl_numeral [simp]:
  "push_bit (numeral w') (numeral w :: int) = push_bit (pred_numeral w') (numeral (num.Bit0 w))"
  "push_bit (numeral w') (- numeral w :: int) = push_bit (pred_numeral w') (- numeral (num.Bit0 w))" by(simp_all add: numeral_eq_Suc shiftl_int_def)
  (metis add_One mult_inc semiring_norm(11) semiring_norm(13) semiring_norm(2) semiring_norm(6) semiring_norm(87))+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_bit (numeral w') (numeral w) = push_bit (pred_numeral w') (numeral (num.Bit0 w)) &&& push_bit (numeral w') (- numeral w) = push_bit (pred_numeral w') (- numeral (num.Bit0 w))
theory Bits_Int

lemma int_shiftl_One_numeral [simp]:
  "push_bit (numeral w) (1::int) = push_bit (pred_numeral w) 2" using int_shiftl_numeral [of Num.One w] by (simp only: numeral_eq_Suc push_bit_Suc) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_bit (numeral w) 1 = push_bit (pred_numeral w) 2 proof (prove)
using this:
push_bit Numeral1 (numeral w) = push_bit (pred_numeral num.One) (numeral (num.Bit0 w))
push_bit Numeral1 (- numeral w) = push_bit (pred_numeral num.One) (- numeral (num.Bit0 w))

goal (1 subgoal):
 1. push_bit (numeral w) 1 = push_bit (pred_numeral w) 2
theory Bits_Int

lemma shiftl_ge_0: fixes i :: int shows "push_bit n i \<ge> 0 \<longleftrightarrow> i \<ge> 0" by (fact push_bit_nonnegative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<le> push_bit n i) = (0 \<le> i)
theory Bits_Int

lemma shiftl_lt_0: fixes i :: int shows "push_bit n i < 0 \<longleftrightarrow> i < 0" by (fact push_bit_negative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (push_bit n i < 0) = (i < 0)
theory Bits_Int

lemma int_shiftl_test_bit: "bit (push_bit i n :: int) m \<longleftrightarrow> m \<ge> i \<and> bit n (m - i)" by (fact bit_push_bit_iff_int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (push_bit i n) m = (i \<le> m \<and> bit n (m - i))
theory Bits_Int

lemma int_0shiftr: "drop_bit x (0 :: int) = 0" by (fact drop_bit_of_0)

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

lemma int_minus1_shiftr: "drop_bit x (-1 :: int) = -1" by (fact drop_bit_minus_one)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_bit x (- 1) = - 1
theory Bits_Int

lemma int_shiftr_ge_0: fixes i :: int shows "drop_bit n i \<ge> 0 \<longleftrightarrow> i \<ge> 0" by (fact drop_bit_nonnegative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 \<le> drop_bit n i) = (0 \<le> i)
theory Bits_Int

lemma int_shiftr_lt_0 [simp]: fixes i :: int shows "drop_bit n i < 0 \<longleftrightarrow> i < 0" by (fact drop_bit_negative_int_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (drop_bit n i < 0) = (i < 0)
theory Bits_Int

lemma int_shiftr_numeral_Suc0 [simp]:
  "drop_bit (Suc 0) (1 :: int) = 0"
  "drop_bit (Suc 0) (numeral num.One :: int) = 0"
  "drop_bit (Suc 0) (numeral (num.Bit0 w) :: int) = numeral w"
  "drop_bit (Suc 0) (numeral (num.Bit1 w) :: int) = numeral w"
  "drop_bit (Suc 0) (- numeral (num.Bit0 w) :: int) = - numeral w"
  "drop_bit (Suc 0) (- numeral (num.Bit1 w) :: int) = - numeral (Num.inc w)" by (simp_all add: drop_bit_Suc add_One)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (drop_bit (Suc 0) 1 = 0 &&& drop_bit (Suc 0) Numeral1 = 0 &&& drop_bit (Suc 0) (numeral (num.Bit0 w)) = numeral w) &&& drop_bit (Suc 0) (numeral (num.Bit1 w)) = numeral w &&& drop_bit (Suc 0) (- numeral (num.Bit0 w)) = - numeral w &&& drop_bit (Suc 0) (- numeral (num.Bit1 w)) = - numeral (Num.inc w)
theory Bits_Int

lemma bin_nth_minus_p2:
  assumes sign: "bin_sign x = 0"
    and y: "y = push_bit n 1"
    and m: "m < n"
    and x: "x < y"
  shows "bit (x - y) m = bit x m" proof - from \<open>bin_sign x = 0\<close> have \<open>x \<ge> 0\<close> by (simp add: sign_Pls_ge_0) moreover from x y have \<open>x < 2 ^ n\<close> by simp ultimately have \<open>q < n\<close> if \<open>bit x q\<close> for q using that by (metis bit_take_bit_iff take_bit_int_eq_self) then have \<open>bit (x + NOT (mask n)) m = bit x m\<close> using \<open>m < n\<close> by (simp add: disjunctive_add bit_simps) also have \<open>x + NOT (mask n) = x - y\<close> using y by (simp flip: minus_exp_eq_not_mask) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (state)
goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (chain)
picking this:
bin_sign x = 0 proof (prove)
using this:
bin_sign x = 0

goal (1 subgoal):
 1. 0 \<le> x proof (state)
this:
0 \<le> x

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (state)
this:
0 \<le> x

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (chain)
picking this:
x < y
y = push_bit n 1 proof (prove)
using this:
x < y
y = push_bit n 1

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

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (chain)
picking this:
0 \<le> x
x < 2 ^ n proof (prove)
using this:
0 \<le> x
x < 2 ^ n

goal (1 subgoal):
 1. q < n proof (prove)
using this:
0 \<le> x
x < 2 ^ n
bit x q

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

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (chain)
picking this:
bit x ?q \<Longrightarrow> ?q < n proof (prove)
using this:
bit x ?q \<Longrightarrow> ?q < n

goal (1 subgoal):
 1. bit (x + NOT (mask n)) m = bit x m proof (prove)
using this:
bit x ?q \<Longrightarrow> ?q < n
m < n

goal (1 subgoal):
 1. bit (x + NOT (mask n)) m = bit x m proof (state)
this:
bit (x + NOT (mask n)) m = bit x m

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (state)
this:
bit (x + NOT (mask n)) m = bit x m

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (prove)
goal (1 subgoal):
 1. x + NOT (mask n) = x - y proof (prove)
using this:
y = push_bit n 1

goal (1 subgoal):
 1. x + NOT (mask n) = x - y proof (state)
this:
x + NOT (mask n) = x - y

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (chain)
picking this:
bit (x - y) m = bit x m proof (prove)
using this:
bit (x - y) m = bit x m

goal (1 subgoal):
 1. bit (x - y) m = bit x m proof (state)
this:
bit (x - y) m = bit x m

goal:
No subgoals!
theory Bits_Int

lemma bin_clr_conv_NAND:
  "bin_sc n False i = i AND NOT (push_bit n 1)" by (rule bit_eqI) (auto simp add: bin_sc_eq bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit i n False = i AND NOT (push_bit n 1)
theory Bits_Int

lemma bin_set_conv_OR:
  "bin_sc n True i = i OR (push_bit n 1)" by (rule bit_eqI) (auto simp add: bin_sc_eq bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit i n True = i OR push_bit n 1
theory Bits_Int

lemma msb_conv_bin_sign:
  "msb x \<longleftrightarrow> bin_sign x = -1" by (simp add: bin_sign_def not_le msb_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb x = (bin_sign x = - 1)
theory Bits_Int

lemma msb_bin_sc:
  "msb (bin_sc n b x) \<longleftrightarrow> msb x" by (simp add: msb_conv_bin_sign)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (set_bit_class.set_bit x n b) = msb x
theory Bits_Int

lemma msb_word_def:
  \<open>msb a \<longleftrightarrow> bin_sign (signed_take_bit (LENGTH('a) - 1) (uint a)) = - 1\<close>
  for a :: \<open>'a::len word\<close> by (simp add: bin_sign_def bit_simps msb_word_iff_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb a = (bin_sign (signed_take_bit (LENGTH('a) - 1) (uint a)) = - 1)
theory Bits_Int

lemma word_msb_def:
  "msb a \<longleftrightarrow> bin_sign (sint a) = - 1" by (simp add: msb_word_def sint_uint)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb a = (bin_sign (sint a) = - 1)
theory Bits_Int

lemma word_rcat_eq:
  \<open>word_rcat ws = word_of_int (bin_rcat (LENGTH('a::len)) (map uint ws))\<close>
  for ws :: \<open>'a::len word list\<close> apply (simp add: word_rcat_def bin_rcat_def rev_map) apply transfer apply (simp add: horner_sum_foldr foldr_map comp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rcat ws = word_of_int (bin_rcat LENGTH('a) (map uint ws)) proof (prove)
goal (1 subgoal):
 1. word_of_int (horner_sum uint (2 ^ LENGTH('a)) (rev ws)) = word_of_int (horner_sum (take_bit LENGTH('a)) (2 ^ LENGTH('a)) (map uint (rev ws))) proof (prove)
goal (1 subgoal):
 1. \<And>ws. take_bit LENGTH('b) (horner_sum (take_bit LENGTH('a)) (2 ^ LENGTH('a)) (rev ws)) = take_bit LENGTH('b) (horner_sum (take_bit LENGTH('a)) (2 ^ LENGTH('a)) (map (take_bit LENGTH('a)) (rev ws))) proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0" by (simp add: sign_Pls_ge_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign (uint x) = 0
theory Bits_Int

lemma setBit_no: "Bit_Operations.set_bit n (numeral bin) = word_of_int (bin_sc n True (numeral bin))" by (rule bit_word_eqI) (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semiring_bit_operations_class.set_bit n (numeral bin) = word_of_int (set_bit_class.set_bit (numeral bin) n True)
theory Bits_Int

lemma clearBit_no:
  "unset_bit n (numeral bin) = word_of_int (bin_sc n False (numeral bin))" by (rule bit_word_eqI) (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unset_bit n (numeral bin) = word_of_int (set_bit_class.set_bit (numeral bin) n False)