8020
|
1 |
|
10007
|
2 |
header {* An old chestnut *}
|
8020
|
3 |
|
10007
|
4 |
theory Puzzle = Main:
|
8020
|
5 |
|
|
6 |
text_raw {*
|
10436
|
7 |
\footnote{A question from ``Bundeswettbewerb Mathematik''. Original
|
|
8 |
pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
|
|
9 |
Tobias Nipkow.}
|
8020
|
10 |
|
10436
|
11 |
\medskip \textbf{Problem.} Given some function $f\colon \Nat \to
|
|
12 |
\Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all
|
|
13 |
$n$. Demonstrate that $f$ is the identity.
|
10007
|
14 |
*}
|
8020
|
15 |
|
10436
|
16 |
theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"
|
|
17 |
proof (rule order_antisym)
|
|
18 |
assume f_ax: "!!n. f (f n) < f (Suc n)"
|
8020
|
19 |
|
|
20 |
txt {*
|
|
21 |
Note that the generalized form of $n \le f \ap n$ is required
|
|
22 |
later for monotonicity as well.
|
10007
|
23 |
*}
|
|
24 |
show ge: "!!n. n <= f n"
|
|
25 |
proof -
|
10436
|
26 |
fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
|
12997
|
27 |
proof (induct k rule: less_induct)
|
10436
|
28 |
fix k assume hyp: "!!m. m < k ==> PROP ?P m"
|
|
29 |
fix n assume k_def: "k == f n"
|
|
30 |
show "n <= k"
|
|
31 |
proof (cases n)
|
|
32 |
assume "n = 0" thus ?thesis by simp
|
10007
|
33 |
next
|
10436
|
34 |
fix m assume Suc: "n = Suc m"
|
|
35 |
from f_ax have "f (f m) < f (Suc m)" .
|
|
36 |
with hyp k_def Suc have "f m <= f (f m)" by simp
|
|
37 |
also from f_ax have "... < f (Suc m)" .
|
|
38 |
finally have less: "f m < f (Suc m)" .
|
|
39 |
with hyp k_def Suc have "m <= f m" by simp
|
|
40 |
also note less
|
|
41 |
finally have "m < f (Suc m)" .
|
|
42 |
hence "n <= f n" by (simp only: Suc)
|
|
43 |
thus ?thesis by (simp only: k_def)
|
10007
|
44 |
qed
|
|
45 |
qed
|
|
46 |
qed
|
8020
|
47 |
|
|
48 |
txt {*
|
|
49 |
In order to show the other direction, we first establish
|
|
50 |
monotonicity of $f$.
|
10007
|
51 |
*}
|
10436
|
52 |
{
|
10007
|
53 |
fix m n
|
10436
|
54 |
have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
|
10007
|
55 |
proof (induct n)
|
10436
|
56 |
assume "m <= 0" hence "m = 0" by simp
|
|
57 |
thus "f m <= f 0" by simp
|
|
58 |
next
|
|
59 |
fix n assume hyp: "PROP ?P n"
|
|
60 |
assume "m <= Suc n"
|
|
61 |
thus "f m <= f (Suc n)"
|
|
62 |
proof (rule le_SucE)
|
|
63 |
assume "m <= n"
|
|
64 |
with hyp have "f m <= f n" .
|
|
65 |
also from ge f_ax have "... < f (Suc n)"
|
|
66 |
by (rule le_less_trans)
|
|
67 |
finally show ?thesis by simp
|
|
68 |
next
|
|
69 |
assume "m = Suc n"
|
|
70 |
thus ?thesis by simp
|
10007
|
71 |
qed
|
|
72 |
qed
|
10436
|
73 |
} note mono = this
|
8020
|
74 |
|
10007
|
75 |
show "f n <= n"
|
10436
|
76 |
proof -
|
|
77 |
have "~ n < f n"
|
10007
|
78 |
proof
|
|
79 |
assume "n < f n"
|
10436
|
80 |
hence "Suc n <= f n" by simp
|
|
81 |
hence "f (Suc n) <= f (f n)" by (rule mono)
|
10007
|
82 |
also have "... < f (Suc n)" by (rule f_ax)
|
|
83 |
finally have "... < ..." . thus False ..
|
|
84 |
qed
|
10436
|
85 |
thus ?thesis by simp
|
10007
|
86 |
qed
|
|
87 |
qed
|
8020
|
88 |
|
10007
|
89 |
end
|