435
|
1 |
(* Title: ZF/Cardinal.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
|
|
6 |
Cardinals in Zermelo-Fraenkel Set Theory
|
|
7 |
*)
|
|
8 |
|
|
9 |
Cardinal = OrderType + Fixedpt + Nat + Sum +
|
|
10 |
consts
|
|
11 |
Least :: "(i=>o) => i" (binder "LEAST " 10)
|
|
12 |
eqpoll, lepoll :: "[i,i] => o" (infixl 50)
|
|
13 |
"cardinal" :: "i=>i" ("|_|")
|
|
14 |
Card :: "i=>o"
|
|
15 |
|
|
16 |
swap :: "[i,i,i]=>i" (*not used; useful??*)
|
|
17 |
|
|
18 |
rules
|
|
19 |
|
|
20 |
(*least ordinal operator*)
|
|
21 |
Least_def "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
|
|
22 |
|
|
23 |
eqpoll_def "A eqpoll B == EX f. f: bij(A,B)"
|
|
24 |
|
|
25 |
lepoll_def "A lepoll B == EX f. f: inj(A,B)"
|
|
26 |
|
|
27 |
cardinal_def "|A| == LEAST i. i eqpoll A"
|
|
28 |
|
|
29 |
Card_def "Card(i) == ( i = |i| )"
|
|
30 |
|
|
31 |
swap_def "swap(A,x,y) == (lam z:A. if(z=x, y, if(z=y, x, z)))"
|
|
32 |
|
|
33 |
end
|