1465
|
1 |
(* Title: HOL/ex/puzzle.ML
|
969
|
2 |
ID: $Id$
|
1465
|
3 |
Author: Tobias Nipkow
|
969
|
4 |
Copyright 1993 TU Muenchen
|
|
5 |
|
5456
|
6 |
A question from "Bundeswettbewerb Mathematik"
|
969
|
7 |
|
|
8 |
Proof due to Herbert Ehler
|
|
9 |
*)
|
|
10 |
|
5456
|
11 |
AddSIs [Puzzle.f_ax];
|
|
12 |
|
5069
|
13 |
Goal "! n. k=f(n) --> n <= f(n)";
|
969
|
14 |
by (res_inst_tac [("n","k")] less_induct 1);
|
8018
|
15 |
by (rtac allI 1);
|
|
16 |
by (rename_tac "i" 1);
|
8423
|
17 |
by (cases_tac "i" 1);
|
8021
|
18 |
by (Asm_simp_tac 1);
|
8022
|
19 |
by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1);
|
1266
|
20 |
val lemma = result() RS spec RS mp;
|
969
|
21 |
|
5069
|
22 |
Goal "n <= f(n)";
|
4089
|
23 |
by (fast_tac (claset() addIs [lemma]) 1);
|
969
|
24 |
qed "lemma1";
|
|
25 |
|
5069
|
26 |
Goal "f(n) < f(Suc(n))";
|
5456
|
27 |
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);
|
969
|
28 |
qed "lemma2";
|
|
29 |
|
8018
|
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";
|
969
|
39 |
|
5069
|
40 |
Goal "f(n) = n";
|
6676
|
41 |
by (rtac order_antisym 1);
|
969
|
42 |
by (rtac lemma1 2);
|
8018
|
43 |
by (fast_tac (claset() addIs [leI] addDs [leD,f_mono,Suc_leI]) 1);
|
|
44 |
qed "f_id";
|