author | paulson |
Wed, 07 Oct 1998 10:31:07 +0200 | |
changeset 5618 | 721671c68324 |
parent 5479 | 5a5dfb0f0d7d |
child 6676 | 62d1e642da30 |
permissions | -rw-r--r-- |
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 |
||
969 | 13 |
(*specialized form of induction needed below*) |
3842 | 14 |
val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)"; |
969 | 15 |
by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]); |
16 |
qed "nat_exh"; |
|
17 |
||
5069 | 18 |
Goal "! n. k=f(n) --> n <= f(n)"; |
969 | 19 |
by (res_inst_tac [("n","k")] less_induct 1); |
20 |
by (rtac nat_exh 1); |
|
1266 | 21 |
by (Simp_tac 1); |
969 | 22 |
by (rtac impI 1); |
23 |
by (rtac classical 1); |
|
24 |
by (dtac not_leE 1); |
|
25 |
by (subgoal_tac "f(na) <= f(f(na))" 1); |
|
5456 | 26 |
by (Blast_tac 2); |
3336 | 27 |
by (rtac Suc_leI 1); |
5456 | 28 |
by (blast_tac (claset() addSDs [spec] addIs [le_less_trans]) 1); |
1266 | 29 |
val lemma = result() RS spec RS mp; |
969 | 30 |
|
5069 | 31 |
Goal "n <= f(n)"; |
4089 | 32 |
by (fast_tac (claset() addIs [lemma]) 1); |
969 | 33 |
qed "lemma1"; |
34 |
||
5069 | 35 |
Goal "f(n) < f(Suc(n))"; |
5456 | 36 |
by (blast_tac (claset() addIs [le_less_trans, lemma1]) 1); |
969 | 37 |
qed "lemma2"; |
38 |
||
5456 | 39 |
val prems = Goal "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)"; |
969 | 40 |
by (res_inst_tac[("n","n")]nat_induct 1); |
1266 | 41 |
by (Simp_tac 1); |
4089 | 42 |
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
5479 | 43 |
by (blast_tac (claset() addIs (le_trans::prems)) 1); |
2017
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset
|
44 |
qed_spec_mp "mono_lemma1"; |
969 | 45 |
|
46 |
val [p1,p2] = goal Puzzle.thy |
|
47 |
"[| !! n. f(n)<=f(Suc(n)); m<=n |] ==> f(m) <= f(n)"; |
|
48 |
by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1); |
|
49 |
by (etac (p1 RS mono_lemma1) 1); |
|
2017
dd3e2a91aeca
Proofs made more robust to work in presence of le_refl
paulson
parents:
1820
diff
changeset
|
50 |
by (Fast_tac 1); |
969 | 51 |
qed "mono_lemma"; |
52 |
||
53 |
val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)"; |
|
5618 | 54 |
by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1); |
969 | 55 |
qed "f_mono"; |
56 |
||
5069 | 57 |
Goal "f(n) = n"; |
969 | 58 |
by (rtac le_anti_sym 1); |
59 |
by (rtac lemma1 2); |
|
4089 | 60 |
by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1); |
969 | 61 |
result(); |