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