# HG changeset patch
# User haftmann
# Date 1598036370 0
# Node ID e4aecb0c729687423a6494aaeee6a198cd101db7
# Parent  bdf77466b6c8dc93013c024861552b3f20c6304d
more lemmas

diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Divides.thy
--- 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
diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Euclidean_Division.thy
--- 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>
 
diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Groups_List.thy
--- 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>
 
diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Library/Bit_Operations.thy
--- 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)
diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Parity.thy
--- 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