src/HOL/Isar_examples/Puzzle.thy
author wenzelm
Wed Nov 16 19:34:19 2005 +0100 (2005-11-16)
changeset 18193 54419506df9e
parent 18191 ef29685acef0
child 18204 c3caf13f621d
permissions -rw-r--r--
tuned document;
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
  fixes n :: nat
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"
wenzelm@18191
    25
    proof (induct k \<equiv> "f n" rule: less_induct fixing: n)
wenzelm@18191
    26
      case (less k n)
wenzelm@18191
    27
      then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
wenzelm@18191
    28
      show "n \<le> f n"
wenzelm@10436
    29
      proof (cases n)
wenzelm@18191
    30
	case (Suc m)
wenzelm@18191
    31
	from f_ax have "f (f m) < f n" by (simp only: Suc)
wenzelm@18191
    32
	with hyp have "f m \<le> f (f m)" .
wenzelm@18191
    33
	also from f_ax have "\<dots> < f n" by (simp only: Suc)
wenzelm@18191
    34
	finally have "f m < f n" .
wenzelm@18191
    35
	with hyp have "m \<le> f m" .
wenzelm@18191
    36
	also note `\<dots> < f n`
wenzelm@18191
    37
	finally have "m < f n" .
wenzelm@18191
    38
	then have "n \<le> f n" by (simp only: Suc)
wenzelm@18191
    39
	then show ?thesis .
wenzelm@10007
    40
      next
wenzelm@18191
    41
	case 0
wenzelm@18191
    42
	then show ?thesis by simp
wenzelm@10007
    43
      qed
wenzelm@10007
    44
    qed
wenzelm@18191
    45
  } note ge = this
wenzelm@8020
    46
wenzelm@10436
    47
  {
wenzelm@18191
    48
    fix m n :: nat
wenzelm@18191
    49
    assume "m \<le> n"
wenzelm@18191
    50
    then have "f m \<le> f n"
wenzelm@10007
    51
    proof (induct n)
wenzelm@18191
    52
      case 0
wenzelm@18191
    53
      then have "m = 0" by simp
wenzelm@18191
    54
      then show ?case by simp
wenzelm@10436
    55
    next
wenzelm@18191
    56
      case (Suc n)
wenzelm@18191
    57
      from Suc.prems show "f m \<le> f (Suc n)"
wenzelm@10436
    58
      proof (rule le_SucE)
wenzelm@18191
    59
        assume "m \<le> n"
wenzelm@18191
    60
        with Suc.hyps have "f m \<le> f n" .
wenzelm@18191
    61
        also from ge f_ax have "\<dots> < f (Suc n)"
wenzelm@10436
    62
          by (rule le_less_trans)
wenzelm@10436
    63
        finally show ?thesis by simp
wenzelm@10436
    64
      next
wenzelm@10436
    65
        assume "m = Suc n"
wenzelm@18191
    66
        then show ?thesis by simp
wenzelm@10007
    67
      qed
wenzelm@10007
    68
    qed
wenzelm@10436
    69
  } note mono = this
wenzelm@8020
    70
wenzelm@18191
    71
  show "f n \<le> n"
wenzelm@10436
    72
  proof -
wenzelm@18191
    73
    have "\<not> n < f n"
wenzelm@10007
    74
    proof
wenzelm@10007
    75
      assume "n < f n"
wenzelm@18191
    76
      then have "Suc n \<le> f n" by simp
wenzelm@18191
    77
      then have "f (Suc n) \<le> f (f n)" by (rule mono)
wenzelm@18191
    78
      also have "\<dots> < f (Suc n)" by (rule f_ax)
wenzelm@18191
    79
      finally have "\<dots> < \<dots>" . then show False ..
wenzelm@10007
    80
    qed
wenzelm@18191
    81
    then show ?thesis by simp
wenzelm@10007
    82
  qed
wenzelm@10007
    83
qed
wenzelm@8020
    84
wenzelm@10007
    85
end