equal
deleted
inserted
replaced
9 (* Trivial implication "WO1 ==> WO8" *) |
9 (* Trivial implication "WO1 ==> WO8" *) |
10 (* ********************************************************************** *) |
10 (* ********************************************************************** *) |
11 |
11 |
12 goalw thy WO_defs "!!Z. WO1 ==> WO8"; |
12 goalw thy WO_defs "!!Z. WO1 ==> WO8"; |
13 by (fast_tac ZF_cs 1); |
13 by (fast_tac ZF_cs 1); |
14 result(); |
14 qed "WO1_WO8"; |
15 |
15 |
16 (* ********************************************************************** *) |
16 (* ********************************************************************** *) |
17 (* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *) |
17 (* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *) |
18 (* ********************************************************************** *) |
18 (* ********************************************************************** *) |
19 |
19 |
25 well_ord_rvimage]) 2); |
25 well_ord_rvimage]) 2); |
26 by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1); |
26 by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1); |
27 by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym] |
27 by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym] |
28 addSIs [lam_type, singletonI] |
28 addSIs [lam_type, singletonI] |
29 addIs [the_equality RS ssubst]) 1); |
29 addIs [the_equality RS ssubst]) 1); |
30 result(); |
30 qed "WO8_WO1"; |