src/HOL/Isar_Examples/Puzzle.thy
author haftmann
Wed Jun 30 16:46:44 2010 +0200 (2010-06-30)
changeset 37659 14cabf5fa710
parent 34915 7894c7dab132
child 37671 fa53d267dab3
permissions -rw-r--r--
more speaking names
wenzelm@10007
     1
header {* An old chestnut *}
wenzelm@8020
     2
wenzelm@31758
     3
theory Puzzle
wenzelm@31758
     4
imports Main
wenzelm@31758
     5
begin
wenzelm@8020
     6
wenzelm@8020
     7
text_raw {*
wenzelm@18193
     8
  \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original
wenzelm@18193
     9
  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
wenzelm@18193
    10
  Tobias Nipkow.}
wenzelm@18193
    11
*}
wenzelm@8020
    12
wenzelm@18193
    13
text {*
wenzelm@18193
    14
  \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$ such
wenzelm@18193
    15
  that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
wenzelm@18193
    16
  Demonstrate that $f$ is the identity.
wenzelm@10007
    17
*}
wenzelm@8020
    18
wenzelm@18191
    19
theorem
wenzelm@18191
    20
  assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
wenzelm@18191
    21
  shows "f n = n"
wenzelm@10436
    22
proof (rule order_antisym)
wenzelm@18191
    23
  {
wenzelm@18191
    24
    fix n show "n \<le> f n"
berghofe@34915
    25
    proof (induct "f n" arbitrary: n rule: less_induct)
berghofe@34915
    26
      case less
wenzelm@18191
    27
      show "n \<le> f n"
wenzelm@10436
    28
      proof (cases n)
wenzelm@32960
    29
        case (Suc m)
wenzelm@32960
    30
        from f_ax have "f (f m) < f n" by (simp only: Suc)
berghofe@34915
    31
        with less have "f m \<le> f (f m)" .
wenzelm@32960
    32
        also from f_ax have "\<dots> < f n" by (simp only: Suc)
wenzelm@32960
    33
        finally have "f m < f n" .
berghofe@34915
    34
        with less have "m \<le> f m" .
wenzelm@32960
    35
        also note `\<dots> < f n`
wenzelm@32960
    36
        finally have "m < f n" .
wenzelm@32960
    37
        then have "n \<le> f n" by (simp only: Suc)
wenzelm@32960
    38
        then show ?thesis .
wenzelm@10007
    39
      next
wenzelm@32960
    40
        case 0
wenzelm@32960
    41
        then show ?thesis by simp
wenzelm@10007
    42
      qed
wenzelm@10007
    43
    qed
wenzelm@18191
    44
  } note ge = this
wenzelm@8020
    45
wenzelm@10436
    46
  {
wenzelm@18191
    47
    fix m n :: nat
wenzelm@18191
    48
    assume "m \<le> n"
wenzelm@18191
    49
    then have "f m \<le> f n"
wenzelm@10007
    50
    proof (induct n)
wenzelm@18191
    51
      case 0
wenzelm@18191
    52
      then have "m = 0" by simp
wenzelm@18191
    53
      then show ?case by simp
wenzelm@10436
    54
    next
wenzelm@18191
    55
      case (Suc n)
wenzelm@18191
    56
      from Suc.prems show "f m \<le> f (Suc n)"
wenzelm@10436
    57
      proof (rule le_SucE)
wenzelm@18191
    58
        assume "m \<le> n"
wenzelm@18191
    59
        with Suc.hyps have "f m \<le> f n" .
wenzelm@18191
    60
        also from ge f_ax have "\<dots> < f (Suc n)"
wenzelm@10436
    61
          by (rule le_less_trans)
wenzelm@10436
    62
        finally show ?thesis by simp
wenzelm@10436
    63
      next
wenzelm@10436
    64
        assume "m = Suc n"
wenzelm@18191
    65
        then show ?thesis by simp
wenzelm@10007
    66
      qed
wenzelm@10007
    67
    qed
wenzelm@10436
    68
  } note mono = this
wenzelm@8020
    69
wenzelm@18191
    70
  show "f n \<le> n"
wenzelm@10436
    71
  proof -
wenzelm@18191
    72
    have "\<not> n < f n"
wenzelm@10007
    73
    proof
wenzelm@10007
    74
      assume "n < f n"
wenzelm@18191
    75
      then have "Suc n \<le> f n" by simp
wenzelm@18191
    76
      then have "f (Suc n) \<le> f (f n)" by (rule mono)
wenzelm@18191
    77
      also have "\<dots> < f (Suc n)" by (rule f_ax)
wenzelm@18191
    78
      finally have "\<dots> < \<dots>" . then show False ..
wenzelm@10007
    79
    qed
wenzelm@18191
    80
    then show ?thesis by simp
wenzelm@10007
    81
  qed
wenzelm@10007
    82
qed
wenzelm@8020
    83
wenzelm@10007
    84
end