src/HOL/Isar_examples/Puzzle.thy
author wenzelm
Sun Sep 17 22:19:02 2000 +0200 (2000-09-17)
changeset 10007 64bf7da1994a
parent 9941 fe05af7ec816
child 10436 98c421dd5972
permissions -rw-r--r--
isar-strip-terminators;
wenzelm@8020
     1
wenzelm@10007
     2
header {* An old chestnut *}
wenzelm@8020
     3
wenzelm@10007
     4
theory Puzzle = Main:
wenzelm@8020
     5
wenzelm@8020
     6
text_raw {*
wenzelm@8020
     7
 \footnote{A question from ``Bundeswettbewerb Mathematik''.
wenzelm@8020
     8
 Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
wenzelm@8020
     9
 script by Tobias Nipkow.}
wenzelm@10007
    10
*}
wenzelm@8020
    11
wenzelm@8020
    12
wenzelm@10007
    13
subsection {* Generalized mathematical induction *}
wenzelm@8020
    14
wenzelm@8020
    15
text {*
wenzelm@8020
    16
 The following derived rule admits induction over some expression
wenzelm@8020
    17
 $f(x)$ wrt.\ the ${<}$ relation on natural numbers.
wenzelm@10007
    18
*}
wenzelm@8020
    19
wenzelm@8020
    20
lemma gen_less_induct:
wenzelm@8020
    21
  "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))
wenzelm@8020
    22
    ==> P x (f x :: nat)"
wenzelm@10007
    23
  (is "(!!x. ?H x ==> ?C x) ==> _")
wenzelm@10007
    24
proof -
wenzelm@10007
    25
  assume asm: "!!x. ?H x ==> ?C x"
wenzelm@10007
    26
  {
wenzelm@10007
    27
    fix k
wenzelm@10007
    28
    have "ALL x. k = f x --> ?C x" (is "?Q k")
wenzelm@10007
    29
    proof (rule nat_less_induct)
wenzelm@10007
    30
      fix k assume hyp: "ALL m<k. ?Q m"
wenzelm@10007
    31
      show "?Q k"
wenzelm@10007
    32
      proof
wenzelm@10007
    33
	fix x show "k = f x --> ?C x"
wenzelm@10007
    34
	proof
wenzelm@10007
    35
	  assume "k = f x"
wenzelm@10007
    36
	  with hyp have "?H x" by blast
wenzelm@10007
    37
	  thus "?C x" by (rule asm)
wenzelm@10007
    38
	qed
wenzelm@10007
    39
      qed
wenzelm@10007
    40
    qed
wenzelm@10007
    41
  }
wenzelm@10007
    42
  thus "?C x" by simp
wenzelm@10007
    43
qed
wenzelm@8020
    44
wenzelm@8020
    45
wenzelm@10007
    46
subsection {* The problem *}
wenzelm@8020
    47
wenzelm@8020
    48
text {*
wenzelm@8020
    49
 Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap
wenzelm@8020
    50
 n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  Demonstrate that $f$ is
wenzelm@8020
    51
 the identity.
wenzelm@10007
    52
*}
wenzelm@8020
    53
wenzelm@10007
    54
consts f :: "nat => nat"
wenzelm@10007
    55
axioms f_ax: "f (f n) < f (Suc n)"
wenzelm@8020
    56
wenzelm@10007
    57
theorem "f n = n"
wenzelm@10007
    58
proof (rule order_antisym)
wenzelm@8020
    59
  txt {*
wenzelm@8020
    60
    Note that the generalized form of $n \le f \ap n$ is required
wenzelm@8020
    61
    later for monotonicity as well.
wenzelm@10007
    62
  *}
wenzelm@10007
    63
  show ge: "!!n. n <= f n"
wenzelm@10007
    64
  proof -
wenzelm@10007
    65
    fix n
wenzelm@10007
    66
    show "?thesis n" (is "?P n (f n)")
wenzelm@10007
    67
    proof (rule gen_less_induct [of f ?P])
wenzelm@10007
    68
      fix n assume hyp: "ALL m. f m < f n --> ?P m (f m)"
wenzelm@10007
    69
      show "?P n (f n)"
wenzelm@10007
    70
      proof (rule nat.exhaust)
wenzelm@10007
    71
	assume "n = 0" thus ?thesis by simp
wenzelm@10007
    72
      next
wenzelm@10007
    73
	fix m assume n_Suc: "n = Suc m"
wenzelm@10007
    74
	from f_ax have "f (f m) < f (Suc m)" .
wenzelm@10007
    75
	with hyp n_Suc have "f m <= f (f m)" by blast
wenzelm@10007
    76
	also from f_ax have "... < f (Suc m)" .
wenzelm@10007
    77
	finally have lt: "f m < f (Suc m)" .
wenzelm@10007
    78
	with hyp n_Suc have "m <= f m" by blast
wenzelm@10007
    79
	also note lt
wenzelm@10007
    80
	finally have "m < f (Suc m)" .
wenzelm@10007
    81
	thus "n <= f n" by (simp only: n_Suc)
wenzelm@10007
    82
      qed
wenzelm@10007
    83
    qed
wenzelm@10007
    84
  qed
wenzelm@8020
    85
wenzelm@8020
    86
  txt {*
wenzelm@8020
    87
    In order to show the other direction, we first establish
wenzelm@8020
    88
    monotonicity of $f$.
wenzelm@10007
    89
  *}
wenzelm@10007
    90
  have mono: "!!m n. m <= n --> f m <= f n"
wenzelm@10007
    91
  proof -
wenzelm@10007
    92
    fix m n
wenzelm@10007
    93
    show "?thesis m n" (is "?P n")
wenzelm@10007
    94
    proof (induct n)
wenzelm@10007
    95
      show "?P 0" by simp
wenzelm@10007
    96
      fix n assume hyp: "?P n"
wenzelm@10007
    97
      show "?P (Suc n)"
wenzelm@10007
    98
      proof
wenzelm@10007
    99
	assume "m <= Suc n"
wenzelm@10007
   100
	thus "f m <= f (Suc n)"
wenzelm@10007
   101
	proof (rule le_SucE)
wenzelm@10007
   102
	  assume "m <= n"
wenzelm@10007
   103
	  with hyp have "f m <= f n" ..
wenzelm@10007
   104
	  also from ge f_ax have "... < f (Suc n)"
wenzelm@10007
   105
	    by (rule le_less_trans)
wenzelm@10007
   106
	  finally show ?thesis by simp
wenzelm@10007
   107
	next
wenzelm@10007
   108
	  assume "m = Suc n"
wenzelm@10007
   109
	  thus ?thesis by simp
wenzelm@10007
   110
	qed
wenzelm@10007
   111
      qed
wenzelm@10007
   112
    qed
wenzelm@10007
   113
  qed
wenzelm@8020
   114
wenzelm@10007
   115
  show "f n <= n"
wenzelm@10007
   116
  proof (rule leI)
wenzelm@10007
   117
    show "~ n < f n"
wenzelm@10007
   118
    proof
wenzelm@10007
   119
      assume "n < f n"
wenzelm@10007
   120
      hence "Suc n <= f n" by (rule Suc_leI)
wenzelm@10007
   121
      hence "f (Suc n) <= f (f n)" by (rule mono [rule_format])
wenzelm@10007
   122
      also have "... < f (Suc n)" by (rule f_ax)
wenzelm@10007
   123
      finally have "... < ..." . thus False ..
wenzelm@10007
   124
    qed
wenzelm@10007
   125
  qed
wenzelm@10007
   126
qed
wenzelm@8020
   127
wenzelm@10007
   128
end