|
435
|
1 |
(* Title: ZF/Ordinal.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1994 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Ordinals in Zermelo-Fraenkel Set Theory
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Ordinal = WF + "simpdata" + "equalities" +
|
|
|
10 |
consts
|
|
|
11 |
Memrel :: "i=>i"
|
|
|
12 |
Transset,Ord :: "i=>o"
|
|
|
13 |
"<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*)
|
|
|
14 |
"le" :: "[i,i] => o" (infixl 50) (*less than or equals*)
|
|
|
15 |
Limit :: "i=>o"
|
|
|
16 |
|
|
|
17 |
translations
|
|
|
18 |
"x le y" == "x < succ(y)"
|
|
|
19 |
|
|
|
20 |
rules
|
|
|
21 |
Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
|
|
|
22 |
Transset_def "Transset(i) == ALL x:i. x<=i"
|
|
|
23 |
Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
|
|
|
24 |
lt_def "i<j == i:j & Ord(j)"
|
|
|
25 |
Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
|
|
|
26 |
|
|
|
27 |
|
|
|
28 |
end
|