1478

1 
(* Title: ZF/CardinalArith.thy

437

2 
ID: $Id$

1478

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

437

4 
Copyright 1994 University of Cambridge


5 


6 
Cardinal Arithmetic


7 
*)


8 

516

9 
CardinalArith = Cardinal + OrderArith + Arith + Finite +

437

10 
consts

467

11 

1401

12 
InfCard :: i=>o


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


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


15 
csquare_rel :: i=>i


16 
jump_cardinal :: i=>i


17 
csucc :: i=>i

437

18 

753

19 
defs

437

20 


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


22 

827

23 
cadd_def "i + j == i+j"

437

24 

827

25 
cmult_def "i * j == i*j"

437

26 


27 
csquare_rel_def

1155

28 
"csquare_rel(K) ==


29 
rvimage(K*K,


30 
lam <x,y>:K*K. <x Un y, x, y>,


31 
rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"

437

32 

484

33 
(*This def is more complex than Kunen's but it more easily proved to


34 
be a cardinal*)


35 
jump_cardinal_def

1155

36 
"jump_cardinal(K) ==


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

484

38 


39 
(*needed because jump_cardinal(K) might not be the successor of K*)


40 
csucc_def "csucc(K) == LEAST L. Card(L) & K<L"


41 

437

42 
end
