1074 |
1074 |
1075 lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))" |
1075 lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))" |
1076 apply (simp add: dvd_def, auto) |
1076 apply (simp add: dvd_def, auto) |
1077 apply (rule_tac [!] x = "-k" in exI, auto) |
1077 apply (rule_tac [!] x = "-k" in exI, auto) |
1078 done |
1078 done |
|
1079 lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" |
|
1080 apply (cases "i > 0", simp) |
|
1081 apply (simp add: dvd_def) |
|
1082 apply (rule iffI) |
|
1083 apply (erule exE) |
|
1084 apply (rule_tac x="- k" in exI, simp) |
|
1085 apply (erule exE) |
|
1086 apply (rule_tac x="- k" in exI, simp) |
|
1087 done |
|
1088 lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" |
|
1089 apply (cases "j > 0", simp) |
|
1090 apply (simp add: dvd_def) |
|
1091 apply (rule iffI) |
|
1092 apply (erule exE) |
|
1093 apply (rule_tac x="- k" in exI, simp) |
|
1094 apply (erule exE) |
|
1095 apply (rule_tac x="- k" in exI, simp) |
|
1096 done |
1079 |
1097 |
1080 lemma zdvd_anti_sym: |
1098 lemma zdvd_anti_sym: |
1081 "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" |
1099 "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" |
1082 apply (simp add: dvd_def, auto) |
1100 apply (simp add: dvd_def, auto) |
1083 apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) |
1101 apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) |
1085 |
1103 |
1086 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" |
1104 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" |
1087 apply (simp add: dvd_def) |
1105 apply (simp add: dvd_def) |
1088 apply (blast intro: right_distrib [symmetric]) |
1106 apply (blast intro: right_distrib [symmetric]) |
1089 done |
1107 done |
|
1108 |
|
1109 lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" |
|
1110 shows "\<bar>a\<bar> = \<bar>b\<bar>" |
|
1111 proof- |
|
1112 from ab obtain k where k:"b = a*k" unfolding dvd_def by blast |
|
1113 from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast |
|
1114 from k k' have "a = a*k*k'" by simp |
|
1115 with mult_cancel_left1[where c="a" and b="k*k'"] |
|
1116 have kk':"k*k' = 1" using anz by (simp add: mult_assoc) |
|
1117 hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff) |
|
1118 thus ?thesis using k k' by auto |
|
1119 qed |
1090 |
1120 |
1091 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)" |
1121 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)" |
1092 apply (simp add: dvd_def) |
1122 apply (simp add: dvd_def) |
1093 apply (blast intro: right_diff_distrib [symmetric]) |
1123 apply (blast intro: right_diff_distrib [symmetric]) |
1094 done |
1124 done |
1161 apply (blast intro: order_less_trans) |
1191 apply (blast intro: order_less_trans) |
1162 apply (simp add: zero_less_mult_iff) |
1192 apply (simp add: zero_less_mult_iff) |
1163 apply (subgoal_tac "n * k < n * 1") |
1193 apply (subgoal_tac "n * k < n * 1") |
1164 apply (drule mult_less_cancel_left [THEN iffD1], auto) |
1194 apply (drule mult_less_cancel_left [THEN iffD1], auto) |
1165 done |
1195 done |
|
1196 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)" |
|
1197 using zmod_zdiv_equality[where a="m" and b="n"] |
|
1198 by (simp add: ring_eq_simps) |
|
1199 |
|
1200 lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m" |
|
1201 apply (subgoal_tac "m mod n = 0") |
|
1202 apply (simp add: zmult_div_cancel) |
|
1203 apply (simp only: zdvd_iff_zmod_eq_0) |
|
1204 done |
|
1205 |
|
1206 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)" |
|
1207 shows "m dvd n" |
|
1208 proof- |
|
1209 from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast |
|
1210 {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp |
|
1211 with h have False by (simp add: mult_assoc)} |
|
1212 hence "n = m * h" by blast |
|
1213 thus ?thesis by blast |
|
1214 qed |
|
1215 |
|
1216 theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))" |
|
1217 apply (simp split add: split_nat) |
|
1218 apply (rule iffI) |
|
1219 apply (erule exE) |
|
1220 apply (rule_tac x = "int x" in exI) |
|
1221 apply simp |
|
1222 apply (erule exE) |
|
1223 apply (rule_tac x = "nat x" in exI) |
|
1224 apply (erule conjE) |
|
1225 apply (erule_tac x = "nat x" in allE) |
|
1226 apply simp |
|
1227 done |
|
1228 |
|
1229 theorem zdvd_int: "(x dvd y) = (int x dvd int y)" |
|
1230 apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric] |
|
1231 nat_0_le cong add: conj_cong) |
|
1232 apply (rule iffI) |
|
1233 apply iprover |
|
1234 apply (erule exE) |
|
1235 apply (case_tac "x=0") |
|
1236 apply (rule_tac x=0 in exI) |
|
1237 apply simp |
|
1238 apply (case_tac "0 \<le> k") |
|
1239 apply iprover |
|
1240 apply (simp add: linorder_not_le) |
|
1241 apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]]) |
|
1242 apply assumption |
|
1243 apply (simp add: mult_ac) |
|
1244 done |
|
1245 |
|
1246 lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" |
|
1247 proof |
|
1248 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1) |
|
1249 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) |
|
1250 hence "nat \<bar>x\<bar> = 1" by simp |
|
1251 thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto) |
|
1252 next |
|
1253 assume "\<bar>x\<bar>=1" thus "x dvd 1" |
|
1254 by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0) |
|
1255 qed |
|
1256 lemma zdvd_mult_cancel1: |
|
1257 assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" |
|
1258 proof |
|
1259 assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" |
|
1260 by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff) |
|
1261 next |
|
1262 assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp |
|
1263 from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) |
|
1264 qed |
1166 |
1265 |
1167 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" |
1266 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" |
1168 apply (auto simp add: dvd_def nat_abs_mult_distrib) |
1267 apply (auto simp add: dvd_def nat_abs_mult_distrib) |
1169 apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm) |
1268 apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm) |
1170 apply (rule_tac x = "-(int k)" in exI) |
1269 apply (rule_tac x = "-(int k)" in exI) |