src/HOL/Isar_Examples/Puzzle.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 34915 7894c7dab132 child 37671 fa53d267dab3 permissions -rw-r--r--
more speaking names
     1 header {* An old chestnut *}

     2

     3 theory Puzzle

     4 imports Main

     5 begin

     6

     7 text_raw {*

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

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

    10   Tobias Nipkow.}

    11 *}

    12

    13 text {*

    14   \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$ such

    15   that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.

    16   Demonstrate that $f$ is the identity.

    17 *}

    18

    19 theorem

    20   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"

    21   shows "f n = n"

    22 proof (rule order_antisym)

    23   {

    24     fix n show "n \<le> f n"

    25     proof (induct "f n" arbitrary: n rule: less_induct)

    26       case less

    27       show "n \<le> f n"

    28       proof (cases n)

    29         case (Suc m)

    30         from f_ax have "f (f m) < f n" by (simp only: Suc)

    31         with less have "f m \<le> f (f m)" .

    32         also from f_ax have "\<dots> < f n" by (simp only: Suc)

    33         finally have "f m < f n" .

    34         with less have "m \<le> f m" .

    35         also note \<dots> < f n

    36         finally have "m < f n" .

    37         then have "n \<le> f n" by (simp only: Suc)

    38         then show ?thesis .

    39       next

    40         case 0

    41         then show ?thesis by simp

    42       qed

    43     qed

    44   } note ge = this

    45

    46   {

    47     fix m n :: nat

    48     assume "m \<le> n"

    49     then have "f m \<le> f n"

    50     proof (induct n)

    51       case 0

    52       then have "m = 0" by simp

    53       then show ?case by simp

    54     next

    55       case (Suc n)

    56       from Suc.prems show "f m \<le> f (Suc n)"

    57       proof (rule le_SucE)

    58         assume "m \<le> n"

    59         with Suc.hyps have "f m \<le> f n" .

    60         also from ge f_ax have "\<dots> < f (Suc n)"

    61           by (rule le_less_trans)

    62         finally show ?thesis by simp

    63       next

    64         assume "m = Suc n"

    65         then show ?thesis by simp

    66       qed

    67     qed

    68   } note mono = this

    69

    70   show "f n \<le> n"

    71   proof -

    72     have "\<not> n < f n"

    73     proof

    74       assume "n < f n"

    75       then have "Suc n \<le> f n" by simp

    76       then have "f (Suc n) \<le> f (f n)" by (rule mono)

    77       also have "\<dots> < f (Suc n)" by (rule f_ax)

    78       finally have "\<dots> < \<dots>" . then show False ..

    79     qed

    80     then show ?thesis by simp

    81   qed

    82 qed

    83

    84 end