src/HOL/Isar_Examples/Puzzle.thy
author haftmann
Tue, 13 Oct 2015 09:21:15 +0200
changeset 61424 c3658c18b7bc
parent 60410 a197387e1854
child 61541 846c72206207
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58882
6e2010ab8bd9 modernized header;
wenzelm
parents: 58614
diff changeset
     1
section \<open>An old chestnut\<close>
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
58614
7338eb25226c more cartouches;
wenzelm
parents: 37671
diff changeset
     7
text_raw \<open>\footnote{A question from ``Bundeswettbewerb Mathematik''.
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 34915
diff changeset
     8
  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
58614
7338eb25226c more cartouches;
wenzelm
parents: 37671
diff changeset
     9
  script by Tobias Nipkow.}\<close>
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    10
58614
7338eb25226c more cartouches;
wenzelm
parents: 37671
diff changeset
    11
text \<open>\textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$
37671
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$.
58614
7338eb25226c more cartouches;
wenzelm
parents: 37671
diff changeset
    13
  Demonstrate that $f$ is the identity.\<close>
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)
60410
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    19
  show ge: "n \<le> f n" for n
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    20
  proof (induct "f n" arbitrary: n rule: less_induct)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    21
    case less
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    22
    show "n \<le> f n"
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    23
    proof (cases n)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    24
      case (Suc m)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    25
      from f_ax have "f (f m) < f n" by (simp only: Suc)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    26
      with less have "f m \<le> f (f m)" .
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    27
      also from f_ax have "\<dots> < f n" by (simp only: Suc)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    28
      finally have "f m < f n" .
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    29
      with less have "m \<le> f m" .
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    30
      also note \<open>\<dots> < f n\<close>
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    31
      finally have "m < f n" .
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    32
      then have "n \<le> f n" by (simp only: Suc)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    33
      then show ?thesis .
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    34
    next
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    35
      case 0
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    36
      then show ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    37
    qed
60410
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    38
  qed
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    39
60410
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    40
  have mono: "m \<le> n \<Longrightarrow> f m \<le> f n" for m n :: nat
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    41
  proof (induct n)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    42
    case 0
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    43
    then have "m = 0" by simp
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    44
    then show ?case by simp
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    45
  next
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    46
    case (Suc n)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    47
    from Suc.prems show "f m \<le> f (Suc n)"
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    48
    proof (rule le_SucE)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    49
      assume "m \<le> n"
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    50
      with Suc.hyps have "f m \<le> f n" .
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    51
      also from ge f_ax have "\<dots> < f (Suc n)"
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    52
        by (rule le_less_trans)
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    53
      finally show ?thesis by simp
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    54
    next
60410
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    55
      assume "m = Suc n"
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    56
      then show ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    57
    qed
60410
a197387e1854 tuned proofs;
wenzelm
parents: 58882
diff changeset
    58
  qed
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    59
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    60
  show "f n \<le> n"
10436
98c421dd5972 simplified induction;
wenzelm
parents: 10007
diff changeset
    61
  proof -
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    62
    have "\<not> n < f n"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    63
    proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    64
      assume "n < f n"
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    65
      then have "Suc n \<le> f n" by simp
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    66
      then have "f (Suc n) \<le> f (f n)" by (rule mono)
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    67
      also have "\<dots> < f (Suc n)" by (rule f_ax)
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    68
      finally have "\<dots> < \<dots>" . then show False ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    69
    qed
18191
ef29685acef0 improved induction proof: local defs/fixes;
wenzelm
parents: 16417
diff changeset
    70
    then show ?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
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents:
diff changeset
    73
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9941
diff changeset
    74
end