src/HOL/Isar_examples/Puzzle.thy
 author haftmann Fri Jun 17 16:12:49 2005 +0200 (2005-06-17) changeset 16417 9bc16273c2d4 parent 12997 80dec7322a8c child 18191 ef29685acef0 permissions -rw-r--r--
migrated theory headers to new format
 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@10436  7  \footnote{A question from Bundeswettbewerb Mathematik''. Original  wenzelm@10436  8  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by  wenzelm@10436  9  Tobias Nipkow.}  wenzelm@8020  10 wenzelm@10436  11  \medskip \textbf{Problem.} Given some function $f\colon \Nat \to  wenzelm@10436  12  \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all  wenzelm@10436  13  $n$. Demonstrate that $f$ is the identity.  wenzelm@10007  14 *}  wenzelm@8020  15 wenzelm@10436  16 theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"  wenzelm@10436  17 proof (rule order_antisym)  wenzelm@10436  18  assume f_ax: "!!n. f (f n) < f (Suc n)"  wenzelm@8020  19 wenzelm@8020  20  txt {*  wenzelm@8020  21  Note that the generalized form of $n \le f \ap n$ is required  wenzelm@8020  22  later for monotonicity as well.  wenzelm@10007  23  *}  wenzelm@10007  24  show ge: "!!n. n <= f n"  wenzelm@10007  25  proof -  wenzelm@10436  26  fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")  wenzelm@12997  27  proof (induct k rule: less_induct)  wenzelm@10436  28  fix k assume hyp: "!!m. m < k ==> PROP ?P m"  wenzelm@10436  29  fix n assume k_def: "k == f n"  wenzelm@10436  30  show "n <= k"  wenzelm@10436  31  proof (cases n)  wenzelm@10436  32  assume "n = 0" thus ?thesis by simp  wenzelm@10007  33  next  wenzelm@10436  34  fix m assume Suc: "n = Suc m"  wenzelm@10436  35  from f_ax have "f (f m) < f (Suc m)" .  wenzelm@10436  36  with hyp k_def Suc have "f m <= f (f m)" by simp  wenzelm@10436  37  also from f_ax have "... < f (Suc m)" .  wenzelm@10436  38  finally have less: "f m < f (Suc m)" .  wenzelm@10436  39  with hyp k_def Suc have "m <= f m" by simp  wenzelm@10436  40  also note less  wenzelm@10436  41  finally have "m < f (Suc m)" .  wenzelm@10436  42  hence "n <= f n" by (simp only: Suc)  wenzelm@10436  43  thus ?thesis by (simp only: k_def)  wenzelm@10007  44  qed  wenzelm@10007  45  qed  wenzelm@10007  46  qed  wenzelm@8020  47 wenzelm@8020  48  txt {*  wenzelm@8020  49  In order to show the other direction, we first establish  wenzelm@8020  50  monotonicity of $f$.  wenzelm@10007  51  *}  wenzelm@10436  52  {  wenzelm@10007  53  fix m n  wenzelm@10436  54  have "m <= n \ f m <= f n" (is "PROP ?P n")  wenzelm@10007  55  proof (induct n)  wenzelm@10436  56  assume "m <= 0" hence "m = 0" by simp  wenzelm@10436  57  thus "f m <= f 0" by simp  wenzelm@10436  58  next  wenzelm@10436  59  fix n assume hyp: "PROP ?P n"  wenzelm@10436  60  assume "m <= Suc n"  wenzelm@10436  61  thus "f m <= f (Suc n)"  wenzelm@10436  62  proof (rule le_SucE)  wenzelm@10436  63  assume "m <= n"  wenzelm@10436  64  with hyp have "f m <= f n" .  wenzelm@10436  65  also from ge f_ax have "... < f (Suc n)"  wenzelm@10436  66  by (rule le_less_trans)  wenzelm@10436  67  finally show ?thesis by simp  wenzelm@10436  68  next  wenzelm@10436  69  assume "m = Suc n"  wenzelm@10436  70  thus ?thesis by simp  wenzelm@10007  71  qed  wenzelm@10007  72  qed  wenzelm@10436  73  } note mono = this  wenzelm@8020  74 wenzelm@10007  75  show "f n <= n"  wenzelm@10436  76  proof -  wenzelm@10436  77  have "~ n < f n"  wenzelm@10007  78  proof  wenzelm@10007  79  assume "n < f n"  wenzelm@10436  80  hence "Suc n <= f n" by simp  wenzelm@10436  81  hence "f (Suc n) <= f (f n)" by (rule mono)  wenzelm@10007  82  also have "... < f (Suc n)" by (rule f_ax)  wenzelm@10007  83  finally have "... < ..." . thus False ..  wenzelm@10007  84  qed  wenzelm@10436  85  thus ?thesis by simp  wenzelm@10007  86  qed  wenzelm@10007  87 qed  wenzelm@8020  88 wenzelm@10007  89 end