437

1 
(* Title: ZF/CardinalArith.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Cardinal Arithmetic


7 
*)


8 


9 
CardinalArith = Cardinal + OrderArith + Arith +


10 
consts


11 
InfCard :: "i=>o"


12 
"*" :: "[i,i]=>i" (infixl 70)


13 
"+" :: "[i,i]=>i" (infixl 65)


14 
csquare_rel :: "i=>i"


15 


16 
rules


17 


18 
InfCard_def "InfCard(i) == Card(i) & nat le i"


19 


20 
cadd_def "i + j ==  i+j "


21 


22 
cmult_def "i * j ==  i*j "


23 


24 
csquare_rel_def


25 
"csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \


26 
\ rmult(k,Memrel(k), k*k, \


27 
\ rmult(k,Memrel(k), k,Memrel(k))))"


28 


29 
end
