src/ZF/OrderType.thy
 changeset 850 a744f9749885 parent 753 ec86863e87c8 child 1033 437728256de3
```--- a/src/ZF/OrderType.thy	Thu Jan 12 03:00:38 1995 +0100
+++ b/src/ZF/OrderType.thy	Thu Jan 12 03:00:58 1995 +0100
@@ -3,7 +3,7 @@
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

-Order types.
+Order types and ordinal arithmetic.

The order type of a well-ordering is the least ordinal isomorphic to it.
*)
@@ -13,10 +13,25 @@
ordermap  :: "[i,i]=>i"
ordertype :: "[i,i]=>i"

+  Ord_alt   :: "i => o"
+
+  "**"      :: "[i,i]=>i"           (infixl 70)
+  "++"      :: "[i,i]=>i"           (infixl 65)
+
+
defs
ordermap_def
"ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"

ordertype_def "ordertype(A,r) == ordermap(A,r)``A"

+  Ord_alt_def    (*alternative definition of ordinal numbers*)
+  "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
+
+  (*ordinal multiplication*)
+  omult_def     "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
+