src/ZF/Ordinal.thy
author clasohm
Sat, 09 Dec 1995 13:36:11 +0100
changeset 1401 0c439768f45c
parent 852 664052e3cf66
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
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
852
664052e3cf66 Now depends upon Bool, so that 1 and 2 are defined
lcp
parents: 753
diff changeset
     9
Ordinal = WF + Bool + "simpdata" + "equalities" +
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    10
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 852
diff changeset
    11
  Memrel      	:: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 852
diff changeset
    12
  Transset,Ord  :: i=>o
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 852
diff changeset
    13
  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 852
diff changeset
    14
  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 852
diff changeset
    15
  Limit         :: i=>o
435
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