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