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