More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
to Isar script.
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 -use "Divides_lemmas.ML"
1.29
1.30 -declare dvdI [intro?] dvdE [elim?] dvd_trans [trans]
1.31 +
1.32 +subsection{*Initial Lemmas*}
1.33 +
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 + wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
1.40 +by (simp add: mod_def)
1.41 +
1.42 +lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)
1.43 + (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
1.44 +by (simp add: div_def)
1.45 +
1.46 +
1.47 +(** Aribtrary definitions for division by zero. Useful to simplify
1.48 + certain equations **)
1.49 +
1.50 +lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
1.51 +by (rule div_eq [THEN wf_less_trans], simp)
1.52 +
1.53 +lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
1.54 +by (rule mod_eq [THEN wf_less_trans], simp)
1.55 +
1.56 +
1.57 +subsection{*Remainder*}
1.58 +
1.59 +lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
1.60 +by (rule mod_eq [THEN wf_less_trans], simp)
1.61 +
1.62 +lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
1.63 +apply (case_tac "n=0", simp)
1.64 +apply (rule mod_eq [THEN wf_less_trans])
1.65 +apply (simp add: diff_less cut_apply less_eq)
1.66 +done
1.67 +
1.68 +(*Avoids the ugly ~m<n above*)
1.69 +lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
1.70 +by (simp add: mod_geq not_less_iff_le)
1.71 +
1.72 +lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
1.73 +by (simp add: mod_geq)
1.74 +
1.75 +lemma mod_1 [simp]: "m mod Suc 0 = 0"
1.76 +apply (induct_tac "m")
1.77 +apply (simp_all (no_asm_simp) add: mod_geq)
1.78 +done
1.79 +
1.80 +lemma mod_self [simp]: "n mod n = (0::nat)"
1.81 +apply (case_tac "n=0")
1.82 +apply (simp_all add: mod_geq)
1.83 +done
1.84 +
1.85 +lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
1.86 +apply (subgoal_tac " (n + m) mod n = (n+m-n) mod n")
1.87 +apply (simp add: add_commute)
1.88 +apply (subst mod_geq [symmetric], simp_all)
1.89 +done
1.90 +
1.91 +lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
1.92 +by (simp add: add_commute mod_add_self2)
1.93 +
1.94 +lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
1.95 +apply (induct_tac "k")
1.96 +apply (simp_all add: add_left_commute [of _ n])
1.97 +done
1.98 +
1.99 +lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
1.100 +by (simp add: mult_commute mod_mult_self1)
1.101 +
1.102 +lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
1.103 +apply (case_tac "n=0", simp)
1.104 +apply (case_tac "k=0", simp)
1.105 +apply (induct_tac "m" rule: nat_less_induct)
1.106 +apply (subst mod_if, simp)
1.107 +apply (simp add: mod_geq diff_less diff_mult_distrib)
1.108 +done
1.109 +
1.110 +lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
1.111 +by (simp add: mult_commute [of k] mod_mult_distrib)
1.112 +
1.113 +lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
1.114 +apply (case_tac "n=0", simp)
1.115 +apply (induct_tac "m", simp)
1.116 +apply (rename_tac "k")
1.117 +apply (cut_tac m = "k*n" and n = n in mod_add_self2)
1.118 +apply (simp add: add_commute)
1.119 +done
1.120 +
1.121 +lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
1.122 +by (simp add: mult_commute mod_mult_self_is_0)
1.123 +
1.124 +
1.125 +subsection{*Quotient*}
1.126 +
1.127 +lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
1.128 +by (rule div_eq [THEN wf_less_trans], simp)
1.129 +
1.130 +lemma div_geq: "[| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"
1.131 +apply (rule div_eq [THEN wf_less_trans])
1.132 +apply (simp add: diff_less cut_apply less_eq)
1.133 +done
1.134 +
1.135 +(*Avoids the ugly ~m<n above*)
1.136 +lemma le_div_geq: "[| 0<n; n\<le>m |] ==> m div n = Suc((m-n) div n)"
1.137 +by (simp add: div_geq not_less_iff_le)
1.138 +
1.139 +lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
1.140 +by (simp add: div_geq)
1.141 +
1.142 +
1.143 +(*Main Result about quotient and remainder.*)
1.144 +lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
1.145 +apply (case_tac "n=0", simp)
1.146 +apply (induct_tac "m" rule: nat_less_induct)
1.147 +apply (subst mod_if)
1.148 +apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
1.149 +done
1.150 +
1.151 +lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
1.152 +apply(cut_tac m = m and n = n in mod_div_equality)
1.153 +apply(simp add: mult_commute)
1.154 +done
1.155 +
1.156 +subsection{*Simproc for Cancelling Div and Mod*}
1.157 +
1.158 +lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
1.159 +apply(simp add: mod_div_equality)
1.160 +done
1.161 +
1.162 +lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
1.163 +apply(simp add: mod_div_equality2)
1.164 +done
1.165 +
1.166 +ML
1.167 +{*
1.168 +val div_mod_equality = thm "div_mod_equality";
1.169 +val div_mod_equality2 = thm "div_mod_equality2";
1.170 +
1.171 +
1.172 +structure CancelDivModData =
1.173 +struct
1.174 +
1.175 +val div_name = "Divides.op div";
1.176 +val mod_name = "Divides.op mod";
1.177 +val mk_binop = HOLogic.mk_binop;
1.178 +val mk_sum = NatArithUtils.mk_sum;
1.179 +val dest_sum = NatArithUtils.dest_sum;
1.180 +
1.181 +(*logic*)
1.182 +
1.183 +val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
1.184 +
1.185 +val trans = trans
1.186 +
1.187 +val prove_eq_sums =
1.188 + let val simps = add_0 :: add_0_right :: add_ac
1.189 + in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
1.190 +
1.191 +end;
1.192 +
1.193 +structure CancelDivMod = CancelDivModFun(CancelDivModData);
1.194 +
1.195 +val cancel_div_mod_proc = NatArithUtils.prep_simproc
1.196 + ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
1.197 +
1.198 +Addsimprocs[cancel_div_mod_proc];
1.199 +*}
1.200 +
1.201 +
1.202 +(* a simple rearrangement of mod_div_equality: *)
1.203 +lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
1.204 +by (cut_tac m = m and n = n in mod_div_equality2, arith)
1.205 +
1.206 +lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
1.207 +apply (induct_tac "m" rule: nat_less_induct)
1.208 +apply (case_tac "na<n", simp)
1.209 +txt{*case @{term "n \<le> na"}*}
1.210 +apply (simp add: mod_geq diff_less)
1.211 +done
1.212 +
1.213 +lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
1.214 +by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
1.215 +
1.216 +lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
1.217 +by (simp add: mult_commute div_mult_self_is_m)
1.218 +
1.219 +(*mod_mult_distrib2 above is the counterpart for remainder*)
1.220 +
1.221 +
1.222 +subsection{*Proving facts about Quotient and Remainder*}
1.223 +
1.224 +lemma unique_quotient_lemma:
1.225 + "[| b*q' + r' \<le> b*q + r; 0 < b; r < b |]
1.226 + ==> q' \<le> (q::nat)"
1.227 +apply (rule leI)
1.228 +apply (subst less_iff_Suc_add)
1.229 +apply (auto simp add: add_mult_distrib2)
1.230 +done
1.231 +
1.232 +lemma unique_quotient:
1.233 + "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b |]
1.234 + ==> q = q'"
1.235 +apply (simp add: split_ifs quorem_def)
1.236 +apply (blast intro: order_antisym
1.237 + dest: order_eq_refl [THEN unique_quotient_lemma] sym)+
1.238 +done
1.239 +
1.240 +lemma unique_remainder:
1.241 + "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b |]
1.242 + ==> r = r'"
1.243 +apply (subgoal_tac "q = q'")
1.244 +prefer 2 apply (blast intro: unique_quotient)
1.245 +apply (simp add: quorem_def)
1.246 +done
1.247 +
1.248 +lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
1.249 +by (auto simp add: quorem_def)
1.250 +
1.251 +lemma quorem_div: "[| quorem((a,b),(q,r)); 0 < b |] ==> a div b = q"
1.252 +by (simp add: quorem_div_mod [THEN unique_quotient])
1.253 +
1.254 +lemma quorem_mod: "[| quorem((a,b),(q,r)); 0 < b |] ==> a mod b = r"
1.255 +by (simp add: quorem_div_mod [THEN unique_remainder])
1.256 +
1.257 +(** A dividend of zero **)
1.258 +
1.259 +lemma div_0 [simp]: "0 div m = (0::nat)"
1.260 +by (case_tac "m=0", simp_all)
1.261 +
1.262 +lemma mod_0 [simp]: "0 mod m = (0::nat)"
1.263 +by (case_tac "m=0", simp_all)
1.264 +
1.265 +(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
1.266 +
1.267 +lemma quorem_mult1_eq:
1.268 + "[| quorem((b,c),(q,r)); 0 < c |]
1.269 + ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
1.270 +apply (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
1.271 +done
1.272 +
1.273 +lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
1.274 +apply (case_tac "c = 0", simp)
1.275 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
1.276 +done
1.277 +
1.278 +lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
1.279 +apply (case_tac "c = 0", simp)
1.280 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
1.281 +done
1.282 +
1.283 +lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
1.284 +apply (rule trans)
1.285 +apply (rule_tac s = "b*a mod c" in trans)
1.286 +apply (rule_tac [2] mod_mult1_eq)
1.287 +apply (simp_all (no_asm) add: mult_commute)
1.288 +done
1.289 +
1.290 +lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
1.291 +apply (rule mod_mult1_eq' [THEN trans])
1.292 +apply (rule mod_mult1_eq)
1.293 +done
1.294 +
1.295 +(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
1.296 +
1.297 +lemma quorem_add1_eq:
1.298 + "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); 0 < c |]
1.299 + ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
1.300 +by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
1.301 +
1.302 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.303 +lemma div_add1_eq:
1.304 + "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
1.305 +apply (case_tac "c = 0", simp)
1.306 +apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
1.307 +done
1.308 +
1.309 +lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
1.310 +apply (case_tac "c = 0", simp)
1.311 +apply (blast intro: quorem_div_mod quorem_div_mod
1.312 + quorem_add1_eq [THEN quorem_mod])
1.313 +done
1.314 +
1.315 +
1.316 +subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
1.317 +
1.318 +(** first, a lemma to bound the remainder **)
1.319 +
1.320 +lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
1.321 +apply (cut_tac m = q and n = c in mod_less_divisor)
1.322 +apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1.323 +apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
1.324 +apply (simp add: add_mult_distrib2)
1.325 +done
1.326 +
1.327 +lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r)); 0 < b; 0 < c |]
1.328 + ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
1.329 +apply (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
1.330 +done
1.331 +
1.332 +lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
1.333 +apply (case_tac "b=0", simp)
1.334 +apply (case_tac "c=0", simp)
1.335 +apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
1.336 +done
1.337 +
1.338 +lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
1.339 +apply (case_tac "b=0", simp)
1.340 +apply (case_tac "c=0", simp)
1.341 +apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
1.342 +done
1.343 +
1.344 +
1.345 +subsection{*Cancellation of Common Factors in Division*}
1.346 +
1.347 +lemma div_mult_mult_lemma:
1.348 + "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b"
1.349 +by (auto simp add: div_mult2_eq)
1.350 +
1.351 +lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
1.352 +apply (case_tac "b = 0")
1.353 +apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
1.354 +done
1.355 +
1.356 +lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
1.357 +apply (drule div_mult_mult1)
1.358 +apply (auto simp add: mult_commute)
1.359 +done
1.360 +
1.361 +
1.362 +(*Distribution of Factors over Remainders:
1.363 +
1.364 +Could prove these as in Integ/IntDiv.ML, but we already have
1.365 +mod_mult_distrib and mod_mult_distrib2 above!
1.366 +
1.367 +Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"
1.368 +qed "mod_mult_mult1";
1.369 +
1.370 +Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
1.371 +qed "mod_mult_mult2";
1.372 + ***)
1.373 +
1.374 +subsection{*Further Facts about Quotient and Remainder*}
1.375 +
1.376 +lemma div_1 [simp]: "m div Suc 0 = m"
1.377 +apply (induct_tac "m")
1.378 +apply (simp_all (no_asm_simp) add: div_geq)
1.379 +done
1.380 +
1.381 +lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
1.382 +by (simp add: div_geq)
1.383 +
1.384 +lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
1.385 +apply (subgoal_tac " (n + m) div n = Suc ((n+m-n) div n) ")
1.386 +apply (simp add: add_commute)
1.387 +apply (subst div_geq [symmetric], simp_all)
1.388 +done
1.389 +
1.390 +lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
1.391 +by (simp add: add_commute div_add_self2)
1.392 +
1.393 +lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
1.394 +apply (subst div_add1_eq)
1.395 +apply (subst div_mult1_eq, simp)
1.396 +done
1.397 +
1.398 +lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
1.399 +by (simp add: mult_commute div_mult_self1)
1.400 +
1.401 +
1.402 +(* Monotonicity of div in first argument *)
1.403 +lemma div_le_mono [rule_format (no_asm)]:
1.404 + "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1.405 +apply (case_tac "k=0", simp)
1.406 +apply (induct_tac "n" rule: nat_less_induct, clarify)
1.407 +apply (case_tac "n<k")
1.408 +(* 1 case n<k *)
1.409 +apply simp
1.410 +(* 2 case n >= k *)
1.411 +apply (case_tac "m<k")
1.412 +(* 2.1 case m<k *)
1.413 +apply simp
1.414 +(* 2.2 case m>=k *)
1.415 +apply (simp add: div_geq diff_less diff_le_mono)
1.416 +done
1.417 +
1.418 +(* Antimonotonicity of div in second argument *)
1.419 +lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
1.420 +apply (subgoal_tac "0<n")
1.421 + prefer 2 apply simp
1.422 +apply (induct_tac "k" rule: nat_less_induct)
1.423 +apply (rename_tac "k")
1.424 +apply (case_tac "k<n", simp)
1.425 +apply (subgoal_tac "~ (k<m) ")
1.426 + prefer 2 apply simp
1.427 +apply (simp add: div_geq)
1.428 +apply (subgoal_tac " (k-n) div n \<le> (k-m) div n")
1.429 + prefer 2
1.430 + apply (blast intro: div_le_mono diff_le_mono2)
1.431 +apply (rule le_trans, simp)
1.432 +apply (simp add: diff_less)
1.433 +done
1.434 +
1.435 +lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
1.436 +apply (case_tac "n=0", simp)
1.437 +apply (subgoal_tac "m div n \<le> m div 1", simp)
1.438 +apply (rule div_le_mono2)
1.439 +apply (simp_all (no_asm_simp))
1.440 +done
1.441 +
1.442 +(* Similar for "less than" *)
1.443 +lemma div_less_dividend [rule_format, simp]:
1.444 + "!!n::nat. 1<n ==> 0 < m --> m div n < m"
1.445 +apply (induct_tac "m" rule: nat_less_induct)
1.446 +apply (rename_tac "m")
1.447 +apply (case_tac "m<n", simp)
1.448 +apply (subgoal_tac "0<n")
1.449 + prefer 2 apply simp
1.450 +apply (simp add: div_geq)
1.451 +apply (case_tac "n<m")
1.452 + apply (subgoal_tac " (m-n) div n < (m-n) ")
1.453 + apply (rule impI less_trans_Suc)+
1.454 +apply assumption
1.455 + apply (simp_all add: diff_less)
1.456 +done
1.457 +
1.458 +text{*A fact for the mutilated chess board*}
1.459 +lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
1.460 +apply (case_tac "n=0", simp)
1.461 +apply (induct_tac "m" rule: nat_less_induct)
1.462 +apply (case_tac "Suc (na) <n")
1.463 +(* case Suc(na) < n *)
1.464 +apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
1.465 +(* case n \<le> Suc(na) *)
1.466 +apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
1.467 +apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
1.468 +done
1.469 +
1.470 +
1.471 +subsection{*The Divides Relation*}
1.472 +
1.473 +lemma dvdI [intro?]: "n = m * k ==> m dvd n"
1.474 +by (unfold dvd_def, blast)
1.475 +
1.476 +lemma dvdE [elim?]: "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"
1.477 +by (unfold dvd_def, blast)
1.478 +
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"
2.1 --- a/src/HOL/Divides_lemmas.ML Mon Nov 24 15:33:07 2003 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,734 +0,0 @@
2.4 -(* Title: HOL/Divides.ML
2.5 - ID: $Id$
2.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.7 - Copyright 1993 University of Cambridge
2.8 -
2.9 -The division operators div, mod and the divides relation "dvd"
2.10 -*)
2.11 -
2.12 -(* ML legacy bindings *)
2.13 -
2.14 -val div_def = thm "div_def";
2.15 -val mod_def = thm "mod_def";
2.16 -val dvd_def = thm "dvd_def";
2.17 -val quorem_def = thm "quorem_def";
2.18 -
2.19 -structure Divides =
2.20 -struct
2.21 - val div_def = div_def
2.22 - val mod_def = mod_def
2.23 - val dvd_def = dvd_def
2.24 - val quorem_def = quorem_def
2.25 -end;
2.26 -
2.27 -(** Less-then properties **)
2.28 -
2.29 -bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS
2.30 - def_wfrec RS trans);
2.31 -
2.32 -Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
2.33 -\ (%f j. if j<n | n=0 then j else f (j-n))";
2.34 -by (simp_tac (simpset() addsimps [mod_def]) 1);
2.35 -qed "mod_eq";
2.36 -
2.37 -Goal "(%m. m div n) = wfrec (trancl pred_nat) \
2.38 -\ (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))";
2.39 -by (simp_tac (simpset() addsimps [div_def]) 1);
2.40 -qed "div_eq";
2.41 -
2.42 -
2.43 -(** Aribtrary definitions for division by zero. Useful to simplify
2.44 - certain equations **)
2.45 -
2.46 -Goal "a div 0 = (0::nat)";
2.47 -by (rtac (div_eq RS wf_less_trans) 1);
2.48 -by (Asm_simp_tac 1);
2.49 -qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*)
2.50 -
2.51 -Goal "a mod 0 = (a::nat)";
2.52 -by (rtac (mod_eq RS wf_less_trans) 1);
2.53 -by (Asm_simp_tac 1);
2.54 -qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*)
2.55 -
2.56 -fun div_undefined_case_tac s i =
2.57 - case_tac s i THEN
2.58 - Full_simp_tac (i+1) THEN
2.59 - asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV,
2.60 - DIVISION_BY_ZERO_MOD]) i;
2.61 -
2.62 -(*** Remainder ***)
2.63 -
2.64 -Goal "m<n ==> m mod n = (m::nat)";
2.65 -by (rtac (mod_eq RS wf_less_trans) 1);
2.66 -by (Asm_simp_tac 1);
2.67 -qed "mod_less";
2.68 -Addsimps [mod_less];
2.69 -
2.70 -Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n";
2.71 -by (div_undefined_case_tac "n=0" 1);
2.72 -by (rtac (mod_eq RS wf_less_trans) 1);
2.73 -by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
2.74 -qed "mod_geq";
2.75 -
2.76 -(*Avoids the ugly ~m<n above*)
2.77 -Goal "(n::nat) <= m ==> m mod n = (m-n) mod n";
2.78 -by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
2.79 -qed "le_mod_geq";
2.80 -
2.81 -Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)";
2.82 -by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
2.83 -qed "mod_if";
2.84 -
2.85 -Goal "m mod Suc 0 = 0";
2.86 -by (induct_tac "m" 1);
2.87 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
2.88 -qed "mod_1";
2.89 -Addsimps [mod_1];
2.90 -
2.91 -Goal "n mod n = (0::nat)";
2.92 -by (div_undefined_case_tac "n=0" 1);
2.93 -by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
2.94 -qed "mod_self";
2.95 -Addsimps [mod_self];
2.96 -
2.97 -Goal "(m+n) mod n = m mod (n::nat)";
2.98 -by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
2.99 -by (stac (mod_geq RS sym) 2);
2.100 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
2.101 -qed "mod_add_self2";
2.102 -
2.103 -Goal "(n+m) mod n = m mod (n::nat)";
2.104 -by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
2.105 -qed "mod_add_self1";
2.106 -
2.107 -Addsimps [mod_add_self1, mod_add_self2];
2.108 -
2.109 -Goal "(m + k*n) mod n = m mod (n::nat)";
2.110 -by (induct_tac "k" 1);
2.111 -by (ALLGOALS
2.112 - (asm_simp_tac
2.113 - (simpset() addsimps [read_instantiate [("y","n")] add_left_commute])));
2.114 -qed "mod_mult_self1";
2.115 -
2.116 -Goal "(m + n*k) mod n = m mod (n::nat)";
2.117 -by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
2.118 -qed "mod_mult_self2";
2.119 -
2.120 -Addsimps [mod_mult_self1, mod_mult_self2];
2.121 -
2.122 -Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)";
2.123 -by (div_undefined_case_tac "n=0" 1);
2.124 -by (div_undefined_case_tac "k=0" 1);
2.125 -by (induct_thm_tac nat_less_induct "m" 1);
2.126 -by (stac mod_if 1);
2.127 -by (Asm_simp_tac 1);
2.128 -by (asm_simp_tac (simpset() addsimps [mod_geq,
2.129 - diff_less, diff_mult_distrib]) 1);
2.130 -qed "mod_mult_distrib";
2.131 -
2.132 -Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)";
2.133 -by (asm_simp_tac
2.134 - (simpset() addsimps [read_instantiate [("m","k")] mult_commute,
2.135 - mod_mult_distrib]) 1);
2.136 -qed "mod_mult_distrib2";
2.137 -
2.138 -Goal "(m*n) mod n = (0::nat)";
2.139 -by (div_undefined_case_tac "n=0" 1);
2.140 -by (induct_tac "m" 1);
2.141 -by (Asm_simp_tac 1);
2.142 -by (rename_tac "k" 1);
2.143 -by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1);
2.144 -by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
2.145 -qed "mod_mult_self_is_0";
2.146 -
2.147 -Goal "(n*m) mod n = (0::nat)";
2.148 -by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1);
2.149 -qed "mod_mult_self1_is_0";
2.150 -Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0];
2.151 -
2.152 -
2.153 -(*** Quotient ***)
2.154 -
2.155 -Goal "m<n ==> m div n = (0::nat)";
2.156 -by (rtac (div_eq RS wf_less_trans) 1);
2.157 -by (Asm_simp_tac 1);
2.158 -qed "div_less";
2.159 -Addsimps [div_less];
2.160 -
2.161 -Goal "[| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)";
2.162 -by (rtac (div_eq RS wf_less_trans) 1);
2.163 -by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
2.164 -qed "div_geq";
2.165 -
2.166 -(*Avoids the ugly ~m<n above*)
2.167 -Goal "[| 0<n; n<=m |] ==> m div n = Suc((m-n) div n)";
2.168 -by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
2.169 -qed "le_div_geq";
2.170 -
2.171 -Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
2.172 -by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
2.173 -qed "div_if";
2.174 -
2.175 -
2.176 -(*Main Result about quotient and remainder.*)
2.177 -Goal "(m div n)*n + m mod n = (m::nat)";
2.178 -by (div_undefined_case_tac "n=0" 1);
2.179 -by (induct_thm_tac nat_less_induct "m" 1);
2.180 -by (stac mod_if 1);
2.181 -by (ALLGOALS (asm_simp_tac
2.182 - (simpset() addsimps [add_assoc, div_geq,
2.183 - add_diff_inverse, diff_less])));
2.184 -qed "mod_div_equality";
2.185 -
2.186 -Goal "n * (m div n) + m mod n = (m::nat)";
2.187 -by(cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
2.188 -by(asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
2.189 -qed "mod_div_equality2";
2.190 -
2.191 -(*-----------------------------------------------------------------------*)
2.192 -(*Simproc for cancelling div and mod *)
2.193 -(*-----------------------------------------------------------------------*)
2.194 -
2.195 -Goal "((m div n)*n + m mod n) + k = (m::nat) + k";
2.196 -by(simp_tac (simpset() addsimps [mod_div_equality]) 1);
2.197 -qed "div_mod_equality";
2.198 -
2.199 -Goal "(n*(m div n) + m mod n) + k = (m::nat) + k";
2.200 -by(simp_tac (simpset() addsimps [thm"mod_div_equality2"]) 1);
2.201 -qed "div_mod_equality2";
2.202 -
2.203 -structure CancelDivModData =
2.204 -struct
2.205 -
2.206 -val div_name = "Divides.op div";
2.207 -val mod_name = "Divides.op mod";
2.208 -val mk_binop = HOLogic.mk_binop;
2.209 -val mk_sum = NatArithUtils.mk_sum;
2.210 -val dest_sum = NatArithUtils.dest_sum;
2.211 -
2.212 -(*logic*)
2.213 -
2.214 -val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
2.215 -
2.216 -val trans = trans
2.217 -
2.218 -val prove_eq_sums =
2.219 - let val simps = add_0 :: add_0_right :: add_ac
2.220 - in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
2.221 -
2.222 -end;
2.223 -
2.224 -structure CancelDivMod = CancelDivModFun(CancelDivModData);
2.225 -
2.226 -val cancel_div_mod_proc = NatArithUtils.prep_simproc
2.227 - ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
2.228 -
2.229 -Addsimprocs[cancel_div_mod_proc];
2.230 -
2.231 -
2.232 -(* a simple rearrangement of mod_div_equality: *)
2.233 -Goal "(n::nat) * (m div n) = m - (m mod n)";
2.234 -by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality2 1);
2.235 -by (arith_tac 1);
2.236 -qed "mult_div_cancel";
2.237 -
2.238 -Goal "0<n ==> m mod n < (n::nat)";
2.239 -by (induct_thm_tac nat_less_induct "m" 1);
2.240 -by (case_tac "na<n" 1);
2.241 -(*case n le na*)
2.242 -by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
2.243 -(*case na<n*)
2.244 -by (Asm_simp_tac 1);
2.245 -qed "mod_less_divisor";
2.246 -Addsimps [mod_less_divisor];
2.247 -
2.248 -(*** More division laws ***)
2.249 -
2.250 -Goal "0<n ==> (m*n) div n = (m::nat)";
2.251 -by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
2.252 -by Auto_tac;
2.253 -qed "div_mult_self_is_m";
2.254 -
2.255 -Goal "0<n ==> (n*m) div n = (m::nat)";
2.256 -by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
2.257 -qed "div_mult_self1_is_m";
2.258 -Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
2.259 -
2.260 -(*mod_mult_distrib2 above is the counterpart for remainder*)
2.261 -
2.262 -
2.263 -(*** Proving facts about div and mod using quorem ***)
2.264 -
2.265 -Goal "[| b*q' + r' <= b*q + r; 0 < b; r < b |] \
2.266 -\ ==> q' <= (q::nat)";
2.267 -by (rtac leI 1);
2.268 -by (stac less_iff_Suc_add 1);
2.269 -by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2]));
2.270 -qed "unique_quotient_lemma";
2.271 -
2.272 -Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b |] \
2.273 -\ ==> q = q'";
2.274 -by (asm_full_simp_tac
2.275 - (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);
2.276 -by (REPEAT
2.277 - (blast_tac (claset() addIs [order_antisym]
2.278 - addDs [order_eq_refl RS unique_quotient_lemma,
2.279 - sym]) 1));
2.280 -qed "unique_quotient";
2.281 -
2.282 -Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b |] \
2.283 -\ ==> r = r'";
2.284 -by (subgoal_tac "q = q'" 1);
2.285 -by (blast_tac (claset() addIs [unique_quotient]) 2);
2.286 -by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1);
2.287 -qed "unique_remainder";
2.288 -
2.289 -Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
2.290 -by (auto_tac
2.291 - (claset() addEs [sym],
2.292 - simpset() addsimps mult_ac@[Divides.quorem_def]));
2.293 -qed "quorem_div_mod";
2.294 -
2.295 -Goal "[| quorem((a,b),(q,r)); 0 < b |] ==> a div b = q";
2.296 -by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
2.297 -qed "quorem_div";
2.298 -
2.299 -Goal "[| quorem((a,b),(q,r)); 0 < b |] ==> a mod b = r";
2.300 -by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
2.301 -qed "quorem_mod";
2.302 -
2.303 -(** A dividend of zero **)
2.304 -
2.305 -Goal "0 div m = (0::nat)";
2.306 -by (div_undefined_case_tac "m=0" 1);
2.307 -by (Asm_simp_tac 1);
2.308 -qed "div_0";
2.309 -
2.310 -Goal "0 mod m = (0::nat)";
2.311 -by (div_undefined_case_tac "m=0" 1);
2.312 -by (Asm_simp_tac 1);
2.313 -qed "mod_0";
2.314 -Addsimps [div_0, mod_0];
2.315 -
2.316 -(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
2.317 -
2.318 -Goal "[| quorem((b,c),(q,r)); 0 < c |] \
2.319 -\ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
2.320 -by (auto_tac
2.321 - (claset(),
2.322 - simpset() addsimps split_ifs@mult_ac@
2.323 - [Divides.quorem_def, add_mult_distrib2]));
2.324 -val lemma = result();
2.325 -
2.326 -Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)";
2.327 -by (div_undefined_case_tac "c = 0" 1);
2.328 -by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
2.329 -qed "div_mult1_eq";
2.330 -
2.331 -Goal "(a*b) mod c = a*(b mod c) mod (c::nat)";
2.332 -by (div_undefined_case_tac "c = 0" 1);
2.333 -by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
2.334 -qed "mod_mult1_eq";
2.335 -
2.336 -Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c";
2.337 -by (rtac trans 1);
2.338 -by (res_inst_tac [("s","b*a mod c")] trans 1);
2.339 -by (rtac mod_mult1_eq 2);
2.340 -by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute])));
2.341 -qed "mod_mult1_eq'";
2.342 -
2.343 -Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c";
2.344 -by (rtac (mod_mult1_eq' RS trans) 1);
2.345 -by (rtac mod_mult1_eq 1);
2.346 -qed "mod_mult_distrib_mod";
2.347 -
2.348 -(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
2.349 -
2.350 -Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); 0 < c |] \
2.351 -\ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
2.352 -by (auto_tac
2.353 - (claset(),
2.354 - simpset() addsimps split_ifs@mult_ac@
2.355 - [Divides.quorem_def, add_mult_distrib2]));
2.356 -val lemma = result();
2.357 -
2.358 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
2.359 -Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)";
2.360 -by (div_undefined_case_tac "c = 0" 1);
2.361 -by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
2.362 - MRS lemma RS quorem_div]) 1);
2.363 -qed "div_add1_eq";
2.364 -
2.365 -Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c";
2.366 -by (div_undefined_case_tac "c = 0" 1);
2.367 -by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
2.368 - MRS lemma RS quorem_mod]) 1);
2.369 -qed "mod_add1_eq";
2.370 -
2.371 -
2.372 -(*** proving a div (b*c) = (a div b) div c ***)
2.373 -
2.374 -(** first, a lemma to bound the remainder **)
2.375 -
2.376 -Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c";
2.377 -by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1);
2.378 -by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2);
2.379 -by Auto_tac;
2.380 -by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1);
2.381 -by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1);
2.382 -val mod_lemma = result();
2.383 -
2.384 -Goal "[| quorem ((a,b), (q,r)); 0 < b; 0 < c |] \
2.385 -\ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
2.386 -by (auto_tac
2.387 - (claset(),
2.388 - simpset() addsimps mult_ac@
2.389 - [Divides.quorem_def, add_mult_distrib2 RS sym,
2.390 - mod_lemma]));
2.391 -val lemma = result();
2.392 -
2.393 -Goal "a div (b*c) = (a div b) div (c::nat)";
2.394 -by (div_undefined_case_tac "b=0" 1);
2.395 -by (div_undefined_case_tac "c=0" 1);
2.396 -by (force_tac (claset(),
2.397 - simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1);
2.398 -qed "div_mult2_eq";
2.399 -
2.400 -Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
2.401 -by (div_undefined_case_tac "b=0" 1);
2.402 -by (div_undefined_case_tac "c=0" 1);
2.403 -by (auto_tac (claset(),
2.404 - simpset() addsimps [mult_commute,
2.405 - quorem_div_mod RS lemma RS quorem_mod]));
2.406 -qed "mod_mult2_eq";
2.407 -
2.408 -
2.409 -(*** Cancellation of common factors in "div" ***)
2.410 -
2.411 -Goal "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b";
2.412 -by (stac div_mult2_eq 1);
2.413 -by Auto_tac;
2.414 -val lemma1 = result();
2.415 -
2.416 -Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b";
2.417 -by (div_undefined_case_tac "b = 0" 1);
2.418 -by (auto_tac
2.419 - (claset(),
2.420 - simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff,
2.421 - lemma1, lemma2]));
2.422 -qed "div_mult_mult1";
2.423 -
2.424 -Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b";
2.425 -by (dtac div_mult_mult1 1);
2.426 -by (auto_tac (claset(), simpset() addsimps [mult_commute]));
2.427 -qed "div_mult_mult2";
2.428 -
2.429 -Addsimps [div_mult_mult1, div_mult_mult2];
2.430 -
2.431 -
2.432 -(*** Distribution of factors over "mod"
2.433 -
2.434 -Could prove these as in Integ/IntDiv.ML, but we already have
2.435 -mod_mult_distrib and mod_mult_distrib2 above!
2.436 -
2.437 -Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)";
2.438 -qed "mod_mult_mult1";
2.439 -
2.440 -Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
2.441 -qed "mod_mult_mult2";
2.442 - ***)
2.443 -
2.444 -(*** Further facts about div and mod ***)
2.445 -
2.446 -Goal "m div Suc 0 = m";
2.447 -by (induct_tac "m" 1);
2.448 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
2.449 -qed "div_1";
2.450 -Addsimps [div_1];
2.451 -
2.452 -Goal "0<n ==> n div n = (1::nat)";
2.453 -by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
2.454 -qed "div_self";
2.455 -Addsimps [div_self];
2.456 -
2.457 -Goal "0<n ==> (m+n) div n = Suc (m div n)";
2.458 -by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
2.459 -by (stac (div_geq RS sym) 2);
2.460 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
2.461 -qed "div_add_self2";
2.462 -
2.463 -Goal "0<n ==> (n+m) div n = Suc (m div n)";
2.464 -by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
2.465 -qed "div_add_self1";
2.466 -
2.467 -Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
2.468 -by (stac div_add1_eq 1);
2.469 -by (stac div_mult1_eq 1);
2.470 -by (Asm_simp_tac 1);
2.471 -qed "div_mult_self1";
2.472 -
2.473 -Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)";
2.474 -by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
2.475 -qed "div_mult_self2";
2.476 -
2.477 -Addsimps [div_mult_self1, div_mult_self2];
2.478 -
2.479 -(* Monotonicity of div in first argument *)
2.480 -Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
2.481 -by (div_undefined_case_tac "k=0" 1);
2.482 -by (induct_thm_tac nat_less_induct "n" 1);
2.483 -by (Clarify_tac 1);
2.484 -by (case_tac "n<k" 1);
2.485 -(* 1 case n<k *)
2.486 -by (Asm_simp_tac 1);
2.487 -(* 2 case n >= k *)
2.488 -by (case_tac "m<k" 1);
2.489 -(* 2.1 case m<k *)
2.490 -by (Asm_simp_tac 1);
2.491 -(* 2.2 case m>=k *)
2.492 -by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
2.493 -qed_spec_mp "div_le_mono";
2.494 -
2.495 -(* Antimonotonicity of div in second argument *)
2.496 -Goal "!!m::nat. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
2.497 -by (subgoal_tac "0<n" 1);
2.498 - by (Asm_simp_tac 2);
2.499 -by (induct_thm_tac nat_less_induct "k" 1);
2.500 -by (rename_tac "k" 1);
2.501 -by (case_tac "k<n" 1);
2.502 - by (Asm_simp_tac 1);
2.503 -by (subgoal_tac "~(k<m)" 1);
2.504 - by (Asm_simp_tac 2);
2.505 -by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
2.506 -by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
2.507 - by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2));
2.508 -by (rtac le_trans 1);
2.509 -by (Asm_simp_tac 1);
2.510 -by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
2.511 -qed "div_le_mono2";
2.512 -
2.513 -Goal "m div n <= (m::nat)";
2.514 -by (div_undefined_case_tac "n=0" 1);
2.515 -by (subgoal_tac "m div n <= m div 1" 1);
2.516 -by (Asm_full_simp_tac 1);
2.517 -by (rtac div_le_mono2 1);
2.518 -by (ALLGOALS Asm_simp_tac);
2.519 -qed "div_le_dividend";
2.520 -Addsimps [div_le_dividend];
2.521 -
2.522 -(* Similar for "less than" *)
2.523 -Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)";
2.524 -by (induct_thm_tac nat_less_induct "m" 1);
2.525 -by (rename_tac "m" 1);
2.526 -by (case_tac "m<n" 1);
2.527 - by (Asm_full_simp_tac 1);
2.528 -by (subgoal_tac "0<n" 1);
2.529 - by (Asm_simp_tac 2);
2.530 -by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
2.531 -by (case_tac "n<m" 1);
2.532 - by (subgoal_tac "(m-n) div n < (m-n)" 1);
2.533 - by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
2.534 - by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
2.535 - by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
2.536 -(* case n=m *)
2.537 -by (subgoal_tac "m=n" 1);
2.538 - by (Asm_simp_tac 2);
2.539 -by (Asm_simp_tac 1);
2.540 -qed_spec_mp "div_less_dividend";
2.541 -Addsimps [div_less_dividend];
2.542 -
2.543 -(*** Further facts about mod (mainly for the mutilated chess board ***)
2.544 -
2.545 -Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
2.546 -by (div_undefined_case_tac "n=0" 1);
2.547 -by (induct_thm_tac nat_less_induct "m" 1);
2.548 -by (case_tac "Suc(na)<n" 1);
2.549 -(* case Suc(na) < n *)
2.550 -by (forward_tac [lessI RS less_trans] 1
2.551 - THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1);
2.552 -(* case n <= Suc(na) *)
2.553 -by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq,
2.554 - mod_geq]) 1);
2.555 -by (auto_tac (claset(),
2.556 - simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
2.557 -qed "mod_Suc";
2.558 -
2.559 -
2.560 -(************************************************)
2.561 -(** Divides Relation **)
2.562 -(************************************************)
2.563 -
2.564 -Goalw [dvd_def] "n = m * k ==> m dvd n";
2.565 -by (Blast_tac 1);
2.566 -qed "dvdI";
2.567 -
2.568 -Goalw [dvd_def] "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P";
2.569 -by (Blast_tac 1);
2.570 -qed "dvdE";
2.571 -
2.572 -Goalw [dvd_def] "m dvd (0::nat)";
2.573 -by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
2.574 -qed "dvd_0_right";
2.575 -AddIffs [dvd_0_right];
2.576 -
2.577 -Goalw [dvd_def] "0 dvd m ==> m = (0::nat)";
2.578 -by Auto_tac;
2.579 -qed "dvd_0_left";
2.580 -
2.581 -Goal "(0 dvd (m::nat)) = (m = 0)";
2.582 -by (blast_tac (claset() addIs [dvd_0_left]) 1);
2.583 -qed "dvd_0_left_iff";
2.584 -AddIffs [dvd_0_left_iff];
2.585 -
2.586 -Goalw [dvd_def] "Suc 0 dvd k";
2.587 -by (Simp_tac 1);
2.588 -qed "dvd_1_left";
2.589 -AddIffs [dvd_1_left];
2.590 -
2.591 -Goal "(m dvd Suc 0) = (m = Suc 0)";
2.592 -by (simp_tac (simpset() addsimps [dvd_def]) 1);
2.593 -qed "dvd_1_iff_1";
2.594 -Addsimps [dvd_1_iff_1];
2.595 -
2.596 -Goalw [dvd_def] "m dvd (m::nat)";
2.597 -by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
2.598 -qed "dvd_refl";
2.599 -Addsimps [dvd_refl];
2.600 -
2.601 -Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
2.602 -by (blast_tac (claset() addIs [mult_assoc] ) 1);
2.603 -qed "dvd_trans";
2.604 -
2.605 -Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
2.606 -by (force_tac (claset() addDs [mult_eq_self_implies_10],
2.607 - simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
2.608 -qed "dvd_anti_sym";
2.609 -
2.610 -Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
2.611 -by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
2.612 -qed "dvd_add";
2.613 -
2.614 -Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
2.615 -by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
2.616 -qed "dvd_diff";
2.617 -
2.618 -Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)";
2.619 -by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
2.620 -by (blast_tac (claset() addIs [dvd_add]) 1);
2.621 -qed "dvd_diffD";
2.622 -
2.623 -Goal "[| k dvd m-n; k dvd m; n<=m |] ==> k dvd (n::nat)";
2.624 -by (dres_inst_tac [("m","m")] dvd_diff 1);
2.625 -by Auto_tac;
2.626 -qed "dvd_diffD1";
2.627 -
2.628 -Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
2.629 -by (blast_tac (claset() addIs [mult_left_commute]) 1);
2.630 -qed "dvd_mult";
2.631 -
2.632 -Goal "k dvd m ==> k dvd (m*n :: nat)";
2.633 -by (stac mult_commute 1);
2.634 -by (etac dvd_mult 1);
2.635 -qed "dvd_mult2";
2.636 -
2.637 -(* k dvd (m*k) *)
2.638 -AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
2.639 -
2.640 -Goal "(k dvd n + k) = (k dvd (n::nat))";
2.641 -by (rtac iffI 1);
2.642 -by (etac dvd_add 2);
2.643 -by (rtac dvd_refl 2);
2.644 -by (subgoal_tac "n = (n+k)-k" 1);
2.645 -by (Simp_tac 2);
2.646 -by (etac ssubst 1);
2.647 -by (etac dvd_diff 1);
2.648 -by (rtac dvd_refl 1);
2.649 -qed "dvd_reduce";
2.650 -
2.651 -Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
2.652 -by (div_undefined_case_tac "n=0" 1);
2.653 -by Auto_tac;
2.654 -by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);
2.655 -qed "dvd_mod";
2.656 -
2.657 -Goal "[| (k::nat) dvd m mod n; k dvd n |] ==> k dvd m";
2.658 -by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
2.659 -by (asm_simp_tac (HOL_basic_ss addsimps [dvd_add, dvd_mult]) 2);
2.660 -by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
2.661 -qed "dvd_mod_imp_dvd";
2.662 -
2.663 -Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
2.664 -by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1);
2.665 -qed "dvd_mod_iff";
2.666 -
2.667 -Goalw [dvd_def] "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n";
2.668 -by (etac exE 1);
2.669 -by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
2.670 -qed "dvd_mult_cancel";
2.671 -
2.672 -Goal "0<m ==> (m*n dvd m) = (n = (1::nat))";
2.673 -by Auto_tac;
2.674 -by (subgoal_tac "m*n dvd m*1" 1);
2.675 -by (dtac dvd_mult_cancel 1);
2.676 -by Auto_tac;
2.677 -qed "dvd_mult_cancel1";
2.678 -
2.679 -Goal "0<m ==> (n*m dvd m) = (n = (1::nat))";
2.680 -by (stac mult_commute 1);
2.681 -by (etac dvd_mult_cancel1 1);
2.682 -qed "dvd_mult_cancel2";
2.683 -
2.684 -Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
2.685 -by (Clarify_tac 1);
2.686 -by (res_inst_tac [("x","k*ka")] exI 1);
2.687 -by (asm_simp_tac (simpset() addsimps mult_ac) 1);
2.688 -qed "mult_dvd_mono";
2.689 -
2.690 -Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
2.691 -by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
2.692 -by (Blast_tac 1);
2.693 -qed "dvd_mult_left";
2.694 -
2.695 -Goalw [dvd_def] "(i*j :: nat) dvd k ==> j dvd k";
2.696 -by (Clarify_tac 1);
2.697 -by (res_inst_tac [("x","i*k")] exI 1);
2.698 -by (simp_tac (simpset() addsimps mult_ac) 1);
2.699 -qed "dvd_mult_right";
2.700 -
2.701 -Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)";
2.702 -by (Clarify_tac 1);
2.703 -by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
2.704 -by (etac conjE 1);
2.705 -by (rtac le_trans 1);
2.706 -by (rtac (le_refl RS mult_le_mono) 2);
2.707 -by (etac Suc_leI 2);
2.708 -by (Simp_tac 1);
2.709 -qed "dvd_imp_le";
2.710 -
2.711 -Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)";
2.712 -by (div_undefined_case_tac "k=0" 1);
2.713 -by Safe_tac;
2.714 -by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
2.715 -by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1);
2.716 -by (stac mult_commute 1);
2.717 -by (Asm_simp_tac 1);
2.718 -qed "dvd_eq_mod_eq_0";
2.719 -
2.720 -Goal "n dvd m ==> n * (m div n) = (m::nat)";
2.721 -by (subgoal_tac "m mod n = 0" 1);
2.722 - by (asm_full_simp_tac (simpset() addsimps [mult_div_cancel]) 1);
2.723 -by (asm_full_simp_tac (HOL_basic_ss addsimps [dvd_eq_mod_eq_0]) 1);
2.724 -qed "dvd_mult_div_cancel";
2.725 -
2.726 -Goal "(m mod d = 0) = (EX q::nat. m = d*q)";
2.727 -by (auto_tac (claset(),
2.728 - simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def]));
2.729 -qed "mod_eq_0_iff";
2.730 -AddSDs [mod_eq_0_iff RS iffD1];
2.731 -
2.732 -(*Loses information, namely we also have r<d provided d is nonzero*)
2.733 -Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
2.734 -by (cut_inst_tac [("m","m")] mod_div_equality 1);
2.735 -by (full_simp_tac (HOL_basic_ss addsimps add_ac) 1);
2.736 -by (blast_tac (claset() addIs [sym]) 1);
2.737 -qed "mod_eqD";
3.1 --- a/src/HOL/Integ/Int.thy Mon Nov 24 15:33:07 2003 +0100
3.2 +++ b/src/HOL/Integ/Int.thy Tue Nov 25 10:37:03 2003 +0100
3.3 @@ -239,15 +239,6 @@
3.4
3.5 subsection{*Instances of the equations above, for zero*}
3.6
3.7 -(*instantiate a variable to zero and simplify*)
3.8 -
3.9 -declare zless_zminus [of 0, simplified, simp]
3.10 -declare zminus_zless [of _ 0, simplified, simp]
3.11 -declare zle_zminus [of 0, simplified, simp]
3.12 -declare zminus_zle [of _ 0, simplified, simp]
3.13 -declare equation_zminus [of 0, simplified, simp]
3.14 -declare zminus_equation [of _ 0, simplified, simp]
3.15 -
3.16 lemma negative_zless_0: "- (int (Suc n)) < 0"
3.17 by (simp add: zless_def)
3.18
3.19 @@ -343,53 +334,10 @@
3.20 apply (auto simp add: nat_mono_iff linorder_not_less)
3.21 done
3.22
3.23 -(* a case theorem distinguishing non-negative and negative int *)
3.24
3.25 -lemma int_cases:
3.26 - "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
3.27 -apply (case_tac "neg z")
3.28 -apply (fast dest!: negD)
3.29 -apply (drule not_neg_nat [symmetric], auto)
3.30 -done
3.31 +subsection{*Strict Monotonicity of Multiplication*}
3.32
3.33 -
3.34 -subsection{*Monotonicity of Multiplication*}
3.35 -
3.36 -lemma zmult_zle_mono1_lemma: "i \<le> (j::int) ==> i * int k \<le> j * int k"
3.37 -apply (induct_tac "k")
3.38 -apply (simp_all (no_asm_simp) add: int_Suc zadd_zmult_distrib2 zadd_zle_mono int_Suc0_eq_1)
3.39 -done
3.40 -
3.41 -lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
3.42 -apply (rule_tac t = k in not_neg_nat [THEN subst])
3.43 -apply (erule_tac [2] zmult_zle_mono1_lemma)
3.44 -apply (simp (no_asm_use) add: not_neg_eq_ge_0)
3.45 -done
3.46 -
3.47 -lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
3.48 -apply (rule zminus_zle_zminus [THEN iffD1])
3.49 -apply (simp add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
3.50 -done
3.51 -
3.52 -lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
3.53 -apply (drule zmult_zle_mono1)
3.54 -apply (simp_all add: zmult_commute)
3.55 -done
3.56 -
3.57 -lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
3.58 -apply (drule zmult_zle_mono1_neg)
3.59 -apply (simp_all add: zmult_commute)
3.60 -done
3.61 -
3.62 -(* \<le> monotonicity, BOTH arguments*)
3.63 -lemma zmult_zle_mono: "[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
3.64 -apply (erule zmult_zle_mono1 [THEN order_trans], assumption)
3.65 -apply (erule zmult_zle_mono2, assumption)
3.66 -done
3.67 -
3.68 -
3.69 -subsection{*strict, in 1st argument; proof is by induction on k>0*}
3.70 -
3.71 +text{*strict, in 1st argument; proof is by induction on k>0*}
3.72 lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
3.73 apply (induct_tac "k", simp)
3.74 apply (simp add: int_Suc)
3.75 @@ -423,6 +371,25 @@
3.76 show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
3.77 qed
3.78
3.79 +subsection{*Monotonicity of Multiplication*}
3.80 +
3.81 +lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
3.82 + by (rule mult_right_mono)
3.83 +
3.84 +lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
3.85 + by (rule mult_right_mono_neg)
3.86 +
3.87 +lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
3.88 + by (rule mult_left_mono)
3.89 +
3.90 +lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
3.91 + by (rule mult_left_mono_neg)
3.92 +
3.93 +(* \<le> monotonicity, BOTH arguments*)
3.94 +lemma zmult_zle_mono:
3.95 + "[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
3.96 + by (rule mult_mono)
3.97 +
3.98 lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
3.99 by (rule Ring_and_Field.mult_strict_right_mono)
3.100
3.101 @@ -467,6 +434,16 @@
3.102 apply (auto simp add: int_Suc symmetric zdiff_def)
3.103 done
3.104
3.105 +(* a case theorem distinguishing non-negative and negative int *)
3.106 +
3.107 +lemma int_cases:
3.108 + "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
3.109 +apply (case_tac "neg z")
3.110 +apply (fast dest!: negD)
3.111 +apply (drule not_neg_nat [symmetric], auto)
3.112 +done
3.113 +
3.114 +
3.115
3.116
3.117 ML
4.1 --- a/src/HOL/Integ/nat_simprocs.ML Mon Nov 24 15:33:07 2003 +0100
4.2 +++ b/src/HOL/Integ/nat_simprocs.ML Tue Nov 25 10:37:03 2003 +0100
4.3 @@ -211,7 +211,7 @@
4.4
4.5 (*Simplify 1*n and n*1 to n*)
4.6 val add_0s = map rename_numerals [add_0, add_0_right];
4.7 -val mult_1s = map rename_numerals [mult_1, mult_1_right];
4.8 +val mult_1s = map rename_numerals [thm"nat_mult_1", thm"nat_mult_1_right"];
4.9
4.10 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
4.11
5.1 --- a/src/HOL/IsaMakefile Mon Nov 24 15:33:07 2003 +0100
5.2 +++ b/src/HOL/IsaMakefile Tue Nov 25 10:37:03 2003 +0100
5.3 @@ -80,7 +80,7 @@
5.4 $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
5.5 $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
5.6 $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
5.7 - Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
5.8 + Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
5.9 Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
5.10 Fun.thy Gfp.ML Gfp.thy \
5.11 Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
6.1 --- a/src/HOL/Nat.thy Mon Nov 24 15:33:07 2003 +0100
6.2 +++ b/src/HOL/Nat.thy Tue Nov 25 10:37:03 2003 +0100
6.3 @@ -21,7 +21,7 @@
6.4 axioms
6.5 -- {* the axiom of infinity in 2 parts *}
6.6 inj_Suc_Rep: "inj Suc_Rep"
6.7 - Suc_Rep_not_Zero_Rep: "Suc_Rep x ~= Zero_Rep"
6.8 + Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
6.9
6.10
6.11 subsection {* Type nat *}
6.12 @@ -64,7 +64,7 @@
6.13
6.14 less_def: "m < n == (m, n) : trancl pred_nat"
6.15
6.16 - le_def: "m <= (n::nat) == ~ (n < m)"
6.17 + le_def: "m \<le> (n::nat) == ~ (n < m)"
6.18
6.19
6.20 text {* Induction *}
6.21 @@ -91,14 +91,14 @@
6.22
6.23 text {* Distinctness of constructors *}
6.24
6.25 -lemma Suc_not_Zero [iff]: "Suc m ~= 0"
6.26 +lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
6.27 apply (unfold Zero_nat_def Suc_def)
6.28 apply (rule inj_on_Abs_Nat [THEN inj_on_contraD])
6.29 apply (rule Suc_Rep_not_Zero_Rep)
6.30 apply (rule Rep_Nat Nat.Suc_RepI Nat.Zero_RepI)+
6.31 done
6.32
6.33 -lemma Zero_not_Suc [iff]: "0 ~= Suc m"
6.34 +lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
6.35 by (rule not_sym, rule Suc_not_Zero not_sym)
6.36
6.37 lemma Suc_neq_Zero: "Suc m = 0 ==> R"
6.38 @@ -127,7 +127,7 @@
6.39 apply (erule arg_cong)
6.40 done
6.41
6.42 -lemma nat_not_singleton: "(ALL x. x = (0::nat)) = False"
6.43 +lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
6.44 by auto
6.45
6.46 text {* @{typ nat} is a datatype *}
6.47 @@ -137,10 +137,10 @@
6.48 inject Suc_Suc_eq
6.49 induction nat_induct
6.50
6.51 -lemma n_not_Suc_n: "n ~= Suc n"
6.52 +lemma n_not_Suc_n: "n \<noteq> Suc n"
6.53 by (induct n) simp_all
6.54
6.55 -lemma Suc_n_not_n: "Suc t ~= t"
6.56 +lemma Suc_n_not_n: "Suc t \<noteq> t"
6.57 by (rule not_sym, rule n_not_Suc_n)
6.58
6.59 text {* A special form of induction for reasoning
6.60 @@ -219,9 +219,9 @@
6.61 lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
6.62 by (rule notE, rule less_not_refl)
6.63
6.64 -lemma less_not_refl2: "n < m ==> m ~= (n::nat)" by blast
6.65 +lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
6.66
6.67 -lemma less_not_refl3: "(s::nat) < t ==> s ~= t"
6.68 +lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
6.69 by (rule not_sym, rule less_not_refl2)
6.70
6.71 lemma lessE:
6.72 @@ -268,7 +268,7 @@
6.73 apply (blast intro: Suc_mono less_SucI elim: lessE)
6.74 done
6.75
6.76 -lemma nat_neq_iff: "((m::nat) ~= n) = (m < n | n < m)"
6.77 +lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
6.78 using less_linear by blast
6.79
6.80 lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
6.81 @@ -284,7 +284,7 @@
6.82
6.83 subsubsection {* Inductive (?) properties *}
6.84
6.85 -lemma Suc_lessI: "m < n ==> Suc m ~= n ==> Suc m < n"
6.86 +lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
6.87 apply (simp add: nat_neq_iff)
6.88 apply (blast elim!: less_irrefl less_SucE elim: less_asym)
6.89 done
6.90 @@ -324,7 +324,7 @@
6.91
6.92 text {* Complete induction, aka course-of-values induction *}
6.93 lemma nat_less_induct:
6.94 - assumes prem: "!!n. ALL m::nat. m < n --> P m ==> P n" shows "P n"
6.95 + assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
6.96 apply (rule_tac a=n in wf_induct)
6.97 apply (rule wf_pred_nat [THEN wf_trancl])
6.98 apply (rule prem)
6.99 @@ -336,119 +336,119 @@
6.100 subsection {* Properties of "less than or equal" *}
6.101
6.102 text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
6.103 -lemma less_Suc_eq_le: "(m < Suc n) = (m <= n)"
6.104 +lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)"
6.105 by (unfold le_def, rule not_less_eq [symmetric])
6.106
6.107 -lemma le_imp_less_Suc: "m <= n ==> m < Suc n"
6.108 +lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
6.109 by (rule less_Suc_eq_le [THEN iffD2])
6.110
6.111 -lemma le0 [iff]: "(0::nat) <= n"
6.112 +lemma le0 [iff]: "(0::nat) \<le> n"
6.113 by (unfold le_def, rule not_less0)
6.114
6.115 -lemma Suc_n_not_le_n: "~ Suc n <= n"
6.116 +lemma Suc_n_not_le_n: "~ Suc n \<le> n"
6.117 by (simp add: le_def)
6.118
6.119 -lemma le_0_eq [iff]: "((i::nat) <= 0) = (i = 0)"
6.120 +lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
6.121 by (induct i) (simp_all add: le_def)
6.122
6.123 -lemma le_Suc_eq: "(m <= Suc n) = (m <= n | m = Suc n)"
6.124 +lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
6.125 by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
6.126
6.127 -lemma le_SucE: "m <= Suc n ==> (m <= n ==> R) ==> (m = Suc n ==> R) ==> R"
6.128 +lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
6.129 by (drule le_Suc_eq [THEN iffD1], rules+)
6.130
6.131 -lemma leI: "~ n < m ==> m <= (n::nat)" by (simp add: le_def)
6.132 +lemma leI: "~ n < m ==> m \<le> (n::nat)" by (simp add: le_def)
6.133
6.134 -lemma leD: "m <= n ==> ~ n < (m::nat)"
6.135 +lemma leD: "m \<le> n ==> ~ n < (m::nat)"
6.136 by (simp add: le_def)
6.137
6.138 lemmas leE = leD [elim_format]
6.139
6.140 -lemma not_less_iff_le: "(~ n < m) = (m <= (n::nat))"
6.141 +lemma not_less_iff_le: "(~ n < m) = (m \<le> (n::nat))"
6.142 by (blast intro: leI elim: leE)
6.143
6.144 -lemma not_leE: "~ m <= n ==> n<(m::nat)"
6.145 +lemma not_leE: "~ m \<le> n ==> n<(m::nat)"
6.146 by (simp add: le_def)
6.147
6.148 -lemma not_le_iff_less: "(~ n <= m) = (m < (n::nat))"
6.149 +lemma not_le_iff_less: "(~ n \<le> m) = (m < (n::nat))"
6.150 by (simp add: le_def)
6.151
6.152 -lemma Suc_leI: "m < n ==> Suc(m) <= n"
6.153 +lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
6.154 apply (simp add: le_def less_Suc_eq)
6.155 apply (blast elim!: less_irrefl less_asym)
6.156 done -- {* formerly called lessD *}
6.157
6.158 -lemma Suc_leD: "Suc(m) <= n ==> m <= n"
6.159 +lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
6.160 by (simp add: le_def less_Suc_eq)
6.161
6.162 text {* Stronger version of @{text Suc_leD} *}
6.163 -lemma Suc_le_lessD: "Suc m <= n ==> m < n"
6.164 +lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
6.165 apply (simp add: le_def less_Suc_eq)
6.166 using less_linear
6.167 apply blast
6.168 done
6.169
6.170 -lemma Suc_le_eq: "(Suc m <= n) = (m < n)"
6.171 +lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
6.172 by (blast intro: Suc_leI Suc_le_lessD)
6.173
6.174 -lemma le_SucI: "m <= n ==> m <= Suc n"
6.175 +lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
6.176 by (unfold le_def) (blast dest: Suc_lessD)
6.177
6.178 -lemma less_imp_le: "m < n ==> m <= (n::nat)"
6.179 +lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
6.180 by (unfold le_def) (blast elim: less_asym)
6.181
6.182 -text {* For instance, @{text "(Suc m < Suc n) = (Suc m <= n) = (m < n)"} *}
6.183 +text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
6.184 lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
6.185
6.186
6.187 -text {* Equivalence of @{term "m <= n"} and @{term "m < n | m = n"} *}
6.188 +text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
6.189
6.190 -lemma le_imp_less_or_eq: "m <= n ==> m < n | m = (n::nat)"
6.191 +lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
6.192 apply (unfold le_def)
6.193 using less_linear
6.194 apply (blast elim: less_irrefl less_asym)
6.195 done
6.196
6.197 -lemma less_or_eq_imp_le: "m < n | m = n ==> m <= (n::nat)"
6.198 +lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
6.199 apply (unfold le_def)
6.200 using less_linear
6.201 apply (blast elim!: less_irrefl elim: less_asym)
6.202 done
6.203
6.204 -lemma le_eq_less_or_eq: "(m <= (n::nat)) = (m < n | m=n)"
6.205 +lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
6.206 by (rules intro: less_or_eq_imp_le le_imp_less_or_eq)
6.207
6.208 text {* Useful with @{text Blast}. *}
6.209 -lemma eq_imp_le: "(m::nat) = n ==> m <= n"
6.210 +lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
6.211 by (rule less_or_eq_imp_le, rule disjI2)
6.212
6.213 -lemma le_refl: "n <= (n::nat)"
6.214 +lemma le_refl: "n \<le> (n::nat)"
6.215 by (simp add: le_eq_less_or_eq)
6.216
6.217 -lemma le_less_trans: "[| i <= j; j < k |] ==> i < (k::nat)"
6.218 +lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
6.219 by (blast dest!: le_imp_less_or_eq intro: less_trans)
6.220
6.221 -lemma less_le_trans: "[| i < j; j <= k |] ==> i < (k::nat)"
6.222 +lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
6.223 by (blast dest!: le_imp_less_or_eq intro: less_trans)
6.224
6.225 -lemma le_trans: "[| i <= j; j <= k |] ==> i <= (k::nat)"
6.226 +lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
6.227 by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
6.228
6.229 -lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)"
6.230 +lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
6.231 by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
6.232
6.233 -lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)"
6.234 +lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
6.235 by (simp add: le_simps)
6.236
6.237 text {* Axiom @{text order_less_le} of class @{text order}: *}
6.238 -lemma nat_less_le: "((m::nat) < n) = (m <= n & m ~= n)"
6.239 +lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
6.240 by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
6.241
6.242 -lemma le_neq_implies_less: "(m::nat) <= n ==> m ~= n ==> m < n"
6.243 +lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
6.244 by (rule iffD2, rule nat_less_le, rule conjI)
6.245
6.246 text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
6.247 -lemma nat_le_linear: "(m::nat) <= n | n <= m"
6.248 +lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
6.249 apply (simp add: le_eq_less_or_eq)
6.250 using less_linear
6.251 apply blast
6.252 @@ -460,10 +460,10 @@
6.253
6.254 text {*
6.255 Rewrite @{term "n < Suc m"} to @{term "n = m"}
6.256 - if @{term "~ n < m"} or @{term "m <= n"} hold.
6.257 + if @{term "~ n < m"} or @{term "m \<le> n"} hold.
6.258 Not suitable as default simprules because they often lead to looping
6.259 *}
6.260 -lemma le_less_Suc_eq: "m <= n ==> (n < Suc m) = (n = m)"
6.261 +lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
6.262 by (rule not_less_less_Suc_eq, rule leD)
6.263
6.264 lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
6.265 @@ -526,20 +526,20 @@
6.266 lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
6.267 by simp
6.268
6.269 -lemma not0_implies_Suc: "n ~= 0 ==> EX m. n = Suc m"
6.270 +lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
6.271 by (case_tac n) simp_all
6.272
6.273 -lemma gr_implies_not0: "!!n::nat. m<n ==> n ~= 0"
6.274 +lemma gr_implies_not0: "!!n::nat. m<n ==> n \<noteq> 0"
6.275 by (case_tac n) simp_all
6.276
6.277 -lemma neq0_conv [iff]: "!!n::nat. (n ~= 0) = (0 < n)"
6.278 +lemma neq0_conv [iff]: "!!n::nat. (n \<noteq> 0) = (0 < n)"
6.279 by (case_tac n) simp_all
6.280
6.281 text {* This theorem is useful with @{text blast} *}
6.282 lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
6.283 by (rule iffD1, rule neq0_conv, rules)
6.284
6.285 -lemma gr0_conv_Suc: "(0 < n) = (EX m. n = Suc m)"
6.286 +lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
6.287 by (fast intro: not0_implies_Suc)
6.288
6.289 lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
6.290 @@ -547,11 +547,11 @@
6.291 apply (rule ccontr, simp_all)
6.292 done
6.293
6.294 -lemma Suc_le_D: "(Suc n <= m') ==> (? m. m' = Suc m)"
6.295 +lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
6.296 by (induct m') simp_all
6.297
6.298 text {* Useful in certain inductive arguments *}
6.299 -lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (EX j. m = Suc j & j < n))"
6.300 +lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
6.301 by (case_tac m) simp_all
6.302
6.303 lemma nat_induct2: "P 0 ==> P (Suc 0) ==> (!!k. P k ==> P (Suc (Suc k))) ==> P n"
6.304 @@ -567,21 +567,21 @@
6.305 lemmas Least_le = wellorder_Least_le
6.306 lemmas not_less_Least = wellorder_not_less_Least
6.307
6.308 -lemma Least_Suc: "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
6.309 +lemma Least_Suc:
6.310 + "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
6.311 apply (case_tac "n", auto)
6.312 apply (frule LeastI)
6.313 apply (drule_tac P = "%x. P (Suc x) " in LeastI)
6.314 - apply (subgoal_tac " (LEAST x. P x) <= Suc (LEAST x. P (Suc x))")
6.315 + apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
6.316 apply (erule_tac [2] Least_le)
6.317 apply (case_tac "LEAST x. P x", auto)
6.318 apply (drule_tac P = "%x. P (Suc x) " in Least_le)
6.319 apply (blast intro: order_antisym)
6.320 done
6.321
6.322 -lemma Least_Suc2: "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
6.323 - apply (erule (1) Least_Suc [THEN ssubst])
6.324 - apply simp
6.325 - done
6.326 +lemma Least_Suc2:
6.327 + "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
6.328 + by (erule (1) Least_Suc [THEN ssubst], simp)
6.329
6.330
6.331
6.332 @@ -640,29 +640,26 @@
6.333
6.334
6.335 text {* Associative law for addition *}
6.336 -lemma add_assoc: "(m + n) + k = m + ((n + k)::nat)"
6.337 +lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
6.338 by (induct m) simp_all
6.339
6.340 text {* Commutative law for addition *}
6.341 -lemma add_commute: "m + n = n + (m::nat)"
6.342 +lemma nat_add_commute: "m + n = n + (m::nat)"
6.343 by (induct m) simp_all
6.344
6.345 -lemma add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
6.346 +lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
6.347 apply (rule mk_left_commute [of "op +"])
6.348 - apply (rule add_assoc)
6.349 - apply (rule add_commute)
6.350 + apply (rule nat_add_assoc)
6.351 + apply (rule nat_add_commute)
6.352 done
6.353
6.354 -text {* Addition is an AC-operator *}
6.355 -lemmas add_ac = add_assoc add_commute add_left_commute
6.356 -
6.357 lemma add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
6.358 by (induct k) simp_all
6.359
6.360 lemma add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
6.361 by (induct k) simp_all
6.362
6.363 -lemma add_left_cancel_le [simp]: "(k + m <= k + n) = (m<=(n::nat))"
6.364 +lemma add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
6.365 by (induct k) simp_all
6.366
6.367 lemma add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
6.368 @@ -684,24 +681,114 @@
6.369
6.370 lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
6.371 apply (drule add_0_right [THEN ssubst])
6.372 - apply (simp add: add_assoc del: add_0_right)
6.373 + apply (simp add: nat_add_assoc del: add_0_right)
6.374 done
6.375
6.376 -subsection {* Additional theorems about "less than" *}
6.377 +subsection {* Monotonicity of Addition *}
6.378
6.379 -text {* Deleted @{text less_natE}; instead use @{text "less_imp_Suc_add RS exE"} *}
6.380 -lemma less_imp_Suc_add: "m < n ==> (EX k. n = Suc (m + k))"
6.381 +text {* strict, in 1st argument *}
6.382 +lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
6.383 + by (induct k) simp_all
6.384 +
6.385 +text {* strict, in both arguments *}
6.386 +lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
6.387 + apply (rule add_less_mono1 [THEN less_trans], assumption+)
6.388 + apply (induct_tac j, simp_all)
6.389 + done
6.390 +
6.391 +text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
6.392 +lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
6.393 apply (induct n)
6.394 apply (simp_all add: order_le_less)
6.395 apply (blast elim!: less_SucE intro!: add_0_right [symmetric] add_Suc_right [symmetric])
6.396 done
6.397
6.398 -lemma le_add2: "n <= ((m + n)::nat)"
6.399 +
6.400 +subsection {* Multiplication *}
6.401 +
6.402 +text {* right annihilation in product *}
6.403 +lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
6.404 + by (induct m) simp_all
6.405 +
6.406 +text {* right successor law for multiplication *}
6.407 +lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
6.408 + by (induct m) (simp_all add: nat_add_left_commute)
6.409 +
6.410 +text {* Commutative law for multiplication *}
6.411 +lemma nat_mult_commute: "m * n = n * (m::nat)"
6.412 + by (induct m) simp_all
6.413 +
6.414 +text {* addition distributes over multiplication *}
6.415 +lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
6.416 + by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
6.417 +
6.418 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
6.419 + by (induct m) (simp_all add: nat_add_assoc)
6.420 +
6.421 +text {* Associative law for multiplication *}
6.422 +lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
6.423 + by (induct m) (simp_all add: add_mult_distrib)
6.424 +
6.425 +lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
6.426 + apply (induct_tac m)
6.427 + apply (induct_tac [2] n, simp_all)
6.428 + done
6.429 +
6.430 +text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
6.431 +lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
6.432 + apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
6.433 + apply (induct_tac x)
6.434 + apply (simp_all add: add_less_mono)
6.435 + done
6.436 +
6.437 +text{*The Naturals Form an Ordered Semiring*}
6.438 +instance nat :: ordered_semiring
6.439 +proof
6.440 + fix i j k :: nat
6.441 + show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
6.442 + show "i + j = j + i" by (rule nat_add_commute)
6.443 + show "0 + i = i" by simp
6.444 + show "(i * j) * k = i * (j * k)" by (rule nat_mult_assoc)
6.445 + show "i * j = j * i" by (rule nat_mult_commute)
6.446 + show "1 * i = i" by simp
6.447 + show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
6.448 + show "0 \<noteq> (1::nat)" by simp
6.449 + show "i \<le> j ==> k + i \<le> k + j" by simp
6.450 + show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
6.451 +qed
6.452 +
6.453 +lemma nat_mult_1: "(1::nat) * n = n"
6.454 + by simp
6.455 +
6.456 +lemma nat_mult_1_right: "n * (1::nat) = n"
6.457 + by simp
6.458 +
6.459 +
6.460 +subsection {* Additional theorems about "less than" *}
6.461 +
6.462 +text {* A [clumsy] way of lifting @{text "<"}
6.463 + monotonicity to @{text "\<le>"} monotonicity *}
6.464 +lemma less_mono_imp_le_mono:
6.465 + assumes lt_mono: "!!i j::nat. i < j ==> f i < f j"
6.466 + and le: "i \<le> j" shows "f i \<le> ((f j)::nat)" using le
6.467 + apply (simp add: order_le_less)
6.468 + apply (blast intro!: lt_mono)
6.469 + done
6.470 +
6.471 +text {* non-strict, in 1st argument *}
6.472 +lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)"
6.473 + by (rule add_right_mono)
6.474 +
6.475 +text {* non-strict, in both arguments *}
6.476 +lemma add_le_mono: "[| i \<le> j; k \<le> l |] ==> i + k \<le> j + (l::nat)"
6.477 + by (rule add_mono)
6.478 +
6.479 +lemma le_add2: "n \<le> ((m + n)::nat)"
6.480 apply (induct m, simp_all)
6.481 apply (erule le_SucI)
6.482 done
6.483
6.484 -lemma le_add1: "n <= ((n + m)::nat)"
6.485 +lemma le_add1: "n \<le> ((n + m)::nat)"
6.486 apply (simp add: add_ac)
6.487 apply (rule le_add2)
6.488 done
6.489 @@ -712,14 +799,14 @@
6.490 lemma less_add_Suc2: "i < Suc (m + i)"
6.491 by (rule le_less_trans, rule le_add2, rule lessI)
6.492
6.493 -lemma less_iff_Suc_add: "(m < n) = (EX k. n = Suc (m + k))"
6.494 +lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
6.495 by (rules intro!: less_add_Suc1 less_imp_Suc_add)
6.496
6.497
6.498 -lemma trans_le_add1: "(i::nat) <= j ==> i <= j + m"
6.499 +lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
6.500 by (rule le_trans, assumption, rule le_add1)
6.501
6.502 -lemma trans_le_add2: "(i::nat) <= j ==> i <= m + j"
6.503 +lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j"
6.504 by (rule le_trans, assumption, rule le_add2)
6.505
6.506 lemma trans_less_add1: "(i::nat) < j ==> i < j + m"
6.507 @@ -741,15 +828,15 @@
6.508 lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
6.509 by (simp add: add_commute not_add_less1)
6.510
6.511 -lemma add_leD1: "m + k <= n ==> m <= (n::nat)"
6.512 +lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
6.513 by (induct k) (simp_all add: le_simps)
6.514
6.515 -lemma add_leD2: "m + k <= n ==> k <= (n::nat)"
6.516 +lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
6.517 apply (simp add: add_commute)
6.518 apply (erule add_leD1)
6.519 done
6.520
6.521 -lemma add_leE: "(m::nat) + k <= n ==> (m <= n ==> k <= n ==> R) ==> R"
6.522 +lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
6.523 by (blast dest: add_leD1 add_leD2)
6.524
6.525 text {* needs @{text "!!k"} for @{text add_ac} to work *}
6.526 @@ -758,106 +845,6 @@
6.527 simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
6.528
6.529
6.530 -subsection {* Monotonicity of Addition *}
6.531 -
6.532 -text {* strict, in 1st argument *}
6.533 -lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
6.534 - by (induct k) simp_all
6.535 -
6.536 -text {* strict, in both arguments *}
6.537 -lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
6.538 - apply (rule add_less_mono1 [THEN less_trans], assumption+)
6.539 - apply (induct_tac j, simp_all)
6.540 - done
6.541 -
6.542 -text {* A [clumsy] way of lifting @{text "<"}
6.543 - monotonicity to @{text "<="} monotonicity *}
6.544 -lemma less_mono_imp_le_mono:
6.545 - assumes lt_mono: "!!i j::nat. i < j ==> f i < f j"
6.546 - and le: "i <= j" shows "f i <= ((f j)::nat)" using le
6.547 - apply (simp add: order_le_less)
6.548 - apply (blast intro!: lt_mono)
6.549 - done
6.550 -
6.551 -text {* non-strict, in 1st argument *}
6.552 -lemma add_le_mono1: "i <= j ==> i + k <= j + (k::nat)"
6.553 - apply (rule_tac f = "%j. j + k" in less_mono_imp_le_mono)
6.554 - apply (erule add_less_mono1, assumption)
6.555 - done
6.556 -
6.557 -text {* non-strict, in both arguments *}
6.558 -lemma add_le_mono: "[| i <= j; k <= l |] ==> i + k <= j + (l::nat)"
6.559 - apply (erule add_le_mono1 [THEN le_trans])
6.560 - apply (simp add: add_commute)
6.561 - done
6.562 -
6.563 -
6.564 -subsection {* Multiplication *}
6.565 -
6.566 -text {* right annihilation in product *}
6.567 -lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
6.568 - by (induct m) simp_all
6.569 -
6.570 -text {* right successor law for multiplication *}
6.571 -lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
6.572 - by (induct m) (simp_all add: add_ac)
6.573 -
6.574 -lemma mult_1: "(1::nat) * n = n" by simp
6.575 -
6.576 -lemma mult_1_right: "n * (1::nat) = n" by simp
6.577 -
6.578 -text {* Commutative law for multiplication *}
6.579 -lemma mult_commute: "m * n = n * (m::nat)"
6.580 - by (induct m) simp_all
6.581 -
6.582 -text {* addition distributes over multiplication *}
6.583 -lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
6.584 - by (induct m) (simp_all add: add_ac)
6.585 -
6.586 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
6.587 - by (induct m) (simp_all add: add_ac)
6.588 -
6.589 -text {* Associative law for multiplication *}
6.590 -lemma mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
6.591 - by (induct m) (simp_all add: add_mult_distrib)
6.592 -
6.593 -lemma mult_left_commute: "x * (y * z) = y * ((x * z)::nat)"
6.594 - apply (rule mk_left_commute [of "op *"])
6.595 - apply (rule mult_assoc)
6.596 - apply (rule mult_commute)
6.597 - done
6.598 -
6.599 -lemmas mult_ac = mult_assoc mult_commute mult_left_commute
6.600 -
6.601 -lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
6.602 - apply (induct_tac m)
6.603 - apply (induct_tac [2] n, simp_all)
6.604 - done
6.605 -
6.606 -text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
6.607 -lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
6.608 - apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
6.609 - apply (induct_tac x)
6.610 - apply (simp_all add: add_less_mono)
6.611 - done
6.612 -
6.613 -text{*The Naturals Form an Ordered Semiring*}
6.614 -instance nat :: ordered_semiring
6.615 -proof
6.616 - fix i j k :: nat
6.617 - show "(i + j) + k = i + (j + k)" by (rule add_assoc)
6.618 - show "i + j = j + i" by (rule add_commute)
6.619 - show "0 + i = i" by simp
6.620 - show "(i * j) * k = i * (j * k)" by (rule mult_assoc)
6.621 - show "i * j = j * i" by (rule mult_commute)
6.622 - show "1 * i = i" by simp
6.623 - show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
6.624 - show "0 \<noteq> (1::nat)" by simp
6.625 - show "i \<le> j ==> k + i \<le> k + j" by simp
6.626 - show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
6.627 -qed
6.628 -
6.629 -
6.630
6.631 subsection {* Difference *}
6.632
6.633 @@ -865,20 +852,20 @@
6.634 by (induct m) simp_all
6.635
6.636 text {* Addition is the inverse of subtraction:
6.637 - if @{term "n <= m"} then @{term "n + (m - n) = m"}. *}
6.638 + if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
6.639 lemma add_diff_inverse: "~ m < n ==> n + (m - n) = (m::nat)"
6.640 by (induct m n rule: diff_induct) simp_all
6.641
6.642 -lemma le_add_diff_inverse [simp]: "n <= m ==> n + (m - n) = (m::nat)"
6.643 +lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
6.644 by (simp add: add_diff_inverse not_less_iff_le)
6.645
6.646 -lemma le_add_diff_inverse2 [simp]: "n <= m ==> (m - n) + n = (m::nat)"
6.647 +lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
6.648 by (simp add: le_add_diff_inverse add_commute)
6.649
6.650
6.651 subsection {* More results about difference *}
6.652
6.653 -lemma Suc_diff_le: "n <= m ==> Suc m - n = Suc (m - n)"
6.654 +lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
6.655 by (induct m n rule: diff_induct) simp_all
6.656
6.657 lemma diff_less_Suc: "m - n < Suc m"
6.658 @@ -887,7 +874,7 @@
6.659 apply (simp_all add: less_Suc_eq)
6.660 done
6.661
6.662 -lemma diff_le_self [simp]: "m - n <= (m::nat)"
6.663 +lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
6.664 by (induct m n rule: diff_induct) (simp_all add: le_SucI)
6.665
6.666 lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
6.667 @@ -908,10 +895,10 @@
6.668 lemma diff_commute: "(i::nat) - j - k = i - k - j"
6.669 by (simp add: diff_diff_left add_commute)
6.670
6.671 -lemma diff_add_assoc: "k <= (j::nat) ==> (i + j) - k = i + (j - k)"
6.672 +lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
6.673 by (induct j k rule: diff_induct) simp_all
6.674
6.675 -lemma diff_add_assoc2: "k <= (j::nat) ==> (j + i) - k = (j - k) + i"
6.676 +lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
6.677 by (simp add: add_commute diff_add_assoc)
6.678
6.679 lemma diff_add_inverse: "(n + m) - n = (m::nat)"
6.680 @@ -920,21 +907,21 @@
6.681 lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
6.682 by (simp add: diff_add_assoc)
6.683
6.684 -lemma le_imp_diff_is_add: "i <= (j::nat) ==> (j - i = k) = (j = k + i)"
6.685 +lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
6.686 apply safe
6.687 apply (simp_all add: diff_add_inverse2)
6.688 done
6.689
6.690 -lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m <= n)"
6.691 +lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)"
6.692 by (induct m n rule: diff_induct) simp_all
6.693
6.694 -lemma diff_is_0_eq' [simp]: "m <= n ==> (m::nat) - n = 0"
6.695 +lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0"
6.696 by (rule iffD2, rule diff_is_0_eq)
6.697
6.698 lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)"
6.699 by (induct m n rule: diff_induct) simp_all
6.700
6.701 -lemma less_imp_add_positive: "i < j ==> EX k::nat. 0 < k & i + k = j"
6.702 +lemma less_imp_add_positive: "i < j ==> \<exists>k::nat. 0 < k & i + k = j"
6.703 apply (rule_tac x = "j - i" in exI)
6.704 apply (simp (no_asm_simp) add: add_diff_inverse less_not_sym)
6.705 done
6.706 @@ -975,16 +962,16 @@
6.707
6.708 subsection {* Monotonicity of Multiplication *}
6.709
6.710 -lemma mult_le_mono1: "i <= (j::nat) ==> i * k <= j * k"
6.711 +lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
6.712 by (induct k) (simp_all add: add_le_mono)
6.713
6.714 -lemma mult_le_mono2: "i <= (j::nat) ==> k * i <= k * j"
6.715 +lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
6.716 apply (drule mult_le_mono1)
6.717 apply (simp add: mult_commute)
6.718 done
6.719
6.720 -text {* @{text "<="} monotonicity, BOTH arguments *}
6.721 -lemma mult_le_mono: "i <= (j::nat) ==> k <= l ==> i * k <= j * l"
6.722 +text {* @{text "\<le>"} monotonicity, BOTH arguments *}
6.723 +lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
6.724 apply (erule mult_le_mono1 [THEN le_trans])
6.725 apply (erule mult_le_mono2)
6.726 done
6.727 @@ -999,7 +986,7 @@
6.728 apply (case_tac [2] n, simp_all)
6.729 done
6.730
6.731 -lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)"
6.732 +lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
6.733 apply (induct m)
6.734 apply (case_tac [2] n, simp_all)
6.735 done
6.736 @@ -1026,10 +1013,10 @@
6.737
6.738 declare mult_less_cancel2 [simp]
6.739
6.740 -lemma mult_le_cancel1 [simp]: "(k * (m::nat) <= k * n) = (0 < k --> m <= n)"
6.741 +lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
6.742 by (simp add: linorder_not_less [symmetric], auto)
6.743
6.744 -lemma mult_le_cancel2 [simp]: "((m::nat) * k <= n * k) = (0 < k --> m <= n)"
6.745 +lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
6.746 by (simp add: linorder_not_less [symmetric], auto)
6.747
6.748 lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))"
6.749 @@ -1045,7 +1032,7 @@
6.750 lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
6.751 by (subst mult_less_cancel1) simp
6.752
6.753 -lemma Suc_mult_le_cancel1: "(Suc k * m <= Suc k * n) = (m <= n)"
6.754 +lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)"
6.755 by (subst mult_le_cancel1) simp
6.756
6.757 lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
7.1 --- a/src/HOL/Ring_and_Field.thy Mon Nov 24 15:33:07 2003 +0100
7.2 +++ b/src/HOL/Ring_and_Field.thy Tue Nov 25 10:37:03 2003 +0100
7.3 @@ -22,7 +22,7 @@
7.4
7.5 mult_assoc: "(a * b) * c = a * (b * c)"
7.6 mult_commute: "a * b = b * a"
7.7 - left_one [simp]: "1 * a = a"
7.8 + mult_1 [simp]: "1 * a = a"
7.9
7.10 left_distrib: "(a + b) * c = a * c + b * c"
7.11 zero_neq_one [simp]: "0 \<noteq> 1"
7.12 @@ -133,10 +133,10 @@
7.13
7.14 subsection {* Derived rules for multiplication *}
7.15
7.16 -lemma right_one [simp]: "a = a * (1::'a::semiring)"
7.17 +lemma mult_1_right [simp]: "a * (1::'a::semiring) = a"
7.18 proof -
7.19 - have "a = 1 * a" by simp
7.20 - also have "... = a * 1" by (simp add: mult_commute)
7.21 + have "a * 1 = 1 * a" by (simp add: mult_commute)
7.22 + also have "... = a" by simp
7.23 finally show ?thesis .
7.24 qed
7.25
7.26 @@ -217,6 +217,12 @@
7.27 lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
7.28 by (simp add: add_commute [of _ c] add_left_mono)
7.29
7.30 +text {* non-strict, in both arguments *}
7.31 +lemma add_mono: "[|a \<le> b; c \<le> d|] ==> a + c \<le> b + (d::'a::ordered_semiring)"
7.32 + apply (erule add_right_mono [THEN order_trans])
7.33 + apply (simp add: add_commute add_left_mono)
7.34 + done
7.35 +
7.36 lemma le_imp_neg_le:
7.37 assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
7.38 proof -
7.39 @@ -261,12 +267,14 @@
7.40 by (simp add: mult_commute [of _ c] mult_strict_left_mono)
7.41
7.42 lemma mult_left_mono:
7.43 - "[|a \<le> b; 0 < c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
7.44 -by (force simp add: mult_strict_left_mono order_le_less)
7.45 + "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_ring)"
7.46 + apply (case_tac "c=0", simp)
7.47 + apply (force simp add: mult_strict_left_mono order_le_less)
7.48 + done
7.49
7.50 lemma mult_right_mono:
7.51 - "[|a \<le> b; 0 < c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
7.52 -by (force simp add: mult_strict_right_mono order_le_less)
7.53 + "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_ring)"
7.54 + by (simp add: mult_left_mono mult_commute [of _ c])
7.55
7.56 lemma mult_strict_left_mono_neg:
7.57 "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
7.58 @@ -281,12 +289,14 @@
7.59 done
7.60
7.61 lemma mult_left_mono_neg:
7.62 - "[|b \<le> a; c < 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
7.63 -by (force simp add: mult_strict_left_mono_neg order_le_less)
7.64 + "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
7.65 +apply (drule mult_left_mono [of _ _ "-c"])
7.66 +apply (simp_all add: minus_mult_left [symmetric])
7.67 +done
7.68
7.69 lemma mult_right_mono_neg:
7.70 - "[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
7.71 -by (force simp add: mult_strict_right_mono_neg order_le_less)
7.72 + "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
7.73 + by (simp add: mult_left_mono_neg mult_commute [of _ c])
7.74
7.75 text{*Strict monotonicity in both arguments*}
7.76 lemma mult_strict_mono:
7.77 @@ -295,6 +305,14 @@
7.78 apply (erule mult_strict_left_mono, assumption)
7.79 done
7.80
7.81 +lemma mult_mono:
7.82 + "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|]
7.83 + ==> a * c \<le> b * (d::'a::ordered_ring)"
7.84 +apply (erule mult_right_mono [THEN order_trans], assumption)
7.85 +apply (erule mult_left_mono, assumption)
7.86 +done
7.87 +
7.88 +
7.89 subsection{*Cancellation Laws for Relationships With a Common Factor*}
7.90
7.91 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},