src/HOL/Induct/Ordinals.thy
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 14981 e73f8140af78
child 19736 d8d0f8f51d69
permissions -rw-r--r--
migrated theory headers to new format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11649
wenzelm
parents: 11641
diff changeset
     1
(*  Title:      HOL/Induct/Ordinals.thy
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     4
*)
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     5
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     6
header {* Ordinals *}
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     8
theory Ordinals imports Main begin
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
     9
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    10
text {*
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    11
  Some basic definitions of ordinal numbers.  Draws an Agda
11649
wenzelm
parents: 11641
diff changeset
    12
  development (in Martin-L\"of type theory) by Peter Hancock (see
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    13
  \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    14
*}
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    15
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    16
datatype ordinal =
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    17
    Zero
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    18
  | Succ ordinal
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    19
  | Limit "nat => ordinal"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    20
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    21
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    22
  pred :: "ordinal => nat => ordinal option"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    23
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    24
  "pred Zero n = None"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    25
  "pred (Succ a) n = Some a"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    26
  "pred (Limit f) n = Some (f n)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    27
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    28
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    29
  iter :: "('a => 'a) => nat => ('a => 'a)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    30
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    31
  "iter f 0 = id"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    32
  "iter f (Suc n) = f \<circ> (iter f n)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    33
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    34
constdefs
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    35
  OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    36
  "OpLim F a == Limit (\<lambda>n. F n a)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    37
  OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>")
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    38
  "\<Squnion>f == OpLim (iter f)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    39
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    40
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    41
  cantor :: "ordinal => ordinal => ordinal"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    42
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    43
  "cantor a Zero = Succ a"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    44
  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    45
  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    46
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    47
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    48
  Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>")
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    49
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    50
  "\<nabla>f Zero = f Zero"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    51
  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    52
  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    53
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    54
constdefs
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    55
  deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    56
  "deriv f == \<nabla>(\<Squnion>f)"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    57
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    58
consts
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    59
  veblen :: "ordinal => ordinal => ordinal"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    60
primrec
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    61
  "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    62
  "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    63
  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    64
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    65
constdefs
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    66
  "veb a == veblen a Zero"
14717
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11649
diff changeset
    67
  "\<epsilon>\<^isub>0 == veb Zero"
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11649
diff changeset
    68
  "\<Gamma>\<^isub>0 == Limit (\<lambda>n. iter veb n Zero)"
11641
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    69
0c248bed5225 added Ordinals example;
wenzelm
parents:
diff changeset
    70
end