src/HOL/Isar_examples/Puzzle.thy
author wenzelm
Wed Nov 16 19:34:19 2005 +0100 (2005-11-16)
changeset 18193 54419506df9e
parent 18191 ef29685acef0
child 18204 c3caf13f621d
permissions -rw-r--r--
tuned document;
     1 
     2 header {* An old chestnut *}
     3 
     4 theory Puzzle imports Main begin
     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 
    12 text {*
    13   \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$ such
    14   that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
    15   Demonstrate that $f$ is the identity.
    16 *}
    17 
    18 theorem
    19   fixes n :: nat
    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 k \<equiv> "f n" rule: less_induct fixing: n)
    26       case (less k n)
    27       then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
    28       show "n \<le> f n"
    29       proof (cases n)
    30 	case (Suc m)
    31 	from f_ax have "f (f m) < f n" by (simp only: Suc)
    32 	with hyp have "f m \<le> f (f m)" .
    33 	also from f_ax have "\<dots> < f n" by (simp only: Suc)
    34 	finally have "f m < f n" .
    35 	with hyp have "m \<le> f m" .
    36 	also note `\<dots> < f n`
    37 	finally have "m < f n" .
    38 	then have "n \<le> f n" by (simp only: Suc)
    39 	then show ?thesis .
    40       next
    41 	case 0
    42 	then show ?thesis by simp
    43       qed
    44     qed
    45   } note ge = this
    46 
    47   {
    48     fix m n :: nat
    49     assume "m \<le> n"
    50     then have "f m \<le> f n"
    51     proof (induct n)
    52       case 0
    53       then have "m = 0" by simp
    54       then show ?case by simp
    55     next
    56       case (Suc n)
    57       from Suc.prems show "f m \<le> f (Suc n)"
    58       proof (rule le_SucE)
    59         assume "m \<le> n"
    60         with Suc.hyps have "f m \<le> f n" .
    61         also from ge f_ax have "\<dots> < f (Suc n)"
    62           by (rule le_less_trans)
    63         finally show ?thesis by simp
    64       next
    65         assume "m = Suc n"
    66         then show ?thesis by simp
    67       qed
    68     qed
    69   } note mono = this
    70 
    71   show "f n \<le> n"
    72   proof -
    73     have "\<not> n < f n"
    74     proof
    75       assume "n < f n"
    76       then have "Suc n \<le> f n" by simp
    77       then have "f (Suc n) \<le> f (f n)" by (rule mono)
    78       also have "\<dots> < f (Suc n)" by (rule f_ax)
    79       finally have "\<dots> < \<dots>" . then show False ..
    80     qed
    81     then show ?thesis by simp
    82   qed
    83 qed
    84 
    85 end