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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ordinal.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
30
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
     4
    Copyright   1993  University of Cambridge
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Ordinals in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
124
858ab9a9b047 made pseudo theories for all ML files;
clasohm
parents: 30
diff changeset
     9
Ord = WF + "simpdata" + "equalities" +
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
consts
30
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    11
  Memrel      	:: "i=>i"
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    12
  Transset,Ord  :: "i=>o"
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    13
  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    14
  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    15
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    16
translations
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    17
  "x le y"      == "x < succ(y)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  Transset_def	"Transset(i) == ALL x:i. x<=i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
30
d49df4181f0d Retrying yet again after network problems
lcp
parents: 0
diff changeset
    23
  lt_def        "i<j         == i:j & Ord(j)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
end