src/ZF/Order.thy
 author wenzelm Thu Sep 02 00:48:07 2010 +0200 (2010-09-02) changeset 38980 af73cf0dc31f parent 32960 69916a850301 child 46820 c656222c4dc1 permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
1 (*  Title:      ZF/Order.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1994  University of Cambridge
5 Results from the book "Set Theory: an Introduction to Independence Proofs"
6         by Kenneth Kunen.  Chapter 1, section 6.
7 Additional definitions and lemmas for reflexive orders.
8 *)
10 header{*Partial and Total Orderings: Basic Definitions and Properties*}
12 theory Order imports WF Perm begin
14 text {* We adopt the following convention: @{text ord} is used for
15   strict orders and @{text order} is used for their reflexive
16   counterparts. *}
18 definition
19   part_ord :: "[i,i]=>o"                (*Strict partial ordering*)  where
20    "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
22 definition
23   linear   :: "[i,i]=>o"                (*Strict total ordering*)  where
24    "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
26 definition
27   tot_ord  :: "[i,i]=>o"                (*Strict total ordering*)  where
28    "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
30 definition
31   "preorder_on(A, r) \<equiv> refl(A, r) \<and> trans[A](r)"
33 definition                              (*Partial ordering*)
34   "partial_order_on(A, r) \<equiv> preorder_on(A, r) \<and> antisym(r)"
36 abbreviation
37   "Preorder(r) \<equiv> preorder_on(field(r), r)"
39 abbreviation
40   "Partial_order(r) \<equiv> partial_order_on(field(r), r)"
42 definition
43   well_ord :: "[i,i]=>o"                (*Well-ordering*)  where
44    "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
46 definition
47   mono_map :: "[i,i,i,i]=>i"            (*Order-preserving maps*)  where
48    "mono_map(A,r,B,s) ==
49               {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
51 definition
52   ord_iso  :: "[i,i,i,i]=>i"            (*Order isomorphisms*)  where
53    "ord_iso(A,r,B,s) ==
54               {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
56 definition
57   pred     :: "[i,i,i]=>i"              (*Set of predecessors*)  where
58    "pred(A,x,r) == {y:A. <y,x>:r}"
60 definition
61   ord_iso_map :: "[i,i,i,i]=>i"         (*Construction for linearity theorem*)  where
62    "ord_iso_map(A,r,B,s) ==
63      \<Union>x\<in>A. \<Union>y\<in>B. \<Union>f \<in> ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
65 definition
66   first :: "[i, i, i] => o"  where
67     "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
70 notation (xsymbols)
71   ord_iso  ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
74 subsection{*Immediate Consequences of the Definitions*}
76 lemma part_ord_Imp_asym:
77     "part_ord(A,r) ==> asym(r Int A*A)"
78 by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
80 lemma linearE:
81     "[| linear(A,r);  x:A;  y:A;
82         <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |]
83      ==> P"
84 by (simp add: linear_def, blast)
87 (** General properties of well_ord **)
89 lemma well_ordI:
90     "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"
91 apply (simp add: irrefl_def part_ord_def tot_ord_def
92                  trans_on_def well_ord_def wf_on_not_refl)
93 apply (fast elim: linearE wf_on_asym wf_on_chain3)
94 done
96 lemma well_ord_is_wf:
97     "well_ord(A,r) ==> wf[A](r)"
98 by (unfold well_ord_def, safe)
100 lemma well_ord_is_trans_on:
101     "well_ord(A,r) ==> trans[A](r)"
102 by (unfold well_ord_def tot_ord_def part_ord_def, safe)
104 lemma well_ord_is_linear: "well_ord(A,r) ==> linear(A,r)"
105 by (unfold well_ord_def tot_ord_def, blast)
108 (** Derived rules for pred(A,x,r) **)
110 lemma pred_iff: "y : pred(A,x,r) <-> <y,x>:r & y:A"
111 by (unfold pred_def, blast)
113 lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
115 lemma predE: "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P"
118 lemma pred_subset_under: "pred(A,x,r) <= r -`` {x}"
119 by (simp add: pred_def, blast)
121 lemma pred_subset: "pred(A,x,r) <= A"
122 by (simp add: pred_def, blast)
124 lemma pred_pred_eq:
125     "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"
126 by (simp add: pred_def, blast)
128 lemma trans_pred_pred_eq:
129     "[| trans[A](r);  <y,x>:r;  x:A;  y:A |]
130      ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"
131 by (unfold trans_on_def pred_def, blast)
134 subsection{*Restricting an Ordering's Domain*}
136 (** The ordering's properties hold over all subsets of its domain
137     [including initial segments of the form pred(A,x,r) **)
139 (*Note: a relation s such that s<=r need not be a partial ordering*)
140 lemma part_ord_subset:
141     "[| part_ord(A,r);  B<=A |] ==> part_ord(B,r)"
142 by (unfold part_ord_def irrefl_def trans_on_def, blast)
144 lemma linear_subset:
145     "[| linear(A,r);  B<=A |] ==> linear(B,r)"
146 by (unfold linear_def, blast)
148 lemma tot_ord_subset:
149     "[| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)"
150 apply (unfold tot_ord_def)
151 apply (fast elim!: part_ord_subset linear_subset)
152 done
154 lemma well_ord_subset:
155     "[| well_ord(A,r);  B<=A |] ==> well_ord(B,r)"
156 apply (unfold well_ord_def)
157 apply (fast elim!: tot_ord_subset wf_on_subset_A)
158 done
161 (** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
163 lemma irrefl_Int_iff: "irrefl(A,r Int A*A) <-> irrefl(A,r)"
164 by (unfold irrefl_def, blast)
166 lemma trans_on_Int_iff: "trans[A](r Int A*A) <-> trans[A](r)"
167 by (unfold trans_on_def, blast)
169 lemma part_ord_Int_iff: "part_ord(A,r Int A*A) <-> part_ord(A,r)"
170 apply (unfold part_ord_def)
171 apply (simp add: irrefl_Int_iff trans_on_Int_iff)
172 done
174 lemma linear_Int_iff: "linear(A,r Int A*A) <-> linear(A,r)"
175 by (unfold linear_def, blast)
177 lemma tot_ord_Int_iff: "tot_ord(A,r Int A*A) <-> tot_ord(A,r)"
178 apply (unfold tot_ord_def)
179 apply (simp add: part_ord_Int_iff linear_Int_iff)
180 done
182 lemma wf_on_Int_iff: "wf[A](r Int A*A) <-> wf[A](r)"
183 apply (unfold wf_on_def wf_def, fast) (*10 times faster than blast!*)
184 done
186 lemma well_ord_Int_iff: "well_ord(A,r Int A*A) <-> well_ord(A,r)"
187 apply (unfold well_ord_def)
188 apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
189 done
192 subsection{*Empty and Unit Domains*}
194 (*The empty relation is well-founded*)
195 lemma wf_on_any_0: "wf[A](0)"
196 by (simp add: wf_on_def wf_def, fast)
198 subsubsection{*Relations over the Empty Set*}
200 lemma irrefl_0: "irrefl(0,r)"
201 by (unfold irrefl_def, blast)
203 lemma trans_on_0: "trans[0](r)"
204 by (unfold trans_on_def, blast)
206 lemma part_ord_0: "part_ord(0,r)"
207 apply (unfold part_ord_def)
208 apply (simp add: irrefl_0 trans_on_0)
209 done
211 lemma linear_0: "linear(0,r)"
212 by (unfold linear_def, blast)
214 lemma tot_ord_0: "tot_ord(0,r)"
215 apply (unfold tot_ord_def)
216 apply (simp add: part_ord_0 linear_0)
217 done
219 lemma wf_on_0: "wf[0](r)"
220 by (unfold wf_on_def wf_def, blast)
222 lemma well_ord_0: "well_ord(0,r)"
223 apply (unfold well_ord_def)
224 apply (simp add: tot_ord_0 wf_on_0)
225 done
228 subsubsection{*The Empty Relation Well-Orders the Unit Set*}
230 text{*by Grabczewski*}
232 lemma tot_ord_unit: "tot_ord({a},0)"
233 by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
235 lemma well_ord_unit: "well_ord({a},0)"
236 apply (unfold well_ord_def)
237 apply (simp add: tot_ord_unit wf_on_any_0)
238 done
241 subsection{*Order-Isomorphisms*}
243 text{*Suppes calls them "similarities"*}
245 (** Order-preserving (monotone) maps **)
247 lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
250 lemma mono_map_is_inj:
251     "[| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"
252 apply (unfold mono_map_def inj_def, clarify)
253 apply (erule_tac x=w and y=x in linearE, assumption+)
254 apply (force intro: apply_type dest: wf_on_not_refl)+
255 done
257 lemma ord_isoI:
258     "[| f: bij(A, B);
259         !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s |]
260      ==> f: ord_iso(A,r,B,s)"
263 lemma ord_iso_is_mono_map:
264     "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"
265 apply (simp add: ord_iso_def mono_map_def)
266 apply (blast dest!: bij_is_fun)
267 done
269 lemma ord_iso_is_bij:
270     "f: ord_iso(A,r,B,s) ==> f: bij(A,B)"
273 (*Needed?  But ord_iso_converse is!*)
274 lemma ord_iso_apply:
275     "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> <f`x, f`y> : s"
278 lemma ord_iso_converse:
279     "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |]
280      ==> <converse(f) ` x, converse(f) ` y> : r"
281 apply (simp add: ord_iso_def, clarify)
282 apply (erule bspec [THEN bspec, THEN iffD2])
283 apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+
284 apply (auto simp add: right_inverse_bij)
285 done
288 (** Symmetry and Transitivity Rules **)
290 (*Reflexivity of similarity*)
291 lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)"
292 by (rule id_bij [THEN ord_isoI], simp)
294 (*Symmetry of similarity*)
295 lemma ord_iso_sym: "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"
297 apply (auto simp add: right_inverse_bij bij_converse_bij
298                       bij_is_fun [THEN apply_funtype])
299 done
301 (*Transitivity of similarity*)
302 lemma mono_map_trans:
303     "[| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |]
304      ==> (f O g): mono_map(A,r,C,t)"
305 apply (unfold mono_map_def)
306 apply (auto simp add: comp_fun)
307 done
309 (*Transitivity of similarity: the order-isomorphism relation*)
310 lemma ord_iso_trans:
311     "[| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |]
312      ==> (f O g): ord_iso(A,r,C,t)"
313 apply (unfold ord_iso_def, clarify)
314 apply (frule bij_is_fun [of f])
315 apply (frule bij_is_fun [of g])
316 apply (auto simp add: comp_bij)
317 done
319 (** Two monotone maps can make an order-isomorphism **)
321 lemma mono_ord_isoI:
322     "[| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);
323         f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"
324 apply (simp add: ord_iso_def mono_map_def, safe)
325 apply (intro fg_imp_bijective, auto)
326 apply (subgoal_tac "<g` (f`x), g` (f`y) > : r")
327 apply (simp add: comp_eq_id_iff [THEN iffD1])
328 apply (blast intro: apply_funtype)
329 done
331 lemma well_ord_mono_ord_isoI:
332      "[| well_ord(A,r);  well_ord(B,s);
333          f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |]
334       ==> f: ord_iso(A,r,B,s)"
335 apply (intro mono_ord_isoI, auto)
336 apply (frule mono_map_is_fun [THEN fun_is_rel])
337 apply (erule converse_converse [THEN subst], rule left_comp_inverse)
338 apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear
339                     well_ord_is_wf)+
340 done
343 (** Order-isomorphisms preserve the ordering's properties **)
345 lemma part_ord_ord_iso:
346     "[| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"
347 apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def)
348 apply (fast intro: bij_is_fun [THEN apply_type])
349 done
351 lemma linear_ord_iso:
352     "[| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)"
353 apply (simp add: linear_def ord_iso_def, safe)
354 apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec])
355 apply (safe elim!: bij_is_fun [THEN apply_type])
356 apply (drule_tac t = "op ` (converse (f))" in subst_context)
358 done
360 lemma wf_on_ord_iso:
361     "[| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)"
362 apply (simp add: wf_on_def wf_def ord_iso_def, safe)
363 apply (drule_tac x = "{f`z. z:Z Int A}" in spec)
364 apply (safe intro!: equalityI)
365 apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+
366 done
368 lemma well_ord_ord_iso:
369     "[| well_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"
370 apply (unfold well_ord_def tot_ord_def)
371 apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
372 done
375 subsection{*Main results of Kunen, Chapter 1 section 6*}
377 (*Inductive argument for Kunen's Lemma 6.1, etc.
378   Simple proof from Halmos, page 72*)
379 lemma well_ord_iso_subset_lemma:
380      "[| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |]
381       ==> ~ <f`y, y>: r"
382 apply (simp add: well_ord_def ord_iso_def)
383 apply (elim conjE CollectE)
384 apply (rule_tac a=y in wf_on_induct, assumption+)
385 apply (blast dest: bij_is_fun [THEN apply_type])
386 done
388 (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
389                      of a well-ordering*)
390 lemma well_ord_iso_predE:
391      "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P"
392 apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x])
394 (*Now we know  f`x < x *)
395 apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
396 (*Now we also know f`x : pred(A,x,r);  contradiction! *)
397 apply (simp add: well_ord_def pred_def)
398 done
400 (*Simple consequence of Lemma 6.1*)
401 lemma well_ord_iso_pred_eq:
402      "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);
403          a:A;  c:A |] ==> a=c"
404 apply (frule well_ord_is_trans_on)
405 apply (frule well_ord_is_linear)
406 apply (erule_tac x=a and y=c in linearE, assumption+)
407 apply (drule ord_iso_sym)
408 (*two symmetric cases*)
409 apply (auto elim!: well_ord_subset [OF _ pred_subset, THEN well_ord_iso_predE]
410             intro!: predI
412 done
414 (*Does not assume r is a wellordering!*)
415 lemma ord_iso_image_pred:
416      "[|f : ord_iso(A,r,B,s);  a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)"
417 apply (unfold ord_iso_def pred_def)
418 apply (erule CollectE)
419 apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
420 apply (rule equalityI)
421 apply (safe elim!: bij_is_fun [THEN apply_type])
422 apply (rule RepFun_eqI)
423 apply (blast intro!: right_inverse_bij [symmetric])
424 apply (auto simp add: right_inverse_bij  bij_is_fun [THEN apply_funtype])
425 done
427 lemma ord_iso_restrict_image:
428      "[| f : ord_iso(A,r,B,s);  C<=A |]
429       ==> restrict(f,C) : ord_iso(C, r, f``C, s)"
431 apply (blast intro: bij_is_inj restrict_bij)
432 done
434 (*But in use, A and B may themselves be initial segments.  Then use
435   trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
436 lemma ord_iso_restrict_pred:
437    "[| f : ord_iso(A,r,B,s);   a:A |]
438     ==> restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
439 apply (simp add: ord_iso_image_pred [symmetric])
440 apply (blast intro: ord_iso_restrict_image elim: predE)
441 done
443 (*Tricky; a lot of forward proof!*)
444 lemma well_ord_iso_preserving:
445      "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;
446          f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);
447          g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);
448          a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s"
449 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+)
450 apply (subgoal_tac "b = g`a")
451 apply (simp (no_asm_simp))
452 apply (rule well_ord_iso_pred_eq, auto)
453 apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+)
454 apply (simp add: well_ord_is_trans_on trans_pred_pred_eq)
455 apply (erule ord_iso_sym [THEN ord_iso_trans], assumption)
456 done
458 (*See Halmos, page 72*)
459 lemma well_ord_iso_unique_lemma:
460      "[| well_ord(A,r);
461          f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |]
462       ==> ~ <g`y, f`y> : s"
463 apply (frule well_ord_iso_subset_lemma)
464 apply (rule_tac f = "converse (f) " and g = g in ord_iso_trans)
465 apply auto
466 apply (blast intro: ord_iso_sym)
467 apply (frule ord_iso_is_bij [of f])
468 apply (frule ord_iso_is_bij [of g])
469 apply (frule ord_iso_converse)
470 apply (blast intro!: bij_converse_bij
471              intro: bij_is_fun apply_funtype)+
472 apply (erule notE)
473 apply (simp add: left_inverse_bij bij_is_fun comp_fun_apply [of _ A B])
474 done
477 (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
478 lemma well_ord_iso_unique: "[| well_ord(A,r);
479          f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g"
480 apply (rule fun_extension)
481 apply (erule ord_iso_is_bij [THEN bij_is_fun])+
482 apply (subgoal_tac "f`x : B & g`x : B & linear(B,s)")
484  apply (blast dest: well_ord_iso_unique_lemma)
485 apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype
486                     well_ord_is_linear well_ord_ord_iso ord_iso_sym)
487 done
489 subsection{*Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation*}
491 lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B"
492 by (unfold ord_iso_map_def, blast)
494 lemma domain_ord_iso_map: "domain(ord_iso_map(A,r,B,s)) <= A"
495 by (unfold ord_iso_map_def, blast)
497 lemma range_ord_iso_map: "range(ord_iso_map(A,r,B,s)) <= B"
498 by (unfold ord_iso_map_def, blast)
500 lemma converse_ord_iso_map:
501     "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"
502 apply (unfold ord_iso_map_def)
503 apply (blast intro: ord_iso_sym)
504 done
506 lemma function_ord_iso_map:
507     "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"
508 apply (unfold ord_iso_map_def function_def)
509 apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans)
510 done
512 lemma ord_iso_map_fun: "well_ord(B,s) ==> ord_iso_map(A,r,B,s)
513            : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"
514 by (simp add: Pi_iff function_ord_iso_map
515                  ord_iso_map_subset [THEN domain_times_range])
517 lemma ord_iso_map_mono_map:
518     "[| well_ord(A,r);  well_ord(B,s) |]
519      ==> ord_iso_map(A,r,B,s)
520            : mono_map(domain(ord_iso_map(A,r,B,s)), r,
521                       range(ord_iso_map(A,r,B,s)), s)"
522 apply (unfold mono_map_def)
523 apply (simp (no_asm_simp) add: ord_iso_map_fun)
524 apply safe
525 apply (subgoal_tac "x:A & ya:A & y:B & yb:B")
526  apply (simp add: apply_equality [OF _  ord_iso_map_fun])
527  apply (unfold ord_iso_map_def)
528  apply (blast intro: well_ord_iso_preserving, blast)
529 done
531 lemma ord_iso_map_ord_iso:
532     "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)
533            : ord_iso(domain(ord_iso_map(A,r,B,s)), r,
534                       range(ord_iso_map(A,r,B,s)), s)"
535 apply (rule well_ord_mono_ord_isoI)
536    prefer 4
537    apply (rule converse_ord_iso_map [THEN subst])
539                     ord_iso_map_subset [THEN converse_converse])
540 apply (blast intro!: domain_ord_iso_map range_ord_iso_map
541              intro: well_ord_subset ord_iso_map_mono_map)+
542 done
545 (*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
546 lemma domain_ord_iso_map_subset:
547      "[| well_ord(A,r);  well_ord(B,s);
548          a: A;  a ~: domain(ord_iso_map(A,r,B,s)) |]
549       ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)"
550 apply (unfold ord_iso_map_def)
551 apply (safe intro!: predI)
552 (*Case analysis on  xa vs a in r *)
553 apply (simp (no_asm_simp))
554 apply (frule_tac A = A in well_ord_is_linear)
555 apply (rename_tac b y f)
556 apply (erule_tac x=b and y=a in linearE, assumption+)
557 (*Trivial case: b=a*)
558 apply clarify
559 apply blast
560 (*Harder case: <a, xa>: r*)
561 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type],
562        (erule asm_rl predI predE)+)
563 apply (frule ord_iso_restrict_pred)
565 apply (simp split: split_if_asm
566           add: well_ord_is_trans_on trans_pred_pred_eq domain_UN domain_Union, blast)
567 done
569 (*For the 4-way case analysis in the main result*)
570 lemma domain_ord_iso_map_cases:
571      "[| well_ord(A,r);  well_ord(B,s) |]
572       ==> domain(ord_iso_map(A,r,B,s)) = A |
573           (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"
574 apply (frule well_ord_is_wf)
575 apply (unfold wf_on_def wf_def)
576 apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec)
577 apply safe
578 (*The first case: the domain equals A*)
579 apply (rule domain_ord_iso_map [THEN equalityI])
580 apply (erule Diff_eq_0_iff [THEN iffD1])
581 (*The other case: the domain equals an initial segment*)
582 apply (blast del: domainI subsetI
583              elim!: predE
584              intro!: domain_ord_iso_map_subset
585              intro: subsetI)+
586 done
588 (*As above, by duality*)
589 lemma range_ord_iso_map_cases:
590     "[| well_ord(A,r);  well_ord(B,s) |]
591      ==> range(ord_iso_map(A,r,B,s)) = B |
592          (EX y:B. range(ord_iso_map(A,r,B,s)) = pred(B,y,s))"
593 apply (rule converse_ord_iso_map [THEN subst])
595 done
597 text{*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*}
598 theorem well_ord_trichotomy:
599    "[| well_ord(A,r);  well_ord(B,s) |]
600     ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |
601         (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) |
602         (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"
603 apply (frule_tac B = B in domain_ord_iso_map_cases, assumption)
604 apply (frule_tac B = B in range_ord_iso_map_cases, assumption)
605 apply (drule ord_iso_map_ord_iso, assumption)
606 apply (elim disjE bexE)
608 apply (rule wf_on_not_refl [THEN notE])
609   apply (erule well_ord_is_wf)
610  apply assumption
611 apply (subgoal_tac "<x,y>: ord_iso_map (A,r,B,s) ")
612  apply (drule rangeI)
614 apply (unfold ord_iso_map_def, blast)
615 done
618 subsection{*Miscellaneous Results by Krzysztof Grabczewski*}
620 (** Properties of converse(r) **)
622 lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
623 by (unfold irrefl_def, blast)
625 lemma trans_on_converse: "trans[A](r) ==> trans[A](converse(r))"
626 by (unfold trans_on_def, blast)
628 lemma part_ord_converse: "part_ord(A,r) ==> part_ord(A,converse(r))"
629 apply (unfold part_ord_def)
630 apply (blast intro!: irrefl_converse trans_on_converse)
631 done
633 lemma linear_converse: "linear(A,r) ==> linear(A,converse(r))"
634 by (unfold linear_def, blast)
636 lemma tot_ord_converse: "tot_ord(A,r) ==> tot_ord(A,converse(r))"
637 apply (unfold tot_ord_def)
638 apply (blast intro!: part_ord_converse linear_converse)
639 done
642 (** By Krzysztof Grabczewski.
643     Lemmas involving the first element of a well ordered set **)
645 lemma first_is_elem: "first(b,B,r) ==> b:B"
646 by (unfold first_def, blast)
648 lemma well_ord_imp_ex1_first:
649         "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"
650 apply (unfold well_ord_def wf_on_def wf_def first_def)
651 apply (elim conjE allE disjE, blast)
652 apply (erule bexE)
653 apply (rule_tac a = x in ex1I, auto)
654 apply (unfold tot_ord_def linear_def, blast)
655 done
657 lemma the_first_in:
658      "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"
659 apply (drule well_ord_imp_ex1_first, assumption+)
660 apply (rule first_is_elem)
661 apply (erule theI)
662 done
665 subsection {* Lemmas for the Reflexive Orders *}
667 lemma subset_vimage_vimage_iff:
668   "[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>
669   r -`` A \<subseteq> r -`` B <-> (ALL a:A. EX b:B. <a, b> : r)"
670   apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
671    apply blast
672   unfolding trans_on_def
673   apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
674           \<forall>z\<in>field(?r). \<langle>x, y\<rangle> \<in> ?r \<longrightarrow> \<langle>y, z\<rangle> \<in> ?r \<longrightarrow> \<langle>x, z\<rangle> \<in> ?r)" in rev_ballE)
675     (* instance obtained from proof term generated by best *)
676    apply best
677   apply blast
678   done
680 lemma subset_vimage1_vimage1_iff:
681   "[| Preorder(r); a : field(r); b : field(r) |] ==>
682   r -`` {a} \<subseteq> r -`` {b} <-> <a, b> : r"
685 lemma Refl_antisym_eq_Image1_Image1_iff:
686   "[| refl(field(r), r); antisym(r); a : field(r); b : field(r) |] ==>
687   r `` {a} = r `` {b} <-> a = b"
688   apply rule
689    apply (frule equality_iffD)
690    apply (drule equality_iffD)
691    apply (simp add: antisym_def refl_def)
692    apply best
693   apply (simp add: antisym_def refl_def)
694   done
696 lemma Partial_order_eq_Image1_Image1_iff:
697   "[| Partial_order(r); a : field(r); b : field(r) |] ==>
698   r `` {a} = r `` {b} <-> a = b"
699   by (simp add: partial_order_on_def preorder_on_def
700     Refl_antisym_eq_Image1_Image1_iff)
702 lemma Refl_antisym_eq_vimage1_vimage1_iff:
703   "[| refl(field(r), r); antisym(r); a : field(r); b : field(r) |] ==>
704   r -`` {a} = r -`` {b} <-> a = b"
705   apply rule
706    apply (frule equality_iffD)
707    apply (drule equality_iffD)
708    apply (simp add: antisym_def refl_def)
709    apply best
710   apply (simp add: antisym_def refl_def)
711   done
713 lemma Partial_order_eq_vimage1_vimage1_iff:
714   "[| Partial_order(r); a : field(r); b : field(r) |] ==>
715   r -`` {a} = r -`` {b} <-> a = b"
716   by (simp add: partial_order_on_def preorder_on_def
717     Refl_antisym_eq_vimage1_vimage1_iff)
719 end