41 [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); |
41 [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); |
42 |
42 |
43 Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc]; |
43 Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc]; |
44 |
44 |
45 |
45 |
|
46 goal Arith.thy "!!k. 0<k ==> EX j. k = Suc(j)"; |
|
47 by (etac rev_mp 1); |
|
48 by (nat_ind_tac "k" 1); |
|
49 by (Simp_tac 1); |
|
50 by (fast_tac HOL_cs 1); |
|
51 val lemma = result(); |
|
52 |
|
53 (* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *) |
|
54 bind_thm ("zero_less_natE", lemma RS exE); |
|
55 |
|
56 |
|
57 |
46 (**** Inductive properties of the operators ****) |
58 (**** Inductive properties of the operators ****) |
47 |
59 |
48 (*** Addition ***) |
60 (*** Addition ***) |
49 |
61 |
50 qed_goal "add_0_right" Arith.thy "m + 0 = m" |
62 qed_goal "add_0_right" Arith.thy "m + 0 = m" |
177 goal Arith.thy "!!n::nat. (n+m) - n = m"; |
189 goal Arith.thy "!!n::nat. (n+m) - n = m"; |
178 by (nat_ind_tac "n" 1); |
190 by (nat_ind_tac "n" 1); |
179 by (ALLGOALS Asm_simp_tac); |
191 by (ALLGOALS Asm_simp_tac); |
180 qed "diff_add_inverse"; |
192 qed "diff_add_inverse"; |
181 |
193 |
|
194 goal Arith.thy "!!n::nat.(m+n) - n = m"; |
|
195 by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1); |
|
196 by (REPEAT (ares_tac [diff_add_inverse] 1)); |
|
197 qed "diff_add_inverse2"; |
|
198 |
|
199 goal Arith.thy "!!k::nat. (k+m) - (k+n) = m - n"; |
|
200 by (nat_ind_tac "k" 1); |
|
201 by (ALLGOALS Asm_simp_tac); |
|
202 qed "diff_cancel"; |
|
203 Addsimps [diff_cancel]; |
|
204 |
|
205 goal Arith.thy "!!m::nat. (m+k) - (n+k) = m - n"; |
|
206 val add_commute_k = read_instantiate [("n","k")] add_commute; |
|
207 by (asm_simp_tac (!simpset addsimps ([add_commute_k])) 1); |
|
208 qed "diff_cancel2"; |
|
209 Addsimps [diff_cancel2]; |
|
210 |
182 goal Arith.thy "!!n::nat. n - (n+m) = 0"; |
211 goal Arith.thy "!!n::nat. n - (n+m) = 0"; |
183 by (nat_ind_tac "n" 1); |
212 by (nat_ind_tac "n" 1); |
184 by (ALLGOALS Asm_simp_tac); |
213 by (ALLGOALS Asm_simp_tac); |
185 qed "diff_add_0"; |
214 qed "diff_add_0"; |
|
215 Addsimps [diff_add_0]; |
|
216 |
|
217 (** Difference distributes over multiplication **) |
|
218 |
|
219 goal Arith.thy "!!m::nat. (m - n) * k = (m * k) - (n * k)"; |
|
220 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
|
221 by (ALLGOALS Asm_simp_tac); |
|
222 qed "diff_mult_distrib" ; |
|
223 |
|
224 goal Arith.thy "!!m::nat. k * (m - n) = (k * m) - (k * n)"; |
|
225 val mult_commute_k = read_instantiate [("m","k")] mult_commute; |
|
226 by (simp_tac (!simpset addsimps [diff_mult_distrib, mult_commute_k]) 1); |
|
227 qed "diff_mult_distrib2" ; |
|
228 (*NOT added as rewrites, since sometimes they are used from right-to-left*) |
|
229 |
|
230 |
|
231 (** Less-then properties **) |
186 |
232 |
187 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
233 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
188 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m"; |
234 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m"; |
189 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1); |
235 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1); |
190 by (fast_tac HOL_cs 1); |
236 by (fast_tac HOL_cs 1); |
415 by (etac subst 1); |
461 by (etac subst 1); |
416 by (simp_tac (!simpset addsimps [less_add_Suc1]) 1); |
462 by (simp_tac (!simpset addsimps [less_add_Suc1]) 1); |
417 qed "less_add_eq_less"; |
463 qed "less_add_eq_less"; |
418 |
464 |
419 |
465 |
420 (** Monotonicity of addition (from ZF/Arith) **) |
466 (*** Monotonicity of Addition ***) |
421 |
|
422 (** Monotonicity results **) |
|
423 |
467 |
424 (*strict, in 1st argument*) |
468 (*strict, in 1st argument*) |
425 goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k"; |
469 goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k"; |
426 by (nat_ind_tac "k" 1); |
470 by (nat_ind_tac "k" 1); |
427 by (ALLGOALS Asm_simp_tac); |
471 by (ALLGOALS Asm_simp_tac); |
457 by (etac (add_le_mono1 RS le_trans) 1); |
501 by (etac (add_le_mono1 RS le_trans) 1); |
458 by (simp_tac (!simpset addsimps [add_commute]) 1); |
502 by (simp_tac (!simpset addsimps [add_commute]) 1); |
459 (*j moves to the end because it is free while k, l are bound*) |
503 (*j moves to the end because it is free while k, l are bound*) |
460 by (etac add_le_mono1 1); |
504 by (etac add_le_mono1 1); |
461 qed "add_le_mono"; |
505 qed "add_le_mono"; |
|
506 |
|
507 (*** Monotonicity of Multiplication ***) |
|
508 |
|
509 goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k"; |
|
510 by (nat_ind_tac "k" 1); |
|
511 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono]))); |
|
512 qed "mult_le_mono1"; |
|
513 |
|
514 (*<=monotonicity, BOTH arguments*) |
|
515 goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l"; |
|
516 by (rtac le_trans 1); |
|
517 by (ALLGOALS |
|
518 (deepen_tac (HOL_cs addIs [mult_commute RS ssubst, mult_le_mono1]) 0)); |
|
519 qed "mult_le_mono"; |
|
520 |
|
521 (*strict, in 1st argument; proof is by induction on k>0*) |
|
522 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j"; |
|
523 be zero_less_natE 1; |
|
524 by (Asm_simp_tac 1); |
|
525 by (nat_ind_tac "x" 1); |
|
526 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono]))); |
|
527 qed "mult_less_mono2"; |
|
528 |
|
529 goal Arith.thy "(0 < m*n) = (0<m & 0<n)"; |
|
530 by (nat_ind_tac "m" 1); |
|
531 by (nat_ind_tac "n" 2); |
|
532 by (ALLGOALS Asm_simp_tac); |
|
533 qed "zero_less_mult_iff"; |
|
534 |
|
535 (*Cancellation law for division*) |
|
536 goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n"; |
|
537 by (res_inst_tac [("n","m")] less_induct 1); |
|
538 by (case_tac "na<n" 1); |
|
539 by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff, |
|
540 mult_less_mono2]) 1); |
|
541 by (subgoal_tac "~ k*na < k*n" 1); |
|
542 by (asm_simp_tac |
|
543 (!simpset addsimps [zero_less_mult_iff, div_geq, |
|
544 diff_mult_distrib2 RS sym, diff_less]) 1); |
|
545 by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, |
|
546 le_refl RS mult_le_mono]) 1); |
|
547 qed "div_cancel"; |
|
548 |
|
549 goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)"; |
|
550 by (res_inst_tac [("n","m")] less_induct 1); |
|
551 by (case_tac "na<n" 1); |
|
552 by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff, |
|
553 mult_less_mono2]) 1); |
|
554 by (subgoal_tac "~ k*na < k*n" 1); |
|
555 by (asm_simp_tac |
|
556 (!simpset addsimps [zero_less_mult_iff, mod_geq, |
|
557 diff_mult_distrib2 RS sym, diff_less]) 1); |
|
558 by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, |
|
559 le_refl RS mult_le_mono]) 1); |
|
560 qed "mult_mod_distrib"; |
|
561 |
|
562 |