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
wenzelm@8020
     1
wenzelm@10007
     2
header {* An old chestnut *}
wenzelm@8020
     3
haftmann@16417
     4
theory Puzzle imports Main begin
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@12997
    27
    proof (induct k rule: less_induct)
wenzelm@10436
    28
      fix k assume hyp: "!!m. m < k ==> PROP ?P m"
wenzelm@10436
    29
      fix n assume k_def: "k == f n"
wenzelm@10436
    30
      show "n <= k"
wenzelm@10436
    31
      proof (cases n)
wenzelm@10436
    32
        assume "n = 0" thus ?thesis by simp
wenzelm@10007
    33
      next
wenzelm@10436
    34
        fix m assume Suc: "n = Suc m"
wenzelm@10436
    35
        from f_ax have "f (f m) < f (Suc m)" .
wenzelm@10436
    36
        with hyp k_def Suc have "f m <= f (f m)" by simp
wenzelm@10436
    37
        also from f_ax have "... < f (Suc m)" .
wenzelm@10436
    38
        finally have less: "f m < f (Suc m)" .
wenzelm@10436
    39
        with hyp k_def Suc have "m <= f m" by simp
wenzelm@10436
    40
        also note less
wenzelm@10436
    41
        finally have "m < f (Suc m)" .
wenzelm@10436
    42
        hence "n <= f n" by (simp only: Suc)
wenzelm@10436
    43
        thus ?thesis by (simp only: k_def)
wenzelm@10007
    44
      qed
wenzelm@10007
    45
    qed
wenzelm@10007
    46
  qed
wenzelm@8020
    47
wenzelm@8020
    48
  txt {*
wenzelm@8020
    49
    In order to show the other direction, we first establish
wenzelm@8020
    50
    monotonicity of $f$.
wenzelm@10007
    51
  *}
wenzelm@10436
    52
  {
wenzelm@10007
    53
    fix m n
wenzelm@10436
    54
    have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
wenzelm@10007
    55
    proof (induct n)
wenzelm@10436
    56
      assume "m <= 0" hence "m = 0" by simp
wenzelm@10436
    57
      thus "f m <= f 0" by simp
wenzelm@10436
    58
    next
wenzelm@10436
    59
      fix n assume hyp: "PROP ?P n"
wenzelm@10436
    60
      assume "m <= Suc n"
wenzelm@10436
    61
      thus "f m <= f (Suc n)"
wenzelm@10436
    62
      proof (rule le_SucE)
wenzelm@10436
    63
        assume "m <= n"
wenzelm@10436
    64
        with hyp have "f m <= f n" .
wenzelm@10436
    65
        also from ge f_ax have "... < f (Suc n)"
wenzelm@10436
    66
          by (rule le_less_trans)
wenzelm@10436
    67
        finally show ?thesis by simp
wenzelm@10436
    68
      next
wenzelm@10436
    69
        assume "m = Suc n"
wenzelm@10436
    70
        thus ?thesis by simp
wenzelm@10007
    71
      qed
wenzelm@10007
    72
    qed
wenzelm@10436
    73
  } note mono = this
wenzelm@8020
    74
wenzelm@10007
    75
  show "f n <= n"
wenzelm@10436
    76
  proof -
wenzelm@10436
    77
    have "~ n < f n"
wenzelm@10007
    78
    proof
wenzelm@10007
    79
      assume "n < f n"
wenzelm@10436
    80
      hence "Suc n <= f n" by simp
wenzelm@10436
    81
      hence "f (Suc n) <= f (f n)" by (rule mono)
wenzelm@10007
    82
      also have "... < f (Suc n)" by (rule f_ax)
wenzelm@10007
    83
      finally have "... < ..." . thus False ..
wenzelm@10007
    84
    qed
wenzelm@10436
    85
    thus ?thesis by simp
wenzelm@10007
    86
  qed
wenzelm@10007
    87
qed
wenzelm@8020
    88
wenzelm@10007
    89
end