src/HOL/Isar_Examples/Puzzle.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63583 a39baba12732
permissions -rw-r--r--
tuned;
wenzelm@58882
     1
section \<open>An old chestnut\<close>
wenzelm@8020
     2
wenzelm@31758
     3
theory Puzzle
wenzelm@63583
     4
  imports Main
wenzelm@31758
     5
begin
wenzelm@8020
     6
wenzelm@61932
     7
text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original
wenzelm@61932
     8
  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias
wenzelm@61932
     9
  Nipkow.\<close>\<close>
wenzelm@8020
    10
wenzelm@61932
    11
text \<open>
wenzelm@61932
    12
  \<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that \<open>f (f n) < f (Suc n)\<close>
wenzelm@61932
    13
  for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.
wenzelm@61932
    14
\<close>
wenzelm@8020
    15
wenzelm@18191
    16
theorem
wenzelm@18191
    17
  assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
wenzelm@18191
    18
  shows "f n = n"
wenzelm@10436
    19
proof (rule order_antisym)
wenzelm@60410
    20
  show ge: "n \<le> f n" for n
wenzelm@60410
    21
  proof (induct "f n" arbitrary: n rule: less_induct)
wenzelm@60410
    22
    case less
wenzelm@60410
    23
    show "n \<le> f n"
wenzelm@60410
    24
    proof (cases n)
wenzelm@60410
    25
      case (Suc m)
wenzelm@60410
    26
      from f_ax have "f (f m) < f n" by (simp only: Suc)
wenzelm@60410
    27
      with less have "f m \<le> f (f m)" .
wenzelm@60410
    28
      also from f_ax have "\<dots> < f n" by (simp only: Suc)
wenzelm@60410
    29
      finally have "f m < f n" .
wenzelm@60410
    30
      with less have "m \<le> f m" .
wenzelm@60410
    31
      also note \<open>\<dots> < f n\<close>
wenzelm@60410
    32
      finally have "m < f n" .
wenzelm@60410
    33
      then have "n \<le> f n" by (simp only: Suc)
wenzelm@60410
    34
      then show ?thesis .
wenzelm@60410
    35
    next
wenzelm@60410
    36
      case 0
wenzelm@60410
    37
      then show ?thesis by simp
wenzelm@10007
    38
    qed
wenzelm@60410
    39
  qed
wenzelm@8020
    40
wenzelm@60410
    41
  have mono: "m \<le> n \<Longrightarrow> f m \<le> f n" for m n :: nat
wenzelm@60410
    42
  proof (induct n)
wenzelm@60410
    43
    case 0
wenzelm@60410
    44
    then have "m = 0" by simp
wenzelm@60410
    45
    then show ?case by simp
wenzelm@60410
    46
  next
wenzelm@60410
    47
    case (Suc n)
wenzelm@60410
    48
    from Suc.prems show "f m \<le> f (Suc n)"
wenzelm@60410
    49
    proof (rule le_SucE)
wenzelm@60410
    50
      assume "m \<le> n"
wenzelm@60410
    51
      with Suc.hyps have "f m \<le> f n" .
wenzelm@60410
    52
      also from ge f_ax have "\<dots> < f (Suc n)"
wenzelm@60410
    53
        by (rule le_less_trans)
wenzelm@60410
    54
      finally show ?thesis by simp
wenzelm@10436
    55
    next
wenzelm@60410
    56
      assume "m = Suc n"
wenzelm@60410
    57
      then show ?thesis by simp
wenzelm@10007
    58
    qed
wenzelm@60410
    59
  qed
wenzelm@8020
    60
wenzelm@18191
    61
  show "f n \<le> n"
wenzelm@10436
    62
  proof -
wenzelm@18191
    63
    have "\<not> n < f n"
wenzelm@10007
    64
    proof
wenzelm@10007
    65
      assume "n < f n"
wenzelm@18191
    66
      then have "Suc n \<le> f n" by simp
wenzelm@18191
    67
      then have "f (Suc n) \<le> f (f n)" by (rule mono)
wenzelm@18191
    68
      also have "\<dots> < f (Suc n)" by (rule f_ax)
wenzelm@18191
    69
      finally have "\<dots> < \<dots>" . then show False ..
wenzelm@10007
    70
    qed
wenzelm@18191
    71
    then show ?thesis by simp
wenzelm@10007
    72
  qed
wenzelm@10007
    73
qed
wenzelm@8020
    74
wenzelm@10007
    75
end