src/HOL/Isar_examples/Puzzle.thy
 author wenzelm Sun May 21 14:49:28 2000 +0200 (2000-05-21) changeset 8902 a705822f4e2a parent 8020 2823ce1753a5 child 9870 2374ba026fc6 permissions -rw-r--r--
replaced {{ }} by { };
 wenzelm@8020  1 wenzelm@8020  2 header {* An old chestnut *};  wenzelm@8020  3 wenzelm@8020  4 theory Puzzle = Main:;  wenzelm@8020  5 wenzelm@8020  6 text_raw {*  wenzelm@8020  7  \footnote{A question from Bundeswettbewerb Mathematik''.  wenzelm@8020  8  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic  wenzelm@8020  9  script by Tobias Nipkow.}  wenzelm@8020  10 *};  wenzelm@8020  11 wenzelm@8020  12 wenzelm@8020  13 subsection {* Generalized mathematical induction *};  wenzelm@8020  14 wenzelm@8020  15 text {*  wenzelm@8020  16  The following derived rule admits induction over some expression  wenzelm@8020  17  $f(x)$ wrt.\ the ${<}$ relation on natural numbers.  wenzelm@8020  18 *};  wenzelm@8020  19 wenzelm@8020  20 lemma gen_less_induct:  wenzelm@8020  21  "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))  wenzelm@8020  22  ==> P x (f x :: nat)"  wenzelm@8020  23  (is "(!!x. ?H x ==> ?C x) ==> _");  wenzelm@8020  24 proof -;  wenzelm@8020  25  assume asm: "!!x. ?H x ==> ?C x";  wenzelm@8902  26  {;  wenzelm@8020  27  fix k;  wenzelm@8020  28  have "ALL x. k = f x --> ?C x" (is "?Q k");  wenzelm@8020  29  proof (rule less_induct);  wenzelm@8020  30  fix k; assume hyp: "ALL m ?C x";  wenzelm@8020  34  proof;  wenzelm@8020  35  assume "k = f x";  wenzelm@8020  36  with hyp; have "?H x"; by blast;  wenzelm@8020  37  thus "?C x"; by (rule asm);  wenzelm@8020  38  qed;  wenzelm@8020  39  qed;  wenzelm@8020  40  qed;  wenzelm@8902  41  };  wenzelm@8020  42  thus "?C x"; by simp;  wenzelm@8020  43 qed;  wenzelm@8020  44 wenzelm@8020  45 wenzelm@8020  46 subsection {* The problem *};  wenzelm@8020  47 wenzelm@8020  48 text {*  wenzelm@8020  49  Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap  wenzelm@8020  50  n) < f \ap (\idt{Suc} \ap n)$ for all $n$. Demonstrate that $f$ is  wenzelm@8020  51  the identity.  wenzelm@8020  52 *};  wenzelm@8020  53 wenzelm@8020  54 consts f :: "nat => nat";  wenzelm@8020  55 axioms f_ax: "f (f n) < f (Suc n)";  wenzelm@8020  56 wenzelm@8020  57 theorem "f n = n";  wenzelm@8020  58 proof (rule order_antisym);  wenzelm@8020  59  txt {*  wenzelm@8020  60  Note that the generalized form of $n \le f \ap n$ is required  wenzelm@8020  61  later for monotonicity as well.  wenzelm@8020  62  *};  wenzelm@8020  63  show ge: "!!n. n <= f n";  wenzelm@8020  64  proof -;  wenzelm@8020  65  fix n;  wenzelm@8020  66  show "?thesis n" (is "?P n (f n)");  wenzelm@8020  67  proof (rule gen_less_induct [of f ?P]);  wenzelm@8020  68  fix n; assume hyp: "ALL m. f m < f n --> ?P m (f m)";  wenzelm@8020  69  show "?P n (f n)";  wenzelm@8020  70  proof (rule nat.exhaust);  wenzelm@8020  71  assume "n = 0"; thus ?thesis; by simp;  wenzelm@8020  72  next;  wenzelm@8020  73  fix m; assume n_Suc: "n = Suc m";  wenzelm@8020  74  from f_ax; have "f (f m) < f (Suc m)"; .;  wenzelm@8020  75  with hyp n_Suc; have "f m <= f (f m)"; by blast;  wenzelm@8020  76  also; from f_ax; have "... < f (Suc m)"; .;  wenzelm@8020  77  finally; have lt: "f m < f (Suc m)"; .;  wenzelm@8020  78  with hyp n_Suc; have "m <= f m"; by blast;  wenzelm@8020  79  also; note lt;  wenzelm@8020  80  finally; have "m < f (Suc m)"; .;  wenzelm@8020  81  thus "n <= f n"; by (simp only: n_Suc);  wenzelm@8020  82  qed;  wenzelm@8020  83  qed;  wenzelm@8020  84  qed;  wenzelm@8020  85 wenzelm@8020  86  txt {*  wenzelm@8020  87  In order to show the other direction, we first establish  wenzelm@8020  88  monotonicity of $f$.  wenzelm@8020  89  *};  wenzelm@8020  90  have mono: "!!m n. m <= n --> f m <= f n";  wenzelm@8020  91  proof -;  wenzelm@8020  92  fix m n;  wenzelm@8020  93  show "?thesis m n" (is "?P n");  wenzelm@8020  94  proof (induct n);  wenzelm@8020  95  show "?P 0"; by simp;  wenzelm@8020  96  fix n; assume hyp: "?P n";  wenzelm@8020  97  show "?P (Suc n)";  wenzelm@8020  98  proof;  wenzelm@8020  99  assume "m <= Suc n";  wenzelm@8020  100  thus "f m <= f (Suc n)";  wenzelm@8020  101  proof (rule le_SucE);  wenzelm@8020  102  assume "m <= n";  wenzelm@8020  103  with hyp; have "f m <= f n"; ..;  wenzelm@8020  104  also; from ge f_ax; have "... < f (Suc n)";  wenzelm@8020  105  by (rule le_less_trans);  wenzelm@8020  106  finally; show ?thesis; by simp;  wenzelm@8020  107  next;  wenzelm@8020  108  assume "m = Suc n";  wenzelm@8020  109  thus ?thesis; by simp;  wenzelm@8020  110  qed;  wenzelm@8020  111  qed;  wenzelm@8020  112  qed;  wenzelm@8020  113  qed;  wenzelm@8020  114 wenzelm@8020  115  show "f n <= n";  wenzelm@8020  116  proof (rule leI);  wenzelm@8020  117  show "~ n < f n";  wenzelm@8020  118  proof;  wenzelm@8020  119  assume "n < f n";  wenzelm@8020  120  hence "Suc n <= f n"; by (rule Suc_leI);  wenzelm@8020  121  hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);  wenzelm@8020  122  also; have "... < f (Suc n)"; by (rule f_ax);  wenzelm@8020  123  finally; have "... < ..."; .; thus False; ..;  wenzelm@8020  124  qed;  wenzelm@8020  125  qed;  wenzelm@8020  126 qed;  wenzelm@8020  127 wenzelm@8020  128 end;