src/HOL/ex/Puzzle.thy
author paulson
Thu Jul 24 16:36:29 2003 +0200 (2003-07-24)
changeset 14126 28824746d046
parent 13116 baabb0fd2ccf
child 16417 9bc16273c2d4
permissions -rw-r--r--
Tidying and replacement of some axioms by specifications
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
paulson@13116
    11
theory Puzzle = Main:
paulson@13116
    12
paulson@13116
    13
consts f :: "nat => nat"
paulson@13116
    14
paulson@14126
    15
specification (f)
paulson@14126
    16
  f_ax [intro!]: "f(f(n)) < f(Suc(n))"
paulson@14126
    17
    by (rule exI [of _ id], simp)
paulson@13116
    18
paulson@13116
    19
paulson@13116
    20
lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"
paulson@13116
    21
apply (induct_tac "k" rule: nat_less_induct)
paulson@13116
    22
apply (rule allI)
paulson@13116
    23
apply (rename_tac "i")
paulson@13116
    24
apply (case_tac "i")
paulson@13116
    25
 apply simp
paulson@13116
    26
apply (blast intro!: Suc_leI intro: le_less_trans)
paulson@13116
    27
done
paulson@13116
    28
paulson@13116
    29
lemma lemma1: "n <= f(n)"
paulson@13116
    30
by (blast intro: lemma0)
paulson@13116
    31
paulson@13116
    32
lemma lemma2: "f(n) < f(Suc(n))"
paulson@13116
    33
by (blast intro: le_less_trans lemma1)
paulson@13116
    34
paulson@13116
    35
lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
paulson@13116
    36
apply (induct_tac "n")
paulson@13116
    37
 apply simp
paulson@13116
    38
apply (rule impI)
paulson@13116
    39
apply (erule le_SucE)
paulson@13116
    40
 apply (cut_tac n = n in lemma2, auto) 
paulson@13116
    41
done
paulson@13116
    42
paulson@13116
    43
lemma f_id: "f(n) = n"
paulson@13116
    44
apply (rule order_antisym)
paulson@13116
    45
apply (rule_tac [2] lemma1) 
paulson@13116
    46
apply (blast intro: leI dest: leD f_mono Suc_leI)
paulson@13116
    47
done
paulson@13116
    48
clasohm@969
    49
end
paulson@13116
    50