src/HOL/IntDiv.thy
 changeset 27651 16a26996c30e parent 26507 6da615cef733 child 27667 62500b980749
```     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.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.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.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.38 +
1.39 +lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
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.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.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.90 @@ -811,12 +823,6 @@
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.96 -
1.97 -lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
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.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.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.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.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)
```