src/HOL/Isar_examples/Puzzle.thy
 author wenzelm Wed Nov 16 17:49:16 2005 +0100 (2005-11-16) changeset 18191 ef29685acef0 parent 16417 9bc16273c2d4 child 18193 54419506df9e permissions -rw-r--r--
improved induction proof: local defs/fixes;
     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  \medskip \textbf{Problem.}  Given some function $f\colon \Nat \to   12 \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all

    13  $n$.  Demonstrate that $f$ is the identity.

    14 *}

    15

    16 theorem

    17   fixes n :: nat

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

    19   shows "f n = n"

    20 proof (rule order_antisym)

    21   {

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

    23     proof (induct k \<equiv> "f n" rule: less_induct fixing: n)

    24       case (less k n)

    25       then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)

    26       show "n \<le> f n"

    27       proof (cases n)

    28 	case (Suc m)

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

    30 	with hyp have "f m \<le> f (f m)" .

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

    32 	finally have "f m < f n" .

    33 	with hyp have "m \<le> f m" .

    34 	also note \<dots> < f n

    35 	finally have "m < f n" .

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

    37 	then show ?thesis .

    38       next

    39 	case 0

    40 	then show ?thesis by simp

    41       qed

    42     qed

    43   } note ge = this

    44

    45   {

    46     fix m n :: nat

    47     assume "m \<le> n"

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

    49     proof (induct n)

    50       case 0

    51       then have "m = 0" by simp

    52       then show ?case by simp

    53     next

    54       case (Suc n)

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

    56       proof (rule le_SucE)

    57         assume "m \<le> n"

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

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

    60           by (rule le_less_trans)

    61         finally show ?thesis by simp

    62       next

    63         assume "m = Suc n"

    64         then show ?thesis by simp

    65       qed

    66     qed

    67   } note mono = this

    68

    69   show "f n \<le> n"

    70   proof -

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

    72     proof

    73       assume "n < f n"

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

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

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

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

    78     qed

    79     then show ?thesis by simp

    80   qed

    81 qed

    82

    83 end