generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
authorhuffman
Mon Jun 15 21:29:04 2009 -0700 (2009-06-15)
changeset 3166257f7ef0dba8e
parent 31661 1e252b8b2334
child 31663 5eb82f064630
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
src/HOL/Divides.thy
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/Divides.thy	Mon Jun 15 17:59:36 2009 -0700
     1.2 +++ b/src/HOL/Divides.thy	Mon Jun 15 21:29:04 2009 -0700
     1.3 @@ -331,6 +331,12 @@
     1.4    "(a * c) mod (b * c) = (a mod b) * c"
     1.5    using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
     1.6  
     1.7 +lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
     1.8 +  unfolding dvd_def by (auto simp add: mod_mult_mult1)
     1.9 +
    1.10 +lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
    1.11 +by (blast intro: dvd_mod_imp_dvd dvd_mod)
    1.12 +
    1.13  lemma div_power:
    1.14    "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
    1.15  apply (induct n)
    1.16 @@ -904,15 +910,6 @@
    1.17    apply (rule dvd_refl)
    1.18    done
    1.19  
    1.20 -lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
    1.21 -  unfolding dvd_def
    1.22 -  apply (case_tac "n = 0", auto)
    1.23 -  apply (blast intro: mod_mult_distrib2 [symmetric])
    1.24 -  done
    1.25 -
    1.26 -lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
    1.27 -by (blast intro: dvd_mod_imp_dvd dvd_mod)
    1.28 -
    1.29  lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
    1.30    unfolding dvd_def
    1.31    apply (erule exE)
     2.1 --- a/src/HOL/IntDiv.thy	Mon Jun 15 17:59:36 2009 -0700
     2.2 +++ b/src/HOL/IntDiv.thy	Mon Jun 15 21:29:04 2009 -0700
     2.3 @@ -1059,13 +1059,10 @@
     2.4  done
     2.5  
     2.6  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
     2.7 -  by (auto elim!: dvdE simp add: mod_mult_mult1)
     2.8 +  by (rule dvd_mod) (* TODO: remove *)
     2.9  
    2.10  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
    2.11 -  apply (subgoal_tac "k dvd n * (m div n) + m mod n")
    2.12 -   apply (simp add: zmod_zdiv_equality [symmetric])
    2.13 -  apply (simp only: dvd_add dvd_mult2)
    2.14 -  done
    2.15 +  by (rule dvd_mod_imp_dvd) (* TODO: remove *)
    2.16  
    2.17  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
    2.18    apply (auto elim!: dvdE)