1478

1 
(* Title: ZF/OrderArith.thy

437

2 
ID: $Id$

1478

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

437

4 
Copyright 1994 University of Cambridge


5 


6 
Towards ordinal arithmetic


7 
*)


8 


9 
OrderArith = Order + Sum +


10 
consts

1401

11 
radd, rmult :: [i,i,i,i]=>i


12 
rvimage :: [i,i,i]=>i

437

13 

753

14 
defs

437

15 
(*disjoint sum of two relations; underlies ordinal addition*)

1155

16 
radd_def "radd(A,r,B,s) ==


17 
{z: (A+B) * (A+B).

1478

18 
(EX x y. z = <Inl(x), Inr(y)>) 


19 
(EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) 

1155

20 
(EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"

437

21 


22 
(*lexicographic product of two relations; underlies ordinal multiplication*)

1155

23 
rmult_def "rmult(A,r,B,s) ==


24 
{z: (A*B) * (A*B).

1478

25 
EX x' y' x y. z = <<x',y'>, <x,y>> &

1155

26 
(<x',x>: r  (x'=x & <y',y>: s))}"

437

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
