src/HOL/Isar_Examples/Puzzle.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 37671 fa53d267dab3
child 58614 7338eb25226c
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
     1
header {* An old chestnut *}
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
     2
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 20503
diff changeset
     3
theory Puzzle
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 20503
diff changeset
     4
imports Main
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 20503
diff changeset
     5
begin
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
     6
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 34915
diff changeset
     7
text_raw {* \footnote{A question from ``Bundeswettbewerb Mathematik''.
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 34915
diff changeset
     8
  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 34915
diff changeset
     9
  script by Tobias Nipkow.} *}
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    10
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 34915
diff changeset
    11
text {* \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 34915
diff changeset
    12
  such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 34915
diff changeset
    13
  Demonstrate that $f$ is the identity. *}
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    14
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    15
theorem
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    16
  assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    17
  shows "f n = n"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    18
proof (rule order_antisym)
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    19
  {
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    20
    fix n show "n \<le> f n"
34915
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 33026
diff changeset
    21
    proof (induct "f n" arbitrary: n rule: less_induct)
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 33026
diff changeset
    22
      case less
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    23
      show "n \<le> f n"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    24
      proof (cases n)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    25
        case (Suc m)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    26
        from f_ax have "f (f m) < f n" by (simp only: Suc)
34915
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 33026
diff changeset
    27
        with less have "f m \<le> f (f m)" .
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    28
        also from f_ax have "\<dots> < f n" by (simp only: Suc)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    29
        finally have "f m < f n" .
34915
7894c7dab132 Adapted to changes in induct method.
berghofe
parents: 33026
diff changeset
    30
        with less have "m \<le> f m" .
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    31
        also note `\<dots> < f n`
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    32
        finally have "m < f n" .
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    33
        then have "n \<le> f n" by (simp only: Suc)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    34
        then show ?thesis .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    35
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    36
        case 0
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31758
diff changeset
    37
        then show ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    38
      qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    39
    qed
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    40
  } note ge = this
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    41
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    42
  {
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    43
    fix m n :: nat
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    44
    assume "m \<le> n"
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    45
    then have "f m \<le> f n"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    46
    proof (induct n)
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    47
      case 0
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    48
      then have "m = 0" by simp
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    49
      then show ?case by simp
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    50
    next
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    51
      case (Suc n)
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    52
      from Suc.prems show "f m \<le> f (Suc n)"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    53
      proof (rule le_SucE)
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    54
        assume "m \<le> n"
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    55
        with Suc.hyps have "f m \<le> f n" .
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    56
        also from ge f_ax have "\<dots> < f (Suc n)"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    57
          by (rule le_less_trans)
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    58
        finally show ?thesis by simp
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    59
      next
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    60
        assume "m = Suc n"
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    61
        then show ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    62
      qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    63
    qed
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    64
  } note mono = this
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    65
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    66
  show "f n \<le> n"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    67
  proof -
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    68
    have "\<not> n < f n"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    69
    proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    70
      assume "n < f n"
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    71
      then have "Suc n \<le> f n" by simp
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    72
      then have "f (Suc n) \<le> f (f n)" by (rule mono)
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    73
      also have "\<dots> < f (Suc n)" by (rule f_ax)
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    74
      finally have "\<dots> < \<dots>" . then show False ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    75
    qed
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    76
    then show ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    77
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    78
qed
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    79
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    80
end