--- a/src/HOL/Divides.thy Fri Aug 21 18:59:29 2020 +0000
+++ b/src/HOL/Divides.thy Fri Aug 21 18:59:30 2020 +0000
@@ -168,41 +168,6 @@
by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
-subsubsection \<open>General Properties of div and mod\<close>
-
-lemma div_pos_pos_trivial [simp]:
- "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
- using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
-
-lemma mod_pos_pos_trivial [simp]:
- "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
- using that by (simp add: mod_eq_self_iff_div_eq_0)
-
-lemma div_neg_neg_trivial [simp]:
- "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
- using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
-
-lemma mod_neg_neg_trivial [simp]:
- "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
- using that by (simp add: mod_eq_self_iff_div_eq_0)
-
-lemma div_pos_neg_trivial:
- "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
- apply (rule div_int_unique [of _ _ _ "k + l"])
- apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>)
- done
-
-lemma mod_pos_neg_trivial:
- "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
- apply (rule mod_int_unique [of _ _ "- 1"])
- apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>)
- done
-
-text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
- because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
-
-
-
subsubsection \<open>Laws for div and mod with Unary Minus\<close>
lemma zminus1_lemma:
@@ -662,31 +627,6 @@
using assms by (simp only: power_add eq) auto
qed
-text \<open>Distributive laws for function \<open>nat\<close>.\<close>
-
-lemma nat_div_distrib:
- assumes "0 \<le> x"
- shows "nat (x div y) = nat x div nat y"
-proof (cases y "0::int" rule: linorder_cases)
- case less
- with assms show ?thesis
- using div_nonneg_neg_le0 by auto
-next
- case greater
- then show ?thesis
- by (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
-qed auto
-
-(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib:
- assumes "0 \<le> x" "0 \<le> y"
- shows "nat (x mod y) = nat x mod nat y"
-proof (cases "y = 0")
- case False
- with assms show ?thesis
- by (simp add: nat_eq_iff zmod_int)
-qed auto
-
text\<open>Suggested by Matthias Daum\<close>
lemma int_div_less_self:
fixes x::int
@@ -1335,4 +1275,6 @@
lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
using that by auto
+find_theorems \<open>(?k::int) mod _ = ?k\<close>
+
end
--- a/src/HOL/Euclidean_Division.thy Fri Aug 21 18:59:29 2020 +0000
+++ b/src/HOL/Euclidean_Division.thy Fri Aug 21 18:59:30 2020 +0000
@@ -1750,6 +1750,67 @@
by (simp only: modulo_int_unfold) simp
qed
+lemma div_pos_pos_trivial [simp]:
+ "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
+ using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
+
+lemma mod_pos_pos_trivial [simp]:
+ "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
+ using that by (simp add: mod_eq_self_iff_div_eq_0)
+
+lemma div_neg_neg_trivial [simp]:
+ "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
+ using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
+
+lemma mod_neg_neg_trivial [simp]:
+ "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
+ using that by (simp add: mod_eq_self_iff_div_eq_0)
+
+lemma div_pos_neg_trivial:
+ "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
+proof (cases \<open>l = - k\<close>)
+ case True
+ with that show ?thesis
+ by (simp add: divide_int_def)
+next
+ case False
+ show ?thesis
+ apply (rule div_eqI [of _ "k + l"])
+ using False that apply (simp_all add: division_segment_int_def)
+ done
+qed
+
+lemma mod_pos_neg_trivial:
+ "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
+proof (cases \<open>l = - k\<close>)
+ case True
+ with that show ?thesis
+ by (simp add: divide_int_def)
+next
+ case False
+ show ?thesis
+ apply (rule mod_eqI [of _ _ \<open>- 1\<close>])
+ using False that apply (simp_all add: division_segment_int_def)
+ done
+qed
+
+text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
+ because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
+
+text \<open>Distributive laws for function \<open>nat\<close>.\<close>
+
+lemma nat_div_distrib:
+ \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> x\<close>
+ using that by (simp add: divide_int_def sgn_if)
+
+lemma nat_div_distrib':
+ \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> y\<close>
+ using that by (simp add: divide_int_def sgn_if)
+
+lemma nat_mod_distrib: \<comment> \<open>Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't\<close>
+ \<open>nat (x mod y) = nat x mod nat y\<close> if \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
+ using that by (simp add: modulo_int_def sgn_if)
+
subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
--- a/src/HOL/Groups_List.thy Fri Aug 21 18:59:29 2020 +0000
+++ b/src/HOL/Groups_List.thy Fri Aug 21 18:59:30 2020 +0000
@@ -455,6 +455,17 @@
end
+lemma horner_sum_of_bool_2_less:
+ \<open>(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\<close>
+proof -
+ have \<open>(\<Sum>n = 0..<length bs. of_bool (bs ! n) * (2::int) ^ n) \<le> (\<Sum>n = 0..<length bs. 2 ^ n)\<close>
+ by (rule sum_mono) simp
+ also have \<open>\<dots> = 2 ^ length bs - 1\<close>
+ by (induction bs) simp_all
+ finally show ?thesis
+ by (simp add: horner_sum_eq_sum)
+qed
+
subsection \<open>Further facts about \<^const>\<open>List.n_lists\<close>\<close>
--- a/src/HOL/Library/Bit_Operations.thy Fri Aug 21 18:59:29 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Fri Aug 21 18:59:30 2020 +0000
@@ -9,27 +9,6 @@
Main
begin
-lemma nat_take_bit_eq:
- \<open>nat (take_bit n k) = take_bit n (nat k)\<close>
- if \<open>k \<ge> 0\<close>
- using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
-
-lemma take_bit_eq_self:
- \<open>take_bit m n = n\<close> if \<open>n < 2 ^ m\<close> for n :: nat
- using that by (simp add: take_bit_eq_mod)
-
-lemma horner_sum_of_bool_2_less:
- \<open>(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\<close>
-proof -
- have \<open>(\<Sum>n = 0..<length bs. of_bool (bs ! n) * (2::int) ^ n) \<le> (\<Sum>n = 0..<length bs. 2 ^ n)\<close>
- by (rule sum_mono) simp
- also have \<open>\<dots> = 2 ^ length bs - 1\<close>
- by (induction bs) simp_all
- finally show ?thesis
- by (simp add: horner_sum_eq_sum)
-qed
-
-
subsection \<open>Bit operations\<close>
class semiring_bit_operations = semiring_bit_shifts +
@@ -840,6 +819,87 @@
\<open>bit (signed_take_bit m k) n = bit k (min m n)\<close>
by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def)
+lemma signed_take_bit_of_0 [simp]:
+ \<open>signed_take_bit n 0 = 0\<close>
+ by (simp add: signed_take_bit_def)
+
+lemma signed_take_bit_of_minus_1 [simp]:
+ \<open>signed_take_bit n (- 1) = - 1\<close>
+ by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask)
+
+lemma signed_take_bit_signed_take_bit [simp]:
+ \<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close>
+ by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
+
+lemma signed_take_bit_eq_iff_take_bit_eq:
+ \<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close>
+proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>)
+ case True
+ moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\<close>
+ for k :: int
+ by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask)
+ ultimately show ?thesis
+ by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq)
+next
+ case False
+ then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close>
+ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
+ then show ?thesis
+ by simp
+qed
+
+lemma take_bit_signed_take_bit:
+ \<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> Suc n\<close>
+ using that by (rule le_SucE; intro bit_eqI)
+ (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
+
+lemma signed_take_bit_add:
+ \<open>signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)\<close>
+proof -
+ have \<open>take_bit (Suc n)
+ (take_bit (Suc n) (signed_take_bit n k) +
+ take_bit (Suc n) (signed_take_bit n l)) =
+ take_bit (Suc n) (k + l)\<close>
+ by (simp add: take_bit_signed_take_bit take_bit_add)
+ then show ?thesis
+ by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_add)
+qed
+
+lemma signed_take_bit_diff:
+ \<open>signed_take_bit n (signed_take_bit n k - signed_take_bit n l) = signed_take_bit n (k - l)\<close>
+proof -
+ have \<open>take_bit (Suc n)
+ (take_bit (Suc n) (signed_take_bit n k) -
+ take_bit (Suc n) (signed_take_bit n l)) =
+ take_bit (Suc n) (k - l)\<close>
+ by (simp add: take_bit_signed_take_bit take_bit_diff)
+ then show ?thesis
+ by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_diff)
+qed
+
+lemma signed_take_bit_minus:
+ \<open>signed_take_bit n (- signed_take_bit n k) = signed_take_bit n (- k)\<close>
+proof -
+ have \<open>take_bit (Suc n)
+ (- take_bit (Suc n) (signed_take_bit n k)) =
+ take_bit (Suc n) (- k)\<close>
+ by (simp add: take_bit_signed_take_bit take_bit_minus)
+ then show ?thesis
+ by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_minus)
+qed
+
+lemma signed_take_bit_mult:
+ \<open>signed_take_bit n (signed_take_bit n k * signed_take_bit n l) = signed_take_bit n (k * l)\<close>
+proof -
+ have \<open>take_bit (Suc n)
+ (take_bit (Suc n) (signed_take_bit n k) *
+ take_bit (Suc n) (signed_take_bit n l)) =
+ take_bit (Suc n) (k * l)\<close>
+ by (simp add: take_bit_signed_take_bit take_bit_mult)
+ then show ?thesis
+ by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult)
+qed
+
text \<open>Modulus centered around 0\<close>
lemma signed_take_bit_eq_take_bit_minus:
@@ -885,40 +945,6 @@
(simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps)
qed
-lemma signed_take_bit_of_0 [simp]:
- \<open>signed_take_bit n 0 = 0\<close>
- by (simp add: signed_take_bit_def)
-
-lemma signed_take_bit_of_minus_1 [simp]:
- \<open>signed_take_bit n (- 1) = - 1\<close>
- by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask)
-
-lemma signed_take_bit_eq_iff_take_bit_eq:
- \<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close>
-proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>)
- case True
- moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\<close>
- for k :: int
- by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask)
- ultimately show ?thesis
- by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq)
-next
- case False
- then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close>
- by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
- then show ?thesis
- by simp
-qed
-
-lemma signed_take_bit_signed_take_bit [simp]:
- \<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close>
- by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
-
-lemma take_bit_signed_take_bit:
- \<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> Suc n\<close>
- using that by (rule le_SucE; intro bit_eqI)
- (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
-
lemma signed_take_bit_take_bit:
\<open>signed_take_bit m (take_bit n k) = (if n \<le> m then take_bit n else signed_take_bit m) k\<close>
by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)
@@ -941,6 +967,10 @@
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>
+ using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self)
+
lemma signed_take_bit_Suc_1 [simp]:
\<open>signed_take_bit (Suc n) 1 = 1\<close>
by (simp add: signed_take_bit_Suc)
--- a/src/HOL/Parity.thy Fri Aug 21 18:59:29 2020 +0000
+++ b/src/HOL/Parity.thy Fri Aug 21 18:59:30 2020 +0000
@@ -1606,6 +1606,11 @@
by simp
qed
+lemma nat_take_bit_eq:
+ \<open>nat (take_bit n k) = take_bit n (nat k)\<close>
+ if \<open>k \<ge> 0\<close>
+ using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
+
lemma not_exp_less_eq_0_int [simp]:
\<open>\<not> 2 ^ n \<le> (0::int)\<close>
by (simp add: power_le_zero_eq)
@@ -1686,6 +1691,27 @@
\<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)
+ assume \<open>\<not> 0 < take_bit m k\<close>
+ then have \<open>take_bit m k = 0\<close>
+ by (auto simp add: not_less intro: order_antisym)
+ then have \<open>bit (take_bit m k) n = bit 0 n\<close>
+ by simp
+ with that show False
+ by (simp add: bit_take_bit_iff)
+qed
+
+lemma take_bit_mult:
+ \<open>take_bit n (take_bit n k * take_bit n l) = take_bit n (k * l)\<close>
+ for k l :: int
+ by (simp add: take_bit_eq_mod mod_mult_eq)
+
lemma (in ring_1) of_nat_nat_take_bit_eq [simp]:
\<open>of_nat (nat (take_bit n k)) = of_int (take_bit n k)\<close>
by simp