src/HOL/Induct/Ordinals.thy
author wenzelm
Mon Oct 01 15:46:35 2001 +0200 (2001-10-01)
changeset 11649 dfb59b9954a6
parent 11641 0c248bed5225
child 14717 7d8d4c9b36fd
permissions -rw-r--r--
tuned;
wenzelm@11649
     1
(*  Title:      HOL/Induct/Ordinals.thy
wenzelm@11641
     2
    ID:         $Id$
wenzelm@11641
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
wenzelm@11641
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@11641
     5
*)
wenzelm@11641
     6
wenzelm@11641
     7
header {* Ordinals *}
wenzelm@11641
     8
wenzelm@11641
     9
theory Ordinals = Main:
wenzelm@11641
    10
wenzelm@11641
    11
text {*
wenzelm@11641
    12
  Some basic definitions of ordinal numbers.  Draws an Agda
wenzelm@11649
    13
  development (in Martin-L\"of type theory) by Peter Hancock (see
wenzelm@11641
    14
  \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
wenzelm@11641
    15
*}
wenzelm@11641
    16
wenzelm@11641
    17
datatype ordinal =
wenzelm@11641
    18
    Zero
wenzelm@11641
    19
  | Succ ordinal
wenzelm@11641
    20
  | Limit "nat => ordinal"
wenzelm@11641
    21
wenzelm@11641
    22
consts
wenzelm@11641
    23
  pred :: "ordinal => nat => ordinal option"
wenzelm@11641
    24
primrec
wenzelm@11641
    25
  "pred Zero n = None"
wenzelm@11641
    26
  "pred (Succ a) n = Some a"
wenzelm@11641
    27
  "pred (Limit f) n = Some (f n)"
wenzelm@11641
    28
wenzelm@11641
    29
consts
wenzelm@11641
    30
  iter :: "('a => 'a) => nat => ('a => 'a)"
wenzelm@11641
    31
primrec
wenzelm@11641
    32
  "iter f 0 = id"
wenzelm@11641
    33
  "iter f (Suc n) = f \<circ> (iter f n)"
wenzelm@11641
    34
wenzelm@11641
    35
constdefs
wenzelm@11641
    36
  OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
wenzelm@11641
    37
  "OpLim F a == Limit (\<lambda>n. F n a)"
wenzelm@11641
    38
  OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>")
wenzelm@11641
    39
  "\<Squnion>f == OpLim (iter f)"
wenzelm@11641
    40
wenzelm@11641
    41
consts
wenzelm@11641
    42
  cantor :: "ordinal => ordinal => ordinal"
wenzelm@11641
    43
primrec
wenzelm@11641
    44
  "cantor a Zero = Succ a"
wenzelm@11641
    45
  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
wenzelm@11641
    46
  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
wenzelm@11641
    47
wenzelm@11641
    48
consts
wenzelm@11641
    49
  Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>")
wenzelm@11641
    50
primrec
wenzelm@11641
    51
  "\<nabla>f Zero = f Zero"
wenzelm@11641
    52
  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
wenzelm@11641
    53
  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
wenzelm@11641
    54
wenzelm@11641
    55
constdefs
wenzelm@11641
    56
  deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
wenzelm@11641
    57
  "deriv f == \<nabla>(\<Squnion>f)"
wenzelm@11641
    58
wenzelm@11641
    59
consts
wenzelm@11641
    60
  veblen :: "ordinal => ordinal => ordinal"
wenzelm@11641
    61
primrec
wenzelm@11641
    62
  "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
wenzelm@11641
    63
  "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
wenzelm@11641
    64
  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
wenzelm@11641
    65
wenzelm@11641
    66
constdefs
wenzelm@11641
    67
  veb :: "ordinal => ordinal"
wenzelm@11641
    68
  "veb a == veblen a Zero"
wenzelm@11641
    69
wenzelm@11641
    70
constdefs
wenzelm@11649
    71
  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
wenzelm@11649
    72
  "\<epsilon>\<^sub>0 == veb Zero"
wenzelm@11641
    73
  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
wenzelm@11641
    74
  "\<Gamma>\<^sub>0 == Limit (\<lambda>n. iter veb n Zero)"
wenzelm@11641
    75
wenzelm@11641
    76
end