|
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
|