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 |
|
9548
|
9 |
CardinalArith = Cardinal + OrderArith + ArithSimp + 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
|