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