author | huffman |
Tue, 02 Mar 2010 09:54:50 -0800 | |
changeset 35512 | d1ef88d7de5a |
parent 34915 | 7894c7dab132 |
child 37671 | fa53d267dab3 |
permissions | -rw-r--r-- |
10007 | 1 |
header {* An old chestnut *} |
8020 | 2 |
|
31758 | 3 |
theory Puzzle |
4 |
imports Main |
|
5 |
begin |
|
8020 | 6 |
|
7 |
text_raw {* |
|
18193 | 8 |
\footnote{A question from ``Bundeswettbewerb Mathematik''. Original |
9 |
pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by |
|
10 |
Tobias Nipkow.} |
|
11 |
*} |
|
8020 | 12 |
|
18193 | 13 |
text {* |
14 |
\textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ such |
|
15 |
that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$. |
|
16 |
Demonstrate that $f$ is the identity. |
|
10007 | 17 |
*} |
8020 | 18 |
|
18191 | 19 |
theorem |
20 |
assumes f_ax: "\<And>n. f (f n) < f (Suc n)" |
|
21 |
shows "f n = n" |
|
10436 | 22 |
proof (rule order_antisym) |
18191 | 23 |
{ |
24 |
fix n show "n \<le> f n" |
|
34915 | 25 |
proof (induct "f n" arbitrary: n rule: less_induct) |
26 |
case less |
|
18191 | 27 |
show "n \<le> f n" |
10436 | 28 |
proof (cases n) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
29 |
case (Suc m) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
30 |
from f_ax have "f (f m) < f n" by (simp only: Suc) |
34915 | 31 |
with less have "f m \<le> f (f m)" . |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
32 |
also from f_ax have "\<dots> < f n" by (simp only: Suc) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
33 |
finally have "f m < f n" . |
34915 | 34 |
with less have "m \<le> f m" . |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
35 |
also note `\<dots> < f n` |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
36 |
finally have "m < f n" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
37 |
then have "n \<le> f n" by (simp only: Suc) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
38 |
then show ?thesis . |
10007 | 39 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
40 |
case 0 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31758
diff
changeset
|
41 |
then show ?thesis by simp |
10007 | 42 |
qed |
43 |
qed |
|
18191 | 44 |
} note ge = this |
8020 | 45 |
|
10436 | 46 |
{ |
18191 | 47 |
fix m n :: nat |
48 |
assume "m \<le> n" |
|
49 |
then have "f m \<le> f n" |
|
10007 | 50 |
proof (induct n) |
18191 | 51 |
case 0 |
52 |
then have "m = 0" by simp |
|
53 |
then show ?case by simp |
|
10436 | 54 |
next |
18191 | 55 |
case (Suc n) |
56 |
from Suc.prems show "f m \<le> f (Suc n)" |
|
10436 | 57 |
proof (rule le_SucE) |
18191 | 58 |
assume "m \<le> n" |
59 |
with Suc.hyps have "f m \<le> f n" . |
|
60 |
also from ge f_ax have "\<dots> < f (Suc n)" |
|
10436 | 61 |
by (rule le_less_trans) |
62 |
finally show ?thesis by simp |
|
63 |
next |
|
64 |
assume "m = Suc n" |
|
18191 | 65 |
then show ?thesis by simp |
10007 | 66 |
qed |
67 |
qed |
|
10436 | 68 |
} note mono = this |
8020 | 69 |
|
18191 | 70 |
show "f n \<le> n" |
10436 | 71 |
proof - |
18191 | 72 |
have "\<not> n < f n" |
10007 | 73 |
proof |
74 |
assume "n < f n" |
|
18191 | 75 |
then have "Suc n \<le> f n" by simp |
76 |
then have "f (Suc n) \<le> f (f n)" by (rule mono) |
|
77 |
also have "\<dots> < f (Suc n)" by (rule f_ax) |
|
78 |
finally have "\<dots> < \<dots>" . then show False .. |
|
10007 | 79 |
qed |
18191 | 80 |
then show ?thesis by simp |
10007 | 81 |
qed |
82 |
qed |
|
8020 | 83 |
|
10007 | 84 |
end |