src/HOL/ex/Puzzle.thy
author wenzelm
Wed Sep 14 22:08:08 2005 +0200 (2005-09-14)
changeset 17388 495c799df31d
parent 16417 9bc16273c2d4
child 23813 5440f9f5522c
permissions -rw-r--r--
tuned headers etc.;
nipkow@2222
     1
(*  Title:      HOL/ex/Puzzle.thy
clasohm@969
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
clasohm@969
     4
    Copyright   1993 TU Muenchen
clasohm@969
     5
nipkow@2222
     6
A question from "Bundeswettbewerb Mathematik"
paulson@13116
     7
paulson@13116
     8
Proof due to Herbert Ehler
clasohm@969
     9
*)
clasohm@969
    10
wenzelm@17388
    11
header {* A question from ``Bundeswettbewerb Mathematik'' *}
wenzelm@17388
    12
haftmann@16417
    13
theory Puzzle imports Main begin
paulson@13116
    14
paulson@13116
    15
consts f :: "nat => nat"
paulson@13116
    16
paulson@14126
    17
specification (f)
paulson@14126
    18
  f_ax [intro!]: "f(f(n)) < f(Suc(n))"
paulson@14126
    19
    by (rule exI [of _ id], simp)
paulson@13116
    20
paulson@13116
    21
paulson@13116
    22
lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"
paulson@13116
    23
apply (induct_tac "k" rule: nat_less_induct)
paulson@13116
    24
apply (rule allI)
paulson@13116
    25
apply (rename_tac "i")
paulson@13116
    26
apply (case_tac "i")
paulson@13116
    27
 apply simp
paulson@13116
    28
apply (blast intro!: Suc_leI intro: le_less_trans)
paulson@13116
    29
done
paulson@13116
    30
paulson@13116
    31
lemma lemma1: "n <= f(n)"
paulson@13116
    32
by (blast intro: lemma0)
paulson@13116
    33
paulson@13116
    34
lemma lemma2: "f(n) < f(Suc(n))"
paulson@13116
    35
by (blast intro: le_less_trans lemma1)
paulson@13116
    36
paulson@13116
    37
lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
paulson@13116
    38
apply (induct_tac "n")
paulson@13116
    39
 apply simp
paulson@13116
    40
apply (rule impI)
paulson@13116
    41
apply (erule le_SucE)
paulson@13116
    42
 apply (cut_tac n = n in lemma2, auto) 
paulson@13116
    43
done
paulson@13116
    44
paulson@13116
    45
lemma f_id: "f(n) = n"
paulson@13116
    46
apply (rule order_antisym)
paulson@13116
    47
apply (rule_tac [2] lemma1) 
paulson@13116
    48
apply (blast intro: leI dest: leD f_mono Suc_leI)
paulson@13116
    49
done
paulson@13116
    50
clasohm@969
    51
end
paulson@13116
    52