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