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