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