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