src/HOL/Isar_Examples/Puzzle.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 37671 fa53d267dab3 child 58614 7338eb25226c permissions -rw-r--r--
 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@37671  7 text_raw {* \footnote{A question from Bundeswettbewerb Mathematik''.  wenzelm@37671  8  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic  wenzelm@37671  9  script by Tobias Nipkow.} *}  wenzelm@8020  10 wenzelm@37671  11 text {* \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$  wenzelm@37671  12  such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  wenzelm@37671  13  Demonstrate that $f$ is the identity. *}  wenzelm@8020  14 wenzelm@18191  15 theorem  wenzelm@18191  16  assumes f_ax: "\n. f (f n) < f (Suc n)"  wenzelm@18191  17  shows "f n = n"  wenzelm@10436  18 proof (rule order_antisym)  wenzelm@18191  19  {  wenzelm@18191  20  fix n show "n \ f n"  berghofe@34915  21  proof (induct "f n" arbitrary: n rule: less_induct)  berghofe@34915  22  case less  wenzelm@18191  23  show "n \ f n"  wenzelm@10436  24  proof (cases n)  wenzelm@32960  25  case (Suc m)  wenzelm@32960  26  from f_ax have "f (f m) < f n" by (simp only: Suc)  berghofe@34915  27  with less have "f m \ f (f m)" .  wenzelm@32960  28  also from f_ax have "\ < f n" by (simp only: Suc)  wenzelm@32960  29  finally have "f m < f n" .  berghofe@34915  30  with less have "m \ f m" .  wenzelm@32960  31  also note \ < f n  wenzelm@32960  32  finally have "m < f n" .  wenzelm@32960  33  then have "n \ f n" by (simp only: Suc)  wenzelm@32960  34  then show ?thesis .  wenzelm@10007  35  next  wenzelm@32960  36  case 0  wenzelm@32960  37  then show ?thesis by simp  wenzelm@10007  38  qed  wenzelm@10007  39  qed  wenzelm@18191  40  } note ge = this  wenzelm@8020  41 wenzelm@10436  42  {  wenzelm@18191  43  fix m n :: nat  wenzelm@18191  44  assume "m \ n"  wenzelm@18191  45  then have "f m \ f n"  wenzelm@10007  46  proof (induct n)  wenzelm@18191  47  case 0  wenzelm@18191  48  then have "m = 0" by simp  wenzelm@18191  49  then show ?case by simp  wenzelm@10436  50  next  wenzelm@18191  51  case (Suc n)  wenzelm@18191  52  from Suc.prems show "f m \ f (Suc n)"  wenzelm@10436  53  proof (rule le_SucE)  wenzelm@18191  54  assume "m \ n"  wenzelm@18191  55  with Suc.hyps have "f m \ f n" .  wenzelm@18191  56  also from ge f_ax have "\ < f (Suc n)"  wenzelm@10436  57  by (rule le_less_trans)  wenzelm@10436  58  finally show ?thesis by simp  wenzelm@10436  59  next  wenzelm@10436  60  assume "m = Suc n"  wenzelm@18191  61  then show ?thesis by simp  wenzelm@10007  62  qed  wenzelm@10007  63  qed  wenzelm@10436  64  } note mono = this  wenzelm@8020  65 wenzelm@18191  66  show "f n \ n"  wenzelm@10436  67  proof -  wenzelm@18191  68  have "\ n < f n"  wenzelm@10007  69  proof  wenzelm@10007  70  assume "n < f n"  wenzelm@18191  71  then have "Suc n \ f n" by simp  wenzelm@18191  72  then have "f (Suc n) \ f (f n)" by (rule mono)  wenzelm@18191  73  also have "\ < f (Suc n)" by (rule f_ax)  wenzelm@18191  74  finally have "\ < \" . then show False ..  wenzelm@10007  75  qed  wenzelm@18191  76  then show ?thesis by simp  wenzelm@10007  77  qed  wenzelm@10007  78 qed  wenzelm@8020  79 wenzelm@10007  80 end