author haftmann Fri, 22 Nov 2019 09:24:54 +0000 changeset 71346 9d2716dc79a6 parent 71345 2e46c0b4042d child 71347 a7d1fb0c9e16
removed unused auxiliary lemmas
 src/HOL/Divides.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Divides.thy	Thu Nov 21 15:22:24 2019 +0100
+++ b/src/HOL/Divides.thy	Fri Nov 22 09:24:54 2019 +0000
@@ -330,69 +330,6 @@
by simp
qed (use assms in auto)

-
-subsubsection \<open>Proving  \<^term>\<open>a div (b * c) = (a div b) div c\<close>\<close>
-
-(*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
-  7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
-  to cause particular problems.*)
-
-text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
-
-lemma zmult2_lemma_aux1:
-  fixes c::int
-  assumes "0 < c" "b < r" "r \<le> 0"
-  shows "b * c < b * (q mod c) + r"
-proof -
-  have "b * (c - q mod c) \<le> b * 1"
-    by (rule mult_left_mono_neg) (use assms in \<open>auto simp: int_one_le_iff_zero_less\<close>)
-  also have "... < r * 1"
-    by (simp add: \<open>b < r\<close>)
-  finally show ?thesis
-qed
-
-lemma zmult2_lemma_aux2:
-  fixes c::int
-  assumes "0 < c" "b < r" "r \<le> 0"
-  shows "b * (q mod c) + r \<le> 0"
-proof -
-  have "b * (q mod c) \<le> 0"
-    using assms by (simp add: mult_le_0_iff)
-  with assms show ?thesis
-    by arith
-qed
-
-lemma zmult2_lemma_aux3:
-  fixes c::int
-  assumes "0 < c" "0 \<le> r" "r < b"
-  shows "0 \<le> b * (q mod c) + r"
-proof -
-  have "0 \<le> b * (q mod c)"
-    using assms by (simp add: mult_le_0_iff)
-  with assms show ?thesis
-    by arith
-qed
-
-lemma zmult2_lemma_aux4:
-  fixes c::int
-  assumes "0 < c" "0 \<le> r" "r < b"
-  shows "b * (q mod c) + r < b * c"
-proof -
-  have "r * 1 < b * 1"
-    by (simp add: \<open>r < b\<close>)
-  also have "\<dots> \<le> b * (c - q mod c) "
-    by (rule mult_left_mono) (use assms in \<open>auto simp: int_one_le_iff_zero_less\<close>)
-  finally show ?thesis