58882
|
1 |
section \<open>An old chestnut\<close>
|
8020
|
2 |
|
31758
|
3 |
theory Puzzle
|
|
4 |
imports Main
|
|
5 |
begin
|
8020
|
6 |
|
58614
|
7 |
text_raw \<open>\footnote{A question from ``Bundeswettbewerb Mathematik''.
|
37671
|
8 |
Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
|
58614
|
9 |
script by Tobias Nipkow.}\<close>
|
8020
|
10 |
|
58614
|
11 |
text \<open>\textbf{Problem.} Given some function $f\colon \Nat \to \Nat$
|
37671
|
12 |
such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
|
58614
|
13 |
Demonstrate that $f$ is the identity.\<close>
|
8020
|
14 |
|
18191
|
15 |
theorem
|
|
16 |
assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
|
|
17 |
shows "f n = n"
|
10436
|
18 |
proof (rule order_antisym)
|
60410
|
19 |
show ge: "n \<le> f n" for n
|
|
20 |
proof (induct "f n" arbitrary: n rule: less_induct)
|
|
21 |
case less
|
|
22 |
show "n \<le> f n"
|
|
23 |
proof (cases n)
|
|
24 |
case (Suc m)
|
|
25 |
from f_ax have "f (f m) < f n" by (simp only: Suc)
|
|
26 |
with less have "f m \<le> f (f m)" .
|
|
27 |
also from f_ax have "\<dots> < f n" by (simp only: Suc)
|
|
28 |
finally have "f m < f n" .
|
|
29 |
with less have "m \<le> f m" .
|
|
30 |
also note \<open>\<dots> < f n\<close>
|
|
31 |
finally have "m < f n" .
|
|
32 |
then have "n \<le> f n" by (simp only: Suc)
|
|
33 |
then show ?thesis .
|
|
34 |
next
|
|
35 |
case 0
|
|
36 |
then show ?thesis by simp
|
10007
|
37 |
qed
|
60410
|
38 |
qed
|
8020
|
39 |
|
60410
|
40 |
have mono: "m \<le> n \<Longrightarrow> f m \<le> f n" for m n :: nat
|
|
41 |
proof (induct n)
|
|
42 |
case 0
|
|
43 |
then have "m = 0" by simp
|
|
44 |
then show ?case by simp
|
|
45 |
next
|
|
46 |
case (Suc n)
|
|
47 |
from Suc.prems show "f m \<le> f (Suc n)"
|
|
48 |
proof (rule le_SucE)
|
|
49 |
assume "m \<le> n"
|
|
50 |
with Suc.hyps have "f m \<le> f n" .
|
|
51 |
also from ge f_ax have "\<dots> < f (Suc n)"
|
|
52 |
by (rule le_less_trans)
|
|
53 |
finally show ?thesis by simp
|
10436
|
54 |
next
|
60410
|
55 |
assume "m = Suc n"
|
|
56 |
then show ?thesis by simp
|
10007
|
57 |
qed
|
60410
|
58 |
qed
|
8020
|
59 |
|
18191
|
60 |
show "f n \<le> n"
|
10436
|
61 |
proof -
|
18191
|
62 |
have "\<not> n < f n"
|
10007
|
63 |
proof
|
|
64 |
assume "n < f n"
|
18191
|
65 |
then have "Suc n \<le> f n" by simp
|
|
66 |
then have "f (Suc n) \<le> f (f n)" by (rule mono)
|
|
67 |
also have "\<dots> < f (Suc n)" by (rule f_ax)
|
|
68 |
finally have "\<dots> < \<dots>" . then show False ..
|
10007
|
69 |
qed
|
18191
|
70 |
then show ?thesis by simp
|
10007
|
71 |
qed
|
|
72 |
qed
|
8020
|
73 |
|
10007
|
74 |
end
|