equal
deleted
inserted
replaced
1 (* Title: HOL/ex/puzzle.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1993 TU Muenchen |
|
5 |
|
6 A question from "Bundeswettbewerb Mathematik" |
|
7 |
|
8 Proof due to Herbert Ehler |
|
9 *) |
|
10 |
|
11 AddSIs [Puzzle.f_ax]; |
|
12 |
|
13 Goal "! n. k=f(n) --> n <= f(n)"; |
|
14 by (induct_thm_tac nat_less_induct "k" 1); |
|
15 by (rtac allI 1); |
|
16 by (rename_tac "i" 1); |
|
17 by (case_tac "i" 1); |
|
18 by (Asm_simp_tac 1); |
|
19 by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1); |
|
20 val lemma = result() RS spec RS mp; |
|
21 |
|
22 Goal "n <= f(n)"; |
|
23 by (fast_tac (claset() addIs [lemma]) 1); |
|
24 qed "lemma1"; |
|
25 |
|
26 Goal "f(n) < f(Suc(n))"; |
|
27 by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1); |
|
28 qed "lemma2"; |
|
29 |
|
30 Goal "m <= n --> f(m) <= f(n)"; |
|
31 by (induct_tac "n" 1); |
|
32 by (Simp_tac 1); |
|
33 by (rtac impI 1); |
|
34 by (etac le_SucE 1); |
|
35 by (cut_inst_tac [("n","n")]lemma2 1); |
|
36 by (arith_tac 1); |
|
37 by (Asm_simp_tac 1); |
|
38 qed_spec_mp "f_mono"; |
|
39 |
|
40 Goal "f(n) = n"; |
|
41 by (rtac order_antisym 1); |
|
42 by (rtac lemma1 2); |
|
43 by (fast_tac (claset() addIs [leI] addDs [leD,f_mono,Suc_leI]) 1); |
|
44 qed "f_id"; |
|