author | lcp |
Fri, 16 Dec 1994 13:43:01 +0100 | |
changeset 794 | 349d41ffa378 |
parent 789 | 30bdc59198ff |
child 812 | bf4b7c37db2c |
permissions | -rw-r--r-- |
435 | 1 |
(* Title: ZF/Order.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
789 | 6 |
Orders in Zermelo-Fraenkel Set Theory |
7 |
||
8 |
Results from the book "Set Theory: an Introduction to Independence Proofs" |
|
9 |
by Ken Kunen. Chapter 1, section 6. |
|
435 | 10 |
*) |
11 |
||
12 |
open Order; |
|
13 |
||
14 |
val bij_apply_cs = ZF_cs addSEs [bij_converse_bij] |
|
15 |
addIs [bij_is_fun, apply_type]; |
|
16 |
||
17 |
(** Basic properties of the definitions **) |
|
18 |
||
789 | 19 |
(*needed?*) |
435 | 20 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def] |
21 |
"!!r. part_ord(A,r) ==> asym(r Int A*A)"; |
|
22 |
by (fast_tac ZF_cs 1); |
|
760 | 23 |
qed "part_ord_Imp_asym"; |
435 | 24 |
|
789 | 25 |
val major::premx::premy::prems = goalw Order.thy [linear_def] |
26 |
"[| linear(A,r); x:A; y:A; \ |
|
27 |
\ <x,y>:r ==> P; x=y ==> P; <y,x>:r ==> P |] ==> P"; |
|
28 |
by (cut_facts_tac [major,premx,premy] 1); |
|
29 |
by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); |
|
30 |
by (EVERY1 (map etac prems)); |
|
31 |
by (ALLGOALS contr_tac); |
|
32 |
qed "linearE"; |
|
33 |
||
34 |
(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) |
|
35 |
val linear_case_tac = |
|
36 |
SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, |
|
37 |
REPEAT_SOME (assume_tac ORELSE' contr_tac)]); |
|
38 |
||
39 |
(** General properties of well_ord **) |
|
40 |
||
41 |
goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, |
|
42 |
trans_on_def, well_ord_def] |
|
43 |
"!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; |
|
44 |
by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1); |
|
45 |
by (safe_tac ZF_cs); |
|
46 |
by (linear_case_tac 1); |
|
47 |
(*case x=xb*) |
|
48 |
by (fast_tac (ZF_cs addSEs [wf_on_asym]) 1); |
|
49 |
(*case x<xb*) |
|
50 |
by (fast_tac (ZF_cs addSEs [wf_on_chain3]) 1); |
|
51 |
qed "well_ordI"; |
|
52 |
||
53 |
goalw Order.thy [well_ord_def] |
|
54 |
"!!r. well_ord(A,r) ==> wf[A](r)"; |
|
55 |
by (safe_tac ZF_cs); |
|
56 |
qed "well_ord_is_wf"; |
|
57 |
||
58 |
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] |
|
59 |
"!!r. well_ord(A,r) ==> trans[A](r)"; |
|
60 |
by (safe_tac ZF_cs); |
|
61 |
qed "well_ord_is_trans_on"; |
|
484 | 62 |
|
789 | 63 |
goalw Order.thy [well_ord_def, tot_ord_def] |
64 |
"!!r. well_ord(A,r) ==> linear(A,r)"; |
|
65 |
by (fast_tac ZF_cs 1); |
|
66 |
qed "well_ord_is_linear"; |
|
67 |
||
68 |
||
69 |
(** Derived rules for pred(A,x,r) **) |
|
70 |
||
71 |
goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A"; |
|
72 |
by (fast_tac ZF_cs 1); |
|
73 |
qed "pred_iff"; |
|
74 |
||
75 |
bind_thm ("predI", conjI RS (pred_iff RS iffD2)); |
|
76 |
||
77 |
val [major,minor] = goalw Order.thy [pred_def] |
|
78 |
"[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P"; |
|
79 |
by (rtac (major RS CollectE) 1); |
|
80 |
by (REPEAT (ares_tac [minor] 1)); |
|
81 |
qed "predE"; |
|
82 |
||
83 |
goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}"; |
|
84 |
by (fast_tac ZF_cs 1); |
|
85 |
qed "pred_subset_under"; |
|
86 |
||
87 |
goalw Order.thy [pred_def] "pred(A,x,r) <= A"; |
|
88 |
by (fast_tac ZF_cs 1); |
|
89 |
qed "pred_subset"; |
|
90 |
||
91 |
goalw Order.thy [pred_def] |
|
92 |
"pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"; |
|
93 |
by (fast_tac eq_cs 1); |
|
94 |
qed "pred_pred_eq"; |
|
95 |
||
96 |
goalw Order.thy [trans_on_def, pred_def] |
|
97 |
"!!r. [| trans[A](r); <y,x>:r; x:A; y:A \ |
|
98 |
\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"; |
|
99 |
by (fast_tac eq_cs 1); |
|
100 |
qed "trans_pred_pred_eq"; |
|
101 |
||
102 |
(** The ordering's properties hold over all subsets of its domain |
|
103 |
[including initial segments of the form pred(A,x,r) **) |
|
484 | 104 |
|
105 |
(*Note: a relation s such that s<=r need not be a partial ordering*) |
|
106 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def] |
|
107 |
"!!A B r. [| part_ord(A,r); B<=A |] ==> part_ord(B,r)"; |
|
108 |
by (fast_tac ZF_cs 1); |
|
760 | 109 |
qed "part_ord_subset"; |
484 | 110 |
|
111 |
goalw Order.thy [linear_def] |
|
112 |
"!!A B r. [| linear(A,r); B<=A |] ==> linear(B,r)"; |
|
113 |
by (fast_tac ZF_cs 1); |
|
760 | 114 |
qed "linear_subset"; |
484 | 115 |
|
116 |
goalw Order.thy [tot_ord_def] |
|
117 |
"!!A B r. [| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"; |
|
118 |
by (fast_tac (ZF_cs addSEs [part_ord_subset, linear_subset]) 1); |
|
760 | 119 |
qed "tot_ord_subset"; |
484 | 120 |
|
121 |
goalw Order.thy [well_ord_def] |
|
122 |
"!!A B r. [| well_ord(A,r); B<=A |] ==> well_ord(B,r)"; |
|
123 |
by (fast_tac (ZF_cs addSEs [tot_ord_subset, wf_on_subset_A]) 1); |
|
760 | 124 |
qed "well_ord_subset"; |
484 | 125 |
|
126 |
||
789 | 127 |
(** Order-preserving (monotone) maps **) |
128 |
||
129 |
(*Rewriting with bijections and converse (function inverse)*) |
|
130 |
val bij_inverse_ss = |
|
131 |
ZF_ss setsolver (type_auto_tac [bij_is_fun, apply_type, |
|
132 |
bij_converse_bij, comp_fun, comp_bij]) |
|
133 |
addsimps [right_inverse_bij, left_inverse_bij, comp_fun_apply]; |
|
134 |
||
135 |
goalw Order.thy [mono_map_def] |
|
136 |
"!!f. f: mono_map(A,r,B,s) ==> f: A->B"; |
|
137 |
by (etac CollectD1 1); |
|
138 |
qed "mono_map_is_fun"; |
|
139 |
||
140 |
goalw Order.thy [mono_map_def, inj_def] |
|
141 |
"!!f. [| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"; |
|
142 |
by (step_tac ZF_cs 1); |
|
143 |
by (linear_case_tac 1); |
|
144 |
by (REPEAT |
|
145 |
(EVERY [eresolve_tac [wf_on_not_refl RS notE] 1, |
|
146 |
eresolve_tac [ssubst] 2, |
|
147 |
fast_tac ZF_cs 2, |
|
148 |
REPEAT (ares_tac [apply_type] 1)])); |
|
149 |
qed "mono_map_is_inj"; |
|
150 |
||
151 |
(*Transitivity of similarity: the order-isomorphism relation*) |
|
152 |
goalw Order.thy [mono_map_def] |
|
153 |
"!!f. [| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ==> \ |
|
154 |
\ (f O g): mono_map(A,r,C,t)"; |
|
155 |
by (safe_tac ZF_cs); |
|
156 |
by (ALLGOALS (asm_full_simp_tac bij_inverse_ss)); |
|
157 |
qed "mono_map_trans"; |
|
158 |
||
159 |
||
160 |
(** Order-isomorphisms -- or similarities, as Suppes calls them **) |
|
161 |
||
162 |
goalw Order.thy [ord_iso_def, mono_map_def] |
|
163 |
"!!f. f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"; |
|
164 |
by (fast_tac (ZF_cs addSDs [bij_is_fun]) 1); |
|
165 |
qed "ord_iso_is_mono_map"; |
|
435 | 166 |
|
167 |
goalw Order.thy [ord_iso_def] |
|
168 |
"!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; |
|
169 |
by (etac CollectD1 1); |
|
760 | 170 |
qed "ord_iso_is_bij"; |
435 | 171 |
|
789 | 172 |
(*Needed? But ord_iso_converse is!*) |
435 | 173 |
goalw Order.thy [ord_iso_def] |
174 |
"!!f. [| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> \ |
|
175 |
\ <f`x, f`y> : s"; |
|
176 |
by (fast_tac ZF_cs 1); |
|
760 | 177 |
qed "ord_iso_apply"; |
435 | 178 |
|
179 |
goalw Order.thy [ord_iso_def] |
|
180 |
"!!f. [| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \ |
|
181 |
\ <converse(f) ` x, converse(f) ` y> : r"; |
|
437 | 182 |
by (etac CollectE 1); |
183 |
by (etac (bspec RS bspec RS iffD2) 1); |
|
435 | 184 |
by (REPEAT (eresolve_tac [asm_rl, |
185 |
bij_converse_bij RS bij_is_fun RS apply_type] 1)); |
|
186 |
by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); |
|
760 | 187 |
qed "ord_iso_converse"; |
435 | 188 |
|
789 | 189 |
(*Symmetry of similarity: the order-isomorphism relation*) |
769 | 190 |
goalw Order.thy [ord_iso_def] |
191 |
"!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"; |
|
192 |
by (safe_tac ZF_cs); |
|
789 | 193 |
by (ALLGOALS (asm_full_simp_tac bij_inverse_ss)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
769
diff
changeset
|
194 |
qed "ord_iso_sym"; |
769 | 195 |
|
789 | 196 |
(*Transitivity of similarity: the order-isomorphism relation*) |
197 |
goalw Order.thy [ord_iso_def] |
|
198 |
"!!f. [| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \ |
|
199 |
\ (f O g): ord_iso(A,r,C,t)"; |
|
200 |
by (safe_tac ZF_cs); |
|
201 |
by (ALLGOALS (asm_full_simp_tac bij_inverse_ss)); |
|
202 |
qed "ord_iso_trans"; |
|
203 |
||
204 |
(** Two monotone maps can make an order-isomorphism **) |
|
205 |
||
206 |
goalw Order.thy [ord_iso_def, mono_map_def] |
|
207 |
"!!f g. [| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); \ |
|
208 |
\ f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"; |
|
209 |
by (safe_tac ZF_cs); |
|
210 |
by (REPEAT_FIRST (ares_tac [fg_imp_bijective])); |
|
211 |
by (fast_tac ZF_cs 1); |
|
212 |
by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1); |
|
213 |
by (fast_tac (ZF_cs addIs [apply_type] addSEs [bspec RS bspec RS mp]) 2); |
|
214 |
by (asm_full_simp_tac |
|
215 |
(ZF_ss addsimps [comp_eq_id_iff RS iffD1]) 1); |
|
216 |
qed "mono_ord_isoI"; |
|
217 |
||
218 |
goal Order.thy |
|
219 |
"!!B. [| well_ord(A,r); well_ord(B,s); \ |
|
220 |
\ f: mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) \ |
|
221 |
\ |] ==> f: ord_iso(A,r,B,s)"; |
|
222 |
by (REPEAT (ares_tac [mono_ord_isoI] 1)); |
|
223 |
by (forward_tac [mono_map_is_fun RS fun_is_rel] 1); |
|
224 |
by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1); |
|
225 |
by (DEPTH_SOLVE (ares_tac [mono_map_is_inj, left_comp_inverse] 1 |
|
226 |
ORELSE eresolve_tac [well_ord_is_linear, well_ord_is_wf] 1)); |
|
227 |
qed "well_ord_mono_ord_isoI"; |
|
228 |
||
229 |
||
230 |
(** Order-isomorphisms preserve the ordering's properties **) |
|
231 |
||
232 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, ord_iso_def] |
|
233 |
"!!A B r. [| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"; |
|
234 |
by (asm_simp_tac ZF_ss 1); |
|
235 |
by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1); |
|
236 |
qed "part_ord_ord_iso"; |
|
435 | 237 |
|
789 | 238 |
goalw Order.thy [linear_def, ord_iso_def] |
239 |
"!!A B r. [| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"; |
|
240 |
by (asm_simp_tac ZF_ss 1); |
|
241 |
by (safe_tac ZF_cs); |
|
242 |
by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1); |
|
243 |
by (safe_tac (ZF_cs addSEs [bij_is_fun RS apply_type])); |
|
244 |
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
|
245 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
246 |
qed "linear_ord_iso"; |
|
247 |
||
248 |
goalw Order.thy [wf_on_def, wf_def, ord_iso_def] |
|
249 |
"!!A B r. [| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; |
|
250 |
(*reversed &-congruence rule handles context of membership in A*) |
|
251 |
by (asm_full_simp_tac (ZF_ss addcongs [conj_cong2]) 1); |
|
252 |
by (safe_tac ZF_cs); |
|
253 |
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1); |
|
254 |
by (safe_tac eq_cs); |
|
255 |
by (dtac equalityD1 1); |
|
256 |
by (fast_tac (ZF_cs addSIs [bexI]) 1); |
|
257 |
by (fast_tac (ZF_cs addSIs [bexI] |
|
258 |
addIs [bij_is_fun RS apply_type]) 1); |
|
259 |
qed "wf_on_ord_iso"; |
|
260 |
||
261 |
goalw Order.thy [well_ord_def, tot_ord_def] |
|
262 |
"!!A B r. [| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"; |
|
263 |
by (fast_tac |
|
264 |
(ZF_cs addSEs [part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso]) 1); |
|
265 |
qed "well_ord_ord_iso"; |
|
266 |
||
267 |
||
268 |
(*** Main results of Kunen, Chapter 1 section 6 ***) |
|
435 | 269 |
|
270 |
(*Inductive argument for proving Kunen's Lemma 6.1*) |
|
271 |
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def, pred_def] |
|
272 |
"!!r. [| well_ord(A,r); x: A; f: ord_iso(A, r, pred(A,x,r), r); y: A |] \ |
|
273 |
\ ==> f`y = y"; |
|
274 |
by (safe_tac ZF_cs); |
|
275 |
by (wf_on_ind_tac "y" [] 1); |
|
276 |
by (forward_tac [ord_iso_is_bij] 1); |
|
277 |
by (subgoal_tac "f`y1 : {y: A . <y, x> : r}" 1); |
|
278 |
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]) 2); |
|
279 |
(*Now we know f`y1 : A and <f`y1, x> : r *) |
|
280 |
by (etac CollectE 1); |
|
281 |
by (linear_case_tac 1); |
|
282 |
(*Case <f`y1, y1> : r *) (*use induction hyp*) |
|
283 |
by (dtac bspec 1 THEN mp_tac 2 THEN assume_tac 1); |
|
284 |
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
|
285 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
286 |
(*The case <y1, f`y1> : r *) |
|
287 |
by (subgoal_tac "<y1,x> : r" 1); |
|
288 |
by (fast_tac (ZF_cs addSEs [trans_onD]) 2); |
|
289 |
by (dtac ord_iso_converse 1 THEN assume_tac 1 THEN fast_tac ZF_cs 2); |
|
290 |
by (fast_tac ZF_cs 1); |
|
291 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
292 |
(*now use induction hyp*) |
|
293 |
by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
294 |
by (dres_inst_tac [("t", "op `(f)")] subst_context 1); |
|
295 |
by (asm_full_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); |
|
760 | 296 |
qed "not_well_ord_iso_pred_lemma"; |
435 | 297 |
|
298 |
||
299 |
(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment |
|
300 |
of a well-ordering*) |
|
301 |
goal Order.thy |
|
789 | 302 |
"!!r. [| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P"; |
435 | 303 |
by (metacut_tac not_well_ord_iso_pred_lemma 1); |
789 | 304 |
by (REPEAT_FIRST assume_tac); |
435 | 305 |
(*Now we know f`x = x*) |
306 |
by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type), |
|
307 |
assume_tac]); |
|
308 |
(*Now we know f`x : pred(A,x,r) *) |
|
309 |
by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1); |
|
310 |
by (fast_tac (ZF_cs addSEs [wf_on_not_refl RS notE]) 1); |
|
789 | 311 |
qed "well_ord_iso_predE"; |
312 |
||
313 |
(*Simple consequence of Lemma 6.1*) |
|
314 |
goal Order.thy |
|
315 |
"!!r. [| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \ |
|
316 |
\ a:A; c:A |] ==> a=c"; |
|
317 |
by (forward_tac [well_ord_is_trans_on] 1); |
|
318 |
by (forward_tac [well_ord_is_linear] 1); |
|
319 |
by (linear_case_tac 1); |
|
320 |
by (dtac ord_iso_sym 1); |
|
321 |
by (REPEAT (*because there are two symmetric cases*) |
|
322 |
(EVERY [eresolve_tac [pred_subset RSN (2, well_ord_subset) RS |
|
323 |
well_ord_iso_predE] 1, |
|
324 |
fast_tac (ZF_cs addSIs [predI]) 2, |
|
325 |
asm_simp_tac (ZF_ss addsimps [trans_pred_pred_eq]) 1])); |
|
326 |
qed "well_ord_iso_pred_eq"; |
|
327 |
||
328 |
(*Does not assume r is a wellordering!*) |
|
329 |
goalw Order.thy [ord_iso_def, pred_def] |
|
330 |
"!!r. [| f : ord_iso(A,r,B,s); a:A |] ==> \ |
|
331 |
\ f `` pred(A,a,r) = pred(B, f`a, s)"; |
|
332 |
by (etac CollectE 1); |
|
333 |
by (asm_simp_tac |
|
334 |
(ZF_ss addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1); |
|
335 |
by (safe_tac (eq_cs addSEs [bij_is_fun RS apply_type])); |
|
336 |
by (resolve_tac [RepFun_eqI] 1); |
|
337 |
by (fast_tac (ZF_cs addSIs [right_inverse_bij RS sym]) 1); |
|
338 |
by (asm_simp_tac |
|
339 |
(ZF_ss addsimps [right_inverse_bij] |
|
340 |
setsolver type_auto_tac |
|
341 |
[bij_is_fun, apply_funtype, bij_converse_bij]) 1); |
|
342 |
qed "ord_iso_image_pred"; |
|
435 | 343 |
|
789 | 344 |
(*But in use, A and B may themselves be initial segments. Then use |
345 |
trans_pred_pred_eq to simplify the pred(pred...) terms. See just below.*) |
|
346 |
goal Order.thy |
|
347 |
"!!r. [| f : ord_iso(A,r,B,s); a:A |] ==> \ |
|
348 |
\ restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"; |
|
349 |
by (asm_simp_tac (ZF_ss addsimps [ord_iso_image_pred RS sym]) 1); |
|
350 |
by (rewrite_goals_tac [ord_iso_def]); |
|
351 |
by (step_tac ZF_cs 1); |
|
352 |
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 2); |
|
353 |
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 2); |
|
354 |
by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1); |
|
355 |
qed "ord_iso_restrict_pred"; |
|
356 |
||
357 |
(*Tricky; a lot of forward proof!*) |
|
358 |
goal Order.thy |
|
359 |
"!!r. [| well_ord(A,r); well_ord(B,s); <a,c>: r; \ |
|
360 |
\ f : ord_iso(pred(A,a,r), r, pred(B,b,s), s); \ |
|
361 |
\ g : ord_iso(pred(A,c,r), r, pred(B,d,s), s); \ |
|
362 |
\ a:A; c:A; b:B; d:B |] ==> <b,d>: s"; |
|
363 |
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN |
|
364 |
REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); |
|
365 |
by (subgoal_tac "b = g`a" 1); |
|
366 |
by (asm_simp_tac ZF_ss 1); |
|
367 |
by (resolve_tac [well_ord_iso_pred_eq] 1); |
|
368 |
by (REPEAT_SOME assume_tac); |
|
369 |
by (forward_tac [ord_iso_restrict_pred] 1 THEN |
|
370 |
REPEAT1 (eresolve_tac [asm_rl, predI] 1)); |
|
371 |
by (asm_full_simp_tac |
|
372 |
(ZF_ss addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); |
|
373 |
by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1); |
|
374 |
by (assume_tac 1); |
|
375 |
qed "well_ord_iso_preserving"; |
|
435 | 376 |
|
377 |
(*Inductive argument for proving Kunen's Lemma 6.2*) |
|
378 |
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] |
|
379 |
"!!r. [| well_ord(A,r); well_ord(B,s); \ |
|
380 |
\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \ |
|
381 |
\ ==> f`y = g`y"; |
|
382 |
by (safe_tac ZF_cs); |
|
383 |
by (wf_on_ind_tac "y" [] 1); |
|
384 |
by (subgoals_tac ["f: bij(A,B)", "g: bij(A,B)", "f`y1 : B", "g`y1 : B"] 1); |
|
385 |
by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 2)); |
|
386 |
by (linear_case_tac 1); |
|
387 |
(*The case <f`y1, g`y1> : s *) |
|
388 |
by (forw_inst_tac [("f","g")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); |
|
389 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
390 |
by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
391 |
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
|
392 |
by (dres_inst_tac [("t", "op `(g)")] subst_context 1); |
|
393 |
by (asm_full_simp_tac bij_inverse_ss 1); |
|
394 |
(*The case <g`y1, f`y1> : s *) |
|
395 |
by (forw_inst_tac [("f","f")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); |
|
396 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
397 |
by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
398 |
by (dres_inst_tac [("t", "op `(converse(g))")] subst_context 1); |
|
399 |
by (dres_inst_tac [("t", "op `(f)")] subst_context 1); |
|
400 |
by (asm_full_simp_tac bij_inverse_ss 1); |
|
760 | 401 |
qed "well_ord_iso_unique_lemma"; |
435 | 402 |
|
403 |
(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) |
|
404 |
goal Order.thy |
|
789 | 405 |
"!!r. [| well_ord(B,s); \ |
435 | 406 |
\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g"; |
437 | 407 |
by (rtac fun_extension 1); |
408 |
by (etac (ord_iso_is_bij RS bij_is_fun) 1); |
|
409 |
by (etac (ord_iso_is_bij RS bij_is_fun) 1); |
|
410 |
by (rtac well_ord_iso_unique_lemma 1); |
|
789 | 411 |
by (REPEAT_SOME (eresolve_tac [asm_rl, well_ord_ord_iso])); |
760 | 412 |
qed "well_ord_iso_unique"; |
435 | 413 |
|
414 |
||
789 | 415 |
(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **) |
416 |
||
417 |
goalw Order.thy [ord_iso_map_def] |
|
418 |
"ord_iso_map(A,r,B,s) <= A*B"; |
|
419 |
by (fast_tac ZF_cs 1); |
|
420 |
qed "ord_iso_map_subset"; |
|
421 |
||
422 |
goalw Order.thy [ord_iso_map_def] |
|
423 |
"domain(ord_iso_map(A,r,B,s)) <= A"; |
|
424 |
by (fast_tac ZF_cs 1); |
|
425 |
qed "domain_ord_iso_map"; |
|
426 |
||
427 |
goalw Order.thy [ord_iso_map_def] |
|
428 |
"range(ord_iso_map(A,r,B,s)) <= B"; |
|
429 |
by (fast_tac ZF_cs 1); |
|
430 |
qed "range_ord_iso_map"; |
|
431 |
||
432 |
goalw Order.thy [ord_iso_map_def] |
|
433 |
"converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"; |
|
434 |
by (fast_tac (eq_cs addIs [ord_iso_sym]) 1); |
|
435 |
qed "converse_ord_iso_map"; |
|
436 |
||
437 |
goalw Order.thy [ord_iso_map_def, function_def] |
|
438 |
"!!B. well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"; |
|
435 | 439 |
by (safe_tac ZF_cs); |
789 | 440 |
by (resolve_tac [well_ord_iso_pred_eq] 1); |
441 |
by (REPEAT_SOME assume_tac); |
|
442 |
by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1); |
|
443 |
by (assume_tac 1); |
|
444 |
qed "function_ord_iso_map"; |
|
445 |
||
446 |
goal Order.thy |
|
447 |
"!!B. well_ord(B,s) ==> ord_iso_map(A,r,B,s) \ |
|
448 |
\ : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"; |
|
449 |
by (asm_simp_tac |
|
450 |
(ZF_ss addsimps [Pi_iff, function_ord_iso_map, |
|
451 |
ord_iso_map_subset RS domain_times_range]) 1); |
|
452 |
qed "ord_iso_map_fun"; |
|
435 | 453 |
|
789 | 454 |
goalw Order.thy [mono_map_def] |
455 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ |
|
456 |
\ : mono_map(domain(ord_iso_map(A,r,B,s)), r, \ |
|
457 |
\ range(ord_iso_map(A,r,B,s)), s)"; |
|
458 |
by (asm_simp_tac (ZF_ss addsimps [ord_iso_map_fun]) 1); |
|
435 | 459 |
by (safe_tac ZF_cs); |
789 | 460 |
by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1); |
461 |
by (REPEAT |
|
462 |
(fast_tac (ZF_cs addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2)); |
|
463 |
by (asm_simp_tac (ZF_ss addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1); |
|
464 |
by (rewrite_goals_tac [ord_iso_map_def]); |
|
465 |
by (safe_tac (ZF_cs addSEs [UN_E])); |
|
466 |
by (resolve_tac [well_ord_iso_preserving] 1 THEN REPEAT_FIRST assume_tac); |
|
467 |
qed "ord_iso_map_mono_map"; |
|
435 | 468 |
|
789 | 469 |
goalw Order.thy [mono_map_def] |
470 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ |
|
471 |
\ : ord_iso(domain(ord_iso_map(A,r,B,s)), r, \ |
|
472 |
\ range(ord_iso_map(A,r,B,s)), s)"; |
|
473 |
by (resolve_tac [well_ord_mono_ord_isoI] 1); |
|
474 |
by (resolve_tac [converse_ord_iso_map RS subst] 4); |
|
475 |
by (asm_simp_tac |
|
476 |
(ZF_ss addsimps [ord_iso_map_subset RS converse_converse, |
|
477 |
domain_converse, range_converse]) 4); |
|
478 |
by (REPEAT (ares_tac [ord_iso_map_mono_map] 3)); |
|
479 |
by (ALLGOALS (etac well_ord_subset)); |
|
480 |
by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map])); |
|
481 |
qed "ord_iso_map_ord_iso"; |
|
467 | 482 |
|
789 | 483 |
(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) |
484 |
goalw Order.thy [ord_iso_map_def] |
|
485 |
"!!B. [| well_ord(A,r); well_ord(B,s); \ |
|
486 |
\ x: A; x ~: domain(ord_iso_map(A,r,B,s)) \ |
|
487 |
\ |] ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, x, r)"; |
|
488 |
by (step_tac (ZF_cs addSIs [predI]) 1); |
|
489 |
(*Case analysis on xaa vs x in r *) |
|
490 |
by (forw_inst_tac [("A","A")] well_ord_is_linear 1); |
|
491 |
by (linear_case_tac 1); |
|
492 |
(*Trivial case: xaa=x*) |
|
435 | 493 |
by (fast_tac ZF_cs 1); |
789 | 494 |
(*Harder case: <x, xaa>: r*) |
495 |
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN |
|
496 |
REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); |
|
497 |
by (forward_tac [ord_iso_restrict_pred] 1 THEN |
|
498 |
REPEAT1 (eresolve_tac [asm_rl, predI] 1)); |
|
499 |
by (asm_full_simp_tac |
|
500 |
(ZF_ss addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); |
|
501 |
by (fast_tac ZF_cs 1); |
|
502 |
qed "domain_ord_iso_map_subset"; |
|
435 | 503 |
|
789 | 504 |
(*For the 4-way case analysis in the main result*) |
505 |
goal Order.thy |
|
506 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
|
507 |
\ domain(ord_iso_map(A,r,B,s)) = A | \ |
|
508 |
\ (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"; |
|
509 |
by (forward_tac [well_ord_is_wf] 1); |
|
510 |
by (rewrite_goals_tac [wf_on_def, wf_def]); |
|
511 |
by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1); |
|
512 |
by (step_tac ZF_cs 1); |
|
513 |
(*The first case: the domain equals A*) |
|
514 |
by (rtac (domain_ord_iso_map RS equalityI) 1); |
|
515 |
by (etac (Diff_eq_0_iff RS iffD1) 1); |
|
516 |
(*The other case: the domain equals an initial segment*) |
|
517 |
by (swap_res_tac [bexI] 1); |
|
518 |
by (assume_tac 2); |
|
519 |
by (rtac equalityI 1); |
|
520 |
(*not ZF_cs below; that would use rules like domainE!*) |
|
521 |
by (fast_tac (pair_cs addSEs [predE]) 2); |
|
522 |
by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1)); |
|
523 |
qed "domain_ord_iso_map_cases"; |
|
467 | 524 |
|
789 | 525 |
(*As above, by duality*) |
526 |
goal Order.thy |
|
527 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
|
528 |
\ range(ord_iso_map(A,r,B,s)) = B | \ |
|
529 |
\ (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))"; |
|
530 |
by (resolve_tac [converse_ord_iso_map RS subst] 1); |
|
531 |
by (asm_simp_tac |
|
532 |
(ZF_ss addsimps [range_converse, domain_ord_iso_map_cases]) 1); |
|
533 |
qed "range_ord_iso_map_cases"; |
|
534 |
||
535 |
(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) |
|
536 |
goal Order.thy |
|
537 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
|
538 |
\ ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) | \ |
|
539 |
\ (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \ |
|
540 |
\ (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"; |
|
541 |
by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1); |
|
542 |
by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2); |
|
543 |
by (REPEAT_FIRST (eresolve_tac [asm_rl, disjE, bexE])); |
|
544 |
by (ALLGOALS (dresolve_tac [ord_iso_map_ord_iso] THEN' assume_tac THEN' |
|
545 |
asm_full_simp_tac (ZF_ss addsimps [bexI]))); |
|
546 |
||
547 |
by (resolve_tac [wf_on_not_refl RS notE] 1); |
|
548 |
by (eresolve_tac [well_ord_is_wf] 1); |
|
549 |
by (assume_tac 1); |
|
550 |
by (subgoal_tac "<x,y>: ord_iso_map(A,r,B,s)" 1); |
|
551 |
by (dresolve_tac [rangeI] 1); |
|
552 |
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); |
|
553 |
by (rewrite_goals_tac [ord_iso_map_def]); |
|
467 | 554 |
by (fast_tac ZF_cs 1); |
789 | 555 |
qed "well_ord_trichotomy"; |
467 | 556 |