author | paulson |
Fri, 03 Jan 1997 15:01:55 +0100 | |
changeset 2469 | b50b8c0eec01 |
parent 1924 | 0f1a583457da |
child 3731 | 71366483323b |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC0_AC1.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
AC0 is equivalent to AC1 |
|
6 |
AC0 comes from Suppes, AC1 from Rubin & Rubin |
|
7 |
*) |
|
8 |
||
9 |
goal thy "!!A. 0~:A ==> A <= Pow(Union(A))-{0}"; |
|
2469 | 10 |
by (Fast_tac 1); |
1123 | 11 |
val subset_Pow_Union = result(); |
12 |
||
13 |
goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)"; |
|
2469 | 14 |
by (fast_tac (!claset addSIs [restrict_type, apply_type]) 1); |
1123 | 15 |
val lemma1 = result(); |
16 |
||
1196 | 17 |
goalw thy AC_defs "!!Z. AC0 ==> AC1"; |
1123 | 18 |
by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1); |
1196 | 19 |
qed "AC0_AC1"; |
1123 | 20 |
|
1196 | 21 |
goalw thy AC_defs "!!Z. AC1 ==> AC0"; |
2469 | 22 |
by (Deepen_tac 0 1); |
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
23 |
(*Large search space. Faster proof by |
2469 | 24 |
by (fast_tac (!claset addSIs [notI, singletonI] addSEs [notE, DiffE]) 1); |
1924
0f1a583457da
Corrected for new classical reasoner: redundant rules
paulson
parents:
1461
diff
changeset
|
25 |
*) |
1196 | 26 |
qed "AC1_AC0"; |