src/HOL/ex/Puzzle.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 23813 5440f9f5522c
child 27789 1bf827e3258d
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 (*  Title:      HOL/ex/Puzzle.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1993 TU Muenchen
     5 
     6 A question from "Bundeswettbewerb Mathematik"
     7 
     8 Proof due to Herbert Ehler
     9 *)
    10 
    11 header {* A question from ``Bundeswettbewerb Mathematik'' *}
    12 
    13 theory Puzzle imports Main begin
    14 
    15 consts f :: "nat => nat"
    16 
    17 specification (f)
    18   f_ax [intro!]: "f(f(n)) < f(Suc(n))"
    19     by (rule exI [of _ id], simp)
    20 
    21 
    22 lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"
    23 apply (induct_tac "k" rule: nat_less_induct)
    24 apply (rule allI)
    25 apply (rename_tac "i")
    26 apply (case_tac "i")
    27  apply simp
    28 apply (blast intro!: Suc_leI intro: le_less_trans)
    29 done
    30 
    31 lemma lemma1: "n <= f(n)"
    32 by (blast intro: lemma0)
    33 
    34 lemma f_mono [rule_format (no_asm)]: "m <= n --> f(m) <= f(n)"
    35 apply (induct_tac "n")
    36  apply simp 
    37  apply (metis f_ax le_SucE le_trans lemma0 nat_le_linear nat_less_le)
    38 done
    39 
    40 lemma f_id: "f(n) = n"
    41 apply (rule order_antisym)
    42 apply (rule_tac [2] lemma1) 
    43 apply (blast intro: leI dest: leD f_mono Suc_leI)
    44 done
    45 
    46 end
    47