src/HOL/Isar_examples/Puzzle.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10436 98c421dd5972
child 12997 80dec7322a8c
permissions -rw-r--r--
improved theory reference in comment
wenzelm@8020
     1
wenzelm@10007
     2
header {* An old chestnut *}
wenzelm@8020
     3
wenzelm@10007
     4
theory Puzzle = Main:
wenzelm@8020
     5
wenzelm@8020
     6
text_raw {*
wenzelm@10436
     7
 \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original
wenzelm@10436
     8
 pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
wenzelm@10436
     9
 Tobias Nipkow.}
wenzelm@8020
    10
wenzelm@10436
    11
 \medskip \textbf{Problem.}  Given some function $f\colon \Nat \to
wenzelm@10436
    12
 \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all
wenzelm@10436
    13
 $n$.  Demonstrate that $f$ is the identity.
wenzelm@10007
    14
*}
wenzelm@8020
    15
wenzelm@10436
    16
theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"
wenzelm@10436
    17
proof (rule order_antisym)
wenzelm@10436
    18
  assume f_ax: "!!n. f (f n) < f (Suc n)"
wenzelm@8020
    19
wenzelm@8020
    20
  txt {*
wenzelm@8020
    21
    Note that the generalized form of $n \le f \ap n$ is required
wenzelm@8020
    22
    later for monotonicity as well.
wenzelm@10007
    23
  *}
wenzelm@10007
    24
  show ge: "!!n. n <= f n"
wenzelm@10007
    25
  proof -
wenzelm@10436
    26
    fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
wenzelm@10436
    27
    proof (induct k
wenzelm@10436
    28
        rule: nat_less_induct [rule_format])
wenzelm@10436
    29
      fix k assume hyp: "!!m. m < k ==> PROP ?P m"
wenzelm@10436
    30
      fix n assume k_def: "k == f n"
wenzelm@10436
    31
      show "n <= k"
wenzelm@10436
    32
      proof (cases n)
wenzelm@10436
    33
        assume "n = 0" thus ?thesis by simp
wenzelm@10007
    34
      next
wenzelm@10436
    35
        fix m assume Suc: "n = Suc m"
wenzelm@10436
    36
        from f_ax have "f (f m) < f (Suc m)" .
wenzelm@10436
    37
        with hyp k_def Suc have "f m <= f (f m)" by simp
wenzelm@10436
    38
        also from f_ax have "... < f (Suc m)" .
wenzelm@10436
    39
        finally have less: "f m < f (Suc m)" .
wenzelm@10436
    40
        with hyp k_def Suc have "m <= f m" by simp
wenzelm@10436
    41
        also note less
wenzelm@10436
    42
        finally have "m < f (Suc m)" .
wenzelm@10436
    43
        hence "n <= f n" by (simp only: Suc)
wenzelm@10436
    44
        thus ?thesis by (simp only: k_def)
wenzelm@10007
    45
      qed
wenzelm@10007
    46
    qed
wenzelm@10007
    47
  qed
wenzelm@8020
    48
wenzelm@8020
    49
  txt {*
wenzelm@8020
    50
    In order to show the other direction, we first establish
wenzelm@8020
    51
    monotonicity of $f$.
wenzelm@10007
    52
  *}
wenzelm@10436
    53
  {
wenzelm@10007
    54
    fix m n
wenzelm@10436
    55
    have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
wenzelm@10007
    56
    proof (induct n)
wenzelm@10436
    57
      assume "m <= 0" hence "m = 0" by simp
wenzelm@10436
    58
      thus "f m <= f 0" by simp
wenzelm@10436
    59
    next
wenzelm@10436
    60
      fix n assume hyp: "PROP ?P n"
wenzelm@10436
    61
      assume "m <= Suc n"
wenzelm@10436
    62
      thus "f m <= f (Suc n)"
wenzelm@10436
    63
      proof (rule le_SucE)
wenzelm@10436
    64
        assume "m <= n"
wenzelm@10436
    65
        with hyp have "f m <= f n" .
wenzelm@10436
    66
        also from ge f_ax have "... < f (Suc n)"
wenzelm@10436
    67
          by (rule le_less_trans)
wenzelm@10436
    68
        finally show ?thesis by simp
wenzelm@10436
    69
      next
wenzelm@10436
    70
        assume "m = Suc n"
wenzelm@10436
    71
        thus ?thesis by simp
wenzelm@10007
    72
      qed
wenzelm@10007
    73
    qed
wenzelm@10436
    74
  } note mono = this
wenzelm@8020
    75
wenzelm@10007
    76
  show "f n <= n"
wenzelm@10436
    77
  proof -
wenzelm@10436
    78
    have "~ n < f n"
wenzelm@10007
    79
    proof
wenzelm@10007
    80
      assume "n < f n"
wenzelm@10436
    81
      hence "Suc n <= f n" by simp
wenzelm@10436
    82
      hence "f (Suc n) <= f (f n)" by (rule mono)
wenzelm@10007
    83
      also have "... < f (Suc n)" by (rule f_ax)
wenzelm@10007
    84
      finally have "... < ..." . thus False ..
wenzelm@10007
    85
    qed
wenzelm@10436
    86
    thus ?thesis by simp
wenzelm@10007
    87
  qed
wenzelm@10007
    88
qed
wenzelm@8020
    89
wenzelm@10007
    90
end