src/HOL/Isar_examples/Puzzle.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 18191 ef29685acef0 permissions -rw-r--r--
Constant "If" is now local
2 header {* An old chestnut *}
4 theory Puzzle imports Main begin
6 text_raw {*
7  \footnote{A question from Bundeswettbewerb Mathematik''.  Original
8  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
9  Tobias Nipkow.}
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.
14 *}
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)"
20   txt {*
21     Note that the generalized form of $n \le f \ap n$ is required
22     later for monotonicity as well.
23   *}
24   show ge: "!!n. n <= f n"
25   proof -
26     fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
27     proof (induct k rule: less_induct)
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
33       next
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)
44       qed
45     qed
46   qed
48   txt {*
49     In order to show the other direction, we first establish
50     monotonicity of $f$.
51   *}
52   {
53     fix m n
54     have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
55     proof (induct n)
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
71       qed
72     qed
73   } note mono = this
75   show "f n <= n"
76   proof -
77     have "~ n < f n"
78     proof
79       assume "n < f n"
80       hence "Suc n <= f n" by simp
81       hence "f (Suc n) <= f (f n)" by (rule mono)
82       also have "... < f (Suc n)" by (rule f_ax)
83       finally have "... < ..." . thus False ..
84     qed
85     thus ?thesis by simp
86   qed
87 qed
89 end