Quelle  Puzzle.thy   Sprache: Isabelle

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