src/HOL/Presburger.thy
changeset 30240 5b25fee0362c
parent 29707 01cae7ad8576
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Presburger.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -412,19 +412,15 @@
     1.4    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
     1.5    by (rule eq_number_of_eq)
     1.6  
     1.7 -lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
     1.8 -unfolding dvd_eq_mod_eq_0[symmetric] ..
     1.9 -
    1.10 -lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
    1.11 -unfolding zdvd_iff_zmod_eq_0[symmetric] ..
    1.12 +declare dvd_eq_mod_eq_0[symmetric, presburger]
    1.13  declare mod_1[presburger] 
    1.14  declare mod_0[presburger]
    1.15 -declare zmod_1[presburger]
    1.16 +declare mod_by_1[presburger]
    1.17  declare zmod_zero[presburger]
    1.18  declare zmod_self[presburger]
    1.19  declare mod_self[presburger]
    1.20  declare mod_by_0[presburger]
    1.21 -declare nat_mod_div_trivial[presburger]
    1.22 +declare mod_div_trivial[presburger]
    1.23  declare div_mod_equality2[presburger]
    1.24  declare div_mod_equality[presburger]
    1.25  declare mod_div_equality2[presburger]