410 by (simp cong: conj_cong) |
410 by (simp cong: conj_cong) |
411 lemma int_eq_number_of_eq: |
411 lemma int_eq_number_of_eq: |
412 "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" |
412 "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" |
413 by (rule eq_number_of_eq) |
413 by (rule eq_number_of_eq) |
414 |
414 |
415 lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m" |
415 declare dvd_eq_mod_eq_0[symmetric, presburger] |
416 unfolding dvd_eq_mod_eq_0[symmetric] .. |
|
417 |
|
418 lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m" |
|
419 unfolding zdvd_iff_zmod_eq_0[symmetric] .. |
|
420 declare mod_1[presburger] |
416 declare mod_1[presburger] |
421 declare mod_0[presburger] |
417 declare mod_0[presburger] |
422 declare zmod_1[presburger] |
418 declare mod_by_1[presburger] |
423 declare zmod_zero[presburger] |
419 declare zmod_zero[presburger] |
424 declare zmod_self[presburger] |
420 declare zmod_self[presburger] |
425 declare mod_self[presburger] |
421 declare mod_self[presburger] |
426 declare mod_by_0[presburger] |
422 declare mod_by_0[presburger] |
427 declare mod_div_trivial[presburger] |
423 declare mod_div_trivial[presburger] |