src/HOL/Integ/IntDiv.thy
changeset 22026 cc60e54aa7cb
parent 21409 6aa28caa96c5
child 22091 d13ad9a479f9
equal deleted inserted replaced
22025:7c5896919eb8 22026:cc60e54aa7cb
  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)