src/ZF/Ordinal.thy
author wenzelm
Thu Jan 23 12:42:07 1997 +0100 (1997-01-23)
changeset 2540 ba8311047f18
parent 2539 ddd22ceee8cc
child 12114 a8e860c86252
permissions -rw-r--r--
added symbols syntax;
     1 (*  Title:      ZF/Ordinal.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Ordinals in Zermelo-Fraenkel Set Theory 
     7 *)
     8 
     9 Ordinal = WF + Bool + equalities +
    10 consts
    11   Memrel        :: i=>i
    12   Transset,Ord  :: i=>o
    13   "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
    14   Limit         :: i=>o
    15 
    16 syntax
    17   "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
    18 
    19 translations
    20   "x le y"      == "x < succ(y)"
    21 
    22 syntax (symbols)
    23   "op le"       :: [i,i] => o  (infixl "\\<le>" 50) (*less than or equals*)
    24 
    25 defs
    26   Memrel_def    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
    27   Transset_def  "Transset(i) == ALL x:i. x<=i"
    28   Ord_def       "Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
    29   lt_def        "i<j         == i:j & Ord(j)"
    30   Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
    31 
    32 end