437

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 

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).


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)}"

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).


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


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
