(* Title: ZF/Ordinal.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Ordinals in Zermelo-Fraenkel Set Theory *) Ordinal = WF + Bool + "simpdata" + "equalities" + consts Memrel :: "i=>i" Transset,Ord :: "i=>o" "<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*) "le" :: "[i,i] => o" (infixl 50) (*less than or equals*) Limit :: "i=>o" translations "x le y" == "x < succ(y)" defs Memrel_def "Memrel(A) == {z: A*A . EX x y. z= & x:y }" Transset_def "Transset(i) == ALL x:i. x<=i" Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))" lt_def "i succ(y)