changeset 4089 | 96fba19bcbe2 |
parent 4032 | 4b1c69d8b767 |
child 4104 | 84433b1ab826 |
4088:9be9e39fd862 | 4089:96fba19bcbe2 |
---|---|
26 |
26 |
27 val major::prems = goal thy |
27 val major::prems = goal thy |
28 "[| i: Nat; P(Zero_Rep); \ |
28 "[| i: Nat; P(Zero_Rep); \ |
29 \ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)"; |
29 \ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)"; |
30 by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1); |
30 by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1); |
31 by (blast_tac (!claset addIs prems) 1); |
31 by (blast_tac (claset() addIs prems) 1); |
32 qed "Nat_induct"; |
32 qed "Nat_induct"; |
33 |
33 |
34 val prems = goalw thy [Zero_def,Suc_def] |
34 val prems = goalw thy [Zero_def,Suc_def] |
35 "[| P(0); \ |
35 "[| P(0); \ |
36 \ !!n. P(n) ==> P(Suc(n)) |] ==> P(n)"; |
36 \ !!n. P(n) ==> P(Suc(n)) |] ==> P(n)"; |
62 |
62 |
63 (*Case analysis on the natural numbers*) |
63 (*Case analysis on the natural numbers*) |
64 val prems = goal thy |
64 val prems = goal thy |
65 "[| n=0 ==> P; !!x. n = Suc(x) ==> P |] ==> P"; |
65 "[| n=0 ==> P; !!x. n = Suc(x) ==> P |] ==> P"; |
66 by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1); |
66 by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1); |
67 by (fast_tac (!claset addSEs prems) 1); |
67 by (fast_tac (claset() addSEs prems) 1); |
68 by (nat_ind_tac "n" 1); |
68 by (nat_ind_tac "n" 1); |
69 by (rtac (refl RS disjI1) 1); |
69 by (rtac (refl RS disjI1) 1); |
70 by (Blast_tac 1); |
70 by (Blast_tac 1); |
71 qed "natE"; |
71 qed "natE"; |
72 |
72 |
142 |
142 |
143 |
143 |
144 (*** nat_case -- the selection operator for nat ***) |
144 (*** nat_case -- the selection operator for nat ***) |
145 |
145 |
146 goalw thy [nat_case_def] "nat_case a f 0 = a"; |
146 goalw thy [nat_case_def] "nat_case a f 0 = a"; |
147 by (blast_tac (!claset addIs [select_equality]) 1); |
147 by (blast_tac (claset() addIs [select_equality]) 1); |
148 qed "nat_case_0"; |
148 qed "nat_case_0"; |
149 |
149 |
150 goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)"; |
150 goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)"; |
151 by (blast_tac (!claset addIs [select_equality]) 1); |
151 by (blast_tac (claset() addIs [select_equality]) 1); |
152 qed "nat_case_Suc"; |
152 qed "nat_case_Suc"; |
153 |
153 |
154 goalw thy [wf_def, pred_nat_def] "wf(pred_nat)"; |
154 goalw thy [wf_def, pred_nat_def] "wf(pred_nat)"; |
155 by (Clarify_tac 1); |
155 by (Clarify_tac 1); |
156 by (nat_ind_tac "x" 1); |
156 by (nat_ind_tac "x" 1); |
174 |
174 |
175 (** conversion rules **) |
175 (** conversion rules **) |
176 |
176 |
177 goal thy "nat_rec c h 0 = c"; |
177 goal thy "nat_rec c h 0 = c"; |
178 by (rtac (nat_rec_unfold RS trans) 1); |
178 by (rtac (nat_rec_unfold RS trans) 1); |
179 by (simp_tac (!simpset addsimps [nat_case_0]) 1); |
179 by (simp_tac (simpset() addsimps [nat_case_0]) 1); |
180 qed "nat_rec_0"; |
180 qed "nat_rec_0"; |
181 |
181 |
182 goal thy "nat_rec c h (Suc n) = h n (nat_rec c h n)"; |
182 goal thy "nat_rec c h (Suc n) = h n (nat_rec c h n)"; |
183 by (rtac (nat_rec_unfold RS trans) 1); |
183 by (rtac (nat_rec_unfold RS trans) 1); |
184 by (simp_tac (!simpset addsimps [nat_case_Suc, pred_nat_def, cut_apply]) 1); |
184 by (simp_tac (simpset() addsimps [nat_case_Suc, pred_nat_def, cut_apply]) 1); |
185 qed "nat_rec_Suc"; |
185 qed "nat_rec_Suc"; |
186 |
186 |
187 (*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) |
187 (*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) |
188 val [rew] = goal thy |
188 val [rew] = goal thy |
189 "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c"; |
189 "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c"; |
216 by (resolve_tac prems 1); |
216 by (resolve_tac prems 1); |
217 by (resolve_tac prems 1); |
217 by (resolve_tac prems 1); |
218 qed "less_trans"; |
218 qed "less_trans"; |
219 |
219 |
220 goalw thy [less_def, pred_nat_def] "n < Suc(n)"; |
220 goalw thy [less_def, pred_nat_def] "n < Suc(n)"; |
221 by (simp_tac (!simpset addsimps [r_into_trancl]) 1); |
221 by (simp_tac (simpset() addsimps [r_into_trancl]) 1); |
222 qed "lessI"; |
222 qed "lessI"; |
223 AddIffs [lessI]; |
223 AddIffs [lessI]; |
224 |
224 |
225 (* i<j ==> i<Suc(j) *) |
225 (* i<j ==> i<Suc(j) *) |
226 bind_thm("less_SucI", lessI RSN (2, less_trans)); |
226 bind_thm("less_SucI", lessI RSN (2, less_trans)); |
235 AddIffs [zero_less_Suc]; |
235 AddIffs [zero_less_Suc]; |
236 |
236 |
237 (** Elimination properties **) |
237 (** Elimination properties **) |
238 |
238 |
239 val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)"; |
239 val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)"; |
240 by (blast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); |
240 by (blast_tac (claset() addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); |
241 qed "less_not_sym"; |
241 qed "less_not_sym"; |
242 |
242 |
243 (* [| n<m; m<n |] ==> R *) |
243 (* [| n<m; m<n |] ==> R *) |
244 bind_thm ("less_asym", (less_not_sym RS notE)); |
244 bind_thm ("less_asym", (less_not_sym RS notE)); |
245 |
245 |
250 |
250 |
251 (* n<n ==> R *) |
251 (* n<n ==> R *) |
252 bind_thm ("less_irrefl", (less_not_refl RS notE)); |
252 bind_thm ("less_irrefl", (less_not_refl RS notE)); |
253 |
253 |
254 goal thy "!!m. n<m ==> m ~= (n::nat)"; |
254 goal thy "!!m. n<m ==> m ~= (n::nat)"; |
255 by (blast_tac (!claset addSEs [less_irrefl]) 1); |
255 by (blast_tac (claset() addSEs [less_irrefl]) 1); |
256 qed "less_not_refl2"; |
256 qed "less_not_refl2"; |
257 |
257 |
258 |
258 |
259 val major::prems = goalw thy [less_def, pred_nat_def] |
259 val major::prems = goalw thy [less_def, pred_nat_def] |
260 "[| i<k; k=Suc(i) ==> P; !!j. [| i<j; k=Suc(j) |] ==> P \ |
260 "[| i<k; k=Suc(i) ==> P; !!j. [| i<j; k=Suc(j) |] ==> P \ |
285 by (rtac less 1); |
285 by (rtac less 1); |
286 by (Blast_tac 1); |
286 by (Blast_tac 1); |
287 qed "less_SucE"; |
287 qed "less_SucE"; |
288 |
288 |
289 goal thy "(m < Suc(n)) = (m < n | m = n)"; |
289 goal thy "(m < Suc(n)) = (m < n | m = n)"; |
290 by (blast_tac (!claset addSEs [less_SucE] addIs [less_trans]) 1); |
290 by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); |
291 qed "less_Suc_eq"; |
291 qed "less_Suc_eq"; |
292 |
292 |
293 goal thy "(n<1) = (n=0)"; |
293 goal thy "(n<1) = (n=0)"; |
294 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
294 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
295 qed "less_one"; |
295 qed "less_one"; |
296 AddIffs [less_one]; |
296 AddIffs [less_one]; |
297 |
297 |
298 val prems = goal thy "m<n ==> n ~= 0"; |
298 val prems = goal thy "m<n ==> n ~= 0"; |
299 by (res_inst_tac [("n","n")] natE 1); |
299 by (res_inst_tac [("n","n")] natE 1); |
313 (** Inductive (?) properties **) |
313 (** Inductive (?) properties **) |
314 |
314 |
315 val [prem] = goal thy "Suc(m) < n ==> m<n"; |
315 val [prem] = goal thy "Suc(m) < n ==> m<n"; |
316 by (rtac (prem RS rev_mp) 1); |
316 by (rtac (prem RS rev_mp) 1); |
317 by (nat_ind_tac "n" 1); |
317 by (nat_ind_tac "n" 1); |
318 by (ALLGOALS (fast_tac (!claset addSIs [lessI RS less_SucI] |
318 by (ALLGOALS (fast_tac (claset() addSIs [lessI RS less_SucI] |
319 addEs [less_trans, lessE]))); |
319 addEs [less_trans, lessE]))); |
320 qed "Suc_lessD"; |
320 qed "Suc_lessD"; |
321 |
321 |
322 val [major,minor] = goal thy |
322 val [major,minor] = goal thy |
323 "[| Suc(i)<k; !!j. [| i<j; k=Suc(j) |] ==> P \ |
323 "[| Suc(i)<k; !!j. [| i<j; k=Suc(j) |] ==> P \ |
327 by (etac (Suc_lessD RS minor) 1); |
327 by (etac (Suc_lessD RS minor) 1); |
328 by (assume_tac 1); |
328 by (assume_tac 1); |
329 qed "Suc_lessE"; |
329 qed "Suc_lessE"; |
330 |
330 |
331 goal thy "!!m n. Suc(m) < Suc(n) ==> m<n"; |
331 goal thy "!!m n. Suc(m) < Suc(n) ==> m<n"; |
332 by (blast_tac (!claset addEs [lessE, make_elim Suc_lessD]) 1); |
332 by (blast_tac (claset() addEs [lessE, make_elim Suc_lessD]) 1); |
333 qed "Suc_less_SucD"; |
333 qed "Suc_less_SucD"; |
334 |
334 |
335 goal thy "!!m n. m<n ==> Suc(m) < Suc(n)"; |
335 goal thy "!!m n. m<n ==> Suc(m) < Suc(n)"; |
336 by (etac rev_mp 1); |
336 by (etac rev_mp 1); |
337 by (nat_ind_tac "n" 1); |
337 by (nat_ind_tac "n" 1); |
338 by (ALLGOALS (fast_tac (!claset addEs [less_trans, lessE]))); |
338 by (ALLGOALS (fast_tac (claset() addEs [less_trans, lessE]))); |
339 qed "Suc_mono"; |
339 qed "Suc_mono"; |
340 |
340 |
341 |
341 |
342 goal thy "(Suc(m) < Suc(n)) = (m<n)"; |
342 goal thy "(Suc(m) < Suc(n)) = (m<n)"; |
343 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]); |
343 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]); |
344 qed "Suc_less_eq"; |
344 qed "Suc_less_eq"; |
345 Addsimps [Suc_less_eq]; |
345 Addsimps [Suc_less_eq]; |
346 |
346 |
347 goal thy "~(Suc(n) < n)"; |
347 goal thy "~(Suc(n) < n)"; |
348 by (blast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1); |
348 by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1); |
349 qed "not_Suc_n_less_n"; |
349 qed "not_Suc_n_less_n"; |
350 Addsimps [not_Suc_n_less_n]; |
350 Addsimps [not_Suc_n_less_n]; |
351 |
351 |
352 goal thy "!!i. i<j ==> j<k --> Suc i < k"; |
352 goal thy "!!i. i<j ==> j<k --> Suc i < k"; |
353 by (nat_ind_tac "k" 1); |
353 by (nat_ind_tac "k" 1); |
354 by (ALLGOALS (asm_simp_tac (!simpset))); |
354 by (ALLGOALS (asm_simp_tac (simpset()))); |
355 by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
355 by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
356 by (blast_tac (!claset addDs [Suc_lessD]) 1); |
356 by (blast_tac (claset() addDs [Suc_lessD]) 1); |
357 qed_spec_mp "less_trans_Suc"; |
357 qed_spec_mp "less_trans_Suc"; |
358 |
358 |
359 (*"Less than" is a linear ordering*) |
359 (*"Less than" is a linear ordering*) |
360 goal thy "m<n | m=n | n<(m::nat)"; |
360 goal thy "m<n | m=n | n<(m::nat)"; |
361 by (nat_ind_tac "m" 1); |
361 by (nat_ind_tac "m" 1); |
362 by (nat_ind_tac "n" 1); |
362 by (nat_ind_tac "n" 1); |
363 by (rtac (refl RS disjI1 RS disjI2) 1); |
363 by (rtac (refl RS disjI1 RS disjI2) 1); |
364 by (rtac (zero_less_Suc RS disjI1) 1); |
364 by (rtac (zero_less_Suc RS disjI1) 1); |
365 by (blast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1); |
365 by (blast_tac (claset() addIs [Suc_mono, less_SucI] addEs [lessE]) 1); |
366 qed "less_linear"; |
366 qed "less_linear"; |
367 |
367 |
368 qed_goal "nat_less_cases" thy |
368 qed_goal "nat_less_cases" thy |
369 "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m" |
369 "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m" |
370 ( fn [major,eqCase,lessCase] => |
370 ( fn [major,eqCase,lessCase] => |
433 Suc_n_not_le_n, |
433 Suc_n_not_le_n, |
434 n_not_Suc_n, Suc_n_not_n, |
434 n_not_Suc_n, Suc_n_not_n, |
435 nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; |
435 nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; |
436 |
436 |
437 goal thy "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)"; |
437 goal thy "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)"; |
438 by (simp_tac (!simpset addsimps [le_eq_less_Suc]) 1); |
438 by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1); |
439 by (blast_tac (!claset addSEs [less_SucE] addIs [less_SucI]) 1); |
439 by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1); |
440 qed "le_Suc_eq"; |
440 qed "le_Suc_eq"; |
441 |
441 |
442 (* |
442 (* |
443 goal thy "(Suc m < n | Suc m = n) = (m < n)"; |
443 goal thy "(Suc m < n | Suc m = n) = (m < n)"; |
444 by (stac (less_Suc_eq RS sym) 1); |
444 by (stac (less_Suc_eq RS sym) 1); |
471 qed "leD"; |
471 qed "leD"; |
472 |
472 |
473 val leE = make_elim leD; |
473 val leE = make_elim leD; |
474 |
474 |
475 goal thy "(~n<m) = (m<=(n::nat))"; |
475 goal thy "(~n<m) = (m<=(n::nat))"; |
476 by (blast_tac (!claset addIs [leI] addEs [leE]) 1); |
476 by (blast_tac (claset() addIs [leI] addEs [leE]) 1); |
477 qed "not_less_iff_le"; |
477 qed "not_less_iff_le"; |
478 |
478 |
479 goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)"; |
479 goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)"; |
480 by (Blast_tac 1); |
480 by (Blast_tac 1); |
481 qed "not_leE"; |
481 qed "not_leE"; |
482 |
482 |
483 goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n"; |
483 goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n"; |
484 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
484 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
485 by (blast_tac (!claset addSEs [less_irrefl,less_asym]) 1); |
485 by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1); |
486 qed "Suc_leI"; (*formerly called lessD*) |
486 qed "Suc_leI"; (*formerly called lessD*) |
487 |
487 |
488 goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; |
488 goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; |
489 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
489 by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
490 qed "Suc_leD"; |
490 qed "Suc_leD"; |
491 |
491 |
492 (* stronger version of Suc_leD *) |
492 (* stronger version of Suc_leD *) |
493 goalw thy [le_def] |
493 goalw thy [le_def] |
494 "!!m. Suc m <= n ==> m < n"; |
494 "!!m. Suc m <= n ==> m < n"; |
495 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
495 by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
496 by (cut_facts_tac [less_linear] 1); |
496 by (cut_facts_tac [less_linear] 1); |
497 by (Blast_tac 1); |
497 by (Blast_tac 1); |
498 qed "Suc_le_lessD"; |
498 qed "Suc_le_lessD"; |
499 |
499 |
500 goal thy "(Suc m <= n) = (m < n)"; |
500 goal thy "(Suc m <= n) = (m < n)"; |
501 by (blast_tac (!claset addIs [Suc_leI, Suc_le_lessD]) 1); |
501 by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1); |
502 qed "Suc_le_eq"; |
502 qed "Suc_le_eq"; |
503 |
503 |
504 goalw thy [le_def] "!!m. m <= n ==> m <= Suc n"; |
504 goalw thy [le_def] "!!m. m <= n ==> m <= Suc n"; |
505 by (blast_tac (!claset addDs [Suc_lessD]) 1); |
505 by (blast_tac (claset() addDs [Suc_lessD]) 1); |
506 qed "le_SucI"; |
506 qed "le_SucI"; |
507 Addsimps[le_SucI]; |
507 Addsimps[le_SucI]; |
508 |
508 |
509 bind_thm ("le_Suc", not_Suc_n_less_n RS leI); |
509 bind_thm ("le_Suc", not_Suc_n_less_n RS leI); |
510 |
510 |
511 goalw thy [le_def] "!!m. m < n ==> m <= (n::nat)"; |
511 goalw thy [le_def] "!!m. m < n ==> m <= (n::nat)"; |
512 by (blast_tac (!claset addEs [less_asym]) 1); |
512 by (blast_tac (claset() addEs [less_asym]) 1); |
513 qed "less_imp_le"; |
513 qed "less_imp_le"; |
514 |
514 |
515 (** Equivalence of m<=n and m<n | m=n **) |
515 (** Equivalence of m<=n and m<n | m=n **) |
516 |
516 |
517 goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)"; |
517 goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)"; |
518 by (cut_facts_tac [less_linear] 1); |
518 by (cut_facts_tac [less_linear] 1); |
519 by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1); |
519 by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1); |
520 qed "le_imp_less_or_eq"; |
520 qed "le_imp_less_or_eq"; |
521 |
521 |
522 goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)"; |
522 goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)"; |
523 by (cut_facts_tac [less_linear] 1); |
523 by (cut_facts_tac [less_linear] 1); |
524 by (blast_tac (!claset addSEs [less_irrefl] addEs [less_asym]) 1); |
524 by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1); |
525 qed "less_or_eq_imp_le"; |
525 qed "less_or_eq_imp_le"; |
526 |
526 |
527 goal thy "(m <= (n::nat)) = (m < n | m=n)"; |
527 goal thy "(m <= (n::nat)) = (m < n | m=n)"; |
528 by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); |
528 by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1)); |
529 qed "le_eq_less_or_eq"; |
529 qed "le_eq_less_or_eq"; |
530 |
530 |
531 goal thy "n <= (n::nat)"; |
531 goal thy "n <= (n::nat)"; |
532 by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
532 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
533 qed "le_refl"; |
533 qed "le_refl"; |
534 |
534 |
535 val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)"; |
535 val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)"; |
536 by (dtac le_imp_less_or_eq 1); |
536 by (dtac le_imp_less_or_eq 1); |
537 by (blast_tac (!claset addIs [less_trans]) 1); |
537 by (blast_tac (claset() addIs [less_trans]) 1); |
538 qed "le_less_trans"; |
538 qed "le_less_trans"; |
539 |
539 |
540 goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)"; |
540 goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)"; |
541 by (dtac le_imp_less_or_eq 1); |
541 by (dtac le_imp_less_or_eq 1); |
542 by (blast_tac (!claset addIs [less_trans]) 1); |
542 by (blast_tac (claset() addIs [less_trans]) 1); |
543 qed "less_le_trans"; |
543 qed "less_le_trans"; |
544 |
544 |
545 goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)"; |
545 goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)"; |
546 by (EVERY1[dtac le_imp_less_or_eq, |
546 by (EVERY1[dtac le_imp_less_or_eq, |
547 dtac le_imp_less_or_eq, |
547 dtac le_imp_less_or_eq, |
548 rtac less_or_eq_imp_le, |
548 rtac less_or_eq_imp_le, |
549 blast_tac (!claset addIs [less_trans])]); |
549 blast_tac (claset() addIs [less_trans])]); |
550 qed "le_trans"; |
550 qed "le_trans"; |
551 |
551 |
552 goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)"; |
552 goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)"; |
553 by (EVERY1[dtac le_imp_less_or_eq, |
553 by (EVERY1[dtac le_imp_less_or_eq, |
554 dtac le_imp_less_or_eq, |
554 dtac le_imp_less_or_eq, |
555 blast_tac (!claset addEs [less_irrefl,less_asym])]); |
555 blast_tac (claset() addEs [less_irrefl,less_asym])]); |
556 qed "le_anti_sym"; |
556 qed "le_anti_sym"; |
557 |
557 |
558 goal thy "(Suc(n) <= Suc(m)) = (n <= m)"; |
558 goal thy "(Suc(n) <= Suc(m)) = (n <= m)"; |
559 by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
559 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
560 qed "Suc_le_mono"; |
560 qed "Suc_le_mono"; |
561 |
561 |
562 AddIffs [Suc_le_mono]; |
562 AddIffs [Suc_le_mono]; |
563 |
563 |
564 (* Axiom 'order_le_less' of class 'order': *) |
564 (* Axiom 'order_le_less' of class 'order': *) |
565 goal thy "(m::nat) < n = (m <= n & m ~= n)"; |
565 goal thy "(m::nat) < n = (m <= n & m ~= n)"; |
566 by (rtac iffI 1); |
566 by (rtac iffI 1); |
567 by (rtac conjI 1); |
567 by (rtac conjI 1); |
568 by (etac less_imp_le 1); |
568 by (etac less_imp_le 1); |
569 by (etac (less_not_refl2 RS not_sym) 1); |
569 by (etac (less_not_refl2 RS not_sym) 1); |
570 by (blast_tac (!claset addSDs [le_imp_less_or_eq]) 1); |
570 by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1); |
571 qed "nat_less_le"; |
571 qed "nat_less_le"; |
572 |
572 |
573 (** LEAST -- the least number operator **) |
573 (** LEAST -- the least number operator **) |
574 |
574 |
575 goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)"; |
575 goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)"; |
576 by (blast_tac (!claset addIs [leI] addEs [leE]) 1); |
576 by (blast_tac (claset() addIs [leI] addEs [leE]) 1); |
577 val lemma = result(); |
577 val lemma = result(); |
578 |
578 |
579 (* This is an old def of Least for nat, which is derived for compatibility *) |
579 (* This is an old def of Least for nat, which is derived for compatibility *) |
580 goalw thy [Least_def] |
580 goalw thy [Least_def] |
581 "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))"; |
581 "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))"; |
582 by (simp_tac (!simpset addsimps [lemma]) 1); |
582 by (simp_tac (simpset() addsimps [lemma]) 1); |
583 by (rtac eq_reflection 1); |
583 by (rtac eq_reflection 1); |
584 by (rtac refl 1); |
584 by (rtac refl 1); |
585 qed "Least_nat_def"; |
585 qed "Least_nat_def"; |
586 |
586 |
587 val [prem1,prem2] = goalw thy [Least_nat_def] |
587 val [prem1,prem2] = goalw thy [Least_nat_def] |
588 "[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k"; |
588 "[| P(k::nat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k"; |
589 by (rtac select_equality 1); |
589 by (rtac select_equality 1); |
590 by (blast_tac (!claset addSIs [prem1,prem2]) 1); |
590 by (blast_tac (claset() addSIs [prem1,prem2]) 1); |
591 by (cut_facts_tac [less_linear] 1); |
591 by (cut_facts_tac [less_linear] 1); |
592 by (blast_tac (!claset addSIs [prem1] addSDs [prem2]) 1); |
592 by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1); |
593 qed "Least_equality"; |
593 qed "Least_equality"; |
594 |
594 |
595 val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))"; |
595 val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))"; |
596 by (rtac (prem RS rev_mp) 1); |
596 by (rtac (prem RS rev_mp) 1); |
597 by (res_inst_tac [("n","k")] less_induct 1); |
597 by (res_inst_tac [("n","k")] less_induct 1); |
610 by (rtac impI 1); |
610 by (rtac impI 1); |
611 by (rtac classical 1); |
611 by (rtac classical 1); |
612 by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); |
612 by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1); |
613 by (assume_tac 1); |
613 by (assume_tac 1); |
614 by (rtac le_refl 2); |
614 by (rtac le_refl 2); |
615 by (blast_tac (!claset addIs [less_imp_le,le_trans]) 1); |
615 by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1); |
616 qed "Least_le"; |
616 qed "Least_le"; |
617 |
617 |
618 val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)"; |
618 val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)"; |
619 by (rtac notI 1); |
619 by (rtac notI 1); |
620 by (etac (rewrite_rule [le_def] Least_le RS notE) 1); |
620 by (etac (rewrite_rule [le_def] Least_le RS notE) 1); |
624 qed_goalw "Least_Suc" thy [Least_nat_def] |
624 qed_goalw "Least_Suc" thy [Least_nat_def] |
625 "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
625 "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
626 (fn _ => [ |
626 (fn _ => [ |
627 rtac select_equality 1, |
627 rtac select_equality 1, |
628 fold_goals_tac [Least_nat_def], |
628 fold_goals_tac [Least_nat_def], |
629 safe_tac (!claset addSEs [LeastI]), |
629 safe_tac (claset() addSEs [LeastI]), |
630 rename_tac "j" 1, |
630 rename_tac "j" 1, |
631 res_inst_tac [("n","j")] natE 1, |
631 res_inst_tac [("n","j")] natE 1, |
632 Blast_tac 1, |
632 Blast_tac 1, |
633 blast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1, |
633 blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1, |
634 rename_tac "k n" 1, |
634 rename_tac "k n" 1, |
635 res_inst_tac [("n","k")] natE 1, |
635 res_inst_tac [("n","k")] natE 1, |
636 Blast_tac 1, |
636 Blast_tac 1, |
637 hyp_subst_tac 1, |
637 hyp_subst_tac 1, |
638 rewtac Least_nat_def, |
638 rewtac Least_nat_def, |
639 rtac (select_equality RS arg_cong RS sym) 1, |
639 rtac (select_equality RS arg_cong RS sym) 1, |
640 safe_tac (!claset), |
640 safe_tac (claset()), |
641 dtac Suc_mono 1, |
641 dtac Suc_mono 1, |
642 Blast_tac 1, |
642 Blast_tac 1, |
643 cut_facts_tac [less_linear] 1, |
643 cut_facts_tac [less_linear] 1, |
644 safe_tac (!claset), |
644 safe_tac (claset()), |
645 atac 2, |
645 atac 2, |
646 Blast_tac 2, |
646 Blast_tac 2, |
647 dtac Suc_mono 1, |
647 dtac Suc_mono 1, |
648 Blast_tac 1]); |
648 Blast_tac 1]); |
649 |
649 |
667 val not_lessI = leI RS leD |
667 val not_lessI = leI RS leD |
668 val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n" |
668 val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n" |
669 (fn _ => [etac swap2 1, etac leD 1]); |
669 (fn _ => [etac swap2 1, etac leD 1]); |
670 val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n" |
670 val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n" |
671 (fn _ => [etac less_SucE 1, |
671 (fn _ => [etac less_SucE 1, |
672 blast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl] |
672 blast_tac (claset() addSDs [Suc_less_SucD] addSEs [less_irrefl] |
673 addDs [less_trans_Suc]) 1, |
673 addDs [less_trans_Suc]) 1, |
674 assume_tac 1]); |
674 assume_tac 1]); |
675 val leD = le_eq_less_Suc RS iffD1; |
675 val leD = le_eq_less_Suc RS iffD1; |
676 val not_lessD = nat_leI RS leD; |
676 val not_lessD = nat_leI RS leD; |
677 val not_leD = not_leE |
677 val not_leD = not_leE |