# HG changeset patch # User haftmann # Date 1594490948 0 # Node ID 08348e364739b0b76d6bcba9e4a8a1bad4b2f0aa # Parent 45865bb06182f2a0c8905291a9bef0e63db3bb5e more thms diff -r 45865bb06182 -r 08348e364739 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sat Jul 11 18:19:08 2020 +0200 +++ b/src/HOL/Divides.thy Sat Jul 11 18:09:08 2020 +0000 @@ -753,6 +753,32 @@ thus ?lhs by simp qed +lemma take_bit_greater_eq: + \k + 2 ^ n \ take_bit n k\ if \k < 0\ for k :: int +proof - + have \k + 2 ^ n \ take_bit n (k + 2 ^ n)\ + proof (cases \k > - (2 ^ n)\) + case False + then have \k + 2 ^ n \ 0\ + by simp + also note take_bit_nonnegative + finally show ?thesis . + next + case True + with that have \0 \ k + 2 ^ n\ and \k + 2 ^ n < 2 ^ n\ + by simp_all + then show ?thesis + by (simp only: take_bit_eq_mod mod_pos_pos_trivial) + qed + then show ?thesis + by (simp add: take_bit_eq_mod) +qed + +lemma take_bit_less_eq: + \take_bit n k \ k - 2 ^ n\ if \2 ^ n \ k\ and \n > 0\ for k :: int + using that zmod_le_nonneg_dividend [of \k - 2 ^ n\ \2 ^ n\] + by (simp add: take_bit_eq_mod) + subsection \Numeral division with a pragmatic type class\ diff -r 45865bb06182 -r 08348e364739 src/HOL/Library/Bit_Operations.thy --- a/src/HOL/Library/Bit_Operations.thy Sat Jul 11 18:19:08 2020 +0200 +++ b/src/HOL/Library/Bit_Operations.thy Sat Jul 11 18:09:08 2020 +0000 @@ -9,43 +9,6 @@ Main begin -subsection \Preliminiaries\ \ \TODO move\ - -lemma take_bit_int_less_exp: - \take_bit n k < 2 ^ n\ for k :: int - by (simp add: take_bit_eq_mod) - -lemma take_bit_Suc_from_most: - \take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\ for k :: int - by (simp only: take_bit_eq_mod power_Suc2) (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one zmod_zmult2_eq) - -lemma take_bit_greater_eq: - \k + 2 ^ n \ take_bit n k\ if \k < 0\ for k :: int -proof - - have \k + 2 ^ n \ take_bit n (k + 2 ^ n)\ - proof (cases \k > - (2 ^ n)\) - case False - then have \k + 2 ^ n \ 0\ - by simp - also note take_bit_nonnegative - finally show ?thesis . - next - case True - with that have \0 \ k + 2 ^ n\ and \k + 2 ^ n < 2 ^ n\ - by simp_all - then show ?thesis - by (simp only: take_bit_eq_mod mod_pos_pos_trivial) - qed - then show ?thesis - by (simp add: take_bit_eq_mod) -qed - -lemma take_bit_less_eq: - \take_bit n k \ k - 2 ^ n\ if \2 ^ n \ k\ and \n > 0\ for k :: int - using that zmod_le_nonneg_dividend [of \k - 2 ^ n\ \2 ^ n\] - by (simp add: take_bit_eq_mod) - - subsection \Bit operations\ class semiring_bit_operations = semiring_bit_shifts + diff -r 45865bb06182 -r 08348e364739 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Sat Jul 11 18:19:08 2020 +0200 +++ b/src/HOL/Parity.thy Sat Jul 11 18:09:08 2020 +0000 @@ -1648,6 +1648,10 @@ \drop_bit n (- 1 :: int) = - 1\ by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int) +lemma take_bit_Suc_from_most: + \take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\ for k :: int + by (simp only: take_bit_eq_mod power_Suc2) (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one zmod_zmult2_eq) + lemma take_bit_minus: \take_bit n (- take_bit n k) = take_bit n (- k)\ for k :: int @@ -1663,6 +1667,10 @@ for k :: int by (simp add: take_bit_eq_mod) +lemma take_bit_int_less_exp: + \take_bit n k < 2 ^ n\ for k :: int + by (simp add: take_bit_eq_mod) + lemma (in ring_1) of_nat_nat_take_bit_eq [simp]: \of_nat (nat (take_bit n k)) = of_int (take_bit n k)\ by simp