author | paulson |
Wed, 08 Jan 1997 15:04:27 +0100 | |
changeset 2493 | bdeb5024353a |
parent 2469 | b50b8c0eec01 |
child 4091 | 771b1f6422a8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/WO1_WO8.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
The proof of WO8 <-> WO1 (Rubin & Rubin p. 6) |
|
6 |
*) |
|
7 |
||
8 |
(* ********************************************************************** *) |
|
1461 | 9 |
(* Trivial implication "WO1 ==> WO8" *) |
1123 | 10 |
(* ********************************************************************** *) |
11 |
||
12 |
goalw thy WO_defs "!!Z. WO1 ==> WO8"; |
|
2469 | 13 |
by (Fast_tac 1); |
1196 | 14 |
qed "WO1_WO8"; |
1123 | 15 |
|
16 |
(* ********************************************************************** *) |
|
1461 | 17 |
(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *) |
1123 | 18 |
(* ********************************************************************** *) |
19 |
||
20 |
goalw thy WO_defs "!!Z. WO8 ==> WO1"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
21 |
by (rtac allI 1); |
1123 | 22 |
by (eres_inst_tac [("x","{{x}. x:A}")] allE 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
23 |
by (etac impE 1); |
2469 | 24 |
by (fast_tac (!claset addSEs [lam_sing_bij RS bij_is_inj RS |
1461 | 25 |
well_ord_rvimage]) 2); |
1123 | 26 |
by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1); |
2493 | 27 |
by (fast_tac (!claset addSIs [lam_type] |
28 |
addss (!simpset addsimps [singleton_eq_iff, the_equality])) 1); |
|
1196 | 29 |
qed "WO8_WO1"; |