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.38 +by (simp add: mod_def)
    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.42 +by (simp add: div_def)
    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.71 +by (simp add: mod_geq)
    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.80 +apply (simp_all add: mod_geq)
    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.85 +apply (simp add: add_commute)
    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.90 +by (simp add: add_commute mod_add_self2)
    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.94 +apply (simp_all add: add_left_commute [of _ n])
    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.116 +apply (simp add: add_commute)
   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.138 +by (simp add: div_geq)
   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.146 +apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
   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.151 +apply(simp add: mult_commute)
   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.157 +apply(simp add: mod_div_equality)
   1.158 +done
   1.159 +
   1.160 +lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
   1.161 +apply(simp add: mod_div_equality2)
   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.186 +  let val simps = add_0 :: add_0_right :: add_ac
   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.196 +Addsimprocs[cancel_div_mod_proc];
   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.226 +apply (subst less_iff_Suc_add)
   1.227 +apply (auto simp add: add_mult_distrib2)
   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.243 +apply (simp add: quorem_def)
   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.268 +apply (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   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.295 +lemma quorem_add1_eq:
   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.298 +by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.299 +
   1.300 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.301 +lemma div_add1_eq:
   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.310 +                    quorem_add1_eq [THEN quorem_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.322 +apply (simp add: add_mult_distrib2)
   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.328 +apply (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
   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.381 +by (simp add: div_geq)
   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.385 +apply (simp add: add_commute)
   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.390 +by (simp add: add_commute div_add_self2)
   1.391 +
   1.392 +lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
   1.393 +apply (subst div_add1_eq)
   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.426 +apply (simp add: div_geq)
   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.431 +apply (simp add: diff_less)
   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.449 +apply (simp add: div_geq)
   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.494 +by (simp add: dvd_def)
   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.523 +apply (blast intro: dvd_add)
   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.544 +apply (erule_tac [2] dvd_add)
   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.571 +apply (simp add: mult_ac)
   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.588 +apply (simp add: mult_ac)
   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.597 +apply (simp add: mult_ac)
   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.612 +apply (simp add: mult_commute)
   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.630 +apply (simp only: add_ac)
   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.654    apply (simp_all add: DIVISION_BY_ZERO_DIV)
   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.677 +val mod_add_self2 = thm "mod_add_self2";
   1.678 +val mod_add_self1 = thm "mod_add_self1";
   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.706 +val div_add1_eq = thm "div_add1_eq";
   1.707 +val mod_add1_eq = thm "mod_add1_eq";
   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.716 +val div_add_self2 = thm "div_add_self2";
   1.717 +val div_add_self1 = thm "div_add_self1";
   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.735 +val dvd_add = thm "dvd_add";
   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"