src/ZF/OrderType.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 2469 b50b8c0eec01 permissions -rw-r--r--
expanded tabs
```     1 (*  Title:      ZF/OrderType.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 Order types and ordinal arithmetic.
```
```     7
```
```     8 The order type of a well-ordering is the least ordinal isomorphic to it.
```
```     9 *)
```
```    10
```
```    11 OrderType = OrderArith + Ordinal +
```
```    12 consts
```
```    13   ordermap  :: [i,i]=>i
```
```    14   ordertype :: [i,i]=>i
```
```    15
```
```    16   Ord_alt   :: i => o
```
```    17
```
```    18   "**"      :: [i,i]=>i           (infixl 70)
```
```    19   "++"      :: [i,i]=>i           (infixl 65)
```
```    20   "--"      :: [i,i]=>i           (infixl 65)
```
```    21
```
```    22
```
```    23 defs
```
```    24   ordermap_def
```
```    25       "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
```
```    26
```
```    27   ordertype_def "ordertype(A,r) == ordermap(A,r)``A"
```
```    28
```
```    29   Ord_alt_def    (*alternative definition of ordinal numbers*)
```
```    30   "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
```
```    31
```
```    32   (*ordinal multiplication*)
```
```    33   omult_def     "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
```
```    34
```
```    35   (*ordinal addition*)
```
```    36   oadd_def      "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
```
```    37
```
```    38   (*ordinal subtraction*)
```
```    39   odiff_def     "i -- j == ordertype(i-j, Memrel(i))"
```
```    40
```
```    41 end
```