1461
|
1 |
(* Title: ZF/AC/AC1_AC17.ML
|
1123
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Krzysztof Grabczewski
|
1123
|
4 |
|
|
5 |
The proof of AC1 ==> AC17
|
|
6 |
*)
|
|
7 |
|
5068
|
8 |
Goal "!!f. f : (PROD X:Pow(A) - {0}. X) ==> f : (Pow(A) - {0} -> A)";
|
1206
|
9 |
by (rtac Pi_type 1 THEN (assume_tac 1));
|
|
10 |
by (dtac apply_type 1 THEN (assume_tac 1));
|
2469
|
11 |
by (Fast_tac 1);
|
1123
|
12 |
val lemma1 = result();
|
|
13 |
|
5068
|
14 |
Goalw AC_defs "!!Z. AC1 ==> AC17";
|
1206
|
15 |
by (rtac allI 1);
|
|
16 |
by (rtac ballI 1);
|
1123
|
17 |
by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
|
1206
|
18 |
by (etac impE 1);
|
2469
|
19 |
by (Fast_tac 1);
|
1206
|
20 |
by (etac exE 1);
|
|
21 |
by (rtac bexI 1);
|
|
22 |
by (etac lemma1 2);
|
|
23 |
by (rtac apply_type 1 THEN (assume_tac 1));
|
4091
|
24 |
by (fast_tac (claset() addSDs [lemma1] addSEs [apply_type]) 1);
|
1196
|
25 |
qed "AC1_AC17";
|