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

467

11 
jump_cardinal :: "i=>i"


12 

437

13 
InfCard :: "i=>o"


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


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


16 
csquare_rel :: "i=>i"


17 


18 
rules


19 

467

20 
jump_cardinal_def


21 
"jump_cardinal(K) == \


22 
\ UN X:Pow(K). {z. r: Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}"


23 


24 

437

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


26 


27 
cadd_def "i + j ==  i+j "


28 


29 
cmult_def "i * j ==  i*j "


30 


31 
csquare_rel_def


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


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


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


35 


36 
end
