src/HOL/Divides.thy
 changeset 22718 936f7580937d parent 22473 753123c89d72 child 22744 5cbe966d67a2
```     1.1 --- a/src/HOL/Divides.thy	Mon Apr 16 16:11:03 2007 +0200
1.2 +++ b/src/HOL/Divides.thy	Tue Apr 17 00:30:44 2007 +0200
1.3 @@ -34,7 +34,7 @@
1.4  instance nat :: "Divides.div"
1.5    mod_def: "m mod n == wfrec (pred_nat^+)
1.6                            (%f j. if j<n | n=0 then j else f (j-n)) m"
1.7 -  div_def:   "m div n == wfrec (pred_nat^+)
1.8 +  div_def:   "m div n == wfrec (pred_nat^+)
1.9                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
1.10
1.11  definition
1.12 @@ -42,13 +42,11 @@
1.13    dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
1.14    dvd_def: "m dvd n \<longleftrightarrow> (\<exists>k. n = m*k)"
1.15
1.16 -consts
1.17 -  quorem :: "(nat*nat) * (nat*nat) => bool"
1.18 -
1.19 -defs
1.20 +definition
1.21 +  quorem :: "(nat*nat) * (nat*nat) => bool" where
1.22    (*This definition helps prove the harder properties of div and mod.
1.23      It is copied from IntDiv.thy; should it be overloaded?*)
1.24 -  quorem_def: "quorem \<equiv> (%((a,b), (q,r)).
1.25 +  "quorem = (%((a,b), (q,r)).
1.26                      a = b*q + r &
1.27                      (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
1.28
1.29 @@ -56,161 +54,150 @@
1.30
1.31  subsection{*Initial Lemmas*}
1.32
1.33 -lemmas wf_less_trans =
1.34 +lemmas wf_less_trans =
1.35         def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
1.36                    standard]
1.37
1.38 -lemma mod_eq: "(%m. m mod n) =
1.39 +lemma mod_eq: "(%m. m mod n) =
1.40                wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
1.42
1.43 -lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
1.44 +lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
1.45                 (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
1.47
1.48
1.49 -(** Aribtrary definitions for division by zero.  Useful to simplify
1.50 +(** Aribtrary definitions for division by zero.  Useful to simplify
1.51      certain equations **)
1.52
1.53  lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
1.54 -by (rule div_eq [THEN wf_less_trans], simp)
1.55 +  by (rule div_eq [THEN wf_less_trans], simp)
1.56
1.57  lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
1.58 -by (rule mod_eq [THEN wf_less_trans], simp)
1.59 +  by (rule mod_eq [THEN wf_less_trans], simp)
1.60
1.61
1.62  subsection{*Remainder*}
1.63
1.64  lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
1.65 -by (rule mod_eq [THEN wf_less_trans], simp)
1.66 +  by (rule mod_eq [THEN wf_less_trans]) simp
1.67
1.68  lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
1.69 -apply (case_tac "n=0", simp)
1.70 -apply (rule mod_eq [THEN wf_less_trans])
1.71 -apply (simp add: cut_apply less_eq)
1.72 -done
1.73 +  apply (cases "n=0")
1.74 +   apply simp
1.75 +  apply (rule mod_eq [THEN wf_less_trans])
1.76 +  apply (simp add: cut_apply less_eq)
1.77 +  done
1.78
1.79  (*Avoids the ugly ~m<n above*)
1.80  lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
1.81 -by (simp add: mod_geq linorder_not_less)
1.82 +  by (simp add: mod_geq linorder_not_less)
1.83
1.84  lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
1.86 +  by (simp add: mod_geq)
1.87
1.88  lemma mod_1 [simp]: "m mod Suc 0 = 0"
1.89 -apply (induct "m")
1.90 -apply (simp_all (no_asm_simp) add: mod_geq)
1.91 -done
1.92 +  by (induct m) (simp_all add: mod_geq)
1.93
1.94  lemma mod_self [simp]: "n mod n = (0::nat)"
1.95 -apply (case_tac "n=0")
1.97 -done
1.98 +  by (cases "n = 0") (simp_all add: mod_geq)
1.99
1.100  lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
1.101 -apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
1.103 -apply (subst mod_geq [symmetric], simp_all)
1.104 -done
1.105 +  apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
1.107 +  apply (subst mod_geq [symmetric], simp_all)
1.108 +  done
1.109
1.110  lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
1.113
1.114  lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
1.115 -apply (induct "k")
1.117 -done
1.119
1.120  lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
1.121 -by (simp add: mult_commute mod_mult_self1)
1.122 +  by (simp add: mult_commute mod_mult_self1)
1.123
1.124  lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
1.125 -apply (case_tac "n=0", simp)
1.126 -apply (case_tac "k=0", simp)
1.127 -apply (induct "m" rule: nat_less_induct)
1.128 -apply (subst mod_if, simp)
1.129 -apply (simp add: mod_geq diff_mult_distrib)
1.130 -done
1.131 +  apply (cases "n = 0", simp)
1.132 +  apply (cases "k = 0", simp)
1.133 +  apply (induct m rule: nat_less_induct)
1.134 +  apply (subst mod_if, simp)
1.135 +  apply (simp add: mod_geq diff_mult_distrib)
1.136 +  done
1.137
1.138  lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
1.139 -by (simp add: mult_commute [of k] mod_mult_distrib)
1.140 +  by (simp add: mult_commute [of k] mod_mult_distrib)
1.141
1.142  lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
1.143 -apply (case_tac "n=0", simp)
1.144 -apply (induct "m", simp)
1.145 -apply (rename_tac "k")
1.146 -apply (cut_tac m = "k*n" and n = n in mod_add_self2)
1.148 -done
1.149 +  apply (cases "n = 0", simp)
1.150 +  apply (induct m, simp)
1.151 +  apply (rename_tac k)
1.152 +  apply (cut_tac m = "k * n" and n = n in mod_add_self2)
1.154 +  done
1.155
1.156  lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
1.157 -by (simp add: mult_commute mod_mult_self_is_0)
1.158 +  by (simp add: mult_commute mod_mult_self_is_0)
1.159
1.160
1.161  subsection{*Quotient*}
1.162
1.163  lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
1.164 -by (rule div_eq [THEN wf_less_trans], simp)
1.165 +  by (rule div_eq [THEN wf_less_trans], simp)
1.166
1.167  lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
1.168 -apply (rule div_eq [THEN wf_less_trans])
1.169 -apply (simp add: cut_apply less_eq)
1.170 -done
1.171 +  apply (rule div_eq [THEN wf_less_trans])
1.172 +  apply (simp add: cut_apply less_eq)
1.173 +  done
1.174
1.175  (*Avoids the ugly ~m<n above*)
1.176  lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
1.177 -by (simp add: div_geq linorder_not_less)
1.178 +  by (simp add: div_geq linorder_not_less)
1.179
1.180  lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
1.182 +  by (simp add: div_geq)
1.183
1.184
1.185  (*Main Result about quotient and remainder.*)
1.186  lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
1.187 -apply (case_tac "n=0", simp)
1.188 -apply (induct "m" rule: nat_less_induct)
1.189 -apply (subst mod_if)
1.191 -done
1.192 +  apply (cases "n = 0", simp)
1.193 +  apply (induct m rule: nat_less_induct)
1.194 +  apply (subst mod_if)
1.196 +  done
1.197
1.198  lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
1.199 -apply(cut_tac m = m and n = n in mod_div_equality)
1.201 -done
1.202 +  apply (cut_tac m = m and n = n in mod_div_equality)
1.203 +  apply (simp add: mult_commute)
1.204 +  done
1.205
1.206  subsection{*Simproc for Cancelling Div and Mod*}
1.207
1.208  lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
1.210 -done
1.211 +  by (simp add: mod_div_equality)
1.212
1.213  lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
1.215 -done
1.216 +  by (simp add: mod_div_equality2)
1.217
1.218  ML
1.219  {*
1.220 -val div_mod_equality = thm "div_mod_equality";
1.221 -val div_mod_equality2 = thm "div_mod_equality2";
1.222 -
1.223 -
1.224  structure CancelDivModData =
1.225  struct
1.226
1.227 -val div_name = "Divides.div";
1.228 -val mod_name = "Divides.mod";
1.229 +val div_name = @{const_name Divides.div};
1.230 +val mod_name = @{const_name Divides.mod};
1.231  val mk_binop = HOLogic.mk_binop;
1.232  val mk_sum = NatArithUtils.mk_sum;
1.233  val dest_sum = NatArithUtils.dest_sum;
1.234
1.235  (*logic*)
1.236
1.237 -val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
1.238 +val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
1.239
1.240  val trans = trans
1.241
1.242  val prove_eq_sums =
1.245    in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
1.246
1.247  end;
1.248 @@ -226,25 +213,26 @@
1.249
1.250  (* a simple rearrangement of mod_div_equality: *)
1.251  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
1.252 -by (cut_tac m = m and n = n in mod_div_equality2, arith)
1.253 +  by (cut_tac m = m and n = n in mod_div_equality2, arith)
1.254
1.255  lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
1.256 -apply (induct "m" rule: nat_less_induct)
1.257 -apply (case_tac "na<n", simp)
1.258 -txt{*case @{term "n \<le> na"}*}
1.260 -done
1.261 +  apply (induct m rule: nat_less_induct)
1.262 +  apply (rename_tac m)
1.263 +  apply (case_tac "m<n", simp)
1.264 +  txt{*case @{term "n \<le> m"}*}
1.265 +  apply (simp add: mod_geq)
1.266 +  done
1.267
1.268  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
1.269 -apply(drule mod_less_divisor[where m = m])
1.270 -apply simp
1.271 -done
1.272 +  apply (drule mod_less_divisor [where m = m])
1.273 +  apply simp
1.274 +  done
1.275
1.276  lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
1.277 -by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
1.278 +  by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
1.279
1.280  lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
1.281 -by (simp add: mult_commute div_mult_self_is_m)
1.282 +  by (simp add: mult_commute div_mult_self_is_m)
1.283
1.284  (*mod_mult_distrib2 above is the counterpart for remainder*)
1.285
1.286 @@ -252,95 +240,93 @@
1.287  subsection{*Proving facts about Quotient and Remainder*}
1.288
1.289  lemma unique_quotient_lemma:
1.290 -     "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
1.291 +     "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
1.292        ==> q' \<le> (q::nat)"
1.293 -apply (rule leI)
1.296 -done
1.297 +  apply (rule leI)
1.300 +  done
1.301
1.302  lemma unique_quotient:
1.303 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
1.304 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
1.305        ==> q = q'"
1.306 -apply (simp add: split_ifs quorem_def)
1.307 -apply (blast intro: order_antisym
1.308 -             dest: order_eq_refl [THEN unique_quotient_lemma] sym)
1.309 -done
1.310 +  apply (simp add: split_ifs quorem_def)
1.311 +  apply (blast intro: order_antisym
1.312 +    dest: order_eq_refl [THEN unique_quotient_lemma] sym)
1.313 +  done
1.314
1.315  lemma unique_remainder:
1.316 -     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
1.317 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]
1.318        ==> r = r'"
1.319 -apply (subgoal_tac "q = q'")
1.320 -prefer 2 apply (blast intro: unique_quotient)
1.322 -done
1.323 +  apply (subgoal_tac "q = q'")
1.324 +   prefer 2 apply (blast intro: unique_quotient)
1.325 +  apply (simp add: quorem_def)
1.326 +  done
1.327
1.328  lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
1.329 -  unfolding quorem_def by simp
1.330 +  unfolding quorem_def by simp
1.331
1.332  lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
1.333 -by (simp add: quorem_div_mod [THEN unique_quotient])
1.334 +  by (simp add: quorem_div_mod [THEN unique_quotient])
1.335
1.336  lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
1.337 -by (simp add: quorem_div_mod [THEN unique_remainder])
1.338 +  by (simp add: quorem_div_mod [THEN unique_remainder])
1.339
1.340  (** A dividend of zero **)
1.341
1.342  lemma div_0 [simp]: "0 div m = (0::nat)"
1.343 -by (case_tac "m=0", simp_all)
1.344 +  by (cases "m = 0") simp_all
1.345
1.346  lemma mod_0 [simp]: "0 mod m = (0::nat)"
1.347 -by (case_tac "m=0", simp_all)
1.348 +  by (cases "m = 0") simp_all
1.349
1.350  (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
1.351
1.352  lemma quorem_mult1_eq:
1.353 -     "[| quorem((b,c),(q,r));  0 < c |]
1.354 +     "[| quorem((b,c),(q,r));  0 < c |]
1.355        ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
1.357 -done
1.359
1.360  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
1.361 -apply (case_tac "c = 0", simp)
1.362 -apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
1.363 -done
1.364 +  apply (cases "c = 0", simp)
1.365 +  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
1.366 +  done
1.367
1.368  lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
1.369 -apply (case_tac "c = 0", simp)
1.370 -apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
1.371 -done
1.372 +  apply (cases "c = 0", simp)
1.373 +  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
1.374 +  done
1.375
1.376  lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
1.377 -apply (rule trans)
1.378 -apply (rule_tac s = "b*a mod c" in trans)
1.379 -apply (rule_tac [2] mod_mult1_eq)
1.380 -apply (simp_all (no_asm) add: mult_commute)
1.381 -done
1.382 +  apply (rule trans)
1.383 +   apply (rule_tac s = "b*a mod c" in trans)
1.384 +    apply (rule_tac [2] mod_mult1_eq)
1.385 +   apply (simp_all add: mult_commute)
1.386 +  done
1.387
1.388  lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
1.389 -apply (rule mod_mult1_eq' [THEN trans])
1.390 -apply (rule mod_mult1_eq)
1.391 -done
1.392 +  apply (rule mod_mult1_eq' [THEN trans])
1.393 +  apply (rule mod_mult1_eq)
1.394 +  done
1.395
1.396  (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
1.397
1.399 -     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]
1.400 +     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]
1.401        ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
1.404
1.405  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.407       "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
1.408 -apply (case_tac "c = 0", simp)
1.409 -apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
1.410 -done
1.411 +  apply (cases "c = 0", simp)
1.412 +  apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
1.413 +  done
1.414
1.415  lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
1.416 -apply (case_tac "c = 0", simp)
1.417 -apply (blast intro: quorem_div_mod quorem_div_mod
1.419 -done
1.420 +  apply (cases "c = 0", simp)
1.421 +  apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
1.422 +  done
1.423
1.424
1.425  subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
1.426 @@ -348,45 +334,44 @@
1.427  (** first, a lemma to bound the remainder **)
1.428
1.429  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
1.430 -apply (cut_tac m = q and n = c in mod_less_divisor)
1.431 -apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1.432 -apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
1.434 -done
1.435 +  apply (cut_tac m = q and n = c in mod_less_divisor)
1.436 +  apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1.437 +  apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
1.439 +  done
1.440
1.441 -lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]
1.442 +lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]
1.443        ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
1.445 -done
1.447
1.448  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
1.449 -apply (case_tac "b=0", simp)
1.450 -apply (case_tac "c=0", simp)
1.451 -apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
1.452 -done
1.453 +  apply (cases "b = 0", simp)
1.454 +  apply (cases "c = 0", simp)
1.455 +  apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
1.456 +  done
1.457
1.458  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
1.459 -apply (case_tac "b=0", simp)
1.460 -apply (case_tac "c=0", simp)
1.461 -apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
1.462 -done
1.463 +  apply (cases "b = 0", simp)
1.464 +  apply (cases "c = 0", simp)
1.465 +  apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
1.466 +  done
1.467
1.468
1.469  subsection{*Cancellation of Common Factors in Division*}
1.470
1.471  lemma div_mult_mult_lemma:
1.472 -     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
1.473 -by (auto simp add: div_mult2_eq)
1.474 +    "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
1.475 +  by (auto simp add: div_mult2_eq)
1.476
1.477  lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
1.478 -apply (case_tac "b = 0")
1.479 -apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
1.480 -done
1.481 +  apply (cases "b = 0")
1.482 +  apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
1.483 +  done
1.484
1.485  lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
1.486 -apply (drule div_mult_mult1)
1.487 -apply (auto simp add: mult_commute)
1.488 -done
1.489 +  apply (drule div_mult_mult1)
1.490 +  apply (auto simp add: mult_commute)
1.491 +  done
1.492
1.493
1.494  (*Distribution of Factors over Remainders:
1.495 @@ -404,34 +389,32 @@
1.496  subsection{*Further Facts about Quotient and Remainder*}
1.497
1.498  lemma div_1 [simp]: "m div Suc 0 = m"
1.499 -apply (induct "m")
1.500 -apply (simp_all (no_asm_simp) add: div_geq)
1.501 -done
1.502 +  by (induct m) (simp_all add: div_geq)
1.503
1.504  lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
1.506 +  by (simp add: div_geq)
1.507
1.508  lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
1.509 -apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
1.511 -apply (subst div_geq [symmetric], simp_all)
1.512 -done
1.513 +  apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
1.515 +  apply (subst div_geq [symmetric], simp_all)
1.516 +  done
1.517
1.518  lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
1.521
1.522  lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
1.524 -apply (subst div_mult1_eq, simp)
1.525 -done
1.527 +  apply (subst div_mult1_eq, simp)
1.528 +  done
1.529
1.530  lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
1.531 -by (simp add: mult_commute div_mult_self1)
1.532 +  by (simp add: mult_commute div_mult_self1)
1.533
1.534
1.535  (* Monotonicity of div in first argument *)
1.536  lemma div_le_mono [rule_format (no_asm)]:
1.537 -     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1.538 +    "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1.539  apply (case_tac "k=0", simp)
1.540  apply (induct "n" rule: nat_less_induct, clarify)
1.541  apply (case_tac "n<k")
1.542 @@ -448,12 +431,12 @@
1.543  (* Antimonotonicity of div in second argument *)
1.544  lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
1.545  apply (subgoal_tac "0<n")
1.546 - prefer 2 apply simp
1.547 + prefer 2 apply simp
1.548  apply (induct_tac k rule: nat_less_induct)
1.549  apply (rename_tac "k")
1.550  apply (case_tac "k<n", simp)
1.551  apply (subgoal_tac "~ (k<m) ")
1.552 - prefer 2 apply simp
1.553 + prefer 2 apply simp
1.555  apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
1.556   prefer 2
1.557 @@ -469,14 +452,14 @@
1.558  apply (simp_all (no_asm_simp))
1.559  done
1.560
1.561 -(* Similar for "less than" *)
1.562 +(* Similar for "less than" *)
1.563  lemma div_less_dividend [rule_format]:
1.564       "!!n::nat. 1<n ==> 0 < m --> m div n < m"
1.565  apply (induct_tac m rule: nat_less_induct)
1.566  apply (rename_tac "m")
1.567  apply (case_tac "m<n", simp)
1.568  apply (subgoal_tac "0<n")
1.569 - prefer 2 apply simp
1.570 + prefer 2 apply simp
1.572  apply (case_tac "n<m")
1.573   apply (subgoal_tac "(m-n) div n < (m-n) ")
1.574 @@ -500,199 +483,187 @@
1.575  done
1.576
1.577  lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
1.578 -by (case_tac "n=0", auto)
1.579 +  by (cases "n = 0") auto
1.580
1.581  lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
1.582 -by (case_tac "n=0", auto)
1.583 +  by (cases "n = 0") auto
1.584
1.585
1.586  subsection{*The Divides Relation*}
1.587
1.588  lemma dvdI [intro?]: "n = m * k ==> m dvd n"
1.589 -by (unfold dvd_def, blast)
1.590 +  unfolding dvd_def by blast
1.591
1.592  lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
1.593 -by (unfold dvd_def, blast)
1.594 +  unfolding dvd_def by blast
1.595
1.596  lemma dvd_0_right [iff]: "m dvd (0::nat)"
1.597 -apply (unfold dvd_def)
1.598 -apply (blast intro: mult_0_right [symmetric])
1.599 -done
1.600 +  unfolding dvd_def by (blast intro: mult_0_right [symmetric])
1.601
1.602  lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
1.603 -by (force simp add: dvd_def)
1.604 +  by (force simp add: dvd_def)
1.605
1.606  lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
1.607 -by (blast intro: dvd_0_left)
1.608 +  by (blast intro: dvd_0_left)
1.609
1.610  lemma dvd_1_left [iff]: "Suc 0 dvd k"
1.611 -by (unfold dvd_def, simp)
1.612 +  unfolding dvd_def by simp
1.613
1.614  lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
1.616 +  by (simp add: dvd_def)
1.617
1.618  lemma dvd_refl [simp]: "m dvd (m::nat)"
1.619 -apply (unfold dvd_def)
1.620 -apply (blast intro: mult_1_right [symmetric])
1.621 -done
1.622 +  unfolding dvd_def by (blast intro: mult_1_right [symmetric])
1.623
1.624  lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
1.625 -apply (unfold dvd_def)
1.626 -apply (blast intro: mult_assoc)
1.627 -done
1.628 +  unfolding dvd_def by (blast intro: mult_assoc)
1.629
1.630  lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
1.631 -apply (unfold dvd_def)
1.632 -apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
1.633 -done
1.634 +  unfolding dvd_def
1.635 +  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
1.636
1.637  lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
1.638 -apply (unfold dvd_def)
1.639 -apply (blast intro: add_mult_distrib2 [symmetric])
1.640 -done
1.641 +  unfolding dvd_def
1.642 +  by (blast intro: add_mult_distrib2 [symmetric])
1.643
1.644  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
1.645 -apply (unfold dvd_def)
1.646 -apply (blast intro: diff_mult_distrib2 [symmetric])
1.647 -done
1.648 +  unfolding dvd_def
1.649 +  by (blast intro: diff_mult_distrib2 [symmetric])
1.650
1.651  lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
1.652 -apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
1.654 -done
1.655 +  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
1.656 +  apply (blast intro: dvd_add)
1.657 +  done
1.658
1.659  lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
1.660 -by (drule_tac m = m in dvd_diff, auto)
1.661 +  by (drule_tac m = m in dvd_diff, auto)
1.662
1.663  lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
1.664 -apply (unfold dvd_def)
1.665 -apply (blast intro: mult_left_commute)
1.666 -done
1.667 +  unfolding dvd_def by (blast intro: mult_left_commute)
1.668
1.669  lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
1.670 -apply (subst mult_commute)
1.671 -apply (erule dvd_mult)
1.672 -done
1.673 +  apply (subst mult_commute)
1.674 +  apply (erule dvd_mult)
1.675 +  done
1.676
1.677  lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
1.678 -by (rule dvd_refl [THEN dvd_mult])
1.679 +  by (rule dvd_refl [THEN dvd_mult])
1.680
1.681  lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
1.682 -by (rule dvd_refl [THEN dvd_mult2])
1.683 +  by (rule dvd_refl [THEN dvd_mult2])
1.684
1.685  lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
1.686 -apply (rule iffI)
1.688 -apply (rule_tac [2] dvd_refl)
1.689 -apply (subgoal_tac "n = (n+k) -k")
1.690 - prefer 2 apply simp
1.691 -apply (erule ssubst)
1.692 -apply (erule dvd_diff)
1.693 -apply (rule dvd_refl)
1.694 -done
1.695 +  apply (rule iffI)
1.696 +   apply (erule_tac [2] dvd_add)
1.697 +   apply (rule_tac [2] dvd_refl)
1.698 +  apply (subgoal_tac "n = (n+k) -k")
1.699 +   prefer 2 apply simp
1.700 +  apply (erule ssubst)
1.701 +  apply (erule dvd_diff)
1.702 +  apply (rule dvd_refl)
1.703 +  done
1.704
1.705  lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
1.706 -apply (unfold dvd_def)
1.707 -apply (case_tac "n=0", auto)
1.708 -apply (blast intro: mod_mult_distrib2 [symmetric])
1.709 -done
1.710 +  unfolding dvd_def
1.711 +  apply (case_tac "n = 0", auto)
1.712 +  apply (blast intro: mod_mult_distrib2 [symmetric])
1.713 +  done
1.714
1.715  lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
1.716 -apply (subgoal_tac "k dvd (m div n) *n + m mod n")
1.717 - apply (simp add: mod_div_equality)
1.718 -apply (simp only: dvd_add dvd_mult)
1.719 -done
1.720 +  apply (subgoal_tac "k dvd (m div n) *n + m mod n")
1.721 +   apply (simp add: mod_div_equality)
1.722 +  apply (simp only: dvd_add dvd_mult)
1.723 +  done
1.724
1.725  lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
1.726 -by (blast intro: dvd_mod_imp_dvd dvd_mod)
1.727 +  by (blast intro: dvd_mod_imp_dvd dvd_mod)
1.728
1.729  lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
1.730 -apply (unfold dvd_def)
1.731 -apply (erule exE)
1.733 -done
1.734 +  unfolding dvd_def
1.735 +  apply (erule exE)
1.736 +  apply (simp add: mult_ac)
1.737 +  done
1.738
1.739  lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
1.740 -apply auto
1.741 -apply (subgoal_tac "m*n dvd m*1")
1.742 -apply (drule dvd_mult_cancel, auto)
1.743 -done
1.744 +  apply auto
1.745 +   apply (subgoal_tac "m*n dvd m*1")
1.746 +   apply (drule dvd_mult_cancel, auto)
1.747 +  done
1.748
1.749  lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
1.750 -apply (subst mult_commute)
1.751 -apply (erule dvd_mult_cancel1)
1.752 -done
1.753 +  apply (subst mult_commute)
1.754 +  apply (erule dvd_mult_cancel1)
1.755 +  done
1.756
1.757  lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
1.758 -apply (unfold dvd_def, clarify)
1.759 -apply (rule_tac x = "k*ka" in exI)
1.761 -done
1.762 +  apply (unfold dvd_def, clarify)
1.763 +  apply (rule_tac x = "k*ka" in exI)
1.764 +  apply (simp add: mult_ac)
1.765 +  done
1.766
1.767  lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
1.768 -by (simp add: dvd_def mult_assoc, blast)
1.769 +  by (simp add: dvd_def mult_assoc, blast)
1.770
1.771  lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
1.772 -apply (unfold dvd_def, clarify)
1.773 -apply (rule_tac x = "i*k" in exI)
1.775 -done
1.776 +  apply (unfold dvd_def, clarify)
1.777 +  apply (rule_tac x = "i*k" in exI)
1.778 +  apply (simp add: mult_ac)
1.779 +  done
1.780
1.781  lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
1.782 -apply (unfold dvd_def, clarify)
1.783 -apply (simp_all (no_asm_use) add: zero_less_mult_iff)
1.784 -apply (erule conjE)
1.785 -apply (rule le_trans)
1.786 -apply (rule_tac [2] le_refl [THEN mult_le_mono])
1.787 -apply (erule_tac [2] Suc_leI, simp)
1.788 -done
1.789 +  apply (unfold dvd_def, clarify)
1.790 +  apply (simp_all (no_asm_use) add: zero_less_mult_iff)
1.791 +  apply (erule conjE)
1.792 +  apply (rule le_trans)
1.793 +   apply (rule_tac [2] le_refl [THEN mult_le_mono])
1.794 +   apply (erule_tac [2] Suc_leI, simp)
1.795 +  done
1.796
1.797  lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
1.798 -apply (unfold dvd_def)
1.799 -apply (case_tac "k=0", simp, safe)
1.801 -apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
1.802 -apply (subst mult_commute, simp)
1.803 -done
1.804 +  apply (unfold dvd_def)
1.805 +  apply (case_tac "k=0", simp, safe)
1.806 +   apply (simp add: mult_commute)
1.807 +  apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
1.808 +  apply (subst mult_commute, simp)
1.809 +  done
1.810
1.811  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
1.812 -apply (subgoal_tac "m mod n = 0")
1.813 - apply (simp add: mult_div_cancel)
1.814 -apply (simp only: dvd_eq_mod_eq_0)
1.815 -done
1.816 +  apply (subgoal_tac "m mod n = 0")
1.817 +   apply (simp add: mult_div_cancel)
1.818 +  apply (simp only: dvd_eq_mod_eq_0)
1.819 +  done
1.820
1.821  lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
1.822 -apply (unfold dvd_def)
1.823 -apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
1.825 -done
1.826 +  apply (unfold dvd_def)
1.827 +  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
1.829 +  done
1.830
1.831  lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
1.832 -by (induct "n", auto)
1.833 +  by (induct n) auto
1.834
1.835  lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
1.836 -apply (induct "j")
1.838 -apply (blast dest!: dvd_mult_right)
1.839 -done
1.840 +  apply (induct j)
1.841 +   apply (simp_all add: le_Suc_eq)
1.842 +  apply (blast dest!: dvd_mult_right)
1.843 +  done
1.844
1.845  lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
1.846 -apply (rule power_le_imp_le_exp, assumption)
1.847 -apply (erule dvd_imp_le, simp)
1.848 -done
1.849 +  apply (rule power_le_imp_le_exp, assumption)
1.850 +  apply (erule dvd_imp_le, simp)
1.851 +  done
1.852
1.853  lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
1.854 -by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
1.855 +  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
1.856
1.857 -lemmas mod_eq_0D = mod_eq_0_iff [THEN iffD1]
1.858 -declare mod_eq_0D [dest!]
1.859 +lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
1.860
1.861  (*Loses information, namely we also have r<d provided d is nonzero*)
1.862  lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
1.863 -apply (cut_tac m = m in mod_div_equality)
1.865 -apply (blast intro: sym)
1.866 -done
1.867 +  apply (cut_tac m = m in mod_div_equality)
1.868 +  apply (simp only: add_ac)
1.869 +  apply (blast intro: sym)
1.870 +  done
1.871
1.872
1.873  lemma split_div:
1.874 @@ -713,11 +684,11 @@
1.875        assume n: "n = k*i + j" and j: "j < k"
1.876        show "P i"
1.877        proof (cases)
1.878 -	assume "i = 0"
1.879 -	with n j P show "P i" by simp
1.880 +        assume "i = 0"
1.881 +        with n j P show "P i" by simp
1.882        next
1.883 -	assume "i \<noteq> 0"
1.884 -	with not0 n j P show "P i" by(simp add:add_ac)
1.885 +        assume "i \<noteq> 0"
1.886 +        with not0 n j P show "P i" by(simp add:add_ac)
1.887        qed
1.888      qed
1.889    qed
1.890 @@ -818,28 +789,28 @@
1.891        assume ih: "?A n"
1.892        show "?A (Suc n)"
1.893        proof (clarsimp)
1.894 -	assume y: "P (p - Suc n)"
1.895 -	have n: "Suc n < p"
1.896 -	proof (rule ccontr)
1.897 -	  assume "\<not>(Suc n < p)"
1.898 -	  hence "p - Suc n = 0"
1.899 -	    by simp
1.900 -	  with y contra show "False"
1.901 -	    by simp
1.902 -	qed
1.903 -	hence n2: "Suc (p - Suc n) = p-n" by arith
1.904 -	from p have "p - Suc n < p" by arith
1.905 -	with y step have z: "P ((Suc (p - Suc n)) mod p)"
1.906 -	  by blast
1.907 -	show "False"
1.908 -	proof (cases "n=0")
1.909 -	  case True
1.910 -	  with z n2 contra show ?thesis by simp
1.911 -	next
1.912 -	  case False
1.913 -	  with p have "p-n < p" by arith
1.914 -	  with z n2 False ih show ?thesis by simp
1.915 -	qed
1.916 +        assume y: "P (p - Suc n)"
1.917 +        have n: "Suc n < p"
1.918 +        proof (rule ccontr)
1.919 +          assume "\<not>(Suc n < p)"
1.920 +          hence "p - Suc n = 0"
1.921 +            by simp
1.922 +          with y contra show "False"
1.923 +            by simp
1.924 +        qed
1.925 +        hence n2: "Suc (p - Suc n) = p-n" by arith
1.926 +        from p have "p - Suc n < p" by arith
1.927 +        with y step have z: "P ((Suc (p - Suc n)) mod p)"
1.928 +          by blast
1.929 +        show "False"
1.930 +        proof (cases "n=0")
1.931 +          case True
1.932 +          with z n2 contra show ?thesis by simp
1.933 +        next
1.934 +          case False
1.935 +          with p have "p-n < p" by arith
1.936 +          with z n2 False ih show ?thesis by simp
1.937 +        qed
1.938        qed
1.939      qed
1.940    qed
1.941 @@ -864,22 +835,22 @@
1.942      show "j<p \<longrightarrow> P j" (is "?A j")
1.943      proof (induct j)
1.944        from step base i show "?A 0"
1.945 -	by (auto elim: mod_induct_0)
1.946 +        by (auto elim: mod_induct_0)
1.947      next
1.948        fix k
1.949        assume ih: "?A k"
1.950        show "?A (Suc k)"
1.951        proof
1.952 -	assume suc: "Suc k < p"
1.953 -	hence k: "k<p" by simp
1.954 -	with ih have "P k" ..
1.955 -	with step k have "P (Suc k mod p)"
1.956 -	  by blast
1.957 -	moreover
1.958 -	from suc have "Suc k mod p = Suc k"
1.959 -	  by simp
1.960 -	ultimately
1.961 -	show "P (Suc k)" by simp
1.962 +        assume suc: "Suc k < p"
1.963 +        hence k: "k<p" by simp
1.964 +        with ih have "P k" ..
1.965 +        with step k have "P (Suc k mod p)"
1.966 +          by blast
1.967 +        moreover
1.968 +        from suc have "Suc k mod p = Suc k"
1.969 +          by simp
1.970 +        ultimately
1.971 +        show "P (Suc k)" by simp
1.972        qed
1.973      qed
1.974    qed
1.975 @@ -889,15 +860,15 @@
1.976
1.977  lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
1.978    apply (rule trans [symmetric])
1.979 -  apply (rule mod_add1_eq, simp)
1.980 +   apply (rule mod_add1_eq, simp)
1.982    done
1.983
1.984  lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
1.985 -apply (rule trans [symmetric])
1.988 -done
1.989 +  apply (rule trans [symmetric])
1.990 +   apply (rule mod_add1_eq, simp)
1.991 +  apply (rule mod_add1_eq [symmetric])
1.992 +  done
1.993
1.994
1.995  subsection {* Code generation for div and mod *}
1.996 @@ -905,25 +876,21 @@
1.997  definition
1.998    "divmod (m\<Colon>nat) n = (m div n, m mod n)"
1.999
1.1000 -lemma divmod_zero [code]:
1.1001 -  "divmod m 0 = (0, m)"
1.1002 +lemma divmod_zero [code]: "divmod m 0 = (0, m)"
1.1003    unfolding divmod_def by simp
1.1004
1.1005  lemma divmod_succ [code]:
1.1006    "divmod m (Suc k) = (if m < Suc k then (0, m) else
1.1007      let
1.1008        (p, q) = divmod (m - Suc k) (Suc k)
1.1009 -    in (Suc p, q)
1.1010 -  )"
1.1011 +    in (Suc p, q))"
1.1012    unfolding divmod_def Let_def split_def
1.1013    by (auto intro: div_geq mod_geq)
1.1014
1.1015 -lemma div_divmod [code]:
1.1016 -  "m div n = fst (divmod m n)"
1.1017 +lemma div_divmod [code]: "m div n = fst (divmod m n)"
1.1018    unfolding divmod_def by simp
1.1019
1.1020 -lemma mod_divmod [code]:
1.1021 -  "m mod n = snd (divmod m n)"
1.1022 +lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
1.1023    unfolding divmod_def by simp
1.1024
1.1025  code_modulename SML
1.1026 @@ -934,7 +901,6 @@
1.1027
1.1028  hide (open) const divmod
1.1029
1.1030 -
1.1031  subsection {* Legacy bindings *}
1.1032
1.1033  ML
1.1034 @@ -1038,7 +1004,6 @@
1.1035  val mod_eqD = thm "mod_eqD";
1.1036  *}
1.1037
1.1038 -
1.1039  (*
1.1040  lemma split_div:
1.1041  assumes m: "m \<noteq> 0"
```