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