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