src/HOL/Isar_examples/Puzzle.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 18191 ef29685acef0
permissions -rw-r--r--
Constant "If" is now local
     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 "(!!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 rule: less_induct)
    28       fix k assume hyp: "!!m. m < k ==> PROP ?P m"
    29       fix n assume k_def: "k == f n"
    30       show "n <= k"
    31       proof (cases n)
    32         assume "n = 0" thus ?thesis by simp
    33       next
    34         fix m assume Suc: "n = Suc m"
    35         from f_ax have "f (f m) < f (Suc m)" .
    36         with hyp k_def Suc have "f m <= f (f m)" by simp
    37         also from f_ax have "... < f (Suc m)" .
    38         finally have less: "f m < f (Suc m)" .
    39         with hyp k_def Suc have "m <= f m" by simp
    40         also note less
    41         finally have "m < f (Suc m)" .
    42         hence "n <= f n" by (simp only: Suc)
    43         thus ?thesis by (simp only: k_def)
    44       qed
    45     qed
    46   qed
    47 
    48   txt {*
    49     In order to show the other direction, we first establish
    50     monotonicity of $f$.
    51   *}
    52   {
    53     fix m n
    54     have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
    55     proof (induct n)
    56       assume "m <= 0" hence "m = 0" by simp
    57       thus "f m <= f 0" by simp
    58     next
    59       fix n assume hyp: "PROP ?P n"
    60       assume "m <= Suc n"
    61       thus "f m <= f (Suc n)"
    62       proof (rule le_SucE)
    63         assume "m <= n"
    64         with hyp have "f m <= f n" .
    65         also from ge f_ax have "... < f (Suc n)"
    66           by (rule le_less_trans)
    67         finally show ?thesis by simp
    68       next
    69         assume "m = Suc n"
    70         thus ?thesis by simp
    71       qed
    72     qed
    73   } note mono = this
    74 
    75   show "f n <= n"
    76   proof -
    77     have "~ n < f n"
    78     proof
    79       assume "n < f n"
    80       hence "Suc n <= f n" by simp
    81       hence "f (Suc n) <= f (f n)" by (rule mono)
    82       also have "... < f (Suc n)" by (rule f_ax)
    83       finally have "... < ..." . thus False ..
    84     qed
    85     thus ?thesis by simp
    86   qed
    87 qed
    88 
    89 end