author | paulson |
Thu, 09 May 2002 17:50:59 +0200 | |
changeset 13125 | be50e0b050b2 |
parent 12114 | a8e860c86252 |
child 13140 | 6d97dbb189a9 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/OrderType.thy |
435 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
435 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
850 | 6 |
Order types and ordinal arithmetic. |
435 | 7 |
|
8 |
The order type of a well-ordering is the least ordinal isomorphic to it. |
|
9 |
*) |
|
10 |
||
2469 | 11 |
OrderType = OrderArith + OrdQuant + |
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
12 |
constdefs |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
13 |
|
1401 | 14 |
ordermap :: [i,i]=>i |
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
15 |
"ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))" |
435 | 16 |
|
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
17 |
ordertype :: [i,i]=>i |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
18 |
"ordertype(A,r) == ordermap(A,r)``A" |
850 | 19 |
|
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
20 |
(*alternative definition of ordinal numbers*) |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
21 |
Ord_alt :: i => o |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
22 |
"Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))" |
435 | 23 |
|
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
24 |
(*coercion to ordinal: if not, just 0*) |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
25 |
ordify :: i=>i |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
26 |
"ordify(x) == if Ord(x) then x else 0" |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
27 |
|
850 | 28 |
(*ordinal multiplication*) |
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
29 |
omult :: [i,i]=>i (infixl "**" 70) |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
30 |
"i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))" |
850 | 31 |
|
32 |
(*ordinal addition*) |
|
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
33 |
raw_oadd :: [i,i]=>i |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
34 |
"raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
35 |
|
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
36 |
oadd :: [i,i]=>i (infixl "++" 65) |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
37 |
"i ++ j == raw_oadd(ordify(i),ordify(j))" |
850 | 38 |
|
1033 | 39 |
(*ordinal subtraction*) |
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
40 |
odiff :: [i,i]=>i (infixl "--" 65) |
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
41 |
"i -- j == ordertype(i-j, Memrel(i))" |
1033 | 42 |
|
13125
be50e0b050b2
ordinal addition now coerces its arguments to ordinals
paulson
parents:
12114
diff
changeset
|
43 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9964
diff
changeset
|
44 |
syntax (xsymbols) |
9964 | 45 |
"op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70) |
46 |
||
47 |
syntax (HTML output) |
|
9683 | 48 |
"op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70) |
9654
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
2469
diff
changeset
|
49 |
|
435 | 50 |
end |