src/ZF/OrderArith.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06 ago) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 9883 c1c8647af477 permissions -rw-r--r--
expanded tabs
```     1 (*  Title:      ZF/OrderArith.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 Towards ordinal arithmetic
```
```     7 *)
```
```     8
```
```     9 OrderArith = Order + Sum +
```
```    10 consts
```
```    11   radd, rmult      :: [i,i,i,i]=>i
```
```    12   rvimage          :: [i,i,i]=>i
```
```    13
```
```    14 defs
```
```    15   (*disjoint sum of two relations; underlies ordinal addition*)
```
```    16   radd_def "radd(A,r,B,s) ==
```
```    17                 {z: (A+B) * (A+B).
```
```    18                     (EX x y. z = <Inl(x), Inr(y)>)   |
```
```    19                     (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |
```
```    20                     (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
```
```    21
```
```    22   (*lexicographic product of two relations; underlies ordinal multiplication*)
```
```    23   rmult_def "rmult(A,r,B,s) ==
```
```    24                 {z: (A*B) * (A*B).
```
```    25                     EX x' y' x y. z = <<x',y'>, <x,y>> &
```
```    26                        (<x',x>: r | (x'=x & <y',y>: s))}"
```
```    27
```
```    28   (*inverse image of a relation*)
```
```    29   rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
```
```    30
```
```    31 end
```