--- a/src/HOL/Int.thy Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Int.thy Tue Oct 27 16:59:44 2020 +0000
@@ -2102,6 +2102,10 @@
"sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
+lemma sub_BitM_One_eq:
+ \<open>(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\<close>
+ by (cases n) simp_all
+
text \<open>Implementations.\<close>
lemma one_int_code [code]: "1 = Pos Num.One"
--- a/src/HOL/Library/Bit_Operations.thy Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy Tue Oct 27 16:59:44 2020 +0000
@@ -5,45 +5,10 @@
theory Bit_Operations
imports
+ Main
"HOL-Library.Boolean_Algebra"
- Main
begin
-lemma sub_BitM_One_eq:
- \<open>(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\<close>
- by (cases n) simp_all
-
-lemma bit_not_int_iff':
- \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
- for k :: int
-proof (induction n arbitrary: k)
- case 0
- show ?case
- by simp
-next
- case (Suc n)
- have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close>
- by simp
- with Suc show ?case
- by (simp add: bit_Suc)
-qed
-
-lemma bit_minus_int_iff:
- \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
- for k :: int
- using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
-
-lemma bit_numeral_int_simps [simp]:
- \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
- \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
- \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
- by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
-
-
subsection \<open>Bit operations\<close>
class semiring_bit_operations = semiring_bit_shifts +
@@ -1570,6 +1535,10 @@
(auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff)
qed
+lemma not_minus_numeral_inc_eq:
+ \<open>NOT (- numeral (Num.inc n)) = (numeral n :: int)\<close>
+ by (simp add: not_int_def sub_inc_One_eq)
+
subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
--- a/src/HOL/Numeral_Simprocs.thy Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Tue Oct 27 16:59:44 2020 +0000
@@ -299,4 +299,14 @@
Numeral_Simprocs.field_divide_cancel_numeral_factor])
\<close>
+lemma bit_numeral_int_simps [simp]:
+ \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
+ \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
+ \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
+ by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
+
end
--- a/src/HOL/Parity.thy Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Parity.thy Tue Oct 27 16:59:44 2020 +0000
@@ -1788,6 +1788,49 @@
instance int :: unique_euclidean_semiring_with_bit_shifts ..
+lemma bit_not_int_iff':
+ \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
+ for k :: int
+proof (induction n arbitrary: k)
+ case 0
+ show ?case
+ by simp
+next
+ case (Suc n)
+ have \<open>- k - 1 = - (k + 2) + 1\<close>
+ by simp
+ also have \<open>(- (k + 2) + 1) div 2 = - (k div 2) - 1\<close>
+ proof (cases \<open>even k\<close>)
+ case True
+ then have \<open>- k div 2 = - (k div 2)\<close>
+ by rule (simp flip: mult_minus_right)
+ with True show ?thesis
+ by simp
+ next
+ case False
+ have \<open>4 = 2 * (2::int)\<close>
+ by simp
+ also have \<open>2 * 2 div 2 = (2::int)\<close>
+ by (simp only: nonzero_mult_div_cancel_left)
+ finally have *: \<open>4 div 2 = (2::int)\<close> .
+ from False obtain l where k: \<open>k = 2 * l + 1\<close> ..
+ then have \<open>- k - 2 = 2 * - (l + 2) + 1\<close>
+ by simp
+ then have \<open>(- k - 2) div 2 + 1 = - (k div 2) - 1\<close>
+ by (simp flip: mult_minus_right add: *) (simp add: k)
+ with False show ?thesis
+ by simp
+ qed
+ finally have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close> .
+ with Suc show ?case
+ by (simp add: bit_Suc)
+qed
+
+lemma bit_minus_int_iff:
+ \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
+ for k :: int
+ using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
+
lemma bit_nat_iff:
\<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
proof (cases \<open>k \<ge> 0\<close>)
--- a/src/HOL/Word/Word.thy Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Word/Word.thy Tue Oct 27 16:59:44 2020 +0000
@@ -120,13 +120,13 @@
end
+lemma exp_eq_zero_iff [simp]:
+ \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
+ by transfer simp
+
lemma word_exp_length_eq_0 [simp]:
\<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
- by transfer simp
-
-lemma exp_eq_zero_iff:
- \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
- by transfer simp
+ by simp
subsubsection \<open>Basic tool setup\<close>
@@ -1102,6 +1102,16 @@
end
+context unique_euclidean_semiring_with_bit_shifts
+begin
+
+lemma unsigned_drop_bit_eq:
+ \<open>unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))\<close>
+ for w :: \<open>'b::len word\<close>
+ by (rule bit_eqI) (auto simp add: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Parity.bit_drop_bit_eq dest: bit_imp_le_length)
+
+end
+
context semiring_bit_operations
begin
@@ -4548,15 +4558,29 @@
subsection \<open>More\<close>
lemma mask_1: "mask 1 = 1"
- by transfer (simp add: min_def mask_Suc_exp)
+ by simp
lemma mask_Suc_0: "mask (Suc 0) = 1"
- using mask_1 by simp
+ by simp
lemma bin_last_bintrunc: "odd (take_bit l n) \<longleftrightarrow> l > 0 \<and> odd n"
by simp
+lemma push_bit_word_beyond [simp]:
+ \<open>push_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+ using that by (transfer fixing: n) (simp add: take_bit_push_bit)
+
+lemma drop_bit_word_beyond [simp]:
+ \<open>drop_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+ using that by (transfer fixing: n) (simp add: drop_bit_take_bit)
+
+lemma signed_drop_bit_beyond:
+ \<open>signed_drop_bit n w = (if bit w (LENGTH('a) - Suc 0) then - 1 else 0)\<close>
+ if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+ by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that)
+
+
subsection \<open>SMT support\<close>
ML_file \<open>Tools/smt_word.ML\<close>