src/HOL/Isar_examples/Puzzle.thy
author wenzelm
Fri Nov 10 19:05:28 2000 +0100 (2000-11-10)
changeset 10436 98c421dd5972
parent 10007 64bf7da1994a
child 12997 80dec7322a8c
permissions -rw-r--r--
simplified induction;
     1 
     2 header {* An old chestnut *}
     3 
     4 theory Puzzle = Main:
     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 "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"
    17 proof (rule order_antisym)
    18   assume f_ax: "!!n. f (f n) < f (Suc n)"
    19 
    20   txt {*
    21     Note that the generalized form of $n \le f \ap n$ is required
    22     later for monotonicity as well.
    23   *}
    24   show ge: "!!n. n <= f n"
    25   proof -
    26     fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
    27     proof (induct k
    28         rule: nat_less_induct [rule_format])
    29       fix k assume hyp: "!!m. m < k ==> PROP ?P m"
    30       fix n assume k_def: "k == f n"
    31       show "n <= k"
    32       proof (cases n)
    33         assume "n = 0" thus ?thesis by simp
    34       next
    35         fix m assume Suc: "n = Suc m"
    36         from f_ax have "f (f m) < f (Suc m)" .
    37         with hyp k_def Suc have "f m <= f (f m)" by simp
    38         also from f_ax have "... < f (Suc m)" .
    39         finally have less: "f m < f (Suc m)" .
    40         with hyp k_def Suc have "m <= f m" by simp
    41         also note less
    42         finally have "m < f (Suc m)" .
    43         hence "n <= f n" by (simp only: Suc)
    44         thus ?thesis by (simp only: k_def)
    45       qed
    46     qed
    47   qed
    48 
    49   txt {*
    50     In order to show the other direction, we first establish
    51     monotonicity of $f$.
    52   *}
    53   {
    54     fix m n
    55     have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
    56     proof (induct n)
    57       assume "m <= 0" hence "m = 0" by simp
    58       thus "f m <= f 0" by simp
    59     next
    60       fix n assume hyp: "PROP ?P n"
    61       assume "m <= Suc n"
    62       thus "f m <= f (Suc n)"
    63       proof (rule le_SucE)
    64         assume "m <= n"
    65         with hyp have "f m <= f n" .
    66         also from ge f_ax have "... < f (Suc n)"
    67           by (rule le_less_trans)
    68         finally show ?thesis by simp
    69       next
    70         assume "m = Suc n"
    71         thus ?thesis by simp
    72       qed
    73     qed
    74   } note mono = this
    75 
    76   show "f n <= n"
    77   proof -
    78     have "~ n < f n"
    79     proof
    80       assume "n < f n"
    81       hence "Suc n <= f n" by simp
    82       hence "f (Suc n) <= f (f n)" by (rule mono)
    83       also have "... < f (Suc n)" by (rule f_ax)
    84       finally have "... < ..." . thus False ..
    85     qed
    86     thus ?thesis by simp
    87   qed
    88 qed
    89 
    90 end