src/HOL/Isar_examples/Puzzle.thy
 author wenzelm Wed Nov 16 19:34:19 2005 +0100 (2005-11-16) changeset 18193 54419506df9e parent 18191 ef29685acef0 child 18204 c3caf13f621d permissions -rw-r--r--
tuned document;
 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  fixes n :: nat  wenzelm@18191  20  assumes f_ax: "\n. f (f n) < f (Suc n)"  wenzelm@18191  21  shows "f n = n"  wenzelm@10436  22 proof (rule order_antisym)  wenzelm@18191  23  {  wenzelm@18191  24  fix n show "n \ f n"  wenzelm@18191  25  proof (induct k \ "f n" rule: less_induct fixing: n)  wenzelm@18191  26  case (less k n)  wenzelm@18191  27  then have hyp: "\m. f m < f n \ m \ f m" by (simp only:)  wenzelm@18191  28  show "n \ f n"  wenzelm@10436  29  proof (cases n)  wenzelm@18191  30  case (Suc m)  wenzelm@18191  31  from f_ax have "f (f m) < f n" by (simp only: Suc)  wenzelm@18191  32  with hyp have "f m \ f (f m)" .  wenzelm@18191  33  also from f_ax have "\ < f n" by (simp only: Suc)  wenzelm@18191  34  finally have "f m < f n" .  wenzelm@18191  35  with hyp have "m \ f m" .  wenzelm@18191  36  also note \ < f n  wenzelm@18191  37  finally have "m < f n" .  wenzelm@18191  38  then have "n \ f n" by (simp only: Suc)  wenzelm@18191  39  then show ?thesis .  wenzelm@10007  40  next  wenzelm@18191  41  case 0  wenzelm@18191  42  then show ?thesis by simp  wenzelm@10007  43  qed  wenzelm@10007  44  qed  wenzelm@18191  45  } note ge = this  wenzelm@8020  46 wenzelm@10436  47  {  wenzelm@18191  48  fix m n :: nat  wenzelm@18191  49  assume "m \ n"  wenzelm@18191  50  then have "f m \ f n"  wenzelm@10007  51  proof (induct n)  wenzelm@18191  52  case 0  wenzelm@18191  53  then have "m = 0" by simp  wenzelm@18191  54  then show ?case by simp  wenzelm@10436  55  next  wenzelm@18191  56  case (Suc n)  wenzelm@18191  57  from Suc.prems show "f m \ f (Suc n)"  wenzelm@10436  58  proof (rule le_SucE)  wenzelm@18191  59  assume "m \ n"  wenzelm@18191  60  with Suc.hyps have "f m \ f n" .  wenzelm@18191  61  also from ge f_ax have "\ < f (Suc n)"  wenzelm@10436  62  by (rule le_less_trans)  wenzelm@10436  63  finally show ?thesis by simp  wenzelm@10436  64  next  wenzelm@10436  65  assume "m = Suc n"  wenzelm@18191  66  then show ?thesis by simp  wenzelm@10007  67  qed  wenzelm@10007  68  qed  wenzelm@10436  69  } note mono = this  wenzelm@8020  70 wenzelm@18191  71  show "f n \ n"  wenzelm@10436  72  proof -  wenzelm@18191  73  have "\ n < f n"  wenzelm@10007  74  proof  wenzelm@10007  75  assume "n < f n"  wenzelm@18191  76  then have "Suc n \ f n" by simp  wenzelm@18191  77  then have "f (Suc n) \ f (f n)" by (rule mono)  wenzelm@18191  78  also have "\ < f (Suc n)" by (rule f_ax)  wenzelm@18191  79  finally have "\ < \" . then show False ..  wenzelm@10007  80  qed  wenzelm@18191  81  then show ?thesis by simp  wenzelm@10007  82  qed  wenzelm@10007  83 qed  wenzelm@8020  84 wenzelm@10007  85 end