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);
|
|
17 |
by (exhaust_tac "i" 1);
|
8019
|
18 |
by Auto_tac;
|
8018
|
19 |
by (subgoal_tac "f(nat) <= f(f(nat))" 1);
|
|
20 |
by (Blast_tac 2);
|
8019
|
21 |
by (blast_tac (claset() addIs [Suc_leI,le_less_trans]) 1);
|
1266
|
22 |
val lemma = result() RS spec RS mp;
|
969
|
23 |
|
5069
|
24 |
Goal "n <= f(n)";
|
4089
|
25 |
by (fast_tac (claset() addIs [lemma]) 1);
|
969
|
26 |
qed "lemma1";
|
|
27 |
|
5069
|
28 |
Goal "f(n) < f(Suc(n))";
|
5456
|
29 |
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1);
|
969
|
30 |
qed "lemma2";
|
|
31 |
|
8018
|
32 |
Goal "m <= n --> f(m) <= f(n)";
|
|
33 |
by (induct_tac "n" 1);
|
|
34 |
by (Simp_tac 1);
|
|
35 |
by (rtac impI 1);
|
|
36 |
by (etac le_SucE 1);
|
|
37 |
by(cut_inst_tac [("n","n")]lemma2 1);
|
|
38 |
by(arith_tac 1);
|
|
39 |
by(Asm_simp_tac 1);
|
|
40 |
qed_spec_mp "f_mono";
|
969
|
41 |
|
5069
|
42 |
Goal "f(n) = n";
|
6676
|
43 |
by (rtac order_antisym 1);
|
969
|
44 |
by (rtac lemma1 2);
|
8018
|
45 |
by (fast_tac (claset() addIs [leI] addDs [leD,f_mono,Suc_leI]) 1);
|
|
46 |
qed "f_id";
|