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