src/ZF/Ordinal.thy
 author lcp Thu Jan 12 03:01:40 1995 +0100 (1995-01-12) changeset 852 664052e3cf66 parent 753 ec86863e87c8 child 1401 0c439768f45c permissions -rw-r--r--
Now depends upon Bool, so that 1 and 2 are defined
 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 ``` lcp@435 ` 11` ``` Memrel :: "i=>i" ``` lcp@435 ` 12` ``` Transset,Ord :: "i=>o" ``` lcp@435 ` 13` ``` "<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*) ``` lcp@435 ` 14` ``` "le" :: "[i,i] => o" (infixl 50) (*less than or equals*) ``` lcp@435 ` 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 }" ``` 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 succ(y)