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