equal
deleted
inserted
replaced
1062 subsection {* The Divides Relation *} |
1062 subsection {* The Divides Relation *} |
1063 |
1063 |
1064 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1064 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1065 by (simp add: dvd_def zmod_eq_0_iff) |
1065 by (simp add: dvd_def zmod_eq_0_iff) |
1066 |
1066 |
1067 definition |
1067 instance int :: dvd_mod |
1068 dvd_int :: "int \<Rightarrow> int \<Rightarrow> bool" |
1068 by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0) |
1069 where |
|
1070 "dvd_int = op dvd" |
|
1071 |
|
1072 lemmas [code inline] = dvd_int_def [symmetric] |
|
1073 lemmas [code, folded dvd_int_def, code func] = zdvd_iff_zmod_eq_0 |
|
1074 |
1069 |
1075 lemmas zdvd_iff_zmod_eq_0_number_of [simp] = |
1070 lemmas zdvd_iff_zmod_eq_0_number_of [simp] = |
1076 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1071 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1077 |
1072 |
1078 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
1073 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |