equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 Auxiliary lemmas concerning cardinalities |
5 Auxiliary lemmas concerning cardinalities |
6 *) |
6 *) |
7 |
|
8 open Cardinal_aux; |
|
9 |
7 |
10 (* ********************************************************************** *) |
8 (* ********************************************************************** *) |
11 (* Lemmas involving ordinals and cardinalities used in the proofs *) |
9 (* Lemmas involving ordinals and cardinalities used in the proofs *) |
12 (* concerning AC16 and DC *) |
10 (* concerning AC16 and DC *) |
13 (* ********************************************************************** *) |
11 (* ********************************************************************** *) |
111 by (fast_tac (claset() addIs [LeastI] addSEs [Ord_in_Ord]) 1); |
109 by (fast_tac (claset() addIs [LeastI] addSEs [Ord_in_Ord]) 1); |
112 qed "UN_sing_lepoll"; |
110 qed "UN_sing_lepoll"; |
113 |
111 |
114 Goal "[| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==> \ |
112 Goal "[| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==> \ |
115 \ ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a"; |
113 \ ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a"; |
116 by (etac nat_induct 1); |
114 by (induct_tac "n" 1); |
117 by (rtac allI 1); |
115 by (rtac allI 1); |
118 by (rtac impI 1); |
116 by (rtac impI 1); |
119 by (res_inst_tac [("b","UN b:a. f`b")] subst 1); |
117 by (res_inst_tac [("b","UN b:a. f`b")] subst 1); |
120 by (rtac empty_lepollI 2); |
118 by (rtac empty_lepollI 2); |
121 by (resolve_tac [equals0I RS sym] 1); |
119 by (resolve_tac [equals0I RS sym] 1); |