src/HOL/Isar_examples/Puzzle.thy
 author wenzelm Fri Nov 10 19:05:28 2000 +0100 (2000-11-10) changeset 10436 98c421dd5972 parent 10007 64bf7da1994a child 12997 80dec7322a8c permissions -rw-r--r--
simplified induction;
     1

     2 header {* An old chestnut *}

     3

     4 theory Puzzle = Main:

     5

     6 text_raw {*

     7  \footnote{A question from Bundeswettbewerb Mathematik''.  Original

     8  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by

     9  Tobias Nipkow.}

    10

    11  \medskip \textbf{Problem.}  Given some function $f\colon \Nat \to   12 \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all

    13  $n$.  Demonstrate that $f$ is the identity.

    14 *}

    15

    16 theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"

    17 proof (rule order_antisym)

    18   assume f_ax: "!!n. f (f n) < f (Suc n)"

    19

    20   txt {*

    21     Note that the generalized form of $n \le f \ap n$ is required

    22     later for monotonicity as well.

    23   *}

    24   show ge: "!!n. n <= f n"

    25   proof -

    26     fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")

    27     proof (induct k

    28         rule: nat_less_induct [rule_format])

    29       fix k assume hyp: "!!m. m < k ==> PROP ?P m"

    30       fix n assume k_def: "k == f n"

    31       show "n <= k"

    32       proof (cases n)

    33         assume "n = 0" thus ?thesis by simp

    34       next

    35         fix m assume Suc: "n = Suc m"

    36         from f_ax have "f (f m) < f (Suc m)" .

    37         with hyp k_def Suc have "f m <= f (f m)" by simp

    38         also from f_ax have "... < f (Suc m)" .

    39         finally have less: "f m < f (Suc m)" .

    40         with hyp k_def Suc have "m <= f m" by simp

    41         also note less

    42         finally have "m < f (Suc m)" .

    43         hence "n <= f n" by (simp only: Suc)

    44         thus ?thesis by (simp only: k_def)

    45       qed

    46     qed

    47   qed

    48

    49   txt {*

    50     In order to show the other direction, we first establish

    51     monotonicity of $f$.

    52   *}

    53   {

    54     fix m n

    55     have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")

    56     proof (induct n)

    57       assume "m <= 0" hence "m = 0" by simp

    58       thus "f m <= f 0" by simp

    59     next

    60       fix n assume hyp: "PROP ?P n"

    61       assume "m <= Suc n"

    62       thus "f m <= f (Suc n)"

    63       proof (rule le_SucE)

    64         assume "m <= n"

    65         with hyp have "f m <= f n" .

    66         also from ge f_ax have "... < f (Suc n)"

    67           by (rule le_less_trans)

    68         finally show ?thesis by simp

    69       next

    70         assume "m = Suc n"

    71         thus ?thesis by simp

    72       qed

    73     qed

    74   } note mono = this

    75

    76   show "f n <= n"

    77   proof -

    78     have "~ n < f n"

    79     proof

    80       assume "n < f n"

    81       hence "Suc n <= f n" by simp

    82       hence "f (Suc n) <= f (f n)" by (rule mono)

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

    84       finally have "... < ..." . thus False ..

    85     qed

    86     thus ?thesis by simp

    87   qed

    88 qed

    89

    90 end