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;
clasohm@1478
     1
(*  Title:      ZF/Ordinal.thy
lcp@435
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@435
     4
    Copyright   1994  University of Cambridge
lcp@435
     5
lcp@435
     6
Ordinals in Zermelo-Fraenkel Set Theory 
lcp@435
     7
*)
lcp@435
     8
paulson@2469
     9
Ordinal = WF + Bool + equalities +
lcp@435
    10
consts
clasohm@1478
    11
  Memrel        :: i=>i
clasohm@1401
    12
  Transset,Ord  :: i=>o
clasohm@1401
    13
  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
wenzelm@2539
    14
  Limit         :: i=>o
wenzelm@2539
    15
wenzelm@2539
    16
syntax
clasohm@1401
    17
  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
lcp@435
    18
lcp@435
    19
translations
lcp@435
    20
  "x le y"      == "x < succ(y)"
lcp@435
    21
wenzelm@2540
    22
syntax (symbols)
wenzelm@2540
    23
  "op le"       :: [i,i] => o  (infixl "\\<le>" 50) (*less than or equals*)
wenzelm@2540
    24
lcp@753
    25
defs
clasohm@1478
    26
  Memrel_def    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
clasohm@1478
    27
  Transset_def  "Transset(i) == ALL x:i. x<=i"
clasohm@1478
    28
  Ord_def       "Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
lcp@435
    29
  lt_def        "i<j         == i:j & Ord(j)"
lcp@435
    30
  Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
lcp@435
    31
lcp@435
    32
end