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