kings-crown/FVELER_Isabelle huggingface dataset:
theory Most_significant_bit

lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1" by (simp add: msb_word_iff_bit le_Suc_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb 1 = (LENGTH('a) = 1)
theory Most_significant_bit

lemma word_msb_nth: "msb w = bit (uint w) (LENGTH('a) - 1)"
  for w :: "'a::len word" by (simp add: msb_word_iff_bit bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb w = bit (uint w) (LENGTH('a) - 1)
theory Most_significant_bit

lemma word_msb_n1 [simp]: "msb (-1::'a::len word)" by (simp add: msb_word_eq not_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb (- 1)
theory Most_significant_bit

lemma msb_shift: "msb w \<longleftrightarrow> w >> LENGTH('a) - 1 \<noteq> 0"
  for w :: "'a::len word" by (simp add: drop_bit_eq_zero_iff_not_bit_last msb_word_eq shiftr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb w = (w >> LENGTH('a) - 1 \<noteq> 0)
theory Most_significant_bit

lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)" apply (cases \<open>LENGTH('a)\<close>) apply (simp_all add: msb_word_iff_bit word_size) apply transfer apply (simp add: signed_take_bit_eq_take_bit_minus) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint x = uint x - (if msb x then 2 ^ size x else 0) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> sint x = uint x - (if msb x then 2 ^ size x else 0)
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> sint x = uint x - (if msb x then 2 ^ size x else 0) proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> (bit x nat \<longrightarrow> sint x = uint x - 2 * 2 ^ nat) \<and> (\<not> bit x nat \<longrightarrow> sint x = uint x) proof (prove)
goal (1 subgoal):
 1. \<And>nat x. LENGTH('a) = Suc nat \<Longrightarrow> (nat < LENGTH('a) \<and> bit x nat \<longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) x = take_bit LENGTH('a) x - 2 * 2 ^ nat) \<and> (\<not> (nat < LENGTH('a) \<and> bit x nat) \<longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) x = take_bit LENGTH('a) x) proof (prove)
goal:
No subgoals!
theory Most_significant_bit

lemma word_sle_msb_le: "x <=s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> y)" apply (simp add: word_sle_eq word_sint_msb_eq word_size word_le_def) apply safe apply (rule order_trans[OF _ uint_ge_0]) apply (simp add: order_less_imp_le) apply (erule notE[OF leD]) apply (rule order_less_le_trans[OF _ uint_ge_0]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<le>s y) = ((msb y \<longrightarrow> msb x) \<and> (msb x \<and> \<not> msb y \<or> x \<le> y)) proof (prove)
goal (1 subgoal):
 1. (msb x \<longrightarrow> \<not> msb y \<longrightarrow> uint x - 2 ^ LENGTH('a) \<le> uint y) \<and> (\<not> msb x \<longrightarrow> msb y \<longrightarrow> \<not> uint x \<le> uint y - 2 ^ LENGTH('a)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>msb x; \<not> msb y\<rbrakk> \<Longrightarrow> uint x - 2 ^ LENGTH('a) \<le> uint y
 2. \<lbrakk>\<not> msb x; msb y; uint x \<le> uint y - 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>msb x; \<not> msb y\<rbrakk> \<Longrightarrow> uint x - 2 ^ LENGTH('a) \<le> 0
 2. \<lbrakk>\<not> msb x; msb y; uint x \<le> uint y - 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> msb x; msb y; uint x \<le> uint y - 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> msb x; msb y\<rbrakk> \<Longrightarrow> uint y - 2 ^ LENGTH('a) < uint x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> msb x; msb y\<rbrakk> \<Longrightarrow> uint y - 2 ^ LENGTH('a) < 0 proof (prove)
goal:
No subgoals!
theory Most_significant_bit

lemma word_sless_msb_less: "x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)" by (auto simp add: word_sless_eq word_sle_msb_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x <s y) = ((msb y \<longrightarrow> msb x) \<and> (msb x \<and> \<not> msb y \<or> x < y))
theory Most_significant_bit

lemma not_msb_from_less:
  "(v :: 'a word) < 2 ^ (LENGTH('a :: len) - 1) \<Longrightarrow> \<not> msb v" apply (clarsimp simp add: msb_nth) apply (drule less_mask_eq) apply (drule word_eqD, drule(1) iffD2) apply (simp add: bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> \<not> msb v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v < 2 ^ (LENGTH('a) - Suc 0); bit v (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bit v (LENGTH('a) - Suc 0); and v (mask (LENGTH('a) - Suc 0)) = v\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bit v (LENGTH('a) - Suc 0); bit (and v (mask (LENGTH('a) - Suc 0))) (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Most_significant_bit

lemma sint_eq_uint:
  "\<not> msb x \<Longrightarrow> sint x = uint x" apply (cases \<open>LENGTH('a)\<close>) apply (simp_all add: msb_word_iff_bit) apply transfer apply (simp add: signed_take_bit_eq_take_bit_minus) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> msb x \<Longrightarrow> sint x = uint x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> msb x; LENGTH('a) = 0\<rbrakk> \<Longrightarrow> sint x = uint x
 2. \<And>nat. \<lbrakk>\<not> msb x; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> sint x = uint x proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<not> bit x nat; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> sint x = uint x proof (prove)
goal (1 subgoal):
 1. \<And>nat x. \<lbrakk>\<not> (nat < LENGTH('a) \<and> bit x nat); LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) x = take_bit LENGTH('a) x proof (prove)
goal:
No subgoals!
theory Most_significant_bit

lemma scast_eq_ucast:
  "\<not> msb x \<Longrightarrow> scast x = ucast x" apply (cases \<open>LENGTH('a)\<close>) apply simp apply (rule bit_word_eqI) apply (auto simp add: bit_signed_iff bit_unsigned_iff min_def msb_word_eq) apply (erule notE) apply (metis le_less_Suc_eq test_bit_bin) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> msb x \<Longrightarrow> scast x = ucast x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> msb x; LENGTH('a) = 0\<rbrakk> \<Longrightarrow> scast x = ucast x
 2. \<And>nat. \<lbrakk>\<not> msb x; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> scast x = ucast x proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<not> msb x; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> scast x = ucast x proof (prove)
goal (1 subgoal):
 1. \<And>nat n. \<lbrakk>\<not> msb x; LENGTH('a) = Suc nat; n < LENGTH('b)\<rbrakk> \<Longrightarrow> bit (scast x) n = bit (ucast x) n proof (prove)
goal (1 subgoal):
 1. \<And>nat n. \<lbrakk>\<not> bit x nat; LENGTH('a) = Suc nat; n < LENGTH('b); nat \<le> n; bit x n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>nat n. \<lbrakk>LENGTH('a) = Suc nat; n < LENGTH('b); nat \<le> n; bit x n\<rbrakk> \<Longrightarrow> bit x nat proof (prove)
goal:
No subgoals!
theory Most_significant_bit

lemma msb_ucast_eq:
    "LENGTH('a) = LENGTH('b) \<Longrightarrow>
         msb (ucast x :: ('a::len) word) = msb (x :: ('b::len) word)" by (simp add: msb_word_eq bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) = LENGTH('b) \<Longrightarrow> msb (ucast x) = msb x
theory Least_significant_bit

lemma bin_last_conv_lsb: "odd = (lsb :: int \<Rightarrow> bool)" by (simp add: lsb_odd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. odd = lsb
theory Least_significant_bit

lemma int_lsb_numeral [simp]:
  "lsb (0 :: int) = False"
  "lsb (1 :: int) = True"
  "lsb (Numeral1 :: int) = True"
  "lsb (- 1 :: int) = True"
  "lsb (- Numeral1 :: int) = True"
  "lsb (numeral (num.Bit0 w) :: int) = False"
  "lsb (numeral (num.Bit1 w) :: int) = True"
  "lsb (- numeral (num.Bit0 w) :: int) = False"
  "lsb (- numeral (num.Bit1 w) :: int) = True" by (simp_all add: lsb_int_def bit_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((lsb 0 = False &&& lsb 1 = True) &&& lsb Numeral1 = True &&& lsb (- 1) = True) &&& (lsb (- Numeral1) = True &&& lsb (numeral (num.Bit0 w)) = False) &&& lsb (numeral (num.Bit1 w)) = True &&& lsb (- numeral (num.Bit0 w)) = False &&& lsb (- numeral (num.Bit1 w)) = True
theory Least_significant_bit

lemma lsb_word_eq:
  \<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close> by (fact lsb_odd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lsb = odd
theory Least_significant_bit

lemma word_lsb_alt: "lsb w = bit w 0"
  for w :: "'a::len word" by (simp add: lsb_word_eq bit_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lsb w = bit w 0
theory Least_significant_bit

lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)" unfolding word_lsb_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lsb 1 \<and> \<not> lsb 0 proof (prove)
goal (1 subgoal):
 1. odd (uint 1) \<and> \<not> odd (uint 0)
theory Least_significant_bit

lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1" apply (simp add: lsb_odd flip: odd_iff_mod_2_eq_one) apply transfer apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lsb w = (uint w mod 2 = 1) proof (prove)
goal (1 subgoal):
 1. even w = even (uint w) proof (prove)
goal (1 subgoal):
 1. \<And>w. even w = even (take_bit LENGTH('a) w) proof (prove)
goal:
No subgoals!
theory Least_significant_bit

lemma word_lsb_numeral [simp]:
  "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> odd (numeral bin :: int)" by (simp only: lsb_odd, transfer) rule

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lsb (numeral bin) = odd (numeral bin)
theory Least_significant_bit

lemma word_lsb_neg_numeral [simp]:
  "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> odd (- numeral bin :: int)" by (simp only: lsb_odd, transfer) rule

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lsb (- numeral bin) = odd (- numeral bin)
theory Generic_set_bit

lemma set_bit_eq:
  \<open>set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\<close>
  for a :: \<open>'a::{ring_bit_operations, set_bit}\<close> by (rule bit_eqI) (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit a n b = (if b then semiring_bit_operations_class.set_bit else unset_bit) n a
theory Generic_set_bit

lemma fixes i :: int
  shows int_set_bit_True_conv_OR [code]: "Generic_set_bit.set_bit i n True = i OR push_bit n 1"
  and int_set_bit_False_conv_NAND [code]: "Generic_set_bit.set_bit i n False = i AND NOT (push_bit n 1)"
  and int_set_bit_conv_ops: "Generic_set_bit.set_bit i n b = (if b then i OR (push_bit n 1) else i AND NOT (push_bit n 1))" by (simp_all add: bit_eq_iff) (auto simp add: 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 &&& set_bit_class.set_bit i n False = i AND NOT (push_bit n 1) &&& set_bit_class.set_bit i n b = (if b then i OR push_bit n 1 else i AND NOT (push_bit n 1))
theory Generic_set_bit

lemma bit_set_bit_word_iff [bit_simps]:
  \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
  for w :: \<open>'a::len word\<close> by (auto simp add: bit_simps dest: bit_imp_le_length)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bit_class.set_bit w m b) n = (if m = n then n < LENGTH('a) \<and> b else bit w n)
theory Generic_set_bit

lemma test_bit_set_gen:
  "bit (set_bit w n x) m \<longleftrightarrow> (if m = n then n < size w \<and> x else bit w m)"
  for w :: "'a::len word" by (simp add: bit_set_bit_word_iff word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bit_class.set_bit w n x) m = (if m = n then n < size w \<and> x else bit w m)
theory Generic_set_bit

lemma test_bit_set:
  "bit (set_bit w n x) n \<longleftrightarrow> n < size w \<and> x"
  for w :: "'a::len word" by (auto simp add: bit_simps word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (set_bit_class.set_bit w n x) n = (n < size w \<and> x)
theory Generic_set_bit

lemma word_set_nth: "set_bit w n (bit w n) = w"
  for w :: "'a::len word" by (rule bit_word_eqI) (simp add: bit_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit w n (bit w n) = w
theory Generic_set_bit

lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
  for w :: "'a::len word" by (rule word_eqI) (simp add : test_bit_set_gen word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (set_bit_class.set_bit w n x) n y = set_bit_class.set_bit w n y
theory Generic_set_bit

lemma word_set_set_diff:
  fixes w :: "'a::len word"
  assumes "m \<noteq> n"
  shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit (set_bit_class.set_bit w m x) n y = set_bit_class.set_bit (set_bit_class.set_bit w n y) m x
theory Generic_set_bit

lemma word_clr_le: "w \<ge> set_bit w n False"
  for w :: "'a::len word" apply (simp add: set_bit_unfold) apply transfer apply (simp add: take_bit_unset_bit_eq unset_bit_less_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit w n False \<le> w proof (prove)
goal (1 subgoal):
 1. unset_bit n w \<le> w proof (prove)
goal (1 subgoal):
 1. \<And>n w. take_bit LENGTH('a) (unset_bit n w) \<le> take_bit LENGTH('a) w proof (prove)
goal:
No subgoals!
theory Generic_set_bit

lemma word_set_ge: "w \<le> set_bit w n True"
  for w :: "'a::len word" apply (simp add: set_bit_unfold) apply transfer apply (simp add: take_bit_set_bit_eq set_bit_greater_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<le> set_bit_class.set_bit w n True proof (prove)
goal (1 subgoal):
 1. w \<le> semiring_bit_operations_class.set_bit n w proof (prove)
goal (1 subgoal):
 1. \<And>w n. take_bit LENGTH('a) w \<le> take_bit LENGTH('a) (semiring_bit_operations_class.set_bit n w) proof (prove)
goal:
No subgoals!
theory Generic_set_bit

lemma set_bit_beyond:
  "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word" by (simp add: word_set_nth_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size x \<le> n \<Longrightarrow> set_bit_class.set_bit x n b = x
theory Generic_set_bit

lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n" apply (rule word_eqI) apply (auto simp add: word_size bit_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 0 n True = 1 << n proof (prove)
goal (1 subgoal):
 1. \<And>na. na < size (set_bit_class.set_bit 0 n True) \<longrightarrow> bit (set_bit_class.set_bit 0 n True) na = bit (1 << n) na proof (prove)
goal:
No subgoals!
theory Generic_set_bit

lemma one_bit_pow: "set_bit 0 n True = (2 :: 'a :: len word) ^ n" by (simp add: one_bit_shiftl shiftl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 0 n True = 2 ^ n
theory Bits_Int

lemma bin_last_def:
  "(odd :: int \<Rightarrow> bool) w \<longleftrightarrow> w mod 2 = 1" by (fact odd_iff_mod_2_eq_one)

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

lemma bin_last_numeral_simps [simp]:
  "\<not> odd (0 :: int)"
  "odd (1 :: int)"
  "odd (- 1 :: int)"
  "odd (Numeral1 :: int)"
  "\<not> odd (numeral (Num.Bit0 w) :: int)"
  "odd (numeral (Num.Bit1 w) :: int)"
  "\<not> odd (- numeral (Num.Bit0 w) :: int)"
  "odd (- numeral (Num.Bit1 w) :: int)" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<not> odd 0 &&& \<not> is_unit 2) &&& odd (- 1) &&& odd Numeral1) &&& (\<not> odd (numeral (num.Bit0 w)) &&& odd (numeral (num.Bit1 w))) &&& \<not> odd (- numeral (num.Bit0 w)) &&& odd (- numeral (num.Bit1 w))
theory Bits_Int

lemma bin_rest_numeral_simps [simp]:
  "(\<lambda>k::int. k div 2) 0 = 0"
  "(\<lambda>k::int. k div 2) 1 = 0"
  "(\<lambda>k::int. k div 2) (- 1) = - 1"
  "(\<lambda>k::int. k div 2) Numeral1 = 0"
  "(\<lambda>k::int. k div 2) (numeral (Num.Bit0 w)) = numeral w"
  "(\<lambda>k::int. k div 2) (numeral (Num.Bit1 w)) = numeral w"
  "(\<lambda>k::int. k div 2) (- numeral (Num.Bit0 w)) = - numeral w"
  "(\<lambda>k::int. k div 2) (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((0 div 2 = 0 &&& 1 div 2 = 0) &&& - 1 div 2 = - 1 &&& Numeral1 div 2 = 0) &&& (numeral (num.Bit0 w) div 2 = numeral w &&& numeral (num.Bit1 w) div 2 = numeral w) &&& - numeral (num.Bit0 w) div 2 = - numeral w &&& - numeral (num.Bit1 w) div 2 = - numeral (w + num.One)
theory Bits_Int

lemma bin_rl_eqI: "\<lbrakk>(\<lambda>k::int. k div 2) x = (\<lambda>k::int. k div 2) y; odd x = odd y\<rbrakk> \<Longrightarrow> x = y" by (auto elim: oddE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x div 2 = y div 2; odd x = odd y\<rbrakk> \<Longrightarrow> x = y
theory Bits_Int

lemma [simp]:
  shows bin_rest_lt0: "(\<lambda>k::int. k div 2) i < 0 \<longleftrightarrow> i < 0"
  and  bin_rest_ge_0: "(\<lambda>k::int. k div 2) i \<ge> 0 \<longleftrightarrow> i \<ge> 0" by auto

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

lemma bin_rest_gt_0 [simp]: "(\<lambda>k::int. k div 2) x > 0 \<longleftrightarrow> x > 1" by auto

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

lemma bin_nth_eq_iff: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) x = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y \<longleftrightarrow> x = y" by (simp add: bit_eq_iff fun_eq_iff)

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

lemma bin_eqI:
  "x = y" if "\<And>n. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n \<longleftrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n" using that by (rule bit_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y proof (prove)
using this:
bit x ?n = bit y ?n

goal (1 subgoal):
 1. x = y
theory Bits_Int

lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n)" by (metis bit_eq_iff)

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

lemma bin_nth_zero [simp]: "\<not> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) 0 n" by simp

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

lemma bin_nth_1 [simp]: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) 1 n \<longleftrightarrow> n = 0" by (cases n) (simp_all add: bit_Suc)

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

lemma bin_nth_minus1 [simp]: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (- 1) n" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (- 1) n
theory Bits_Int

lemma bin_nth_numeral: "(\<lambda>k::int. k div 2) x = y \<Longrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x (numeral n) = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y (pred_numeral n)" by (simp add: numeral_eq_Suc bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x div 2 = y \<Longrightarrow> bit x (numeral n) = bit y (pred_numeral n)
theory Bits_Int

lemma nth_2p_bin: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (2 ^ n) m = (m = n)" \<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close> by (auto simp add: bit_exp_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (2 ^ n) m = (m = n)
theory Bits_Int

lemma nth_rest_power_bin: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (((\<lambda>k::int. k div 2) ^^ k) w) n = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w (n + k)" apply (induct k arbitrary: n) apply clarsimp apply clarsimp apply (simp only: bit_Suc [symmetric] add_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k) proof (prove)
goal (2 subgoals):
 1. \<And>n. bit (((\<lambda>k. k div 2) ^^ 0) w) n = bit w (n + 0)
 2. \<And>k n. (\<And>n. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k)) \<Longrightarrow> bit (((\<lambda>k. k div 2) ^^ Suc k) w) n = bit w (n + Suc k) proof (prove)
goal (1 subgoal):
 1. \<And>k n. (\<And>n. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k)) \<Longrightarrow> bit (((\<lambda>k. k div 2) ^^ Suc k) w) n = bit w (n + Suc k) proof (prove)
goal (1 subgoal):
 1. \<And>k n. (\<And>n. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k)) \<Longrightarrow> bit (((\<lambda>k. k div 2) ^^ k) w div 2) n = bit w (Suc (n + k)) proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_nth_numeral_unfold:
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral (num.Bit0 x)) n \<longleftrightarrow> n > 0 \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral x) (n - 1)"
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral (num.Bit1 x)) n \<longleftrightarrow> (n > 0 \<longrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral x) (n - 1))" by (cases n; simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (numeral (num.Bit0 x)) n = (0 < n \<and> bit (numeral x) (n - 1)) &&& bit (numeral (num.Bit1 x)) n = (0 < n \<longrightarrow> bit (numeral x) (n - 1))
theory Bits_Int

lemma bin_sign_simps [simp]:
  "bin_sign 0 = 0"
  "bin_sign 1 = 0"
  "bin_sign (- 1) = - 1"
  "bin_sign (numeral k) = 0"
  "bin_sign (- numeral k) = -1" by (simp_all add: bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (bin_sign 0 = 0 &&& bin_sign 1 = 0) &&& bin_sign (- 1) = - 1 &&& bin_sign (numeral k) = 0 &&& bin_sign (- numeral k) = - 1
theory Bits_Int

lemma bin_sign_rest [simp]: "bin_sign ((\<lambda>k::int. k div 2) w) = bin_sign w" by (simp add: bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign (w div 2) = bin_sign w
theory Bits_Int

lemma sbintrunc_mod2p: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n" by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n
theory Bits_Int

lemma sbintrunc_eq_take_bit:
  \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close> by (fact signed_take_bit_eq_take_bit_shift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n
theory Bits_Int

lemma sign_bintr: "bin_sign ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = 0" by (simp add: bin_sign_def)

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

lemma bintrunc_n_0: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n 0 = 0" by (fact take_bit_of_0)

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

lemma sbintrunc_n_0: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n 0 = 0" by (fact signed_take_bit_of_0)

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

lemma sbintrunc_n_minus1: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1) = -1" by (fact signed_take_bit_of_minus_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n (- 1) = - 1