src/HOL/Isar_examples/Puzzle.thy
 author wenzelm Sun Sep 17 22:19:02 2000 +0200 (2000-09-17) changeset 10007 64bf7da1994a parent 9941 fe05af7ec816 child 10436 98c421dd5972 permissions -rw-r--r--
isar-strip-terminators;
     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 [rule_format])

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

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

   124     qed

   125   qed

   126 qed

   127

   128 end