--- a/src/HOL/Divides.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Divides.thy Thu Sep 17 09:57:30 2020 +0000
@@ -1251,6 +1251,87 @@
code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+subsection \<open>More on bit operations\<close>
+
+lemma take_bit_incr_eq:
+ \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close>
+ for k :: int
+proof -
+ from that have \<open>2 ^ n \<noteq> k mod 2 ^ n + 1\<close>
+ by (simp add: take_bit_eq_mod)
+ moreover have \<open>k mod 2 ^ n < 2 ^ n\<close>
+ by simp
+ ultimately have *: \<open>k mod 2 ^ n + 1 < 2 ^ n\<close>
+ by linarith
+ have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
+ by (simp add: mod_simps)
+ also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
+ using * by (simp add: zmod_trival_iff)
+ finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_decr_eq:
+ \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close>
+ for k :: int
+proof -
+ from that have \<open>k mod 2 ^ n \<noteq> 0\<close>
+ by (simp add: take_bit_eq_mod)
+ moreover have \<open>k mod 2 ^ n \<ge> 0\<close> \<open>k mod 2 ^ n < 2 ^ n\<close>
+ by simp_all
+ ultimately have *: \<open>k mod 2 ^ n > 0\<close>
+ by linarith
+ have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
+ by (simp add: mod_simps)
+ also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
+ by (simp add: zmod_trival_iff)
+ (use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
+ finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_less_eq_self_iff:
+ \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for k :: int
+proof
+ assume ?P
+ show ?Q
+ proof (rule ccontr)
+ assume \<open>\<not> 0 \<le> k\<close>
+ then have \<open>k < 0\<close>
+ by simp
+ with \<open>?P\<close>
+ have \<open>take_bit n k < 0\<close>
+ by (rule le_less_trans)
+ then show False
+ by simp
+ qed
+next
+ assume ?Q
+ then show ?P
+ by (simp add: take_bit_eq_mod zmod_le_nonneg_dividend)
+qed
+
+lemma take_bit_int_less_self_iff:
+ \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+ for k :: int
+ by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
+ intro: order_trans [of 0 \<open>2 ^ n\<close> k])
+
+lemma take_bit_int_greater_self_iff:
+ \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close>
+ for k :: int
+ using take_bit_int_less_eq_self_iff [of n k] by auto
+
+lemma take_bit_int_greater_eq_self_iff:
+ \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+ for k :: int
+ by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
+ dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
+
+
subsection \<open>Lemmas of doubtful value\<close>
lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
--- a/src/HOL/Library/Bit_Operations.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy Thu Sep 17 09:57:30 2020 +0000
@@ -1106,23 +1106,45 @@
for k :: int
by (simp add: signed_take_bit_def not_less concat_bit_def)
-lemma signed_take_bit_greater_eq:
+lemma signed_take_bit_int_eq_self_iff:
+ \<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
+ for k :: int
+ by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_less_eq_self_iff:
+ \<open>signed_take_bit n k \<le> k \<longleftrightarrow> - (2 ^ n) \<le> k\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_eq_self_iff algebra_simps)
+ linarith
+
+lemma signed_take_bit_int_less_self_iff:
+ \<open>signed_take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_self_iff algebra_simps)
+
+lemma signed_take_bit_int_greater_self_iff:
+ \<open>k < signed_take_bit n k \<longleftrightarrow> k < - (2 ^ n)\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_self_iff algebra_simps)
+ linarith
+
+lemma signed_take_bit_int_greater_eq_self_iff:
+ \<open>k \<le> signed_take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_eq_self_iff algebra_simps)
+
+lemma signed_take_bit_int_greater_eq:
\<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k < - (2 ^ n)\<close>
for k :: int
using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
by (simp add: signed_take_bit_eq_take_bit_shift)
-lemma signed_take_bit_less_eq:
+lemma signed_take_bit_int_less_eq:
\<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close>
for k :: int
using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
by (simp add: signed_take_bit_eq_take_bit_shift)
-lemma signed_take_bit_eq_self:
- \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
- for k :: int
- using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self)
-
lemma signed_take_bit_Suc_bit0 [simp]:
\<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\<close>
by (simp add: signed_take_bit_Suc)
--- a/src/HOL/Parity.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Parity.thy Thu Sep 17 09:57:30 2020 +0000
@@ -1024,6 +1024,37 @@
qed
qed
+lemma
+ exp_add_not_zero_imp_left: \<open>2 ^ m \<noteq> 0\<close>
+ and exp_add_not_zero_imp_right: \<open>2 ^ n \<noteq> 0\<close>
+ if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+ have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+ proof (rule notI)
+ assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+ then have \<open>2 ^ (m + n) = 0\<close>
+ by (rule disjE) (simp_all add: power_add)
+ with that show False ..
+ qed
+ then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+ by simp_all
+qed
+
+lemma exp_not_zero_imp_exp_diff_not_zero:
+ \<open>2 ^ (n - m) \<noteq> 0\<close> if \<open>2 ^ n \<noteq> 0\<close>
+proof (cases \<open>m \<le> n\<close>)
+ case True
+ moreover define q where \<open>q = n - m\<close>
+ ultimately have \<open>n = m + q\<close>
+ by simp
+ with that show ?thesis
+ by (simp add: exp_add_not_zero_imp_right)
+next
+ case False
+ with that show ?thesis
+ by simp
+qed
+
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -1147,7 +1178,7 @@
also have "\<dots> = - int (2 * n) - 1"
by (simp add: algebra_simps)
finally show ?case
- using even by simp
+ using even.prems by simp
next
case (odd n)
have "P (- int (Suc n) * 2)"
@@ -1155,7 +1186,7 @@
also have "\<dots> = - int (Suc (2 * n)) - 1"
by (simp add: algebra_simps)
finally show ?case
- using odd by simp
+ using odd.prems by simp
qed
qed
@@ -1584,6 +1615,56 @@
\<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
by (auto simp add: bit_push_bit_iff)
+lemma take_bit_nat_less_exp:
+ \<open>take_bit n m < 2 ^ n\<close> for n m ::nat
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nat_eq_self_iff:
+ \<open>take_bit n m = m \<longleftrightarrow> m < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for n m :: nat
+proof
+ assume ?P
+ moreover note take_bit_nat_less_exp [of n m]
+ ultimately show ?Q
+ by simp
+next
+ assume ?Q
+ then show ?P
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_nat_less_eq_self:
+ \<open>take_bit n m \<le> m\<close> for n m :: nat
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nonnegative [simp]:
+ \<open>take_bit n k \<ge> 0\<close>
+ for k :: int
+ by (simp add: take_bit_eq_mod)
+
+lemma not_take_bit_negative [simp]:
+ \<open>\<not> take_bit n k < 0\<close>
+ for k :: int
+ by (simp add: not_less)
+
+lemma take_bit_int_less_exp:
+ \<open>take_bit n k < 2 ^ n\<close> for k :: int
+ by (simp add: take_bit_eq_mod)
+
+lemma take_bit_int_eq_self_iff:
+ \<open>take_bit n k = k \<longleftrightarrow> 0 \<le> k \<and> k < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for k :: int
+proof
+ assume ?P
+ moreover note take_bit_int_less_exp [of n k] take_bit_nonnegative [of n k]
+ ultimately show ?Q
+ by simp
+next
+ assume ?Q
+ then show ?P
+ by (simp add: take_bit_eq_mod)
+qed
+
class unique_euclidean_semiring_with_bit_shifts =
unique_euclidean_semiring_with_nat + semiring_bit_shifts
begin
@@ -1752,10 +1833,6 @@
"drop_bit n (Suc 0) = of_bool (n = 0)"
using drop_bit_of_1 [where ?'a = nat] by simp
-lemma take_bit_eq_self:
- \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for n m :: nat
- using that by (simp add: take_bit_eq_mod)
-
lemma push_bit_minus_one:
"push_bit n (- 1 :: int) = - (2 ^ n)"
by (simp add: push_bit_eq_mult)
@@ -1782,24 +1859,6 @@
for k l :: int
by (simp add: take_bit_eq_mod mod_diff_eq)
-lemma take_bit_nonnegative [simp]:
- \<open>take_bit n k \<ge> 0\<close>
- for k :: int
- by (simp add: take_bit_eq_mod)
-
-lemma not_take_bit_negative [simp]:
- \<open>\<not> take_bit n k < 0\<close>
- for k :: int
- by (simp add: not_less)
-
-lemma take_bit_int_less_exp:
- \<open>take_bit n k < 2 ^ n\<close> for k :: int
- by (simp add: take_bit_eq_mod)
-
-lemma take_bit_int_eq_self:
- \<open>take_bit n k = k\<close> if \<open>0 \<le> k\<close> \<open>k < 2 ^ n\<close> for k :: int
- using that by (simp add: take_bit_eq_mod)
-
lemma bit_imp_take_bit_positive:
\<open>0 < take_bit m k\<close> if \<open>n < m\<close> and \<open>bit k n\<close> for k :: int
proof (rule ccontr)
--- a/src/HOL/Word/Bits_Int.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy Thu Sep 17 09:57:30 2020 +0000
@@ -372,11 +372,11 @@
lemma sbintrunc_inc:
\<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close>
- using that by (fact signed_take_bit_greater_eq)
+ using that by (fact signed_take_bit_int_greater_eq)
lemma sbintrunc_dec:
\<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
- using that by (fact signed_take_bit_less_eq)
+ using that by (fact signed_take_bit_int_less_eq)
lemma bintr_ge0: "0 \<le> bintrunc n w"
by (simp add: bintrunc_mod2p)
--- a/src/HOL/Word/Conversions.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Word/Conversions.thy Thu Sep 17 09:57:30 2020 +0000
@@ -455,7 +455,7 @@
by (simp add: nat_less_iff take_bit_int_less_exp)
finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
(nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_eq_self)
+ by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
qed
lemma unat_mod_distrib:
@@ -468,7 +468,7 @@
by (simp add: nat_less_iff take_bit_int_less_exp)
finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
(nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_eq_self)
+ by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
qed
lemma uint_div_distrib:
--- a/src/HOL/Word/Word.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Word/Word.thy Thu Sep 17 09:57:30 2020 +0000
@@ -358,7 +358,7 @@
by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l)
moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
- by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
+ by (simp add: l take_bit_eq_mod)
ultimately have \<open>P (2 * of_nat n)\<close>
by (rule word_even)
then show ?case
@@ -371,7 +371,7 @@
by simp
moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
- by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
+ by (simp add: l take_bit_eq_mod)
ultimately have \<open>P (1 + 2 * of_nat n)\<close>
by (rule word_odd)
then show ?case
@@ -1396,8 +1396,8 @@
"n = LENGTH('a::len) \<Longrightarrow>
td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
apply (standard; transfer)
- apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self)
- apply (simp add: take_bit_eq_mod)
+ apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_nat_eq_self_iff
+ flip: take_bit_eq_mod)
done
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
@@ -3882,7 +3882,7 @@
by (cases \<open>LENGTH('a)\<close>) simp_all
have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close>
\<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close>
- using signed_take_bit_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_less_eq [of n \<open>sint x + sint y\<close>]
+ using signed_take_bit_int_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_int_less_eq [of n \<open>sint x + sint y\<close>]
by (auto intro: ccontr)
have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
(sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
@@ -4433,7 +4433,7 @@
apply (subst take_bit_diff [symmetric])
apply (subst nat_take_bit_eq)
apply (simp add: nat_le_eq_zle)
- apply (simp add: nat_diff_distrib take_bit_eq_self less_imp_diff_less bintr_lt2p)
+ apply (simp add: nat_diff_distrib take_bit_nat_eq_self_iff less_imp_diff_less bintr_lt2p)
done
qed