# HG changeset patch # User haftmann # Date 1603817984 0 # Node ID 83b5911c0164f833f7002832375cf798ba803182 # Parent 460d743010bc570fdad6e26fc16fdea435026d8f more lemmas diff -r 460d743010bc -r 83b5911c0164 src/HOL/Int.thy --- 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: + \(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\ + by (cases n) simp_all + text \Implementations.\ lemma one_int_code [code]: "1 = Pos Num.One" diff -r 460d743010bc -r 83b5911c0164 src/HOL/Library/Bit_Operations.thy --- 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: - \(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\ - by (cases n) simp_all - -lemma bit_not_int_iff': - \bit (- k - 1) n \ \ bit k n\ - for k :: int -proof (induction n arbitrary: k) - case 0 - show ?case - by simp -next - case (Suc n) - have \(- k - 1) div 2 = - (k div 2) - 1\ - by simp - with Suc show ?case - by (simp add: bit_Suc) -qed - -lemma bit_minus_int_iff: - \bit (- k) n \ \ bit (k - 1) n\ - for k :: int - using bit_not_int_iff' [of \k - 1\] by simp - -lemma bit_numeral_int_simps [simp]: - \bit (1 :: int) (numeral n) \ bit (0 :: int) (pred_numeral n)\ - \bit (numeral (num.Bit0 w) :: int) (numeral n) \ bit (numeral w :: int) (pred_numeral n)\ - \bit (numeral (num.Bit1 w) :: int) (numeral n) \ bit (numeral w :: int) (pred_numeral n)\ - \bit (numeral (Num.BitM w) :: int) (numeral n) \ \ bit (- numeral w :: int) (pred_numeral n)\ - \bit (- numeral (num.Bit0 w) :: int) (numeral n) \ bit (- numeral w :: int) (pred_numeral n)\ - \bit (- numeral (num.Bit1 w) :: int) (numeral n) \ \ bit (numeral w :: int) (pred_numeral n)\ - \bit (- numeral (Num.BitM w) :: int) (numeral n) \ bit (- (numeral w) :: int) (pred_numeral n)\ - by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff) - - subsection \Bit operations\ 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: + \NOT (- numeral (Num.inc n)) = (numeral n :: int)\ + by (simp add: not_int_def sub_inc_One_eq) + subsection \Instance \<^typ>\nat\\ diff -r 460d743010bc -r 83b5911c0164 src/HOL/Numeral_Simprocs.thy --- 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]) \ +lemma bit_numeral_int_simps [simp]: + \bit (1 :: int) (numeral n) \ bit (0 :: int) (pred_numeral n)\ + \bit (numeral (num.Bit0 w) :: int) (numeral n) \ bit (numeral w :: int) (pred_numeral n)\ + \bit (numeral (num.Bit1 w) :: int) (numeral n) \ bit (numeral w :: int) (pred_numeral n)\ + \bit (numeral (Num.BitM w) :: int) (numeral n) \ \ bit (- numeral w :: int) (pred_numeral n)\ + \bit (- numeral (num.Bit0 w) :: int) (numeral n) \ bit (- numeral w :: int) (pred_numeral n)\ + \bit (- numeral (num.Bit1 w) :: int) (numeral n) \ \ bit (numeral w :: int) (pred_numeral n)\ + \bit (- numeral (Num.BitM w) :: int) (numeral n) \ bit (- (numeral w) :: int) (pred_numeral n)\ + by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff) + end diff -r 460d743010bc -r 83b5911c0164 src/HOL/Parity.thy --- 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': + \bit (- k - 1) n \ \ bit k n\ + for k :: int +proof (induction n arbitrary: k) + case 0 + show ?case + by simp +next + case (Suc n) + have \- k - 1 = - (k + 2) + 1\ + by simp + also have \(- (k + 2) + 1) div 2 = - (k div 2) - 1\ + proof (cases \even k\) + case True + then have \- k div 2 = - (k div 2)\ + by rule (simp flip: mult_minus_right) + with True show ?thesis + by simp + next + case False + have \4 = 2 * (2::int)\ + by simp + also have \2 * 2 div 2 = (2::int)\ + by (simp only: nonzero_mult_div_cancel_left) + finally have *: \4 div 2 = (2::int)\ . + from False obtain l where k: \k = 2 * l + 1\ .. + then have \- k - 2 = 2 * - (l + 2) + 1\ + by simp + then have \(- k - 2) div 2 + 1 = - (k div 2) - 1\ + by (simp flip: mult_minus_right add: *) (simp add: k) + with False show ?thesis + by simp + qed + finally have \(- k - 1) div 2 = - (k div 2) - 1\ . + with Suc show ?case + by (simp add: bit_Suc) +qed + +lemma bit_minus_int_iff: + \bit (- k) n \ \ bit (k - 1) n\ + for k :: int + using bit_not_int_iff' [of \k - 1\] by simp + lemma bit_nat_iff: \bit (nat k) n \ k \ 0 \ bit k n\ proof (cases \k \ 0\) diff -r 460d743010bc -r 83b5911c0164 src/HOL/Word/Word.thy --- 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]: + \2 ^ n = (0 :: 'a::len word) \ n \ LENGTH('a)\ + by transfer simp + lemma word_exp_length_eq_0 [simp]: \(2 :: 'a::len word) ^ LENGTH('a) = 0\ - by transfer simp - -lemma exp_eq_zero_iff: - \2 ^ n = (0 :: 'a::len word) \ n \ LENGTH('a)\ - by transfer simp + by simp subsubsection \Basic tool setup\ @@ -1102,6 +1102,16 @@ end +context unique_euclidean_semiring_with_bit_shifts +begin + +lemma unsigned_drop_bit_eq: + \unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))\ + for w :: \'b::len word\ + 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 \More\ 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) \ l > 0 \ odd n" by simp +lemma push_bit_word_beyond [simp]: + \push_bit n w = 0\ if \LENGTH('a) \ n\ for w :: \'a::len word\ + using that by (transfer fixing: n) (simp add: take_bit_push_bit) + +lemma drop_bit_word_beyond [simp]: + \drop_bit n w = 0\ if \LENGTH('a) \ n\ for w :: \'a::len word\ + using that by (transfer fixing: n) (simp add: drop_bit_take_bit) + +lemma signed_drop_bit_beyond: + \signed_drop_bit n w = (if bit w (LENGTH('a) - Suc 0) then - 1 else 0)\ + if \LENGTH('a) \ n\ for w :: \'a::len word\ + by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that) + + subsection \SMT support\ ML_file \Tools/smt_word.ML\