author | haftmann |
Fri, 18 Apr 2008 09:44:16 +0200 | |
changeset 26719 | a259d259c797 |
parent 23813 | 5440f9f5522c |
child 27789 | 1bf827e3258d |
permissions | -rw-r--r-- |
2222 | 1 |
(* Title: HOL/ex/Puzzle.thy |
969 | 2 |
ID: $Id$ |
1476 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1993 TU Muenchen |
5 |
||
2222 | 6 |
A question from "Bundeswettbewerb Mathematik" |
13116 | 7 |
|
8 |
Proof due to Herbert Ehler |
|
969 | 9 |
*) |
10 |
||
17388 | 11 |
header {* A question from ``Bundeswettbewerb Mathematik'' *} |
12 |
||
16417 | 13 |
theory Puzzle imports Main begin |
13116 | 14 |
|
15 |
consts f :: "nat => nat" |
|
16 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13116
diff
changeset
|
17 |
specification (f) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13116
diff
changeset
|
18 |
f_ax [intro!]: "f(f(n)) < f(Suc(n))" |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13116
diff
changeset
|
19 |
by (rule exI [of _ id], simp) |
13116 | 20 |
|
21 |
||
22 |
lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)" |
|
23 |
apply (induct_tac "k" rule: nat_less_induct) |
|
24 |
apply (rule allI) |
|
25 |
apply (rename_tac "i") |
|
26 |
apply (case_tac "i") |
|
27 |
apply simp |
|
28 |
apply (blast intro!: Suc_leI intro: le_less_trans) |
|
29 |
done |
|
30 |
||
31 |
lemma lemma1: "n <= f(n)" |
|
32 |
by (blast intro: lemma0) |
|
33 |
||
34 |
lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)" |
|
35 |
apply (induct_tac "n") |
|
23813 | 36 |
apply simp |
37 |
apply (metis f_ax le_SucE le_trans lemma0 nat_le_linear nat_less_le) |
|
13116 | 38 |
done |
39 |
||
40 |
lemma f_id: "f(n) = n" |
|
41 |
apply (rule order_antisym) |
|
42 |
apply (rule_tac [2] lemma1) |
|
43 |
apply (blast intro: leI dest: leD f_mono Suc_leI) |
|
44 |
done |
|
45 |
||
969 | 46 |
end |
13116 | 47 |