equal
deleted
inserted
replaced
2 |
2 |
3 theory Puzzle |
3 theory Puzzle |
4 imports Main |
4 imports Main |
5 begin |
5 begin |
6 |
6 |
7 text_raw {* |
7 text_raw {* \footnote{A question from ``Bundeswettbewerb Mathematik''. |
8 \footnote{A question from ``Bundeswettbewerb Mathematik''. Original |
8 Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic |
9 pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by |
9 script by Tobias Nipkow.} *} |
10 Tobias Nipkow.} |
|
11 *} |
|
12 |
10 |
13 text {* |
11 text {* \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ |
14 \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ such |
12 such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$. |
15 that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$. |
13 Demonstrate that $f$ is the identity. *} |
16 Demonstrate that $f$ is the identity. |
|
17 *} |
|
18 |
14 |
19 theorem |
15 theorem |
20 assumes f_ax: "\<And>n. f (f n) < f (Suc n)" |
16 assumes f_ax: "\<And>n. f (f n) < f (Suc n)" |
21 shows "f n = n" |
17 shows "f n = n" |
22 proof (rule order_antisym) |
18 proof (rule order_antisym) |