src/HOL/Isar_examples/Puzzle.thy
author wenzelm
Mon Sep 11 21:35:19 2006 +0200 (2006-09-11)
changeset 20503 503ac4c5ef91
parent 18204 c3caf13f621d
child 31758 3edd5f813f01
permissions -rw-r--r--
induct method: renamed 'fixing' to 'arbitrary';
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@18193
     7
  \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original
wenzelm@18193
     8
  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
wenzelm@18193
     9
  Tobias Nipkow.}
wenzelm@18193
    10
*}
wenzelm@8020
    11
wenzelm@18193
    12
text {*
wenzelm@18193
    13
  \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$ such
wenzelm@18193
    14
  that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
wenzelm@18193
    15
  Demonstrate that $f$ is the identity.
wenzelm@10007
    16
*}
wenzelm@8020
    17
wenzelm@18191
    18
theorem
wenzelm@18191
    19
  assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
wenzelm@18191
    20
  shows "f n = n"
wenzelm@10436
    21
proof (rule order_antisym)
wenzelm@18191
    22
  {
wenzelm@18191
    23
    fix n show "n \<le> f n"
wenzelm@20503
    24
    proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)
wenzelm@18191
    25
      case (less k n)
wenzelm@18191
    26
      then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
wenzelm@18191
    27
      show "n \<le> f n"
wenzelm@10436
    28
      proof (cases n)
wenzelm@18191
    29
	case (Suc m)
wenzelm@18191
    30
	from f_ax have "f (f m) < f n" by (simp only: Suc)
wenzelm@18191
    31
	with hyp have "f m \<le> f (f m)" .
wenzelm@18191
    32
	also from f_ax have "\<dots> < f n" by (simp only: Suc)
wenzelm@18191
    33
	finally have "f m < f n" .
wenzelm@18191
    34
	with hyp have "m \<le> f m" .
wenzelm@18191
    35
	also note `\<dots> < f n`
wenzelm@18191
    36
	finally have "m < f n" .
wenzelm@18191
    37
	then have "n \<le> f n" by (simp only: Suc)
wenzelm@18191
    38
	then show ?thesis .
wenzelm@10007
    39
      next
wenzelm@18191
    40
	case 0
wenzelm@18191
    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