|
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 |
|
|
516
|
9 |
CardinalArith = Cardinal + OrderArith + Arith + Finite +
|
|
437
|
10 |
consts
|
|
467
|
11 |
|
|
827
|
12 |
InfCard :: "i=>o"
|
|
|
13 |
"|*|" :: "[i,i]=>i" (infixl 70)
|
|
|
14 |
"|+|" :: "[i,i]=>i" (infixl 65)
|
|
|
15 |
csquare_rel :: "i=>i"
|
|
484
|
16 |
jump_cardinal :: "i=>i"
|
|
827
|
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
|
|
827
|
28 |
"csquare_rel(K) == \
|
|
|
29 |
\ rvimage(K*K, \
|
|
|
30 |
\ lam z:K*K. split(%x y. <x Un y, <x,y>>, z), \
|
|
|
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
|
|
|
36 |
"jump_cardinal(K) == \
|
|
|
37 |
\ UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
|
|
|
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
|