1478
|
1 |
(* Title: ZF/AC/DC.thy
|
1196
|
2 |
ID: $Id$
|
1478
|
3 |
Author: Krzysztof Grabczewski
|
1196
|
4 |
|
|
5 |
Theory file for the proofs concernind the Axiom of Dependent Choice
|
|
6 |
*)
|
|
7 |
|
3892
|
8 |
DC = AC_Equiv + Hartog + Cardinal_aux + DC_lemmas +
|
1196
|
9 |
|
|
10 |
consts
|
|
11 |
|
1401
|
12 |
DC :: i => o
|
|
13 |
DC0 :: o
|
|
14 |
ff :: [i, i, i, i] => i
|
1196
|
15 |
|
|
16 |
rules
|
|
17 |
|
5482
|
18 |
DC_def "DC(a) ==
|
|
19 |
ALL X R. R<=Pow(X)*X &
|
|
20 |
(ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
|
|
21 |
--> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
|
1196
|
22 |
|
|
23 |
DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R)
|
5482
|
24 |
--> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
|
|
25 |
|
|
26 |
ff_def "ff(b, X, Q, R) ==
|
|
27 |
transrec(b, %c r. THE x. first(x, {x:X. <r``c, x> : R}, Q))"
|
|
28 |
|
|
29 |
|
|
30 |
locale DC0_imp =
|
|
31 |
fixes
|
|
32 |
XX :: i
|
|
33 |
RR :: i
|
|
34 |
X :: i
|
|
35 |
R :: i
|
|
36 |
|
|
37 |
assumes
|
|
38 |
all_ex "ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R)"
|
|
39 |
|
|
40 |
defines
|
|
41 |
XX_def "XX == (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R})"
|
|
42 |
RR_def "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))
|
|
43 |
& restrict(z2, domain(z1)) = z1}"
|
|
44 |
|
1196
|
45 |
|
5482
|
46 |
locale imp_DC0 =
|
|
47 |
fixes
|
|
48 |
XX :: i
|
|
49 |
RR :: i
|
|
50 |
x :: i
|
|
51 |
R :: i
|
|
52 |
f :: i
|
|
53 |
allRR :: o
|
|
54 |
|
|
55 |
defines
|
|
56 |
XX_def "XX == (UN n:nat.
|
|
57 |
{f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R})"
|
|
58 |
RR_def
|
|
59 |
"RR == {<z1,z2>:Fin(XX)*XX.
|
|
60 |
(domain(z2)=succ(UN f:z1. domain(f))
|
|
61 |
& (ALL f:z1. restrict(z2, domain(f)) = f))
|
|
62 |
| (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f))
|
|
63 |
& (ALL f:z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}"
|
|
64 |
allRR_def
|
|
65 |
"allRR == ALL b<nat.
|
|
66 |
<f``b, f`b> :
|
|
67 |
{<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f))
|
|
68 |
& (UN f:z1. domain(f)) = b
|
|
69 |
& (ALL f:z1. restrict(z2,domain(f)) = f))}"
|
1196
|
70 |
end
|