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