src/ZF/Ordinal.thy
author lcp
Tue, 29 Nov 1994 00:31:31 +0100
changeset 753 ec86863e87c8
parent 435 ca5356bd315a
child 852 664052e3cf66
permissions -rw-r--r--
replaced "rules" by "defs"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/Ordinal.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     5
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     6
Ordinals in Zermelo-Fraenkel Set Theory 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     7
*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     8
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     9
Ordinal = WF + "simpdata" + "equalities" +
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    10
consts
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    11
  Memrel      	:: "i=>i"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    12
  Transset,Ord  :: "i=>o"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    13
  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    14
  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    15
  Limit         :: "i=>o"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    16
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    17
translations
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    18
  "x le y"      == "x < succ(y)"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    19
753
ec86863e87c8 replaced "rules" by "defs"
lcp
parents: 435
diff changeset
    20
defs
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    21
  Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    22
  Transset_def	"Transset(i) == ALL x:i. x<=i"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    23
  Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    24
  lt_def        "i<j         == i:j & Ord(j)"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    25
  Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    26
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    27
end