src/ZF/Ord.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 124 858ab9a9b047
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.

(*  Title: 	ZF/ordinal.thy
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Ordinals in Zermelo-Fraenkel Set Theory 
*)

Ord = WF + "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*)

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

rules
  Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & 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<j         == i:j & Ord(j)"

end