|
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)
|
|
832
|
12 |
eqpoll, lepoll,
|
|
|
13 |
lesspoll :: "[i,i] => o" (infixl 50)
|
|
|
14 |
cardinal :: "i=>i" ("|_|")
|
|
|
15 |
Finite, Card :: "i=>o"
|
|
435
|
16 |
|
|
753
|
17 |
defs
|
|
435
|
18 |
|
|
|
19 |
(*least ordinal operator*)
|
|
832
|
20 |
Least_def "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
|
|
435
|
21 |
|
|
832
|
22 |
eqpoll_def "A eqpoll B == EX f. f: bij(A,B)"
|
|
435
|
23 |
|
|
832
|
24 |
lepoll_def "A lepoll B == EX f. f: inj(A,B)"
|
|
435
|
25 |
|
|
832
|
26 |
lesspoll_def "A lesspoll B == A lepoll B & ~(A eqpoll B)"
|
|
|
27 |
|
|
|
28 |
Finite_def "Finite(A) == EX n:nat. A eqpoll n"
|
|
435
|
29 |
|
|
832
|
30 |
cardinal_def "|A| == LEAST i. i eqpoll A"
|
|
435
|
31 |
|
|
832
|
32 |
Card_def "Card(i) == (i = |i|)"
|
|
435
|
33 |
|
|
|
34 |
end
|