1 (* Title: ZF/OrderArith.thy |
1 (* Title: ZF/OrderArith.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Towards ordinal arithmetic |
6 Towards ordinal arithmetic |
7 *) |
7 *) |
8 |
8 |
13 |
13 |
14 defs |
14 defs |
15 (*disjoint sum of two relations; underlies ordinal addition*) |
15 (*disjoint sum of two relations; underlies ordinal addition*) |
16 radd_def "radd(A,r,B,s) == |
16 radd_def "radd(A,r,B,s) == |
17 {z: (A+B) * (A+B). |
17 {z: (A+B) * (A+B). |
18 (EX x y. z = <Inl(x), Inr(y)>) | |
18 (EX x y. z = <Inl(x), Inr(y)>) | |
19 (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) | |
19 (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) | |
20 (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}" |
20 (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}" |
21 |
21 |
22 (*lexicographic product of two relations; underlies ordinal multiplication*) |
22 (*lexicographic product of two relations; underlies ordinal multiplication*) |
23 rmult_def "rmult(A,r,B,s) == |
23 rmult_def "rmult(A,r,B,s) == |
24 {z: (A*B) * (A*B). |
24 {z: (A*B) * (A*B). |
25 EX x' y' x y. z = <<x',y'>, <x,y>> & |
25 EX x' y' x y. z = <<x',y'>, <x,y>> & |
26 (<x',x>: r | (x'=x & <y',y>: s))}" |
26 (<x',x>: r | (x'=x & <y',y>: s))}" |
27 |
27 |
28 (*inverse image of a relation*) |
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}" |
29 rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}" |
30 |
30 |