# HG changeset patch
# User haftmann
# Date 1413126334 -7200
# Node ID a62065b5e1e28536686fd49f9dfa4c4adb1229b2
# Parent  3ccafeb9a1d167a55138d91dcf0aa2b3df860aec
generalized and consolidated some theorems concerning divisibility

diff -r 3ccafeb9a1d1 -r a62065b5e1e2 NEWS
--- a/NEWS	Sun Oct 12 16:31:43 2014 +0200
+++ b/NEWS	Sun Oct 12 17:05:34 2014 +0200
@@ -42,6 +42,12 @@
 
 *** HOL ***
 
+* Generalized and consolidated some theorems concerning divsibility:
+  dvd_reduce ~> dvd_add_triv_right_iff
+  dvd_plus_eq_right ~> dvd_add_right_iff
+  dvd_plus_eq_left ~> dvd_add_left_iff
+Minor INCOMPATIBILITY.
+
 * More foundational definition for predicate "even":
   even_def ~> even_iff_mod_2_eq_zero
 Minor INCOMPATIBILITY.
diff -r 3ccafeb9a1d1 -r a62065b5e1e2 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Oct 12 16:31:43 2014 +0200
+++ b/src/HOL/Int.thy	Sun Oct 12 17:05:34 2014 +0200
@@ -1242,19 +1242,10 @@
 qed
 
 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
-  apply (subgoal_tac "m = n + (m - n)")
-   apply (erule ssubst)
-   apply (blast intro: dvd_add, simp)
-  done
+  using dvd_add_right_iff [of k "- n" m] by simp 
 
 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
-apply (rule iffI)
- apply (erule_tac [2] dvd_add)
- apply (subgoal_tac "n = (n + k * m) - k * m")
-  apply (erule ssubst)
-  apply (erule dvd_diff)
-  apply(simp_all)
-done
+  using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
 
 lemma dvd_imp_le_int:
   fixes d i :: int
diff -r 3ccafeb9a1d1 -r a62065b5e1e2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Oct 12 16:31:43 2014 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 12 17:05:34 2014 +0200
@@ -1950,34 +1950,6 @@
   shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
 by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
 
-lemma dvd_plusE:
-  fixes m n q :: nat
-  assumes "m dvd n + q" "m dvd n"
-  obtains "m dvd q"
-proof (cases "m = 0")
-  case True with assms that show thesis by simp
-next
-  case False then have "m > 0" by simp
-  from assms obtain r s where "n = m * r" and "n + q = m * s" by (blast elim: dvdE)
-  then have *: "m * r + q = m * s" by simp
-  show thesis proof (cases "r \<le> s")
-    case False then have "s < r" by (simp add: not_le)
-    with * have "m * r + q - m * s = m * s - m * s" by simp
-    then have "m * r + q - m * s = 0" by simp
-    with `m > 0` `s < r` have "m * r - m * s + q = 0" by (unfold less_le_not_le) auto
-    then have "m * (r - s) + q = 0" by auto
-    then have "m * (r - s) = 0" by simp
-    then have "m = 0 \<or> r - s = 0" by simp
-    with `s < r` have "m = 0" by (simp add: less_le_not_le)
-    with `m > 0` show thesis by auto
-  next
-    case True with * have "m * r + q - m * r = m * s - m * r" by simp
-    with `m > 0` `r \<le> s` have "m * r - m * r + q = m * s - m * r" by simp
-    then have "q = m * (s - r)" by (simp add: diff_mult_distrib2)
-    with assms that show thesis by (auto intro: dvdI)
-  qed
-qed
-
 lemma less_eq_dvd_minus:
   fixes m n :: nat
   assumes "m \<le> n"
@@ -1999,7 +1971,7 @@
   shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)"
 proof -
   have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
-    by (auto elim: dvd_plusE)
+    using dvd_add_times_triv_left_iff [of m r] by simp
   also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
   also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
   also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute)
@@ -2015,21 +1987,6 @@
 lemma nat_mult_1_right: "n * (1::nat) = n"
   by (fact mult_1_right)
 
-lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
-  by (fact dvd_add_triv_right_iff)
-
-lemma dvd_plus_eq_right:
-  fixes m n q :: nat
-  assumes "m dvd n"
-  shows "m dvd n + q \<longleftrightarrow> m dvd q"
-  using assms by (fact dvd_add_eq_right)
-
-lemma dvd_plus_eq_left:
-  fixes m n q :: nat
-  assumes "m dvd q"
-  shows "m dvd n + q \<longleftrightarrow> m dvd n"
-  using assms by (fact dvd_add_eq_left)
-
 
 subsection {* Size of a datatype value *}
 
diff -r 3ccafeb9a1d1 -r a62065b5e1e2 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Sun Oct 12 16:31:43 2014 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sun Oct 12 17:05:34 2014 +0200
@@ -142,7 +142,7 @@
     }
     then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)"
       by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v]
-        dvd_plus_eq_left dvd_plus_eq_right)
+        dvd_add_left_iff dvd_add_right_iff)
     moreover from q have "Suc q = m + w + r" by (simp add: w_def)
     moreover from q have "Suc (Suc q) = v + w + r" by (simp add: v_def w_def)
     ultimately have "w dvd Suc (Suc (q + (w - v mod w))) \<longleftrightarrow> w dvd Suc (q + (w - m mod w))"
diff -r 3ccafeb9a1d1 -r a62065b5e1e2 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 12 16:31:43 2014 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 12 17:05:34 2014 +0200
@@ -228,15 +228,15 @@
   "a dvd b + a \<longleftrightarrow> a dvd b"
   using dvd_add_times_triv_right_iff [of a b 1] by simp
 
-lemma dvd_add_eq_right:
+lemma dvd_add_right_iff:
   assumes "a dvd b"
   shows "a dvd b + c \<longleftrightarrow> a dvd c"
   using assms by (auto dest: dvd_addD)
 
-lemma dvd_add_eq_left:
+lemma dvd_add_left_iff:
   assumes "a dvd c"
   shows "a dvd b + c \<longleftrightarrow> a dvd b"
-  using assms dvd_add_eq_right [of a c b] by (simp add: ac_simps)
+  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
 
 end