|
1196
|
1 |
(* Title: ZF/AC/DC.thy
|
|
|
2 |
ID: $Id$
|
|
1203
|
3 |
Author: Krzysztof Grabczewski
|
|
1196
|
4 |
|
|
|
5 |
Theory file for the proofs concernind the Axiom of Dependent Choice
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
DC = AC_Equiv + Hartog + first + Cardinal_aux + "DC_lemmas" +
|
|
|
9 |
|
|
|
10 |
consts
|
|
|
11 |
|
|
1401
|
12 |
DC :: i => o
|
|
|
13 |
DC0 :: o
|
|
|
14 |
ff :: [i, i, i, i] => i
|
|
1196
|
15 |
|
|
|
16 |
rules
|
|
|
17 |
|
|
|
18 |
DC_def "DC(a) == ALL X R. R<=Pow(X)*X &
|
|
|
19 |
(ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
|
|
|
20 |
--> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
|
|
|
21 |
|
|
|
22 |
DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R)
|
|
|
23 |
--> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
|
|
|
24 |
|
|
|
25 |
ff_def "ff(b, X, Q, R) == transrec(b, %c r.
|
|
|
26 |
THE x. first(x, {x:X. <r``c, x> : R}, Q))"
|
|
|
27 |
|
|
|
28 |
end
|