src/HOL/Isar_examples/Puzzle.thy
author kleing
Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840 399c8103a98f
parent 12997 80dec7322a8c
child 16417 9bc16273c2d4
permissions -rw-r--r--
keep a copy of generated files in repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
     1
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
     2
header {* An old chestnut *}
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
     3
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
     4
theory Puzzle = Main:
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
     5
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
     6
text_raw {*
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
     7
 \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
     8
 pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
     9
 Tobias Nipkow.}
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    10
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    11
 \medskip \textbf{Problem.}  Given some function $f\colon \Nat \to
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    12
 \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    13
 $n$.  Demonstrate that $f$ is the identity.
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    14
*}
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    15
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    16
theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    17
proof (rule order_antisym)
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    18
  assume f_ax: "!!n. f (f n) < f (Suc n)"
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    19
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    20
  txt {*
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    21
    Note that the generalized form of $n \le f \ap n$ is required
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    22
    later for monotonicity as well.
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    23
  *}
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    24
  show ge: "!!n. n <= f n"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    25
  proof -
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    26
    fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
12997
wenzelm
parents: 10436
diff changeset
    27
    proof (induct k rule: less_induct)
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    28
      fix k assume hyp: "!!m. m < k ==> PROP ?P m"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    29
      fix n assume k_def: "k == f n"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    30
      show "n <= k"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    31
      proof (cases n)
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    32
        assume "n = 0" thus ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    33
      next
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    34
        fix m assume Suc: "n = Suc m"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    35
        from f_ax have "f (f m) < f (Suc m)" .
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    36
        with hyp k_def Suc have "f m <= f (f m)" by simp
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    37
        also from f_ax have "... < f (Suc m)" .
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    38
        finally have less: "f m < f (Suc m)" .
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    39
        with hyp k_def Suc have "m <= f m" by simp
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    40
        also note less
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    41
        finally have "m < f (Suc m)" .
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    42
        hence "n <= f n" by (simp only: Suc)
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    43
        thus ?thesis by (simp only: k_def)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    44
      qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    45
    qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    46
  qed
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    47
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    48
  txt {*
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    49
    In order to show the other direction, we first establish
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    50
    monotonicity of $f$.
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    51
  *}
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    52
  {
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    53
    fix m n
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    54
    have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    55
    proof (induct n)
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    56
      assume "m <= 0" hence "m = 0" by simp
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    57
      thus "f m <= f 0" by simp
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    58
    next
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    59
      fix n assume hyp: "PROP ?P n"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    60
      assume "m <= Suc n"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    61
      thus "f m <= f (Suc n)"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    62
      proof (rule le_SucE)
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    63
        assume "m <= n"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    64
        with hyp have "f m <= f n" .
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    65
        also from ge f_ax have "... < f (Suc n)"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    66
          by (rule le_less_trans)
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    67
        finally show ?thesis by simp
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    68
      next
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    69
        assume "m = Suc n"
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    70
        thus ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    71
      qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    72
    qed
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    73
  } note mono = this
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    74
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    75
  show "f n <= n"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    76
  proof -
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    77
    have "~ n < f n"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    78
    proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    79
      assume "n < f n"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    80
      hence "Suc n <= f n" by simp
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    81
      hence "f (Suc n) <= f (f n)" by (rule mono)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    82
      also have "... < f (Suc n)" by (rule f_ax)
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    83
      finally have "... < ..." . thus False ..
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    84
    qed
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    85
    thus ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    86
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    87
qed
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    88
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    89
end