src/HOL/Isar_examples/Puzzle.thy
 author wenzelm Thu Sep 07 21:10:11 2000 +0200 (2000-09-07) changeset 9906 5c027cca6262 parent 9870 2374ba026fc6 child 9941 fe05af7ec816 permissions -rw-r--r--
updated attribute names;
     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 nat_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 [rulified]);

   122       also; have "... < f (Suc n)"; by (rule f_ax);

   123       finally; have "... < ..."; .; thus False; ..;

   124     qed;

   125   qed;

   126 qed;

   127

   128 end;