# HG changeset patch
# User huffman
# Date 1332855611 -7200
# Node ID 9d7d919b9fd8c711519a8806030d4baa8bb9c228
# Parent  8a32c2294498d5e9e2dbf1738f9d7b87a124e53a
remove redundant lemma

diff -r 8a32c2294498 -r 9d7d919b9fd8 NEWS
--- a/NEWS	Tue Mar 27 15:34:36 2012 +0200
+++ b/NEWS	Tue Mar 27 15:40:11 2012 +0200
@@ -151,6 +151,7 @@
   zmod_zminus2 ~> mod_minus_right
   zdiv_minus1_right ~> div_minus1_right
   zmod_minus1_right ~> mod_minus1_right
+  zdvd_mult_div_cancel ~> dvd_mult_div_cancel
   mod_mult_distrib ~> mult_mod_left
   mod_mult_distrib2 ~> mult_mod_right
 
diff -r 8a32c2294498 -r 9d7d919b9fd8 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 15:34:36 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 15:40:11 2012 +0200
@@ -2207,12 +2207,6 @@
 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
 
-lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
-apply (subgoal_tac "m mod n = 0")
- apply (simp add: zmult_div_cancel)
-apply (simp only: dvd_eq_mod_eq_0)
-done
-
 text{*Suggested by Matthias Daum*}
 lemma int_power_div_base:
      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
diff -r 8a32c2294498 -r 9d7d919b9fd8 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Tue Mar 27 15:34:36 2012 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy	Tue Mar 27 15:40:11 2012 +0200
@@ -40,7 +40,7 @@
     from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
     have gpos: "?g > 0" by arith
     have gdvd: "?g dvd a" "?g dvd b" by arith+
-    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz
+    from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz
     have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
     from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
     from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
@@ -56,7 +56,7 @@
       assume b: "b < 0"
       { assume b': "?b' \<ge> 0"
         from gpos have th: "?g \<ge> 0" by arith
-        from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
+        from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)]
         have False using b by arith }
       hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
       from anz bnz nz' b b' gp1 have ?thesis
diff -r 8a32c2294498 -r 9d7d919b9fd8 src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 27 15:34:36 2012 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 27 15:40:11 2012 +0200
@@ -105,7 +105,7 @@
   by (simp add: zgcd_zmult_cancel)
 
 lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
-  by (metis abs_of_pos zdvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
+  by (metis abs_of_pos dvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
 
 
 
@@ -197,7 +197,7 @@
   apply (subgoal_tac "m dvd n * ka")
    apply (subgoal_tac "m dvd ka")
     apply (case_tac [2] "0 \<le> ka")
-  apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
+  apply (metis dvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
   apply (metis abs_dvd_iff abs_of_nonneg add_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs mult_1_right mult_commute)
   apply (metis mult_le_0_iff  zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff order_antisym linorder_linear order_refl mult_commute zrelprime_zdvd_zmult)
   apply (metis dvd_triv_left)
diff -r 8a32c2294498 -r 9d7d919b9fd8 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Mar 27 15:34:36 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Mar 27 15:40:11 2012 +0200
@@ -643,8 +643,8 @@
     unfolding dvd_def by blast
   then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
-    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
-      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
+      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   have "?g \<noteq> 0" using nz by simp
   then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
   from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .