src/ZF/Ordinal.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 1401 0c439768f45c
parent 852 664052e3cf66
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
lcp@435
     1
(*  Title: 	ZF/Ordinal.thy
lcp@435
     2
    ID:         $Id$
lcp@435
     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
lcp@852
     9
Ordinal = WF + Bool + "simpdata" + "equalities" +
lcp@435
    10
consts
clasohm@1401
    11
  Memrel      	:: i=>i
clasohm@1401
    12
  Transset,Ord  :: i=>o
clasohm@1401
    13
  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
clasohm@1401
    14
  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
clasohm@1401
    15
  Limit         :: i=>o
lcp@435
    16
lcp@435
    17
translations
lcp@435
    18
  "x le y"      == "x < succ(y)"
lcp@435
    19
lcp@753
    20
defs
lcp@435
    21
  Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
lcp@435
    22
  Transset_def	"Transset(i) == ALL x:i. x<=i"
lcp@435
    23
  Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
lcp@435
    24
  lt_def        "i<j         == i:j & Ord(j)"
lcp@435
    25
  Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
lcp@435
    26
lcp@435
    27
end