remove redundant lemma
authorhuffman
Tue Mar 27 15:40:11 2012 +0200 (2012-03-27)
changeset 471629d7d919b9fd8
parent 47161 8a32c2294498
child 47163 248376f8881d
remove redundant lemma
NEWS
src/HOL/Divides.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
     1.1 --- a/NEWS	Tue Mar 27 15:34:36 2012 +0200
     1.2 +++ b/NEWS	Tue Mar 27 15:40:11 2012 +0200
     1.3 @@ -151,6 +151,7 @@
     1.4    zmod_zminus2 ~> mod_minus_right
     1.5    zdiv_minus1_right ~> div_minus1_right
     1.6    zmod_minus1_right ~> mod_minus1_right
     1.7 +  zdvd_mult_div_cancel ~> dvd_mult_div_cancel
     1.8    mod_mult_distrib ~> mult_mod_left
     1.9    mod_mult_distrib2 ~> mult_mod_right
    1.10  
     2.1 --- a/src/HOL/Divides.thy	Tue Mar 27 15:34:36 2012 +0200
     2.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:40:11 2012 +0200
     2.3 @@ -2207,12 +2207,6 @@
     2.4  lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
     2.5  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
     2.6  
     2.7 -lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
     2.8 -apply (subgoal_tac "m mod n = 0")
     2.9 - apply (simp add: zmult_div_cancel)
    2.10 -apply (simp only: dvd_eq_mod_eq_0)
    2.11 -done
    2.12 -
    2.13  text{*Suggested by Matthias Daum*}
    2.14  lemma int_power_div_base:
    2.15       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
     3.1 --- a/src/HOL/Library/Abstract_Rat.thy	Tue Mar 27 15:34:36 2012 +0200
     3.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Tue Mar 27 15:40:11 2012 +0200
     3.3 @@ -40,7 +40,7 @@
     3.4      from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
     3.5      have gpos: "?g > 0" by arith
     3.6      have gdvd: "?g dvd a" "?g dvd b" by arith+
     3.7 -    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz
     3.8 +    from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz
     3.9      have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
    3.10      from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
    3.11      from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
    3.12 @@ -56,7 +56,7 @@
    3.13        assume b: "b < 0"
    3.14        { assume b': "?b' \<ge> 0"
    3.15          from gpos have th: "?g \<ge> 0" by arith
    3.16 -        from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    3.17 +        from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)]
    3.18          have False using b by arith }
    3.19        hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
    3.20        from anz bnz nz' b b' gp1 have ?thesis
     4.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 27 15:34:36 2012 +0200
     4.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 27 15:40:11 2012 +0200
     4.3 @@ -105,7 +105,7 @@
     4.4    by (simp add: zgcd_zmult_cancel)
     4.5  
     4.6  lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
     4.7 -  by (metis abs_of_pos zdvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
     4.8 +  by (metis abs_of_pos dvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
     4.9  
    4.10  
    4.11  
    4.12 @@ -197,7 +197,7 @@
    4.13    apply (subgoal_tac "m dvd n * ka")
    4.14     apply (subgoal_tac "m dvd ka")
    4.15      apply (case_tac [2] "0 \<le> ka")
    4.16 -  apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
    4.17 +  apply (metis dvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
    4.18    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)
    4.19    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)
    4.20    apply (metis dvd_triv_left)
     5.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Mar 27 15:34:36 2012 +0200
     5.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Mar 27 15:40:11 2012 +0200
     5.3 @@ -643,8 +643,8 @@
     5.4      unfolding dvd_def by blast
     5.5    then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
     5.6    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
     5.7 -    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
     5.8 -      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
     5.9 +    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    5.10 +      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
    5.11    have "?g \<noteq> 0" using nz by simp
    5.12    then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
    5.13    from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .