src/HOL/Divides.thy
 changeset 14267 b963e9cee2a0 parent 14208 144f45277d5a child 14430 5cb24165a2e1
```     1.1 --- a/src/HOL/Divides.thy	Mon Nov 24 15:33:07 2003 +0100
1.2 +++ b/src/HOL/Divides.thy	Tue Nov 25 10:37:03 2003 +0100
1.3 @@ -6,7 +6,7 @@
1.4  The division operators div, mod and the divides relation "dvd"
1.5  *)
1.6
1.7 -theory Divides = NatArith files("Divides_lemmas.ML"):
1.8 +theory Divides = NatArith:
1.9
1.10  (*We use the same class for div and mod;
1.11    moreover, dvd is defined whenever multiplication is*)
1.12 @@ -32,7 +32,7 @@
1.13                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
1.14
1.15  (*The definition of dvd is polymorphic!*)
1.16 -  dvd_def:   "m dvd n == EX k. n = m*k"
1.17 +  dvd_def:   "m dvd n == \<exists>k. n = m*k"
1.18
1.19  (*This definition helps prove the harder properties of div and mod.
1.20    It is copied from IntDiv.thy; should it be overloaded?*)
1.21 @@ -40,11 +40,612 @@
1.22    quorem :: "(nat*nat) * (nat*nat) => bool"
1.23      "quorem == %((a,b), (q,r)).
1.24                        a = b*q + r &
1.25 -                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
1.26 +                      (if 0<b then 0\<le>r & r<b else b<r & r \<le>0)"
1.27 +
1.28 +
1.29 +
1.30 +subsection{*Initial Lemmas*}
1.31 +
1.32 +lemmas wf_less_trans =
1.33 +       def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
1.34 +                  standard]
1.35 +
1.36 +lemma mod_eq: "(%m. m mod n) =
1.37 +              wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
1.39 +
1.40 +lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)
1.41 +               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
1.43 +
1.44 +
1.45 +(** Aribtrary definitions for division by zero.  Useful to simplify
1.46 +    certain equations **)
1.47 +
1.48 +lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
1.49 +by (rule div_eq [THEN wf_less_trans], simp)
1.50 +
1.51 +lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
1.52 +by (rule mod_eq [THEN wf_less_trans], simp)
1.53 +
1.54 +
1.55 +subsection{*Remainder*}
1.56 +
1.57 +lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
1.58 +by (rule mod_eq [THEN wf_less_trans], simp)
1.59 +
1.60 +lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
1.61 +apply (case_tac "n=0", simp)
1.62 +apply (rule mod_eq [THEN wf_less_trans])
1.63 +apply (simp add: diff_less cut_apply less_eq)
1.64 +done
1.65 +
1.66 +(*Avoids the ugly ~m<n above*)
1.67 +lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
1.68 +by (simp add: mod_geq not_less_iff_le)
1.69 +
1.70 +lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
1.72 +
1.73 +lemma mod_1 [simp]: "m mod Suc 0 = 0"
1.74 +apply (induct_tac "m")
1.75 +apply (simp_all (no_asm_simp) add: mod_geq)
1.76 +done
1.77 +
1.78 +lemma mod_self [simp]: "n mod n = (0::nat)"
1.79 +apply (case_tac "n=0")
1.81 +done
1.82 +
1.83 +lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
1.84 +apply (subgoal_tac " (n + m) mod n = (n+m-n) mod n")
1.86 +apply (subst mod_geq [symmetric], simp_all)
1.87 +done
1.88 +
1.89 +lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
1.91 +
1.92 +lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
1.93 +apply (induct_tac "k")
1.95 +done
1.96 +
1.97 +lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
1.98 +by (simp add: mult_commute mod_mult_self1)
1.99 +
1.100 +lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
1.101 +apply (case_tac "n=0", simp)
1.102 +apply (case_tac "k=0", simp)
1.103 +apply (induct_tac "m" rule: nat_less_induct)
1.104 +apply (subst mod_if, simp)
1.105 +apply (simp add: mod_geq diff_less diff_mult_distrib)
1.106 +done
1.107 +
1.108 +lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
1.109 +by (simp add: mult_commute [of k] mod_mult_distrib)
1.110 +
1.111 +lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
1.112 +apply (case_tac "n=0", simp)
1.113 +apply (induct_tac "m", simp)
1.114 +apply (rename_tac "k")
1.115 +apply (cut_tac m = "k*n" and n = n in mod_add_self2)
1.117 +done
1.118 +
1.119 +lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
1.120 +by (simp add: mult_commute mod_mult_self_is_0)
1.121 +
1.122 +
1.123 +subsection{*Quotient*}
1.124 +
1.125 +lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
1.126 +by (rule div_eq [THEN wf_less_trans], simp)
1.127 +
1.128 +lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
1.129 +apply (rule div_eq [THEN wf_less_trans])
1.130 +apply (simp add: diff_less cut_apply less_eq)
1.131 +done
1.132 +
1.133 +(*Avoids the ugly ~m<n above*)
1.134 +lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
1.135 +by (simp add: div_geq not_less_iff_le)
1.136 +
1.137 +lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
1.139 +
1.140 +
1.141 +(*Main Result about quotient and remainder.*)
1.142 +lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
1.143 +apply (case_tac "n=0", simp)
1.144 +apply (induct_tac "m" rule: nat_less_induct)
1.145 +apply (subst mod_if)
1.147 +done
1.148 +
1.149 +lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
1.150 +apply(cut_tac m = m and n = n in mod_div_equality)
1.152 +done
1.153 +
1.154 +subsection{*Simproc for Cancelling Div and Mod*}
1.155 +
1.156 +lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
1.158 +done
1.159 +
1.160 +lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
1.162 +done
1.163 +
1.164 +ML
1.165 +{*
1.166 +val div_mod_equality = thm "div_mod_equality";
1.167 +val div_mod_equality2 = thm "div_mod_equality2";
1.168 +
1.169 +
1.170 +structure CancelDivModData =
1.171 +struct
1.172 +
1.173 +val div_name = "Divides.op div";
1.174 +val mod_name = "Divides.op mod";
1.175 +val mk_binop = HOLogic.mk_binop;
1.176 +val mk_sum = NatArithUtils.mk_sum;
1.177 +val dest_sum = NatArithUtils.dest_sum;
1.178 +
1.179 +(*logic*)
1.180 +
1.181 +val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
1.182 +
1.183 +val trans = trans
1.184 +
1.185 +val prove_eq_sums =
1.187 +  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
1.188 +
1.189 +end;
1.190 +
1.191 +structure CancelDivMod = CancelDivModFun(CancelDivModData);
1.192 +
1.193 +val cancel_div_mod_proc = NatArithUtils.prep_simproc
1.194 +      ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
1.195 +
1.197 +*}
1.198 +
1.199 +
1.200 +(* a simple rearrangement of mod_div_equality: *)
1.201 +lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
1.202 +by (cut_tac m = m and n = n in mod_div_equality2, arith)
1.203 +
1.204 +lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
1.205 +apply (induct_tac "m" rule: nat_less_induct)
1.206 +apply (case_tac "na<n", simp)
1.207 +txt{*case @{term "n \<le> na"}*}
1.208 +apply (simp add: mod_geq diff_less)
1.209 +done
1.210 +
1.211 +lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
1.212 +by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
1.213 +
1.214 +lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
1.215 +by (simp add: mult_commute div_mult_self_is_m)
1.216 +
1.217 +(*mod_mult_distrib2 above is the counterpart for remainder*)
1.218 +
1.219 +
1.220 +subsection{*Proving facts about Quotient and Remainder*}
1.221 +
1.222 +lemma unique_quotient_lemma:
1.223 +     "[| b*q' + r'  \<le> b*q + r;  0 < b;  r < b |]
1.224 +      ==> q' \<le> (q::nat)"
1.225 +apply (rule leI)
1.228 +done
1.229 +
1.230 +lemma unique_quotient:
1.231 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
1.232 +      ==> q = q'"
1.233 +apply (simp add: split_ifs quorem_def)
1.234 +apply (blast intro: order_antisym
1.235 +             dest: order_eq_refl [THEN unique_quotient_lemma] sym)+
1.236 +done
1.237 +
1.238 +lemma unique_remainder:
1.239 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
1.240 +      ==> r = r'"
1.241 +apply (subgoal_tac "q = q'")
1.242 +prefer 2 apply (blast intro: unique_quotient)
1.244 +done
1.245 +
1.246 +lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
1.247 +by (auto simp add: quorem_def)
1.248 +
1.249 +lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
1.250 +by (simp add: quorem_div_mod [THEN unique_quotient])
1.251 +
1.252 +lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
1.253 +by (simp add: quorem_div_mod [THEN unique_remainder])
1.254 +
1.255 +(** A dividend of zero **)
1.256 +
1.257 +lemma div_0 [simp]: "0 div m = (0::nat)"
1.258 +by (case_tac "m=0", simp_all)
1.259 +
1.260 +lemma mod_0 [simp]: "0 mod m = (0::nat)"
1.261 +by (case_tac "m=0", simp_all)
1.262 +
1.263 +(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
1.264 +
1.265 +lemma quorem_mult1_eq:
1.266 +     "[| quorem((b,c),(q,r));  0 < c |]
1.267 +      ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
1.269 +done
1.270 +
1.271 +lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
1.272 +apply (case_tac "c = 0", simp)
1.273 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
1.274 +done
1.275 +
1.276 +lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
1.277 +apply (case_tac "c = 0", simp)
1.278 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
1.279 +done
1.280 +
1.281 +lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
1.282 +apply (rule trans)
1.283 +apply (rule_tac s = "b*a mod c" in trans)
1.284 +apply (rule_tac [2] mod_mult1_eq)
1.285 +apply (simp_all (no_asm) add: mult_commute)
1.286 +done
1.287 +
1.288 +lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
1.289 +apply (rule mod_mult1_eq' [THEN trans])
1.290 +apply (rule mod_mult1_eq)
1.291 +done
1.292 +
1.293 +(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
1.294 +
1.296 +     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]
1.297 +      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
1.299 +
1.300 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.302 +     "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
1.303 +apply (case_tac "c = 0", simp)
1.304 +apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
1.305 +done
1.306 +
1.307 +lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
1.308 +apply (case_tac "c = 0", simp)
1.309 +apply (blast intro: quorem_div_mod quorem_div_mod
1.311 +done
1.312 +
1.313 +
1.314 +subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
1.315 +
1.316 +(** first, a lemma to bound the remainder **)
1.317 +
1.318 +lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
1.319 +apply (cut_tac m = q and n = c in mod_less_divisor)
1.320 +apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1.321 +apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
1.323 +done
1.324
1.325 -use "Divides_lemmas.ML"
1.326 +lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]
1.327 +      ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
1.329 +done
1.330 +
1.331 +lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
1.332 +apply (case_tac "b=0", simp)
1.333 +apply (case_tac "c=0", simp)
1.334 +apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
1.335 +done
1.336 +
1.337 +lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
1.338 +apply (case_tac "b=0", simp)
1.339 +apply (case_tac "c=0", simp)
1.340 +apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
1.341 +done
1.342 +
1.343 +
1.344 +subsection{*Cancellation of Common Factors in Division*}
1.345 +
1.346 +lemma div_mult_mult_lemma:
1.347 +     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
1.348 +by (auto simp add: div_mult2_eq)
1.349 +
1.350 +lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
1.351 +apply (case_tac "b = 0")
1.352 +apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
1.353 +done
1.354 +
1.355 +lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
1.356 +apply (drule div_mult_mult1)
1.357 +apply (auto simp add: mult_commute)
1.358 +done
1.359 +
1.360 +
1.361 +(*Distribution of Factors over Remainders:
1.362 +
1.363 +Could prove these as in Integ/IntDiv.ML, but we already have
1.364 +mod_mult_distrib and mod_mult_distrib2 above!
1.365 +
1.366 +Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"
1.367 +qed "mod_mult_mult1";
1.368 +
1.369 +Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
1.370 +qed "mod_mult_mult2";
1.371 + ***)
1.372 +
1.373 +subsection{*Further Facts about Quotient and Remainder*}
1.374 +
1.375 +lemma div_1 [simp]: "m div Suc 0 = m"
1.376 +apply (induct_tac "m")
1.377 +apply (simp_all (no_asm_simp) add: div_geq)
1.378 +done
1.379 +
1.380 +lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
1.382 +
1.383 +lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
1.384 +apply (subgoal_tac " (n + m) div n = Suc ((n+m-n) div n) ")
1.386 +apply (subst div_geq [symmetric], simp_all)
1.387 +done
1.388 +
1.389 +lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
1.391 +
1.392 +lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
1.394 +apply (subst div_mult1_eq, simp)
1.395 +done
1.396 +
1.397 +lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
1.398 +by (simp add: mult_commute div_mult_self1)
1.399 +
1.400 +
1.401 +(* Monotonicity of div in first argument *)
1.402 +lemma div_le_mono [rule_format (no_asm)]:
1.403 +     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1.404 +apply (case_tac "k=0", simp)
1.405 +apply (induct_tac "n" rule: nat_less_induct, clarify)
1.406 +apply (case_tac "n<k")
1.407 +(* 1  case n<k *)
1.408 +apply simp
1.409 +(* 2  case n >= k *)
1.410 +apply (case_tac "m<k")
1.411 +(* 2.1  case m<k *)
1.412 +apply simp
1.413 +(* 2.2  case m>=k *)
1.414 +apply (simp add: div_geq diff_less diff_le_mono)
1.415 +done
1.416 +
1.417 +(* Antimonotonicity of div in second argument *)
1.418 +lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
1.419 +apply (subgoal_tac "0<n")
1.420 + prefer 2 apply simp
1.421 +apply (induct_tac "k" rule: nat_less_induct)
1.422 +apply (rename_tac "k")
1.423 +apply (case_tac "k<n", simp)
1.424 +apply (subgoal_tac "~ (k<m) ")
1.425 + prefer 2 apply simp
1.427 +apply (subgoal_tac " (k-n) div n \<le> (k-m) div n")
1.428 + prefer 2
1.429 + apply (blast intro: div_le_mono diff_le_mono2)
1.430 +apply (rule le_trans, simp)
1.432 +done
1.433 +
1.434 +lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
1.435 +apply (case_tac "n=0", simp)
1.436 +apply (subgoal_tac "m div n \<le> m div 1", simp)
1.437 +apply (rule div_le_mono2)
1.438 +apply (simp_all (no_asm_simp))
1.439 +done
1.440 +
1.441 +(* Similar for "less than" *)
1.442 +lemma div_less_dividend [rule_format, simp]:
1.443 +     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
1.444 +apply (induct_tac "m" rule: nat_less_induct)
1.445 +apply (rename_tac "m")
1.446 +apply (case_tac "m<n", simp)
1.447 +apply (subgoal_tac "0<n")
1.448 + prefer 2 apply simp
1.450 +apply (case_tac "n<m")
1.451 + apply (subgoal_tac " (m-n) div n < (m-n) ")
1.452 +  apply (rule impI less_trans_Suc)+
1.453 +apply assumption
1.454 +  apply (simp_all add: diff_less)
1.455 +done
1.456 +
1.457 +text{*A fact for the mutilated chess board*}
1.458 +lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
1.459 +apply (case_tac "n=0", simp)
1.460 +apply (induct_tac "m" rule: nat_less_induct)
1.461 +apply (case_tac "Suc (na) <n")
1.462 +(* case Suc(na) < n *)
1.463 +apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
1.464 +(* case n \<le> Suc(na) *)
1.465 +apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
1.466 +apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
1.467 +done
1.468 +
1.469 +
1.470 +subsection{*The Divides Relation*}
1.471 +
1.472 +lemma dvdI [intro?]: "n = m * k ==> m dvd n"
1.473 +by (unfold dvd_def, blast)
1.474 +
1.475 +lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
1.476 +by (unfold dvd_def, blast)
1.477
1.478 -declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
1.479 +lemma dvd_0_right [iff]: "m dvd (0::nat)"
1.480 +apply (unfold dvd_def)
1.481 +apply (blast intro: mult_0_right [symmetric])
1.482 +done
1.483 +
1.484 +lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
1.485 +by (force simp add: dvd_def)
1.486 +
1.487 +lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
1.488 +by (blast intro: dvd_0_left)
1.489 +
1.490 +lemma dvd_1_left [iff]: "Suc 0 dvd k"
1.491 +by (unfold dvd_def, simp)
1.492 +
1.493 +lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
1.495 +
1.496 +lemma dvd_refl [simp]: "m dvd (m::nat)"
1.497 +apply (unfold dvd_def)
1.498 +apply (blast intro: mult_1_right [symmetric])
1.499 +done
1.500 +
1.501 +lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
1.502 +apply (unfold dvd_def)
1.503 +apply (blast intro: mult_assoc)
1.504 +done
1.505 +
1.506 +lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
1.507 +apply (unfold dvd_def)
1.508 +apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
1.509 +done
1.510 +
1.511 +lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
1.512 +apply (unfold dvd_def)
1.513 +apply (blast intro: add_mult_distrib2 [symmetric])
1.514 +done
1.515 +
1.516 +lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
1.517 +apply (unfold dvd_def)
1.518 +apply (blast intro: diff_mult_distrib2 [symmetric])
1.519 +done
1.520 +
1.521 +lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
1.522 +apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
1.524 +done
1.525 +
1.526 +lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
1.527 +by (drule_tac m = m in dvd_diff, auto)
1.528 +
1.529 +lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
1.530 +apply (unfold dvd_def)
1.531 +apply (blast intro: mult_left_commute)
1.532 +done
1.533 +
1.534 +lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
1.535 +apply (subst mult_commute)
1.536 +apply (erule dvd_mult)
1.537 +done
1.538 +
1.539 +(* k dvd (m*k) *)
1.540 +declare dvd_refl [THEN dvd_mult, iff] dvd_refl [THEN dvd_mult2, iff]
1.541 +
1.542 +lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
1.543 +apply (rule iffI)
1.545 +apply (rule_tac [2] dvd_refl)
1.546 +apply (subgoal_tac "n = (n+k) -k")
1.547 + prefer 2 apply simp
1.548 +apply (erule ssubst)
1.549 +apply (erule dvd_diff)
1.550 +apply (rule dvd_refl)
1.551 +done
1.552 +
1.553 +lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
1.554 +apply (unfold dvd_def)
1.555 +apply (case_tac "n=0", auto)
1.556 +apply (blast intro: mod_mult_distrib2 [symmetric])
1.557 +done
1.558 +
1.559 +lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
1.560 +apply (subgoal_tac "k dvd (m div n) *n + m mod n")
1.561 + apply (simp add: mod_div_equality)
1.562 +apply (simp only: dvd_add dvd_mult)
1.563 +done
1.564 +
1.565 +lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
1.566 +by (blast intro: dvd_mod_imp_dvd dvd_mod)
1.567 +
1.568 +lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
1.569 +apply (unfold dvd_def)
1.570 +apply (erule exE)
1.572 +done
1.573 +
1.574 +lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
1.575 +apply auto
1.576 +apply (subgoal_tac "m*n dvd m*1")
1.577 +apply (drule dvd_mult_cancel, auto)
1.578 +done
1.579 +
1.580 +lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
1.581 +apply (subst mult_commute)
1.582 +apply (erule dvd_mult_cancel1)
1.583 +done
1.584 +
1.585 +lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
1.586 +apply (unfold dvd_def, clarify)
1.587 +apply (rule_tac x = "k*ka" in exI)
1.589 +done
1.590 +
1.591 +lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
1.592 +by (simp add: dvd_def mult_assoc, blast)
1.593 +
1.594 +lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
1.595 +apply (unfold dvd_def, clarify)
1.596 +apply (rule_tac x = "i*k" in exI)
1.598 +done
1.599 +
1.600 +lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
1.601 +apply (unfold dvd_def, clarify)
1.602 +apply (simp_all (no_asm_use) add: zero_less_mult_iff)
1.603 +apply (erule conjE)
1.604 +apply (rule le_trans)
1.605 +apply (rule_tac [2] le_refl [THEN mult_le_mono])
1.606 +apply (erule_tac [2] Suc_leI, simp)
1.607 +done
1.608 +
1.609 +lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
1.610 +apply (unfold dvd_def)
1.611 +apply (case_tac "k=0", simp, safe)
1.613 +apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
1.614 +apply (subst mult_commute, simp)
1.615 +done
1.616 +
1.617 +lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
1.618 +apply (subgoal_tac "m mod n = 0")
1.619 + apply (simp add: mult_div_cancel)
1.620 +apply (simp only: dvd_eq_mod_eq_0)
1.621 +done
1.622 +
1.623 +lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
1.624 +by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
1.625 +declare mod_eq_0_iff [THEN iffD1, dest!]
1.626 +
1.627 +(*Loses information, namely we also have r<d provided d is nonzero*)
1.628 +lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
1.629 +apply (cut_tac m = m in mod_div_equality)
1.631 +apply (blast intro: sym)
1.632 +done
1.633 +
1.634
1.635  lemma split_div:
1.636   "P(n div k :: nat) =
1.637 @@ -87,7 +688,7 @@
1.638  qed
1.639
1.640  lemma split_div_lemma:
1.641 -  "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
1.642 +  "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
1.643    apply (rule iffI)
1.644    apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
1.645    apply (simp_all add: quorem_def, arith)
1.646 @@ -103,7 +704,7 @@
1.647
1.648  theorem split_div':
1.649    "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
1.650 -   (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"
1.651 +   (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
1.652    apply (case_tac "0 < n")
1.653    apply (simp only: add: split_div_lemma)
1.655 @@ -148,6 +749,106 @@
1.656    apply arith
1.657    done
1.658
1.659 +ML
1.660 +{*
1.661 +val div_def = thm "div_def"
1.662 +val mod_def = thm "mod_def"
1.663 +val dvd_def = thm "dvd_def"
1.664 +val quorem_def = thm "quorem_def"
1.665 +
1.666 +val wf_less_trans = thm "wf_less_trans";
1.667 +val mod_eq = thm "mod_eq";
1.668 +val div_eq = thm "div_eq";
1.669 +val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";
1.670 +val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";
1.671 +val mod_less = thm "mod_less";
1.672 +val mod_geq = thm "mod_geq";
1.673 +val le_mod_geq = thm "le_mod_geq";
1.674 +val mod_if = thm "mod_if";
1.675 +val mod_1 = thm "mod_1";
1.676 +val mod_self = thm "mod_self";
1.679 +val mod_mult_self1 = thm "mod_mult_self1";
1.680 +val mod_mult_self2 = thm "mod_mult_self2";
1.681 +val mod_mult_distrib = thm "mod_mult_distrib";
1.682 +val mod_mult_distrib2 = thm "mod_mult_distrib2";
1.683 +val mod_mult_self_is_0 = thm "mod_mult_self_is_0";
1.684 +val mod_mult_self1_is_0 = thm "mod_mult_self1_is_0";
1.685 +val div_less = thm "div_less";
1.686 +val div_geq = thm "div_geq";
1.687 +val le_div_geq = thm "le_div_geq";
1.688 +val div_if = thm "div_if";
1.689 +val mod_div_equality = thm "mod_div_equality";
1.690 +val mod_div_equality2 = thm "mod_div_equality2";
1.691 +val div_mod_equality = thm "div_mod_equality";
1.692 +val div_mod_equality2 = thm "div_mod_equality2";
1.693 +val mult_div_cancel = thm "mult_div_cancel";
1.694 +val mod_less_divisor = thm "mod_less_divisor";
1.695 +val div_mult_self_is_m = thm "div_mult_self_is_m";
1.696 +val div_mult_self1_is_m = thm "div_mult_self1_is_m";
1.697 +val unique_quotient_lemma = thm "unique_quotient_lemma";
1.698 +val unique_quotient = thm "unique_quotient";
1.699 +val unique_remainder = thm "unique_remainder";
1.700 +val div_0 = thm "div_0";
1.701 +val mod_0 = thm "mod_0";
1.702 +val div_mult1_eq = thm "div_mult1_eq";
1.703 +val mod_mult1_eq = thm "mod_mult1_eq";
1.704 +val mod_mult1_eq' = thm "mod_mult1_eq'";
1.705 +val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";
1.708 +val mod_lemma = thm "mod_lemma";
1.709 +val div_mult2_eq = thm "div_mult2_eq";
1.710 +val mod_mult2_eq = thm "mod_mult2_eq";
1.711 +val div_mult_mult_lemma = thm "div_mult_mult_lemma";
1.712 +val div_mult_mult1 = thm "div_mult_mult1";
1.713 +val div_mult_mult2 = thm "div_mult_mult2";
1.714 +val div_1 = thm "div_1";
1.715 +val div_self = thm "div_self";
1.718 +val div_mult_self1 = thm "div_mult_self1";
1.719 +val div_mult_self2 = thm "div_mult_self2";
1.720 +val div_le_mono = thm "div_le_mono";
1.721 +val div_le_mono2 = thm "div_le_mono2";
1.722 +val div_le_dividend = thm "div_le_dividend";
1.723 +val div_less_dividend = thm "div_less_dividend";
1.724 +val mod_Suc = thm "mod_Suc";
1.725 +val dvdI = thm "dvdI";
1.726 +val dvdE = thm "dvdE";
1.727 +val dvd_0_right = thm "dvd_0_right";
1.728 +val dvd_0_left = thm "dvd_0_left";
1.729 +val dvd_0_left_iff = thm "dvd_0_left_iff";
1.730 +val dvd_1_left = thm "dvd_1_left";
1.731 +val dvd_1_iff_1 = thm "dvd_1_iff_1";
1.732 +val dvd_refl = thm "dvd_refl";
1.733 +val dvd_trans = thm "dvd_trans";
1.734 +val dvd_anti_sym = thm "dvd_anti_sym";
1.736 +val dvd_diff = thm "dvd_diff";
1.737 +val dvd_diffD = thm "dvd_diffD";
1.738 +val dvd_diffD1 = thm "dvd_diffD1";
1.739 +val dvd_mult = thm "dvd_mult";
1.740 +val dvd_mult2 = thm "dvd_mult2";
1.741 +val dvd_reduce = thm "dvd_reduce";
1.742 +val dvd_mod = thm "dvd_mod";
1.743 +val dvd_mod_imp_dvd = thm "dvd_mod_imp_dvd";
1.744 +val dvd_mod_iff = thm "dvd_mod_iff";
1.745 +val dvd_mult_cancel = thm "dvd_mult_cancel";
1.746 +val dvd_mult_cancel1 = thm "dvd_mult_cancel1";
1.747 +val dvd_mult_cancel2 = thm "dvd_mult_cancel2";
1.748 +val mult_dvd_mono = thm "mult_dvd_mono";
1.749 +val dvd_mult_left = thm "dvd_mult_left";
1.750 +val dvd_mult_right = thm "dvd_mult_right";
1.751 +val dvd_imp_le = thm "dvd_imp_le";
1.752 +val dvd_eq_mod_eq_0 = thm "dvd_eq_mod_eq_0";
1.753 +val dvd_mult_div_cancel = thm "dvd_mult_div_cancel";
1.754 +val mod_eq_0_iff = thm "mod_eq_0_iff";
1.755 +val mod_eqD = thm "mod_eqD";
1.756 +*}
1.757 +
1.758 +
1.759  (*
1.760  lemma split_div:
1.761  assumes m: "m \<noteq> 0"
```