author | paulson |
Thu, 13 Jul 2000 13:05:58 +0200 | |
changeset 9305 | 3dfae8f90dcf |
parent 5470 | 855654b691db |
child 11317 | 7f9e4c389318 |
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 |
||
2167 | 8 |
(*Establishing the existence of a bijection -- hence the need for uresult*) |
1123 | 9 |
val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \ |
1461 | 10 |
\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})"; |
1123 | 11 |
by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); |
1206 | 12 |
by (rtac f_subsets_imp_UN_HH_eq_x 1); |
1123 | 13 |
by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
5470 | 14 |
by (fast_tac (claset() addSDs [prem RS apply_type]) 1); |
4091 | 15 |
by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); |
2167 | 16 |
val lemma1 = uresult() |> standard; |
1123 | 17 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
18 |
Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; |
1206 | 19 |
by (rtac allI 1); |
1123 | 20 |
by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
4091 | 21 |
by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1); |
1196 | 22 |
qed "AC1_WO2"; |