src/HOL/Induct/Ordinals.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 21404 eb85850d3eb7
child 36862 952b2b102a0a
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:      HOL/Induct/Ordinals.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Ordinals *}
     7 
     8 theory Ordinals imports Main begin
     9 
    10 text {*
    11   Some basic definitions of ordinal numbers.  Draws an Agda
    12   development (in Martin-L\"of type theory) by Peter Hancock (see
    13   \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
    14 *}
    15 
    16 datatype ordinal =
    17     Zero
    18   | Succ ordinal
    19   | Limit "nat => ordinal"
    20 
    21 consts
    22   pred :: "ordinal => nat => ordinal option"
    23 primrec
    24   "pred Zero n = None"
    25   "pred (Succ a) n = Some a"
    26   "pred (Limit f) n = Some (f n)"
    27 
    28 consts
    29   iter :: "('a => 'a) => nat => ('a => 'a)"
    30 primrec
    31   "iter f 0 = id"
    32   "iter f (Suc n) = f \<circ> (iter f n)"
    33 
    34 definition
    35   OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where
    36   "OpLim F a = Limit (\<lambda>n. F n a)"
    37 
    38 definition
    39   OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>") where
    40   "\<Squnion>f = OpLim (iter f)"
    41 
    42 consts
    43   cantor :: "ordinal => ordinal => ordinal"
    44 primrec
    45   "cantor a Zero = Succ a"
    46   "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
    47   "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
    48 
    49 consts
    50   Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>")
    51 primrec
    52   "\<nabla>f Zero = f Zero"
    53   "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
    54   "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
    55 
    56 definition
    57   deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where
    58   "deriv f = \<nabla>(\<Squnion>f)"
    59 
    60 consts
    61   veblen :: "ordinal => ordinal => ordinal"
    62 primrec
    63   "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
    64   "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
    65   "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
    66 
    67 definition "veb a = veblen a Zero"
    68 definition "\<epsilon>\<^isub>0 = veb Zero"
    69 definition "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)"
    70 
    71 end