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


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
