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
```