src/HOL/Isar_examples/Puzzle.thy
 author haftmann Mon Jan 30 08:20:56 2006 +0100 (2006-01-30) changeset 18851 9502ce541f01 parent 18204 c3caf13f621d child 20503 503ac4c5ef91 permissions -rw-r--r--
 wenzelm@8020  1 wenzelm@10007  2 header {* An old chestnut *}  wenzelm@8020  3 haftmann@16417  4 theory Puzzle imports Main begin  wenzelm@8020  5 wenzelm@8020  6 text_raw {*  wenzelm@18193  7  \footnote{A question from Bundeswettbewerb Mathematik''. Original  wenzelm@18193  8  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by  wenzelm@18193  9  Tobias Nipkow.}  wenzelm@18193  10 *}  wenzelm@8020  11 wenzelm@18193  12 text {*  wenzelm@18193  13  \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ such  wenzelm@18193  14  that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  wenzelm@18193  15  Demonstrate that $f$ is the identity.  wenzelm@10007  16 *}  wenzelm@8020  17 wenzelm@18191  18 theorem  wenzelm@18191  19  assumes f_ax: "\n. f (f n) < f (Suc n)"  wenzelm@18191  20  shows "f n = n"  wenzelm@10436  21 proof (rule order_antisym)  wenzelm@18191  22  {  wenzelm@18191  23  fix n show "n \ f n"  wenzelm@18204  24  proof (induct k \ "f n" fixing: n rule: less_induct)  wenzelm@18191  25  case (less k n)  wenzelm@18191  26  then have hyp: "\m. f m < f n \ m \ f m" by (simp only:)  wenzelm@18191  27  show "n \ f n"  wenzelm@10436  28  proof (cases n)  wenzelm@18191  29  case (Suc m)  wenzelm@18191  30  from f_ax have "f (f m) < f n" by (simp only: Suc)  wenzelm@18191  31  with hyp have "f m \ f (f m)" .  wenzelm@18191  32  also from f_ax have "\ < f n" by (simp only: Suc)  wenzelm@18191  33  finally have "f m < f n" .  wenzelm@18191  34  with hyp have "m \ f m" .  wenzelm@18191  35  also note \ < f n  wenzelm@18191  36  finally have "m < f n" .  wenzelm@18191  37  then have "n \ f n" by (simp only: Suc)  wenzelm@18191  38  then show ?thesis .  wenzelm@10007  39  next  wenzelm@18191  40  case 0  wenzelm@18191  41  then show ?thesis by simp  wenzelm@10007  42  qed  wenzelm@10007  43  qed  wenzelm@18191  44  } note ge = this  wenzelm@8020  45 wenzelm@10436  46  {  wenzelm@18191  47  fix m n :: nat  wenzelm@18191  48  assume "m \ n"  wenzelm@18191  49  then have "f m \ f n"  wenzelm@10007  50  proof (induct n)  wenzelm@18191  51  case 0  wenzelm@18191  52  then have "m = 0" by simp  wenzelm@18191  53  then show ?case by simp  wenzelm@10436  54  next  wenzelm@18191  55  case (Suc n)  wenzelm@18191  56  from Suc.prems show "f m \ f (Suc n)"  wenzelm@10436  57  proof (rule le_SucE)  wenzelm@18191  58  assume "m \ n"  wenzelm@18191  59  with Suc.hyps have "f m \ f n" .  wenzelm@18191  60  also from ge f_ax have "\ < f (Suc n)"  wenzelm@10436  61  by (rule le_less_trans)  wenzelm@10436  62  finally show ?thesis by simp  wenzelm@10436  63  next  wenzelm@10436  64  assume "m = Suc n"  wenzelm@18191  65  then show ?thesis by simp  wenzelm@10007  66  qed  wenzelm@10007  67  qed  wenzelm@10436  68  } note mono = this  wenzelm@8020  69 wenzelm@18191  70  show "f n \ n"  wenzelm@10436  71  proof -  wenzelm@18191  72  have "\ n < f n"  wenzelm@10007  73  proof  wenzelm@10007  74  assume "n < f n"  wenzelm@18191  75  then have "Suc n \ f n" by simp  wenzelm@18191  76  then have "f (Suc n) \ f (f n)" by (rule mono)  wenzelm@18191  77  also have "\ < f (Suc n)" by (rule f_ax)  wenzelm@18191  78  finally have "\ < \" . then show False ..  wenzelm@10007  79  qed  wenzelm@18191  80  then show ?thesis by simp  wenzelm@10007  81  qed  wenzelm@10007  82 qed  wenzelm@8020  83 wenzelm@10007  84 end