1135 |
1135 |
1136 |
1136 |
1137 subsection {* The Divides Relation *} |
1137 subsection {* The Divides Relation *} |
1138 |
1138 |
1139 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1139 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1140 by (simp add: dvd_def zmod_eq_0_iff) |
1140 by (rule dvd_eq_mod_eq_0) |
1141 |
1141 |
1142 lemmas zdvd_iff_zmod_eq_0_number_of [simp] = |
1142 lemmas zdvd_iff_zmod_eq_0_number_of [simp] = |
1143 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1143 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1144 |
1144 |
1145 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
1145 lemma zdvd_0_right: "(m::int) dvd 0" |
1146 by (simp add: dvd_def) |
1146 by (rule dvd_0_right) (* already declared [iff] *) |
1147 |
1147 |
1148 lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)" |
1148 lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)" |
1149 by (simp add: dvd_def) |
1149 by (rule dvd_0_left_iff) (* already declared [noatp,simp] *) |
1150 |
1150 |
1151 lemma zdvd_1_left [iff]: "1 dvd (m::int)" |
1151 lemma zdvd_1_left: "1 dvd (m::int)" |
1152 by (simp add: dvd_def) |
1152 by (rule one_dvd) (* already declared [simp] *) |
1153 |
1153 |
1154 lemma zdvd_refl [simp]: "m dvd (m::int)" |
1154 lemma zdvd_refl [simp]: "m dvd (m::int)" |
1155 by (auto simp add: dvd_def intro: zmult_1_right [symmetric]) |
1155 by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *) |
1156 |
1156 |
1157 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" |
1157 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" |
1158 by (auto simp add: dvd_def intro: mult_assoc) |
1158 by (rule dvd_trans) |
1159 |
1159 |
1160 lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)" |
1160 lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)" |
1161 proof |
1161 by (rule dvd_minus_iff) |
1162 assume "m dvd - n" |
|
1163 then obtain k where "- n = m * k" .. |
|
1164 then have "n = m * - k" by simp |
|
1165 then show "m dvd n" .. |
|
1166 next |
|
1167 assume "m dvd n" |
|
1168 then have "m dvd n * -1" by (rule dvd_mult2) |
|
1169 then show "m dvd - n" by simp |
|
1170 qed |
|
1171 |
1162 |
1172 lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)" |
1163 lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)" |
1173 proof |
1164 by (rule minus_dvd_iff) |
1174 assume "- m dvd n" |
|
1175 then obtain k where "n = - m * k" .. |
|
1176 then have "n = m * - k" by simp |
|
1177 then show "m dvd n" .. |
|
1178 next |
|
1179 assume "m dvd n" |
|
1180 then obtain k where "n = m * k" .. |
|
1181 then have "n = - m * - k" by simp |
|
1182 then show "- m dvd n" .. |
|
1183 qed |
|
1184 |
1165 |
1185 lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" |
1166 lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" |
1186 by (cases "i > 0") (simp_all add: zdvd_zminus2_iff) |
1167 by (cases "i > 0") (simp_all add: zdvd_zminus2_iff) |
1187 |
1168 |
1188 lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" |
1169 lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" |
1193 apply (simp add: dvd_def, auto) |
1174 apply (simp add: dvd_def, auto) |
1194 apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) |
1175 apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) |
1195 done |
1176 done |
1196 |
1177 |
1197 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" |
1178 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" |
1198 apply (simp add: dvd_def) |
1179 by (rule dvd_add) |
1199 apply (blast intro: right_distrib [symmetric]) |
|
1200 done |
|
1201 |
1180 |
1202 lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" |
1181 lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" |
1203 shows "\<bar>a\<bar> = \<bar>b\<bar>" |
1182 shows "\<bar>a\<bar> = \<bar>b\<bar>" |
1204 proof- |
1183 proof- |
1205 from ab obtain k where k:"b = a*k" unfolding dvd_def by blast |
1184 from ab obtain k where k:"b = a*k" unfolding dvd_def by blast |
1210 hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff) |
1189 hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff) |
1211 thus ?thesis using k k' by auto |
1190 thus ?thesis using k k' by auto |
1212 qed |
1191 qed |
1213 |
1192 |
1214 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)" |
1193 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)" |
1215 apply (simp add: dvd_def) |
1194 by (rule Ring_and_Field.dvd_diff) |
1216 apply (blast intro: right_diff_distrib [symmetric]) |
|
1217 done |
|
1218 |
1195 |
1219 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" |
1196 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" |
1220 apply (subgoal_tac "m = n + (m - n)") |
1197 apply (subgoal_tac "m = n + (m - n)") |
1221 apply (erule ssubst) |
1198 apply (erule ssubst) |
1222 apply (blast intro: zdvd_zadd, simp) |
1199 apply (blast intro: zdvd_zadd, simp) |
1223 done |
1200 done |
1224 |
1201 |
1225 lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" |
1202 lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" |
1226 apply (simp add: dvd_def) |
1203 by (rule dvd_mult) |
1227 apply (blast intro: mult_left_commute) |
|
1228 done |
|
1229 |
1204 |
1230 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n" |
1205 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n" |
1231 apply (subst mult_commute) |
1206 by (rule dvd_mult2) |
1232 apply (erule zdvd_zmult) |
1207 |
1233 done |
1208 lemma zdvd_triv_right: "(k::int) dvd m * k" |
1234 |
1209 by (rule dvd_triv_right) (* already declared [simp] *) |
1235 lemma zdvd_triv_right [iff]: "(k::int) dvd m * k" |
1210 |
1236 apply (rule zdvd_zmult) |
1211 lemma zdvd_triv_left: "(k::int) dvd k * m" |
1237 apply (rule zdvd_refl) |
1212 by (rule dvd_triv_left) (* already declared [simp] *) |
1238 done |
|
1239 |
|
1240 lemma zdvd_triv_left [iff]: "(k::int) dvd k * m" |
|
1241 apply (rule zdvd_zmult2) |
|
1242 apply (rule zdvd_refl) |
|
1243 done |
|
1244 |
1213 |
1245 lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" |
1214 lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" |
1246 apply (simp add: dvd_def) |
1215 by (rule dvd_mult_left) |
1247 apply (simp add: mult_assoc, blast) |
|
1248 done |
|
1249 |
1216 |
1250 lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)" |
1217 lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)" |
1251 apply (rule zdvd_zmultD2) |
1218 by (rule dvd_mult_right) |
1252 apply (subst mult_commute, assumption) |
|
1253 done |
|
1254 |
1219 |
1255 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" |
1220 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" |
1256 by (rule mult_dvd_mono) |
1221 by (rule mult_dvd_mono) |
1257 |
1222 |
1258 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" |
1223 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" |
1299 proof- |
1264 proof- |
1300 from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast |
1265 from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast |
1301 {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp |
1266 {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp |
1302 with h have False by (simp add: mult_assoc)} |
1267 with h have False by (simp add: mult_assoc)} |
1303 hence "n = m * h" by blast |
1268 hence "n = m * h" by blast |
1304 thus ?thesis by blast |
1269 thus ?thesis by simp |
1305 qed |
1270 qed |
1306 |
1271 |
1307 lemma zdvd_zmult_cancel_disj[simp]: |
1272 lemma zdvd_zmult_cancel_disj[simp]: |
1308 "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))" |
1273 "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))" |
1309 by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel) |
1274 by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel) |
1337 also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int) |
1302 also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int) |
1338 finally have "- int (x * Suc n) = int y" .. |
1303 finally have "- int (x * Suc n) = int y" .. |
1339 then show ?thesis by (simp only: negative_eq_positive) auto |
1304 then show ?thesis by (simp only: negative_eq_positive) auto |
1340 qed |
1305 qed |
1341 qed |
1306 qed |
1342 then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric]) |
1307 then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult) |
1343 qed |
1308 qed |
1344 |
1309 |
1345 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" |
1310 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" |
1346 proof |
1311 proof |
1347 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1) |
1312 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1) |
1348 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) |
1313 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) |
1370 |
1335 |
1371 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" |
1336 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" |
1372 by (auto simp add: dvd_int_iff) |
1337 by (auto simp add: dvd_int_iff) |
1373 |
1338 |
1374 lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))" |
1339 lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))" |
1375 by (simp add: zdvd_zminus2_iff) |
1340 by (rule minus_dvd_iff) |
1376 |
1341 |
1377 lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))" |
1342 lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))" |
1378 by (simp add: zdvd_zminus_iff) |
1343 by (rule dvd_minus_iff) |
1379 |
1344 |
1380 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)" |
1345 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)" |
1381 apply (rule_tac z=n in int_cases) |
1346 apply (rule_tac z=n in int_cases) |
1382 apply (auto simp add: dvd_int_iff) |
1347 apply (auto simp add: dvd_int_iff) |
1383 apply (rule_tac z=z in int_cases) |
1348 apply (rule_tac z=z in int_cases) |