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.} *}

 text {* \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

   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"

   shows "f n = n"

 proof (rule order_antisym)

   {

     fix n show "n \<le> f n"

     proof (induct "f n" arbitrary: n rule: less_induct)

       case less

       show "n \<le> 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 \<le> f (f m)" .

         also from f_ax have "\<dots> < f n" by (simp only: Suc)

         finally have "f m < f n" .

         with less have "m \<le> f m" .

         also note `\<dots> < f n`

         finally have "m < f n" .

         then have "n \<le> f n" by (simp only: Suc)

         then show ?thesis .

       next

         case 0

         then show ?thesis by simp

       qed

     qed

   } note ge = this

   {

     fix m n :: nat

     assume "m \<le> n"

     then have "f m \<le> f n"

     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 \<le> f (Suc n)"

       proof (rule le_SucE)

         assume "m \<le> n"

         with Suc.hyps have "f m \<le> f n" .

         also from ge f_ax have "\<dots> < 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

   } note mono = this

   show "f n \<le> n"

   proof -

     have "\<not> n < f n"

     proof

       assume "n < f n"

       then have "Suc n \<le> f n" by simp

       then have "f (Suc n) \<le> f (f n)" by (rule mono)

       also have "\<dots> < f (Suc n)" by (rule f_ax)

       finally have "\<dots> < \<dots>" . then show False ..

     qed

     then show ?thesis by simp

   qed

 qed

 end