author | wenzelm |
Tue, 22 Apr 1997 11:37:12 +0200 | |
changeset 3007 | e5efa177ee0c |
parent 2925 | b0ae2e13db93 |
child 3207 | fe79ad367d77 |
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 |
||
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2493
diff
changeset
|
14 |
val op addss = op unsafe_addss; |
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2493
diff
changeset
|
15 |
|
435 | 16 |
(** Basic properties of the definitions **) |
17 |
||
789 | 18 |
(*needed?*) |
435 | 19 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def] |
20 |
"!!r. part_ord(A,r) ==> asym(r Int A*A)"; |
|
2925 | 21 |
by (Blast_tac 1); |
760 | 22 |
qed "part_ord_Imp_asym"; |
435 | 23 |
|
789 | 24 |
val major::premx::premy::prems = goalw Order.thy [linear_def] |
25 |
"[| linear(A,r); x:A; y:A; \ |
|
26 |
\ <x,y>:r ==> P; x=y ==> P; <y,x>:r ==> P |] ==> P"; |
|
27 |
by (cut_facts_tac [major,premx,premy] 1); |
|
28 |
by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); |
|
29 |
by (EVERY1 (map etac prems)); |
|
30 |
by (ALLGOALS contr_tac); |
|
31 |
qed "linearE"; |
|
32 |
||
33 |
(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) |
|
34 |
val linear_case_tac = |
|
35 |
SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, |
|
1461 | 36 |
REPEAT_SOME (assume_tac ORELSE' contr_tac)]); |
789 | 37 |
|
38 |
(** General properties of well_ord **) |
|
39 |
||
40 |
goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, |
|
1461 | 41 |
trans_on_def, well_ord_def] |
789 | 42 |
"!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; |
2469 | 43 |
by (asm_simp_tac (!simpset addsimps [wf_on_not_refl]) 1); |
44 |
by (fast_tac (!claset addEs [linearE, wf_on_asym, wf_on_chain3]) 1); |
|
789 | 45 |
qed "well_ordI"; |
46 |
||
47 |
goalw Order.thy [well_ord_def] |
|
48 |
"!!r. well_ord(A,r) ==> wf[A](r)"; |
|
2469 | 49 |
by (safe_tac (!claset)); |
789 | 50 |
qed "well_ord_is_wf"; |
51 |
||
52 |
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] |
|
53 |
"!!r. well_ord(A,r) ==> trans[A](r)"; |
|
2469 | 54 |
by (safe_tac (!claset)); |
789 | 55 |
qed "well_ord_is_trans_on"; |
484 | 56 |
|
789 | 57 |
goalw Order.thy [well_ord_def, tot_ord_def] |
58 |
"!!r. well_ord(A,r) ==> linear(A,r)"; |
|
2925 | 59 |
by (Blast_tac 1); |
789 | 60 |
qed "well_ord_is_linear"; |
61 |
||
62 |
||
63 |
(** Derived rules for pred(A,x,r) **) |
|
64 |
||
65 |
goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A"; |
|
2925 | 66 |
by (Blast_tac 1); |
789 | 67 |
qed "pred_iff"; |
68 |
||
69 |
bind_thm ("predI", conjI RS (pred_iff RS iffD2)); |
|
70 |
||
71 |
val [major,minor] = goalw Order.thy [pred_def] |
|
72 |
"[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P"; |
|
73 |
by (rtac (major RS CollectE) 1); |
|
74 |
by (REPEAT (ares_tac [minor] 1)); |
|
75 |
qed "predE"; |
|
76 |
||
77 |
goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}"; |
|
2925 | 78 |
by (Blast_tac 1); |
789 | 79 |
qed "pred_subset_under"; |
80 |
||
81 |
goalw Order.thy [pred_def] "pred(A,x,r) <= A"; |
|
2925 | 82 |
by (Blast_tac 1); |
789 | 83 |
qed "pred_subset"; |
84 |
||
85 |
goalw Order.thy [pred_def] |
|
86 |
"pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"; |
|
2925 | 87 |
by (Blast_tac 1); |
789 | 88 |
qed "pred_pred_eq"; |
89 |
||
90 |
goalw Order.thy [trans_on_def, pred_def] |
|
91 |
"!!r. [| trans[A](r); <y,x>:r; x:A; y:A \ |
|
92 |
\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"; |
|
2925 | 93 |
by (Blast_tac 1); |
789 | 94 |
qed "trans_pred_pred_eq"; |
95 |
||
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
96 |
|
789 | 97 |
(** The ordering's properties hold over all subsets of its domain |
98 |
[including initial segments of the form pred(A,x,r) **) |
|
484 | 99 |
|
100 |
(*Note: a relation s such that s<=r need not be a partial ordering*) |
|
101 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def] |
|
102 |
"!!A B r. [| part_ord(A,r); B<=A |] ==> part_ord(B,r)"; |
|
2925 | 103 |
by (Blast_tac 1); |
760 | 104 |
qed "part_ord_subset"; |
484 | 105 |
|
106 |
goalw Order.thy [linear_def] |
|
107 |
"!!A B r. [| linear(A,r); B<=A |] ==> linear(B,r)"; |
|
2925 | 108 |
by (Blast_tac 1); |
760 | 109 |
qed "linear_subset"; |
484 | 110 |
|
111 |
goalw Order.thy [tot_ord_def] |
|
112 |
"!!A B r. [| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"; |
|
2469 | 113 |
by (fast_tac (!claset addSEs [part_ord_subset, linear_subset]) 1); |
760 | 114 |
qed "tot_ord_subset"; |
484 | 115 |
|
116 |
goalw Order.thy [well_ord_def] |
|
117 |
"!!A B r. [| well_ord(A,r); B<=A |] ==> well_ord(B,r)"; |
|
2469 | 118 |
by (fast_tac (!claset addSEs [tot_ord_subset, wf_on_subset_A]) 1); |
760 | 119 |
qed "well_ord_subset"; |
484 | 120 |
|
121 |
||
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
122 |
(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **) |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
123 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
124 |
goalw Order.thy [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)"; |
2925 | 125 |
by (Blast_tac 1); |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
126 |
qed "irrefl_Int_iff"; |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
127 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
128 |
goalw Order.thy [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)"; |
2925 | 129 |
by (Blast_tac 1); |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
130 |
qed "trans_on_Int_iff"; |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
131 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
132 |
goalw Order.thy [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)"; |
2469 | 133 |
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
|
134 |
qed "part_ord_Int_iff"; |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
135 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
136 |
goalw Order.thy [linear_def] "linear(A,r Int A*A) <-> linear(A,r)"; |
2925 | 137 |
by (Blast_tac 1); |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
138 |
qed "linear_Int_iff"; |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
139 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
140 |
goalw Order.thy [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)"; |
2469 | 141 |
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
|
142 |
qed "tot_ord_Int_iff"; |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
143 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
144 |
goalw Order.thy [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)"; |
2925 | 145 |
by (Blast_tac 1); |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
146 |
qed "wf_on_Int_iff"; |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
147 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
148 |
goalw Order.thy [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)"; |
2469 | 149 |
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
|
150 |
qed "well_ord_Int_iff"; |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
151 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
152 |
|
848 | 153 |
(** Relations over the Empty Set **) |
154 |
||
155 |
goalw Order.thy [irrefl_def] "irrefl(0,r)"; |
|
2925 | 156 |
by (Blast_tac 1); |
848 | 157 |
qed "irrefl_0"; |
158 |
||
159 |
goalw Order.thy [trans_on_def] "trans[0](r)"; |
|
2925 | 160 |
by (Blast_tac 1); |
848 | 161 |
qed "trans_on_0"; |
162 |
||
163 |
goalw Order.thy [part_ord_def] "part_ord(0,r)"; |
|
2469 | 164 |
by (simp_tac (!simpset addsimps [irrefl_0, trans_on_0]) 1); |
848 | 165 |
qed "part_ord_0"; |
166 |
||
167 |
goalw Order.thy [linear_def] "linear(0,r)"; |
|
2925 | 168 |
by (Blast_tac 1); |
848 | 169 |
qed "linear_0"; |
170 |
||
171 |
goalw Order.thy [tot_ord_def] "tot_ord(0,r)"; |
|
2469 | 172 |
by (simp_tac (!simpset addsimps [part_ord_0, linear_0]) 1); |
848 | 173 |
qed "tot_ord_0"; |
174 |
||
175 |
goalw Order.thy [wf_on_def, wf_def] "wf[0](r)"; |
|
2925 | 176 |
by (Blast_tac 1); |
848 | 177 |
qed "wf_on_0"; |
178 |
||
179 |
goalw Order.thy [well_ord_def] "well_ord(0,r)"; |
|
2469 | 180 |
by (simp_tac (!simpset addsimps [tot_ord_0, wf_on_0]) 1); |
848 | 181 |
qed "well_ord_0"; |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
182 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
183 |
|
789 | 184 |
(** Order-preserving (monotone) maps **) |
185 |
||
186 |
goalw Order.thy [mono_map_def] |
|
187 |
"!!f. f: mono_map(A,r,B,s) ==> f: A->B"; |
|
188 |
by (etac CollectD1 1); |
|
189 |
qed "mono_map_is_fun"; |
|
190 |
||
191 |
goalw Order.thy [mono_map_def, inj_def] |
|
192 |
"!!f. [| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"; |
|
2469 | 193 |
by (step_tac (!claset) 1); |
789 | 194 |
by (linear_case_tac 1); |
195 |
by (REPEAT |
|
196 |
(EVERY [eresolve_tac [wf_on_not_refl RS notE] 1, |
|
1461 | 197 |
etac ssubst 2, |
2469 | 198 |
Fast_tac 2, |
1461 | 199 |
REPEAT (ares_tac [apply_type] 1)])); |
789 | 200 |
qed "mono_map_is_inj"; |
201 |
||
202 |
||
203 |
(** Order-isomorphisms -- or similarities, as Suppes calls them **) |
|
204 |
||
848 | 205 |
val prems = goalw Order.thy [ord_iso_def] |
1461 | 206 |
"[| f: bij(A, B); \ |
207 |
\ !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \ |
|
848 | 208 |
\ |] ==> f: ord_iso(A,r,B,s)"; |
2925 | 209 |
by (blast_tac (!claset addSIs prems) 1); |
848 | 210 |
qed "ord_isoI"; |
211 |
||
789 | 212 |
goalw Order.thy [ord_iso_def, mono_map_def] |
213 |
"!!f. f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"; |
|
2925 | 214 |
by (blast_tac (!claset addSDs [bij_is_fun]) 1); |
789 | 215 |
qed "ord_iso_is_mono_map"; |
435 | 216 |
|
217 |
goalw Order.thy [ord_iso_def] |
|
218 |
"!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; |
|
219 |
by (etac CollectD1 1); |
|
760 | 220 |
qed "ord_iso_is_bij"; |
435 | 221 |
|
789 | 222 |
(*Needed? But ord_iso_converse is!*) |
435 | 223 |
goalw Order.thy [ord_iso_def] |
224 |
"!!f. [| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> \ |
|
225 |
\ <f`x, f`y> : s"; |
|
2925 | 226 |
by (Blast_tac 1); |
760 | 227 |
qed "ord_iso_apply"; |
435 | 228 |
|
229 |
goalw Order.thy [ord_iso_def] |
|
230 |
"!!f. [| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \ |
|
231 |
\ <converse(f) ` x, converse(f) ` y> : r"; |
|
437 | 232 |
by (etac CollectE 1); |
233 |
by (etac (bspec RS bspec RS iffD2) 1); |
|
435 | 234 |
by (REPEAT (eresolve_tac [asm_rl, |
1461 | 235 |
bij_converse_bij RS bij_is_fun RS apply_type] 1)); |
2469 | 236 |
by (asm_simp_tac (!simpset addsimps [right_inverse_bij]) 1); |
760 | 237 |
qed "ord_iso_converse"; |
435 | 238 |
|
812
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
239 |
|
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
240 |
(*Rewriting with bijections and converse (function inverse)*) |
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
241 |
val bij_inverse_ss = |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2493
diff
changeset
|
242 |
!simpset setSolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type, |
2469 | 243 |
bij_converse_bij, comp_fun, comp_bij]) |
244 |
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
|
245 |
|
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
246 |
(** Symmetry and Transitivity Rules **) |
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
247 |
|
848 | 248 |
(*Reflexivity of similarity*) |
249 |
goal Order.thy "id(A): ord_iso(A,r,A,r)"; |
|
250 |
by (resolve_tac [id_bij RS ord_isoI] 1); |
|
2469 | 251 |
by (Asm_simp_tac 1); |
848 | 252 |
qed "ord_iso_refl"; |
253 |
||
254 |
(*Symmetry of similarity*) |
|
769 | 255 |
goalw Order.thy [ord_iso_def] |
256 |
"!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"; |
|
2469 | 257 |
by (fast_tac (!claset addss bij_inverse_ss) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
769
diff
changeset
|
258 |
qed "ord_iso_sym"; |
769 | 259 |
|
848 | 260 |
(*Transitivity of similarity*) |
812
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
261 |
goalw Order.thy [mono_map_def] |
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
262 |
"!!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
|
263 |
\ (f O g): mono_map(A,r,C,t)"; |
2469 | 264 |
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
|
265 |
qed "mono_map_trans"; |
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
266 |
|
bf4b7c37db2c
Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp
parents:
794
diff
changeset
|
267 |
(*Transitivity of similarity: the order-isomorphism relation*) |
789 | 268 |
goalw Order.thy [ord_iso_def] |
269 |
"!!f. [| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \ |
|
270 |
\ (f O g): ord_iso(A,r,C,t)"; |
|
2469 | 271 |
by (fast_tac (!claset addss bij_inverse_ss) 1); |
789 | 272 |
qed "ord_iso_trans"; |
273 |
||
274 |
(** Two monotone maps can make an order-isomorphism **) |
|
275 |
||
276 |
goalw Order.thy [ord_iso_def, mono_map_def] |
|
1461 | 277 |
"!!f g. [| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); \ |
789 | 278 |
\ f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"; |
2469 | 279 |
by (safe_tac (!claset)); |
789 | 280 |
by (REPEAT_FIRST (ares_tac [fg_imp_bijective])); |
2925 | 281 |
by (Blast_tac 1); |
789 | 282 |
by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1); |
2925 | 283 |
by (blast_tac (!claset addIs [apply_funtype]) 2); |
2469 | 284 |
by (asm_full_simp_tac (!simpset addsimps [comp_eq_id_iff RS iffD1]) 1); |
789 | 285 |
qed "mono_ord_isoI"; |
286 |
||
287 |
goal Order.thy |
|
1461 | 288 |
"!!B. [| well_ord(A,r); well_ord(B,s); \ |
289 |
\ f: mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) \ |
|
789 | 290 |
\ |] ==> f: ord_iso(A,r,B,s)"; |
291 |
by (REPEAT (ares_tac [mono_ord_isoI] 1)); |
|
292 |
by (forward_tac [mono_map_is_fun RS fun_is_rel] 1); |
|
293 |
by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1); |
|
294 |
by (DEPTH_SOLVE (ares_tac [mono_map_is_inj, left_comp_inverse] 1 |
|
295 |
ORELSE eresolve_tac [well_ord_is_linear, well_ord_is_wf] 1)); |
|
296 |
qed "well_ord_mono_ord_isoI"; |
|
297 |
||
298 |
||
299 |
(** Order-isomorphisms preserve the ordering's properties **) |
|
300 |
||
301 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, ord_iso_def] |
|
302 |
"!!A B r. [| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"; |
|
2469 | 303 |
by (Asm_simp_tac 1); |
2493 | 304 |
by (fast_tac (!claset addIs [bij_is_fun RS apply_type]) 1); |
789 | 305 |
qed "part_ord_ord_iso"; |
435 | 306 |
|
789 | 307 |
goalw Order.thy [linear_def, ord_iso_def] |
308 |
"!!A B r. [| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"; |
|
2469 | 309 |
by (Asm_simp_tac 1); |
310 |
by (safe_tac (!claset)); |
|
789 | 311 |
by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1); |
2469 | 312 |
by (safe_tac (!claset addSEs [bij_is_fun RS apply_type])); |
789 | 313 |
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
2469 | 314 |
by (asm_full_simp_tac (!simpset addsimps [left_inverse_bij]) 1); |
789 | 315 |
qed "linear_ord_iso"; |
316 |
||
317 |
goalw Order.thy [wf_on_def, wf_def, ord_iso_def] |
|
318 |
"!!A B r. [| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; |
|
319 |
(*reversed &-congruence rule handles context of membership in A*) |
|
2469 | 320 |
by (asm_full_simp_tac (!simpset addcongs [conj_cong2]) 1); |
321 |
by (safe_tac (!claset)); |
|
789 | 322 |
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1); |
2493 | 323 |
by (safe_tac (!claset addSIs [equalityI])); |
2925 | 324 |
by (ALLGOALS (blast_tac |
325 |
(!claset addSDs [equalityD1] addIs [bij_is_fun RS apply_type]))); |
|
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); |
2925 | 346 |
by (Blast_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, |
2925 | 373 |
blast_tac (!claset addSIs [predI]) 2, |
2469 | 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); |
2925 | 387 |
by (blast_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 |
|
2925 | 424 |
val bij_apply_cs = !claset addSIs [bij_converse_bij] |
425 |
addIs [ord_iso_is_bij, bij_is_fun, apply_funtype]; |
|
2469 | 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); |
2925 | 437 |
by (EVERY (map (blast_tac bij_apply_cs) [1,1,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); |
2925 | 448 |
by (REPEAT (blast_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 |
||
2925 | 458 |
goalw Order.thy [ord_iso_map_def] "ord_iso_map(A,r,B,s) <= A*B"; |
459 |
by (Blast_tac 1); |
|
789 | 460 |
qed "ord_iso_map_subset"; |
461 |
||
2925 | 462 |
goalw Order.thy [ord_iso_map_def] "domain(ord_iso_map(A,r,B,s)) <= A"; |
463 |
by (Blast_tac 1); |
|
789 | 464 |
qed "domain_ord_iso_map"; |
465 |
||
2925 | 466 |
goalw Order.thy [ord_iso_map_def] "range(ord_iso_map(A,r,B,s)) <= B"; |
467 |
by (Blast_tac 1); |
|
789 | 468 |
qed "range_ord_iso_map"; |
469 |
||
470 |
goalw Order.thy [ord_iso_map_def] |
|
471 |
"converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"; |
|
2925 | 472 |
by (blast_tac (!claset addIs [ord_iso_sym]) 1); |
789 | 473 |
qed "converse_ord_iso_map"; |
474 |
||
475 |
goalw Order.thy [ord_iso_map_def, function_def] |
|
476 |
"!!B. well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"; |
|
2925 | 477 |
by (blast_tac (!claset addIs [well_ord_iso_pred_eq, |
478 |
ord_iso_sym, ord_iso_trans]) 1); |
|
789 | 479 |
qed "function_ord_iso_map"; |
480 |
||
481 |
goal Order.thy |
|
1461 | 482 |
"!!B. well_ord(B,s) ==> ord_iso_map(A,r,B,s) \ |
789 | 483 |
\ : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"; |
484 |
by (asm_simp_tac |
|
2469 | 485 |
(!simpset addsimps [Pi_iff, function_ord_iso_map, |
1461 | 486 |
ord_iso_map_subset RS domain_times_range]) 1); |
789 | 487 |
qed "ord_iso_map_fun"; |
435 | 488 |
|
789 | 489 |
goalw Order.thy [mono_map_def] |
1461 | 490 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ |
491 |
\ : mono_map(domain(ord_iso_map(A,r,B,s)), r, \ |
|
492 |
\ range(ord_iso_map(A,r,B,s)), s)"; |
|
2469 | 493 |
by (asm_simp_tac (!simpset addsimps [ord_iso_map_fun]) 1); |
494 |
by (safe_tac (!claset)); |
|
789 | 495 |
by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1); |
496 |
by (REPEAT |
|
2925 | 497 |
(blast_tac (!claset addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2)); |
498 |
by (asm_simp_tac |
|
499 |
(!simpset addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1); |
|
1461 | 500 |
by (rewtac ord_iso_map_def); |
2469 | 501 |
by (safe_tac (!claset addSEs [UN_E])); |
1461 | 502 |
by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac); |
789 | 503 |
qed "ord_iso_map_mono_map"; |
435 | 504 |
|
789 | 505 |
goalw Order.thy [mono_map_def] |
1461 | 506 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ |
507 |
\ : ord_iso(domain(ord_iso_map(A,r,B,s)), r, \ |
|
508 |
\ range(ord_iso_map(A,r,B,s)), s)"; |
|
509 |
by (rtac well_ord_mono_ord_isoI 1); |
|
789 | 510 |
by (resolve_tac [converse_ord_iso_map RS subst] 4); |
511 |
by (asm_simp_tac |
|
2469 | 512 |
(!simpset addsimps [ord_iso_map_subset RS converse_converse]) 4); |
789 | 513 |
by (REPEAT (ares_tac [ord_iso_map_mono_map] 3)); |
514 |
by (ALLGOALS (etac well_ord_subset)); |
|
515 |
by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map])); |
|
516 |
qed "ord_iso_map_ord_iso"; |
|
467 | 517 |
|
789 | 518 |
(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) |
519 |
goalw Order.thy [ord_iso_map_def] |
|
1461 | 520 |
"!!B. [| well_ord(A,r); well_ord(B,s); \ |
521 |
\ 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
|
522 |
\ |] ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)"; |
2469 | 523 |
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
|
524 |
(*Case analysis on xaa vs a in r *) |
789 | 525 |
by (forw_inst_tac [("A","A")] well_ord_is_linear 1); |
526 |
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
|
527 |
(*Trivial case: a=xa*) |
2925 | 528 |
by (Blast_tac 2); |
1015
75110179587d
Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
lcp
parents:
990
diff
changeset
|
529 |
(*Harder case: <a, xa>: r*) |
789 | 530 |
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN |
531 |
REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); |
|
532 |
by (forward_tac [ord_iso_restrict_pred] 1 THEN |
|
533 |
REPEAT1 (eresolve_tac [asm_rl, predI] 1)); |
|
534 |
by (asm_full_simp_tac |
|
2469 | 535 |
(!simpset addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); |
2925 | 536 |
by (Blast_tac 1); |
789 | 537 |
qed "domain_ord_iso_map_subset"; |
435 | 538 |
|
789 | 539 |
(*For the 4-way case analysis in the main result*) |
540 |
goal Order.thy |
|
541 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
|
1461 | 542 |
\ domain(ord_iso_map(A,r,B,s)) = A | \ |
789 | 543 |
\ (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"; |
544 |
by (forward_tac [well_ord_is_wf] 1); |
|
545 |
by (rewrite_goals_tac [wf_on_def, wf_def]); |
|
546 |
by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1); |
|
2469 | 547 |
by (step_tac (!claset) 1); |
789 | 548 |
(*The first case: the domain equals A*) |
549 |
by (rtac (domain_ord_iso_map RS equalityI) 1); |
|
550 |
by (etac (Diff_eq_0_iff RS iffD1) 1); |
|
551 |
(*The other case: the domain equals an initial segment*) |
|
552 |
by (swap_res_tac [bexI] 1); |
|
553 |
by (assume_tac 2); |
|
554 |
by (rtac equalityI 1); |
|
2469 | 555 |
(*not (!claset) below; that would use rules like domainE!*) |
2925 | 556 |
by (blast_tac (!claset addSEs [predE]) 2); |
789 | 557 |
by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1)); |
558 |
qed "domain_ord_iso_map_cases"; |
|
467 | 559 |
|
789 | 560 |
(*As above, by duality*) |
561 |
goal Order.thy |
|
1461 | 562 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
563 |
\ range(ord_iso_map(A,r,B,s)) = B | \ |
|
789 | 564 |
\ (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))"; |
565 |
by (resolve_tac [converse_ord_iso_map RS subst] 1); |
|
566 |
by (asm_simp_tac |
|
2469 | 567 |
(!simpset addsimps [range_converse, domain_ord_iso_map_cases]) 1); |
789 | 568 |
qed "range_ord_iso_map_cases"; |
569 |
||
570 |
(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) |
|
571 |
goal Order.thy |
|
1461 | 572 |
"!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
573 |
\ ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) | \ |
|
789 | 574 |
\ (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \ |
575 |
\ (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"; |
|
576 |
by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1); |
|
577 |
by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2); |
|
578 |
by (REPEAT_FIRST (eresolve_tac [asm_rl, disjE, bexE])); |
|
1461 | 579 |
by (ALLGOALS (dtac ord_iso_map_ord_iso THEN' assume_tac THEN' |
2469 | 580 |
asm_full_simp_tac (!simpset addsimps [bexI]))); |
789 | 581 |
by (resolve_tac [wf_on_not_refl RS notE] 1); |
1461 | 582 |
by (etac well_ord_is_wf 1); |
789 | 583 |
by (assume_tac 1); |
584 |
by (subgoal_tac "<x,y>: ord_iso_map(A,r,B,s)" 1); |
|
1461 | 585 |
by (dtac rangeI 1); |
2469 | 586 |
by (asm_full_simp_tac (!simpset addsimps [pred_def]) 1); |
1461 | 587 |
by (rewtac ord_iso_map_def); |
2925 | 588 |
by (Blast_tac 1); |
789 | 589 |
qed "well_ord_trichotomy"; |
467 | 590 |
|
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
591 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
592 |
(*** Properties of converse(r), by Krzysztof Grabczewski ***) |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
593 |
|
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
594 |
goalw Order.thy [irrefl_def] |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
595 |
"!!A. irrefl(A,r) ==> irrefl(A,converse(r))"; |
2925 | 596 |
by (blast_tac (!claset addSIs [converseI]) 1); |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
597 |
qed "irrefl_converse"; |
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 [trans_on_def] |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
600 |
"!!A. trans[A](r) ==> trans[A](converse(r))"; |
2925 | 601 |
by (blast_tac (!claset addSIs [converseI]) 1); |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
602 |
qed "trans_on_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 [part_ord_def] |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
605 |
"!!A. part_ord(A,r) ==> part_ord(A,converse(r))"; |
2925 | 606 |
by (blast_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
|
607 |
qed "part_ord_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 [linear_def] |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
610 |
"!!A. linear(A,r) ==> linear(A,converse(r))"; |
2925 | 611 |
by (blast_tac (!claset addSIs [converseI]) 1); |
836
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
612 |
qed "linear_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 [tot_ord_def] |
627f4842b020
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
lcp
parents:
812
diff
changeset
|
615 |
"!!A. tot_ord(A,r) ==> tot_ord(A,converse(r))"; |
2925 | 616 |
by (blast_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
|
617 |
qed "tot_ord_converse"; |
2469 | 618 |
|
619 |
||
620 |
(** By Krzysztof Grabczewski. |
|
621 |
Lemmas involving the first element of a well ordered set **) |
|
622 |
||
623 |
goalw thy [first_def] "!!b. first(b,B,r) ==> b:B"; |
|
2925 | 624 |
by (Blast_tac 1); |
2469 | 625 |
qed "first_is_elem"; |
626 |
||
627 |
goalw thy [well_ord_def, wf_on_def, wf_def, first_def] |
|
628 |
"!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; |
|
629 |
by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); |
|
630 |
by (contr_tac 1); |
|
631 |
by (etac bexE 1); |
|
632 |
by (res_inst_tac [("a","x")] ex1I 1); |
|
2925 | 633 |
by (Blast_tac 2); |
2469 | 634 |
by (rewrite_goals_tac [tot_ord_def, linear_def]); |
2925 | 635 |
by (Blast.depth_tac (!claset) 7 1); |
2469 | 636 |
qed "well_ord_imp_ex1_first"; |
637 |
||
638 |
goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"; |
|
639 |
by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1)); |
|
640 |
by (rtac first_is_elem 1); |
|
641 |
by (etac theI 1); |
|
642 |
qed "the_first_in"; |