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