some more facts on divisibility
authorhaftmann
Sun Oct 12 17:05:35 2014 +0200 (2014-10-12)
changeset 586501ddba8bcbb58
parent 58649 a62065b5e1e2
child 58651 cfdd09041638
some more facts on divisibility
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Sun Oct 12 17:05:34 2014 +0200
     1.2 +++ b/src/HOL/Int.thy	Sun Oct 12 17:05:35 2014 +0200
     1.3 @@ -1333,6 +1333,10 @@
     1.4  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
     1.5    unfolding zdvd_int by (cases "z \<ge> 0") simp_all
     1.6  
     1.7 +lemma dvd_int_unfold_dvd_nat:
     1.8 +  "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
     1.9 +  unfolding dvd_int_iff [symmetric] by simp
    1.10 +
    1.11  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
    1.12    by (auto simp add: dvd_int_iff)
    1.13