0

1 
(* Title: ZF/ordinal.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

30

4 
Copyright 1993 University of Cambridge

0

5 


6 
Ordinals in ZermeloFraenkel Set Theory


7 
*)


8 

124

9 
Ord = WF + "simpdata" + "equalities" +

0

10 
consts

30

11 
Memrel :: "i=>i"


12 
Transset,Ord :: "i=>o"


13 
"<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*)


14 
"le" :: "[i,i] => o" (infixl 50) (*less than or equals*)


15 


16 
translations


17 
"x le y" == "x < succ(y)"

0

18 


19 
rules


20 
Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"


21 
Transset_def "Transset(i) == ALL x:i. x<=i"


22 
Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"

30

23 
lt_def "i<j == i:j & Ord(j)"

0

24 


25 
end
