Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/IntDiv.thy
changeset 31734 a4a79836d07b
parent 31662 57f7ef0dba8e
child 31998 2c7a24f74db9 
     1.1 --- a/src/HOL/IntDiv.thy	Sun Jun 21 15:47:41 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Sun Jun 21 23:04:37 2009 +0200
     1.3 @@ -1064,6 +1064,16 @@
     1.4  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
     1.5    by (rule dvd_mod_imp_dvd) (* TODO: remove *)
     1.6  
     1.7 +lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
     1.8 +apply(auto simp:abs_if)
     1.9 +   apply(clarsimp simp:dvd_def mult_less_0_iff)
    1.10 +  using mult_le_cancel_left_neg[of _ "-1::int"]
    1.11 +  apply(clarsimp simp:dvd_def mult_less_0_iff)
    1.12 + apply(clarsimp simp:dvd_def mult_less_0_iff
    1.13 +         minus_mult_right simp del: mult_minus_right)
    1.14 +apply(clarsimp simp:dvd_def mult_less_0_iff)
    1.15 +done
    1.16 +
    1.17  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
    1.18    apply (auto elim!: dvdE)
    1.19    apply (subgoal_tac "0 < n")
isabelle