author | paulson |
Tue, 04 Aug 1998 16:05:19 +0200 | |
changeset 5241 | e5129172cb2b |
parent 5147 | 825877190618 |
child 5470 | 855654b691db |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC1_WO2.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
The proof of AC1 ==> WO2 |
|
6 |
*) |
|
7 |
||
8 |
open AC1_WO2; |
|
9 |
||
2167 | 10 |
(*Establishing the existence of a bijection -- hence the need for uresult*) |
1123 | 11 |
val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \ |
1461 | 12 |
\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})"; |
1123 | 13 |
by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); |
1206 | 14 |
by (rtac f_subsets_imp_UN_HH_eq_x 1); |
1123 | 15 |
by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
5241 | 16 |
by (fast_tac (claset() addSEs [equals0E] addSDs [prem RS apply_type]) 1); |
4091 | 17 |
by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); |
2167 | 18 |
val lemma1 = uresult() |> standard; |
1123 | 19 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
20 |
Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; |
1206 | 21 |
by (rtac allI 1); |
1123 | 22 |
by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
4091 | 23 |
by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1); |
1196 | 24 |
qed "AC1_WO2"; |