src/HOL/Isar_Examples/Puzzle.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 37671 fa53d267dab3 child 58614 7338eb25226c permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
     1 header {* An old chestnut *}

     2

     3 theory Puzzle

     4 imports Main

     5 begin

     6

     7 text_raw {* \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 text {* \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$

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

    13   Demonstrate that $f$ is the identity. *}

    14

    15 theorem

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

    17   shows "f n = n"

    18 proof (rule order_antisym)

    19   {

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

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

    22       case less

    23       show "n \<le> f n"

    24       proof (cases n)

    25         case (Suc m)

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

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

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

    29         finally have "f m < f n" .

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

    31         also note \<dots> < f n

    32         finally have "m < f n" .

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

    34         then show ?thesis .

    35       next

    36         case 0

    37         then show ?thesis by simp

    38       qed

    39     qed

    40   } note ge = this

    41

    42   {

    43     fix m n :: nat

    44     assume "m \<le> n"

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

    46     proof (induct n)

    47       case 0

    48       then have "m = 0" by simp

    49       then show ?case by simp

    50     next

    51       case (Suc n)

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

    53       proof (rule le_SucE)

    54         assume "m \<le> n"

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

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

    57           by (rule le_less_trans)

    58         finally show ?thesis by simp

    59       next

    60         assume "m = Suc n"

    61         then show ?thesis by simp

    62       qed

    63     qed

    64   } note mono = this

    65

    66   show "f n \<le> n"

    67   proof -

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

    69     proof

    70       assume "n < f n"

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

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

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

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

    75     qed

    76     then show ?thesis by simp

    77   qed

    78 qed

    79

    80 end