# Theory Puzzle

section ‹An old chestnut›
theory Puzzle
imports Main
begin
text_raw ‹⁋‹A question from ``Bundeswettbewerb Mathematik''. Original
pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias
Nipkow.››
text ‹
❙‹Problem.› Given some function ‹f: ℕ → ℕ› such that ‹f (f n) < f (Suc n)›
for all ‹n›. Demonstrate that ‹f› is the identity.
›
theorem
assumes f_ax: "⋀n. f (f n) < f (Suc n)"
shows "f n = n"
proof (rule order_antisym)
show ge: "n ≤ f n" for n
proof (induct "f n" arbitrary: n rule: less_induct)
case less
show "n ≤ f n"
proof (cases n)
case (Suc m)
from f_ax have "f (f m) < f n" by (simp only: Suc)
with less have "f m ≤ f (f m)" .
also from f_ax have "… < f n" by (simp only: Suc)
finally have "f m < f n" .
with less have "m ≤ f m" .
also note ‹… < f n›
finally have "m < f n" .
then have "n ≤ f n" by (simp only: Suc)
then show ?thesis .
next
case 0
then show ?thesis by simp
qed
qed
have mono: "m ≤ n ⟹ f m ≤ f n" for m n :: nat
proof (induct n)
case 0
then have "m = 0" by simp
then show ?case by simp
next
case (Suc n)
from Suc.prems show "f m ≤ f (Suc n)"
proof (rule le_SucE)
assume "m ≤ n"
with Suc.hyps 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"
then show ?thesis by simp
qed
qed
show "f n ≤ n"
proof -
have "¬ n < f n"
proof
assume "n < f n"
then have "Suc n ≤ f n" by simp
then have "f (Suc n) ≤ f (f n)" by (rule mono)
also have "… < f (Suc n)" by (rule f_ax)
finally have "… < …" . then show False ..
qed
then show ?thesis by simp
qed
qed
end