1.1 --- a/src/HOL/IntDiv.thy Fri Jul 18 17:09:48 2008 +0200
1.2 +++ b/src/HOL/IntDiv.thy Fri Jul 18 18:25:53 2008 +0200
1.3 @@ -747,8 +747,49 @@
1.4 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
1.5 by (simp add: zdiv_zmult1_eq)
1.6
1.7 +lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
1.8 +apply (case_tac "b = 0", simp)
1.9 +apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
1.10 +done
1.11 +
1.12 +lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
1.13 +apply (case_tac "b = 0", simp)
1.14 +apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
1.15 +done
1.16 +
1.17 +text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
1.18 +
1.19 +lemma zadd1_lemma:
1.20 + "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 |]
1.21 + ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
1.22 +by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
1.23 +
1.24 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.25 +lemma zdiv_zadd1_eq:
1.26 + "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
1.27 +apply (case_tac "c = 0", simp)
1.28 +apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
1.29 +done
1.30 +
1.31 +lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
1.32 +apply (case_tac "c = 0", simp)
1.33 +apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
1.34 +done
1.35 +
1.36 +lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
1.37 +by (simp add: zdiv_zadd1_eq)
1.38 +
1.39 +lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
1.40 +by (simp add: zdiv_zadd1_eq)
1.41 +
1.42 instance int :: semiring_div
1.43 - by intro_classes auto
1.44 +proof
1.45 + fix a b c :: int
1.46 + assume not0: "b \<noteq> 0"
1.47 + show "(a + c * b) div b = c + a div b"
1.48 + unfolding zdiv_zadd1_eq [of a "c * b"] using not0
1.49 + by (simp add: zmod_zmult1_eq)
1.50 +qed auto
1.51
1.52 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
1.53 by (subst mult_commute, erule zdiv_zmult_self1)
1.54 @@ -770,35 +811,6 @@
1.55
1.56 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
1.57
1.58 -text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
1.59 -
1.60 -lemma zadd1_lemma:
1.61 - "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 |]
1.62 - ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
1.63 -by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
1.64 -
1.65 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.66 -lemma zdiv_zadd1_eq:
1.67 - "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
1.68 -apply (case_tac "c = 0", simp)
1.69 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
1.70 -done
1.71 -
1.72 -lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
1.73 -apply (case_tac "c = 0", simp)
1.74 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
1.75 -done
1.76 -
1.77 -lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
1.78 -apply (case_tac "b = 0", simp)
1.79 -apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
1.80 -done
1.81 -
1.82 -lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
1.83 -apply (case_tac "b = 0", simp)
1.84 -apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
1.85 -done
1.86 -
1.87 lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
1.88 apply (rule trans [symmetric])
1.89 apply (rule zmod_zadd1_eq, simp)
1.90 @@ -811,12 +823,6 @@
1.91 apply (rule zmod_zadd1_eq [symmetric])
1.92 done
1.93
1.94 -lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
1.95 -by (simp add: zdiv_zadd1_eq)
1.96 -
1.97 -lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
1.98 -by (simp add: zdiv_zadd1_eq)
1.99 -
1.100 lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
1.101 apply (case_tac "a = 0", simp)
1.102 apply (simp add: zmod_zadd1_eq)
1.103 @@ -1183,33 +1189,36 @@
1.104 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
1.105 by (auto simp add: dvd_def intro: mult_assoc)
1.106
1.107 -lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
1.108 - apply (simp add: dvd_def, auto)
1.109 - apply (rule_tac [!] x = "-k" in exI, auto)
1.110 - done
1.111 +lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
1.112 +proof
1.113 + assume "m dvd - n"
1.114 + then obtain k where "- n = m * k" ..
1.115 + then have "n = m * - k" by simp
1.116 + then show "m dvd n" ..
1.117 +next
1.118 + assume "m dvd n"
1.119 + then have "m dvd n * -1" by (rule dvd_mult2)
1.120 + then show "m dvd - n" by simp
1.121 +qed
1.122
1.123 -lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"
1.124 - apply (simp add: dvd_def, auto)
1.125 - apply (rule_tac [!] x = "-k" in exI, auto)
1.126 - done
1.127 +lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
1.128 +proof
1.129 + assume "- m dvd n"
1.130 + then obtain k where "n = - m * k" ..
1.131 + then have "n = m * - k" by simp
1.132 + then show "m dvd n" ..
1.133 +next
1.134 + assume "m dvd n"
1.135 + then obtain k where "n = m * k" ..
1.136 + then have "n = - m * - k" by simp
1.137 + then show "- m dvd n" ..
1.138 +qed
1.139 +
1.140 lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
1.141 - apply (cases "i > 0", simp)
1.142 - apply (simp add: dvd_def)
1.143 - apply (rule iffI)
1.144 - apply (erule exE)
1.145 - apply (rule_tac x="- k" in exI, simp)
1.146 - apply (erule exE)
1.147 - apply (rule_tac x="- k" in exI, simp)
1.148 - done
1.149 + by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
1.150 +
1.151 lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
1.152 - apply (cases "j > 0", simp)
1.153 - apply (simp add: dvd_def)
1.154 - apply (rule iffI)
1.155 - apply (erule exE)
1.156 - apply (rule_tac x="- k" in exI, simp)
1.157 - apply (erule exE)
1.158 - apply (rule_tac x="- k" in exI, simp)
1.159 - done
1.160 + by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
1.161
1.162 lemma zdvd_anti_sym:
1.163 "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
1.164 @@ -1276,10 +1285,7 @@
1.165 done
1.166
1.167 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
1.168 - apply (simp add: dvd_def, clarify)
1.169 - apply (rule_tac x = "k * ka" in exI)
1.170 - apply (simp add: mult_ac)
1.171 - done
1.172 + by (rule mult_dvd_mono)
1.173
1.174 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
1.175 apply (rule iffI)
1.176 @@ -1301,7 +1307,7 @@
1.177 done
1.178
1.179 lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
1.180 - apply (simp add: dvd_def, auto)
1.181 + apply (auto elim!: dvdE)
1.182 apply (subgoal_tac "0 < n")
1.183 prefer 2
1.184 apply (blast intro: order_less_trans)
1.185 @@ -1309,6 +1315,7 @@
1.186 apply (subgoal_tac "n * k < n * 1")
1.187 apply (drule mult_less_cancel_left [THEN iffD1], auto)
1.188 done
1.189 +
1.190 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
1.191 using zmod_zdiv_equality[where a="m" and b="n"]
1.192 by (simp add: ring_simps)
1.193 @@ -1348,21 +1355,24 @@
1.194 done
1.195
1.196 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1.197 -apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
1.198 - nat_0_le cong add: conj_cong)
1.199 -apply (rule iffI)
1.200 -apply iprover
1.201 -apply (erule exE)
1.202 -apply (case_tac "x=0")
1.203 -apply (rule_tac x=0 in exI)
1.204 -apply simp
1.205 -apply (case_tac "0 \<le> k")
1.206 -apply iprover
1.207 -apply (simp add: neq0_conv linorder_not_le)
1.208 -apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
1.209 -apply assumption
1.210 -apply (simp add: mult_ac)
1.211 -done
1.212 +proof -
1.213 + have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
1.214 + proof -
1.215 + fix k
1.216 + assume A: "int y = int x * k"
1.217 + then show "x dvd y" proof (cases k)
1.218 + case (1 n) with A have "y = x * n" by (simp add: zmult_int)
1.219 + then show ?thesis ..
1.220 + next
1.221 + case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
1.222 + also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
1.223 + also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
1.224 + finally have "- int (x * Suc n) = int y" ..
1.225 + then show ?thesis by (simp only: negative_eq_positive) auto
1.226 + qed
1.227 + qed
1.228 + then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
1.229 +qed
1.230
1.231 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
1.232 proof
1.233 @@ -1385,41 +1395,19 @@
1.234 qed
1.235
1.236 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
1.237 - apply (auto simp add: dvd_def nat_abs_mult_distrib)
1.238 - apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
1.239 - apply (rule_tac x = "-(int k)" in exI)
1.240 - apply (auto simp add: int_mult)
1.241 - done
1.242 + unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
1.243
1.244 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
1.245 - apply (auto simp add: dvd_def abs_if int_mult)
1.246 - apply (rule_tac [3] x = "nat k" in exI)
1.247 - apply (rule_tac [2] x = "-(int k)" in exI)
1.248 - apply (rule_tac x = "nat (-k)" in exI)
1.249 - apply (cut_tac [3] k = m in int_less_0_conv)
1.250 - apply (cut_tac k = m in int_less_0_conv)
1.251 - apply (auto simp add: zero_le_mult_iff mult_less_0_iff
1.252 - nat_mult_distrib [symmetric] nat_eq_iff2)
1.253 - done
1.254 + unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
1.255
1.256 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
1.257 - apply (auto simp add: dvd_def int_mult)
1.258 - apply (rule_tac x = "nat k" in exI)
1.259 - apply (cut_tac k = m in int_less_0_conv)
1.260 - apply (auto simp add: zero_le_mult_iff mult_less_0_iff
1.261 - nat_mult_distrib [symmetric] nat_eq_iff2)
1.262 - done
1.263 + by (auto simp add: dvd_int_iff)
1.264
1.265 lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
1.266 - apply (auto simp add: dvd_def)
1.267 - apply (rule_tac [!] x = "-k" in exI, auto)
1.268 - done
1.269 + by (simp add: zdvd_zminus2_iff)
1.270
1.271 lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
1.272 - apply (auto simp add: dvd_def)
1.273 - apply (drule minus_equation_iff [THEN iffD1])
1.274 - apply (rule_tac [!] x = "-k" in exI, auto)
1.275 - done
1.276 + by (simp add: zdvd_zminus_iff)
1.277
1.278 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
1.279 apply (rule_tac z=n in int_cases)