--- 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
--- 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)"
--- 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
--- 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)
--- 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" .