|
1 (* Title: ZF/AC/HH.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Gr`abczewski |
|
4 |
|
5 Some properties of the recursive definition of HH used in the proofs of |
|
6 AC17 ==> AC1 |
|
7 AC1 ==> WO2 |
|
8 AC15 ==> WO6 |
|
9 *) |
|
10 |
|
11 open HH; |
|
12 |
|
13 (* ********************************************************************** *) |
|
14 (* Lemmas useful in each of the three proofs *) |
|
15 (* ********************************************************************** *) |
|
16 |
|
17 goal thy "HH(f,x,a) = \ |
|
18 \ (lam y:Pow(x). if(f`y : Pow(y)-{0},f`y,{x}))` \ |
|
19 \ (x - (UN b:a. HH(f,x,b)))"; |
|
20 by (resolve_tac [HH_def RS def_transrec RS trans] 1); |
|
21 by (asm_full_simp_tac ZF_ss 1); |
|
22 val HH_def_satisfies_eq = result(); |
|
23 |
|
24 goal thy "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}"; |
|
25 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
|
26 by (asm_full_simp_tac (ZF_ss addsimps [Diff_subset RS PowI]) 1); |
|
27 by (split_tac [expand_if] 1); |
|
28 by (fast_tac ZF_cs 1); |
|
29 val HH_values = result(); |
|
30 |
|
31 goal thy "!!A. B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))"; |
|
32 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
|
33 val subset_imp_Diff_eq = result(); |
|
34 |
|
35 goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a"; |
|
36 by (eresolve_tac [ltE] 1); |
|
37 by (dres_inst_tac [("x","c")] Ord_linear 1); |
|
38 by (fast_tac (AC_cs addEs [Ord_in_Ord]) 1); |
|
39 by (fast_tac (AC_cs addSIs [ltI] addIs [Ord_in_Ord]) 1); |
|
40 val Ord_DiffE = result(); |
|
41 |
|
42 val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x"; |
|
43 by (asm_full_simp_tac (AC_ss addsimps prems) 1); |
|
44 by (fast_tac (AC_cs addSIs [equalityI] addSDs [prem] |
|
45 addSEs [RepFunE, mem_irrefl]) 1); |
|
46 val Diff_UN_eq_self = result(); |
|
47 |
|
48 goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \ |
|
49 \ ==> HH(f,x,a) = HH(f,x,a1)"; |
|
50 by (resolve_tac [HH_def_satisfies_eq RS |
|
51 (HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1); |
|
52 by (eresolve_tac [subst_context] 1); |
|
53 val HH_eq = result(); |
|
54 |
|
55 goal thy "!!a. [| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}"; |
|
56 by (res_inst_tac [("P","b<a")] impE 1 THEN REPEAT (assume_tac 2)); |
|
57 by (eresolve_tac [lt_Ord2 RS trans_induct] 1); |
|
58 by (resolve_tac [impI] 1); |
|
59 by (resolve_tac [HH_eq RS trans] 1 THEN (assume_tac 2)); |
|
60 by (resolve_tac [leI RS le_imp_subset RS subset_imp_Diff_eq RS ssubst] 1 |
|
61 THEN (assume_tac 1)); |
|
62 by (res_inst_tac [("t","%z. z-?X")] subst_context 1); |
|
63 by (resolve_tac [Diff_UN_eq_self] 1); |
|
64 by (dresolve_tac [Ord_DiffE] 1 THEN (assume_tac 1)); |
|
65 by (fast_tac (AC_cs addEs [ltE]) 1); |
|
66 val HH_is_x_gt_too = result(); |
|
67 |
|
68 goal thy "!!a. [| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}"; |
|
69 by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); |
|
70 by (dresolve_tac [HH_is_x_gt_too] 1 THEN (assume_tac 1)); |
|
71 by (dresolve_tac [subst] 1 THEN (assume_tac 1)); |
|
72 by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); |
|
73 val HH_subset_x_lt_too = result(); |
|
74 |
|
75 goal thy "!!a. HH(f,x,a) : Pow(x)-{0} \ |
|
76 \ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}"; |
|
77 by (dresolve_tac [HH_def_satisfies_eq RS subst] 1); |
|
78 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
|
79 by (asm_full_simp_tac (AC_ss addsimps [Diff_subset RS PowI]) 1); |
|
80 by (dresolve_tac [expand_if RS iffD1] 1); |
|
81 by (split_tac [expand_if] 1); |
|
82 by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); |
|
83 val HH_subset_x_imp_subset_Diff_UN = result(); |
|
84 |
|
85 goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P"; |
|
86 by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1)); |
|
87 by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1); |
|
88 by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1)); |
|
89 by (fast_tac (AC_cs addSIs [singleton_iff RS iffD2, equals0I]) 1); |
|
90 val HH_eq_arg_lt = result(); |
|
91 |
|
92 goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,w): Pow(x)-{0}; \ |
|
93 \ Ord(v); Ord(w) |] ==> v=w"; |
|
94 by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac); |
|
95 by (resolve_tac [sym RS (ltD RSN (3, HH_eq_arg_lt))] 2 |
|
96 THEN REPEAT (assume_tac 2)); |
|
97 by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1)); |
|
98 by (fast_tac (FOL_cs addDs [ltD] addSEs [HH_eq_arg_lt]) 1); |
|
99 val HH_eq_imp_arg_eq = result(); |
|
100 |
|
101 goalw thy [lepoll_def, inj_def] |
|
102 "!!i. [| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"; |
|
103 by (res_inst_tac [("x","lam j:i. HH(f, x, j)")] exI 1); |
|
104 by (asm_simp_tac AC_ss 1); |
|
105 by (fast_tac (FOL_cs addSEs [HH_eq_imp_arg_eq, Ord_in_Ord, HH_subset_x_lt_too] |
|
106 addSIs [lam_type, ballI, ltI] addIs [bexI]) 1); |
|
107 val HH_subset_x_imp_lepoll = result(); |
|
108 |
|
109 goal thy "HH(f, x, Hartog(Pow(x)-{0})) = {x}"; |
|
110 by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 2)); |
|
111 by (fast_tac (FOL_cs addSDs [HH_subset_x_imp_lepoll] |
|
112 addSIs [Ord_Hartog] addSEs [HartogE]) 1); |
|
113 val HH_Hartog_is_x = result(); |
|
114 |
|
115 goal thy "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}"; |
|
116 by (fast_tac (AC_cs addSIs [Ord_Hartog, HH_Hartog_is_x, LeastI]) 1); |
|
117 val HH_Least_eq_x = result(); |
|
118 |
|
119 goal thy "!!a. a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}"; |
|
120 by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); |
|
121 by (resolve_tac [less_LeastE] 1); |
|
122 by (eresolve_tac [Ord_Least RSN (2, ltI)] 2); |
|
123 by (assume_tac 1); |
|
124 val less_Least_subset_x = result(); |
|
125 |
|
126 (* ********************************************************************** *) |
|
127 (* Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1 *) |
|
128 (* ********************************************************************** *) |
|
129 |
|
130 goalw thy [inj_def] |
|
131 "(lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) : \ |
|
132 \ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"; |
|
133 by (asm_full_simp_tac AC_ss 1); |
|
134 by (fast_tac (AC_cs addSIs [lam_type] addDs [less_Least_subset_x] |
|
135 addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1); |
|
136 val lam_Least_HH_inj_Pow = result(); |
|
137 |
|
138 goal thy "!!x. ALL a:(LEAST i. HH(f,x,i)={x}). EX z:x. HH(f,x,a) = {z} \ |
|
139 \ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
|
140 \ : inj(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; |
|
141 by (resolve_tac [lam_Least_HH_inj_Pow RS inj_strengthen_type] 1); |
|
142 by (asm_full_simp_tac AC_ss 1); |
|
143 by (fast_tac (AC_cs addSEs [RepFun_eqI]) 1); |
|
144 val lam_Least_HH_inj = result(); |
|
145 |
|
146 goal thy "!!A. [| A={a}; b:A |] ==> b=a"; |
|
147 by (fast_tac AC_cs 1); |
|
148 val elem_of_sing_eq = result(); |
|
149 |
|
150 goalw thy [surj_def] |
|
151 "!!x. [| x - (UN a:A. F(a)) = 0; \ |
|
152 \ ALL a:A. EX z:x. F(a) = {z} |] \ |
|
153 \ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})"; |
|
154 by (asm_full_simp_tac (AC_ss addsimps [Diff_eq_0_iff]) 1); |
|
155 by (resolve_tac [conjI] 1); |
|
156 by (fast_tac (AC_cs addSIs [lam_type] addSEs [RepFun_eqI]) 1); |
|
157 by (resolve_tac [ballI] 1); |
|
158 by (eresolve_tac [RepFunE] 1); |
|
159 by (dresolve_tac [subsetD] 1 THEN (assume_tac 1)); |
|
160 by (eresolve_tac [UN_E] 1); |
|
161 by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); |
|
162 by (eresolve_tac [bexE] 1); |
|
163 by (resolve_tac [bexI] 1 THEN (assume_tac 2)); |
|
164 by (forward_tac [elem_of_sing_eq] 1 THEN (assume_tac 1)); |
|
165 by (fast_tac AC_cs 1); |
|
166 val lam_surj_sing = result(); |
|
167 |
|
168 goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0"; |
|
169 by (fast_tac (AC_cs addSIs [equals0I, singletonI RS subst_elem] |
|
170 addSDs [equals0D]) 1); |
|
171 val not_emptyI2 = result(); |
|
172 |
|
173 goal thy "!!f. f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0} \ |
|
174 \ ==> HH(f, x, i) : Pow(x) - {0}"; |
|
175 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
|
176 by (asm_full_simp_tac (AC_ss addsimps [Diff_subset RS PowI, |
|
177 not_emptyI2 RS if_P]) 1); |
|
178 by (fast_tac AC_cs 1); |
|
179 val f_subset_imp_HH_subset = result(); |
|
180 |
|
181 val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \ |
|
182 \ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"; |
|
183 by (excluded_middle_tac "?P : {0}" 1); |
|
184 by (fast_tac AC_cs 2); |
|
185 by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS |
|
186 f_subset_imp_HH_subset] 1); |
|
187 by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)] |
|
188 addSEs [mem_irrefl]) 1); |
|
189 val f_subsets_imp_UN_HH_eq_x = result(); |
|
190 |
|
191 goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}"; |
|
192 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
|
193 by (asm_full_simp_tac (ZF_ss addsimps [Diff_subset RS PowI]) 1); |
|
194 by (split_tac [expand_if] 1); |
|
195 by (fast_tac ZF_cs 1); |
|
196 val HH_values2 = result(); |
|
197 |
|
198 goal thy "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; |
|
199 by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1)); |
|
200 by (fast_tac (AC_cs addSEs [equalityE, mem_irrefl] |
|
201 addSDs [singleton_subsetD]) 1); |
|
202 val HH_subset_imp_eq = result(); |
|
203 |
|
204 goal thy "!!f. [| f : (PROD X:Pow(x)-{0}. {{z}. z:x}); \ |
|
205 \ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}"; |
|
206 by (dresolve_tac [less_Least_subset_x] 1); |
|
207 by (forward_tac [HH_subset_imp_eq] 1); |
|
208 by (dresolve_tac [apply_type] 1); |
|
209 by (resolve_tac [Diff_subset RS PowI RS DiffI] 1); |
|
210 by (fast_tac (AC_cs addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); |
|
211 by (fast_tac (AC_cs addSEs [RepFunE] addEs [ssubst]) 1); |
|
212 val f_sing_imp_HH_sing = result(); |
|
213 |
|
214 goalw thy [bij_def] |
|
215 "!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \ |
|
216 \ f : (PROD X:Pow(x)-{0}. {{z}. z:x}) |] \ |
|
217 \ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
|
218 \ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; |
|
219 by (fast_tac (AC_cs addSIs [lam_Least_HH_inj, lam_surj_sing, |
|
220 f_sing_imp_HH_sing]) 1); |
|
221 val f_sing_lam_bij = result(); |
|
222 |
|
223 goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \ |
|
224 \ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})"; |
|
225 by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2] |
|
226 addDs [apply_type]) 1); |
|
227 val lam_singI = result(); |
|
228 |
|
229 val bij_Least_HH_x = standard (lam_singI RSN (2, |
|
230 [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij] MRS comp_bij)); |