src/HOL/Isar_Examples/Puzzle.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 34915 7894c7dab132 child 37671 fa53d267dab3 permissions -rw-r--r--
more speaking names
 wenzelm@10007  1 header {* An old chestnut *}  wenzelm@8020  2 wenzelm@31758  3 theory Puzzle  wenzelm@31758  4 imports Main  wenzelm@31758  5 begin  wenzelm@8020  6 wenzelm@8020  7 text_raw {*  wenzelm@18193  8  \footnote{A question from Bundeswettbewerb Mathematik''. Original  wenzelm@18193  9  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by  wenzelm@18193  10  Tobias Nipkow.}  wenzelm@18193  11 *}  wenzelm@8020  12 wenzelm@18193  13 text {*  wenzelm@18193  14  \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ such  wenzelm@18193  15  that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  wenzelm@18193  16  Demonstrate that $f$ is the identity.  wenzelm@10007  17 *}  wenzelm@8020  18 wenzelm@18191  19 theorem  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"  berghofe@34915  25  proof (induct "f n" arbitrary: n rule: less_induct)  berghofe@34915  26  case less  wenzelm@18191  27  show "n \ f n"  wenzelm@10436  28  proof (cases n)  wenzelm@32960  29  case (Suc m)  wenzelm@32960  30  from f_ax have "f (f m) < f n" by (simp only: Suc)  berghofe@34915  31  with less have "f m \ f (f m)" .  wenzelm@32960  32  also from f_ax have "\ < f n" by (simp only: Suc)  wenzelm@32960  33  finally have "f m < f n" .  berghofe@34915  34  with less have "m \ f m" .  wenzelm@32960  35  also note \ < f n  wenzelm@32960  36  finally have "m < f n" .  wenzelm@32960  37  then have "n \ f n" by (simp only: Suc)  wenzelm@32960  38  then show ?thesis .  wenzelm@10007  39  next  wenzelm@32960  40  case 0  wenzelm@32960  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