header {* An old chestnut *}
theory Puzzle imports Main begin
text_raw {*
\footnote{A question from ``Bundeswettbewerb Mathematik''. Original
pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
Tobias Nipkow.}
\medskip \textbf{Problem.} Given some function $f\colon \Nat \to
\Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all
$n$. Demonstrate that $f$ is the identity.
*}
theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"
proof (rule order_antisym)
assume f_ax: "!!n. f (f n) < f (Suc n)"
txt {*
Note that the generalized form of $n \le f \ap n$ is required
later for monotonicity as well.
*}
show ge: "!!n. n <= f n"
proof -
fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
proof (induct k rule: less_induct)
fix k assume hyp: "!!m. m < k ==> PROP ?P m"
fix n assume k_def: "k == f n"
show "n <= k"
proof (cases n)
assume "n = 0" thus ?thesis by simp
next
fix m assume Suc: "n = Suc m"
from f_ax have "f (f m) < f (Suc m)" .
with hyp k_def Suc have "f m <= f (f m)" by simp
also from f_ax have "... < f (Suc m)" .
finally have less: "f m < f (Suc m)" .
with hyp k_def Suc have "m <= f m" by simp
also note less
finally have "m < f (Suc m)" .
hence "n <= f n" by (simp only: Suc)
thus ?thesis by (simp only: k_def)
qed
qed
qed
txt {*
In order to show the other direction, we first establish
monotonicity of $f$.
*}
{
fix m n
have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
proof (induct n)
assume "m <= 0" hence "m = 0" by simp
thus "f m <= f 0" by simp
next
fix n assume hyp: "PROP ?P n"
assume "m <= Suc n"
thus "f m <= f (Suc n)"
proof (rule le_SucE)
assume "m <= n"
with hyp have "f m <= f n" .
also from ge f_ax have "... < f (Suc n)"
by (rule le_less_trans)
finally show ?thesis by simp
next
assume "m = Suc n"
thus ?thesis by simp
qed
qed
} note mono = this
show "f n <= n"
proof -
have "~ n < f n"
proof
assume "n < f n"
hence "Suc n <= f n" by simp
hence "f (Suc n) <= f (f n)" by (rule mono)
also have "... < f (Suc n)" by (rule f_ax)
finally have "... < ..." . thus False ..
qed
thus ?thesis by simp
qed
qed
end