# HG changeset patch
# User lcp
# Date 789876058 -3600
# Node ID a744f9749885aabe180a4387d0409bc18ae44d32
# Parent  013a16d3addb7d844e0227ec1287dd6d78f15914
Added constants Ord_alt, ++, **

diff -r 013a16d3addb -r a744f9749885 src/ZF/OrderType.thy
--- 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
     Copyright   1994  University of Cambridge
 
-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)))"
+
+  (*ordinal addition*)
+  oadd_def      "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
+
 end