1461
|
1 |
(* Title: ZF/AC/HH.ML
|
1123
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Krzysztof Grabczewski
|
1123
|
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 |
(* ********************************************************************** *)
|
1461
|
14 |
(* Lemmas useful in each of the three proofs *)
|
1123
|
15 |
(* ********************************************************************** *)
|
|
16 |
|
|
17 |
goal thy "HH(f,x,a) = \
|
1461
|
18 |
\ (let z = x - (UN b:a. HH(f,x,b)) \
|
|
19 |
\ in if(f`z:Pow(z)-{0}, f`z, {x}))";
|
1123
|
20 |
by (resolve_tac [HH_def RS def_transrec RS trans] 1);
|
2469
|
21 |
by (Simp_tac 1);
|
1123
|
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);
|
2469
|
26 |
by (simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI]
|
1200
|
27 |
setloop split_tac [expand_if]) 1);
|
2469
|
28 |
by (Fast_tac 1);
|
1123
|
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))";
|
2469
|
32 |
by (fast_tac (!claset addSIs [equalityI]) 1);
|
1123
|
33 |
val subset_imp_Diff_eq = result();
|
|
34 |
|
|
35 |
goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a";
|
1207
|
36 |
by (etac ltE 1);
|
1123
|
37 |
by (dres_inst_tac [("x","c")] Ord_linear 1);
|
2469
|
38 |
by (fast_tac (!claset addEs [Ord_in_Ord]) 1);
|
|
39 |
by (fast_tac (!claset addSIs [ltI] addIs [Ord_in_Ord]) 1);
|
1123
|
40 |
val Ord_DiffE = result();
|
|
41 |
|
|
42 |
val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x";
|
2469
|
43 |
by (asm_full_simp_tac (!simpset addsimps prems) 1);
|
|
44 |
by (fast_tac (!claset addSIs [equalityI] addSDs [prem]
|
1461
|
45 |
addSEs [RepFunE, mem_irrefl]) 1);
|
1123
|
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)) \
|
1461
|
49 |
\ ==> HH(f,x,a) = HH(f,x,a1)";
|
1123
|
50 |
by (resolve_tac [HH_def_satisfies_eq RS
|
1461
|
51 |
(HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1);
|
1207
|
52 |
by (etac subst_context 1);
|
1123
|
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);
|
1207
|
58 |
by (rtac impI 1);
|
1123
|
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
|
1461
|
61 |
THEN (assume_tac 1));
|
1123
|
62 |
by (res_inst_tac [("t","%z. z-?X")] subst_context 1);
|
1207
|
63 |
by (rtac Diff_UN_eq_self 1);
|
|
64 |
by (dtac Ord_DiffE 1 THEN (assume_tac 1));
|
2469
|
65 |
by (fast_tac (!claset addEs [ltE]) 1);
|
1123
|
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));
|
1207
|
70 |
by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1));
|
|
71 |
by (dtac subst 1 THEN (assume_tac 1));
|
2469
|
72 |
by (fast_tac (!claset addSEs [mem_irrefl]) 1);
|
1123
|
73 |
val HH_subset_x_lt_too = result();
|
|
74 |
|
|
75 |
goal thy "!!a. HH(f,x,a) : Pow(x)-{0} \
|
1461
|
76 |
\ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}";
|
1123
|
77 |
by (dresolve_tac [HH_def_satisfies_eq RS subst] 1);
|
|
78 |
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
|
2469
|
79 |
by (asm_full_simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI]) 1);
|
1123
|
80 |
by (dresolve_tac [expand_if RS iffD1] 1);
|
2469
|
81 |
by (simp_tac (!simpset setloop split_tac [expand_if] ) 1);
|
1200
|
82 |
by (fast_tac (subset_cs addSEs [mem_irrefl]) 1);
|
1123
|
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);
|
1207
|
88 |
by (dtac subst_elem 1 THEN (assume_tac 1));
|
2469
|
89 |
by (fast_tac (!claset addSIs [singleton_iff RS iffD2, equals0I]) 1);
|
1123
|
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}; \
|
1461
|
93 |
\ Ord(v); Ord(w) |] ==> v=w";
|
1123
|
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
|
1461
|
96 |
THEN REPEAT (assume_tac 2));
|
1207
|
97 |
by (dtac subst_elem 1 THEN (assume_tac 1));
|
1123
|
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]
|
1461
|
102 |
"!!i. [| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}";
|
1123
|
103 |
by (res_inst_tac [("x","lam j:i. HH(f, x, j)")] exI 1);
|
2469
|
104 |
by (Asm_simp_tac 1);
|
1123
|
105 |
by (fast_tac (FOL_cs addSEs [HH_eq_imp_arg_eq, Ord_in_Ord, HH_subset_x_lt_too]
|
1461
|
106 |
addSIs [lam_type, ballI, ltI] addIs [bexI]) 1);
|
1123
|
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]
|
1461
|
112 |
addSIs [Ord_Hartog] addSEs [HartogE]) 1);
|
1123
|
113 |
val HH_Hartog_is_x = result();
|
|
114 |
|
|
115 |
goal thy "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}";
|
2469
|
116 |
by (fast_tac (!claset addSIs [Ord_Hartog, HH_Hartog_is_x, LeastI]) 1);
|
1123
|
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));
|
1207
|
121 |
by (rtac less_LeastE 1);
|
1123
|
122 |
by (eresolve_tac [Ord_Least RSN (2, ltI)] 2);
|
|
123 |
by (assume_tac 1);
|
|
124 |
val less_Least_subset_x = result();
|
|
125 |
|
|
126 |
(* ********************************************************************** *)
|
1461
|
127 |
(* Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1 *)
|
1123
|
128 |
(* ********************************************************************** *)
|
|
129 |
|
|
130 |
goalw thy [inj_def]
|
1461
|
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})";
|
2469
|
133 |
by (Asm_full_simp_tac 1);
|
|
134 |
by (fast_tac (!claset addSIs [lam_type] addDs [less_Least_subset_x]
|
1461
|
135 |
addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1);
|
1123
|
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} \
|
1461
|
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})";
|
1123
|
141 |
by (resolve_tac [lam_Least_HH_inj_Pow RS inj_strengthen_type] 1);
|
2469
|
142 |
by (Asm_full_simp_tac 1);
|
1123
|
143 |
val lam_Least_HH_inj = result();
|
|
144 |
|
|
145 |
goalw thy [surj_def]
|
1461
|
146 |
"!!x. [| x - (UN a:A. F(a)) = 0; \
|
|
147 |
\ ALL a:A. EX z:x. F(a) = {z} |] \
|
|
148 |
\ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})";
|
2469
|
149 |
by (asm_full_simp_tac (!simpset addsimps [lam_type, Diff_eq_0_iff]) 1);
|
|
150 |
by (Step_tac 1);
|
|
151 |
by (set_mp_tac 1);
|
2493
|
152 |
by (deepen_tac (!claset addSIs [bexI] addSEs [equalityE]) 4 1);
|
1123
|
153 |
val lam_surj_sing = result();
|
|
154 |
|
|
155 |
goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0";
|
2469
|
156 |
by (fast_tac (!claset addSIs [equals0I, singletonI RS subst_elem]
|
1461
|
157 |
addSDs [equals0D]) 1);
|
1123
|
158 |
val not_emptyI2 = result();
|
|
159 |
|
|
160 |
goal thy "!!f. f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0} \
|
1461
|
161 |
\ ==> HH(f, x, i) : Pow(x) - {0}";
|
1123
|
162 |
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
|
2469
|
163 |
by (asm_full_simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI,
|
1461
|
164 |
not_emptyI2 RS if_P]) 1);
|
2469
|
165 |
by (Fast_tac 1);
|
1123
|
166 |
val f_subset_imp_HH_subset = result();
|
|
167 |
|
|
168 |
val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \
|
1461
|
169 |
\ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0";
|
1123
|
170 |
by (excluded_middle_tac "?P : {0}" 1);
|
2469
|
171 |
by (Fast_tac 2);
|
1123
|
172 |
by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS
|
1461
|
173 |
f_subset_imp_HH_subset] 1);
|
2469
|
174 |
by (fast_tac (!claset addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)]
|
1461
|
175 |
addSEs [mem_irrefl]) 1);
|
1123
|
176 |
val f_subsets_imp_UN_HH_eq_x = result();
|
|
177 |
|
|
178 |
goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}";
|
|
179 |
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
|
2469
|
180 |
by (simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI]
|
1461
|
181 |
setloop split_tac [expand_if]) 1);
|
1123
|
182 |
val HH_values2 = result();
|
|
183 |
|
1200
|
184 |
goal thy
|
|
185 |
"!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))";
|
1123
|
186 |
by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1));
|
2469
|
187 |
by (fast_tac (!claset addSEs [equalityE, mem_irrefl]
|
1461
|
188 |
addSDs [singleton_subsetD]) 1);
|
1123
|
189 |
val HH_subset_imp_eq = result();
|
|
190 |
|
2493
|
191 |
goal thy "!!f. [| f : (Pow(x)-{0}) -> {{z}. z:x}; \
|
1461
|
192 |
\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
|
1207
|
193 |
by (dtac less_Least_subset_x 1);
|
1123
|
194 |
by (forward_tac [HH_subset_imp_eq] 1);
|
1207
|
195 |
by (dtac apply_type 1);
|
1123
|
196 |
by (resolve_tac [Diff_subset RS PowI RS DiffI] 1);
|
2493
|
197 |
by (fast_tac
|
|
198 |
(!claset addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
|
|
199 |
by (fast_tac (!claset addss (!simpset)) 1);
|
1123
|
200 |
val f_sing_imp_HH_sing = result();
|
|
201 |
|
|
202 |
goalw thy [bij_def]
|
1461
|
203 |
"!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \
|
2493
|
204 |
\ f : (Pow(x)-{0}) -> {{z}. z:x} |] \
|
1461
|
205 |
\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
|
|
206 |
\ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})";
|
2469
|
207 |
by (fast_tac (!claset addSIs [lam_Least_HH_inj, lam_surj_sing,
|
2493
|
208 |
f_sing_imp_HH_sing]) 1);
|
1123
|
209 |
val f_sing_lam_bij = result();
|
|
210 |
|
|
211 |
goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \
|
1461
|
212 |
\ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})";
|
1123
|
213 |
by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2]
|
2493
|
214 |
addDs [apply_type]) 1);
|
1123
|
215 |
val lam_singI = result();
|
|
216 |
|
2493
|
217 |
val bij_Least_HH_x =
|
|
218 |
(lam_singI RSN (2, [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij]
|
|
219 |
MRS comp_bij)) |> standard;
|