src/ZF/Order.ML
author nipkow
Tue Sep 21 19:11:07 1999 +0200 (1999-09-21)
changeset 7570 a9391550eea1
parent 7499 23e090051cb8
child 8201 a81d18b0a9b1
permissions -rw-r--r--
Mod because of new solver interface.
clasohm@1461
     1
(*  Title:      ZF/Order.ML
lcp@435
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@435
     4
    Copyright   1994  University of Cambridge
lcp@435
     5
lcp@789
     6
Orders in Zermelo-Fraenkel Set Theory 
lcp@789
     7
lcp@789
     8
Results from the book "Set Theory: an Introduction to Independence Proofs"
clasohm@1461
     9
        by Ken Kunen.  Chapter 1, section 6.
lcp@435
    10
*)
lcp@435
    11
lcp@435
    12
open Order;
lcp@435
    13
lcp@435
    14
(** Basic properties of the definitions **)
lcp@435
    15
lcp@789
    16
(*needed?*)
wenzelm@5067
    17
Goalw [part_ord_def, irrefl_def, trans_on_def, asym_def]
paulson@5147
    18
    "part_ord(A,r) ==> asym(r Int A*A)";
paulson@2925
    19
by (Blast_tac 1);
clasohm@760
    20
qed "part_ord_Imp_asym";
lcp@435
    21
paulson@5268
    22
val major::premx::premy::prems = Goalw [linear_def]
lcp@789
    23
    "[| linear(A,r);  x:A;  y:A;  \
lcp@789
    24
\       <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |] ==> P";
lcp@789
    25
by (cut_facts_tac [major,premx,premy] 1);
lcp@789
    26
by (REPEAT_FIRST (eresolve_tac [ballE,disjE]));
lcp@789
    27
by (EVERY1 (map etac prems));
lcp@789
    28
by (ALLGOALS contr_tac);
lcp@789
    29
qed "linearE";
lcp@789
    30
lcp@789
    31
(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*)
lcp@789
    32
val linear_case_tac =
lcp@789
    33
    SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1,
clasohm@1461
    34
                        REPEAT_SOME (assume_tac ORELSE' contr_tac)]);
lcp@789
    35
lcp@789
    36
(** General properties of well_ord **)
lcp@789
    37
wenzelm@5067
    38
Goalw [irrefl_def, part_ord_def, tot_ord_def, 
clasohm@1461
    39
                 trans_on_def, well_ord_def]
paulson@5147
    40
    "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)";
wenzelm@4091
    41
by (asm_simp_tac (simpset() addsimps [wf_on_not_refl]) 1);
wenzelm@4091
    42
by (fast_tac (claset() addEs [linearE, wf_on_asym, wf_on_chain3]) 1);
lcp@789
    43
qed "well_ordI";
lcp@789
    44
wenzelm@5067
    45
Goalw [well_ord_def]
paulson@5147
    46
    "well_ord(A,r) ==> wf[A](r)";
paulson@4152
    47
by Safe_tac;
lcp@789
    48
qed "well_ord_is_wf";
lcp@789
    49
wenzelm@5067
    50
Goalw [well_ord_def, tot_ord_def, part_ord_def]
paulson@5147
    51
    "well_ord(A,r) ==> trans[A](r)";
paulson@4152
    52
by Safe_tac;
lcp@789
    53
qed "well_ord_is_trans_on";
lcp@484
    54
wenzelm@5067
    55
Goalw [well_ord_def, tot_ord_def]
paulson@5147
    56
  "well_ord(A,r) ==> linear(A,r)";
paulson@2925
    57
by (Blast_tac 1);
lcp@789
    58
qed "well_ord_is_linear";
lcp@789
    59
lcp@789
    60
lcp@789
    61
(** Derived rules for pred(A,x,r) **)
lcp@789
    62
wenzelm@5067
    63
Goalw [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
paulson@2925
    64
by (Blast_tac 1);
lcp@789
    65
qed "pred_iff";
lcp@789
    66
lcp@789
    67
bind_thm ("predI", conjI RS (pred_iff RS iffD2));
lcp@789
    68
paulson@5268
    69
val [major,minor] = Goalw [pred_def]
lcp@789
    70
    "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
lcp@789
    71
by (rtac (major RS CollectE) 1);
lcp@789
    72
by (REPEAT (ares_tac [minor] 1));
lcp@789
    73
qed "predE";
lcp@789
    74
wenzelm@5067
    75
Goalw [pred_def] "pred(A,x,r) <= r -`` {x}";
paulson@2925
    76
by (Blast_tac 1);
lcp@789
    77
qed "pred_subset_under";
lcp@789
    78
wenzelm@5067
    79
Goalw [pred_def] "pred(A,x,r) <= A";
paulson@2925
    80
by (Blast_tac 1);
lcp@789
    81
qed "pred_subset";
lcp@789
    82
wenzelm@5067
    83
Goalw [pred_def]
lcp@789
    84
    "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
paulson@2925
    85
by (Blast_tac 1);
lcp@789
    86
qed "pred_pred_eq";
lcp@789
    87
wenzelm@5067
    88
Goalw [trans_on_def, pred_def]
paulson@5147
    89
    "[| trans[A](r);  <y,x>:r;  x:A;  y:A \
lcp@789
    90
\         |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
paulson@2925
    91
by (Blast_tac 1);
lcp@789
    92
qed "trans_pred_pred_eq";
lcp@789
    93
lcp@836
    94
lcp@789
    95
(** The ordering's properties hold over all subsets of its domain 
lcp@789
    96
    [including initial segments of the form pred(A,x,r) **)
lcp@484
    97
lcp@484
    98
(*Note: a relation s such that s<=r need not be a partial ordering*)
wenzelm@5067
    99
Goalw [part_ord_def, irrefl_def, trans_on_def]
paulson@5147
   100
    "[| part_ord(A,r);  B<=A |] ==> part_ord(B,r)";
paulson@2925
   101
by (Blast_tac 1);
clasohm@760
   102
qed "part_ord_subset";
lcp@484
   103
wenzelm@5067
   104
Goalw [linear_def]
paulson@5147
   105
    "[| linear(A,r);  B<=A |] ==> linear(B,r)";
paulson@2925
   106
by (Blast_tac 1);
clasohm@760
   107
qed "linear_subset";
lcp@484
   108
wenzelm@5067
   109
Goalw [tot_ord_def]
paulson@5147
   110
    "[| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)";
wenzelm@4091
   111
by (fast_tac (claset() addSEs [part_ord_subset, linear_subset]) 1);
clasohm@760
   112
qed "tot_ord_subset";
lcp@484
   113
wenzelm@5067
   114
Goalw [well_ord_def]
paulson@5147
   115
    "[| well_ord(A,r);  B<=A |] ==> well_ord(B,r)";
wenzelm@4091
   116
by (fast_tac (claset() addSEs [tot_ord_subset, wf_on_subset_A]) 1);
clasohm@760
   117
qed "well_ord_subset";
lcp@484
   118
lcp@484
   119
lcp@836
   120
(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
lcp@836
   121
wenzelm@5067
   122
Goalw [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)";
paulson@2925
   123
by (Blast_tac 1);
lcp@836
   124
qed "irrefl_Int_iff";
lcp@836
   125
wenzelm@5067
   126
Goalw [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)";
paulson@2925
   127
by (Blast_tac 1);
lcp@836
   128
qed "trans_on_Int_iff";
lcp@836
   129
wenzelm@5067
   130
Goalw [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)";
wenzelm@4091
   131
by (simp_tac (simpset() addsimps [irrefl_Int_iff, trans_on_Int_iff]) 1);
lcp@836
   132
qed "part_ord_Int_iff";
lcp@836
   133
wenzelm@5067
   134
Goalw [linear_def] "linear(A,r Int A*A) <-> linear(A,r)";
paulson@2925
   135
by (Blast_tac 1);
lcp@836
   136
qed "linear_Int_iff";
lcp@836
   137
wenzelm@5067
   138
Goalw [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)";
wenzelm@4091
   139
by (simp_tac (simpset() addsimps [part_ord_Int_iff, linear_Int_iff]) 1);
lcp@836
   140
qed "tot_ord_Int_iff";
lcp@836
   141
wenzelm@5067
   142
Goalw [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
paulson@4311
   143
by (Fast_tac 1);   (*10 times faster than Blast_tac!*) 
lcp@836
   144
qed "wf_on_Int_iff";
lcp@836
   145
wenzelm@5067
   146
Goalw [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
wenzelm@4091
   147
by (simp_tac (simpset() addsimps [tot_ord_Int_iff, wf_on_Int_iff]) 1);
lcp@836
   148
qed "well_ord_Int_iff";
lcp@836
   149
lcp@836
   150
lcp@848
   151
(** Relations over the Empty Set **)
lcp@848
   152
wenzelm@5067
   153
Goalw [irrefl_def] "irrefl(0,r)";
paulson@2925
   154
by (Blast_tac 1);
lcp@848
   155
qed "irrefl_0";
lcp@848
   156
wenzelm@5067
   157
Goalw [trans_on_def] "trans[0](r)";
paulson@2925
   158
by (Blast_tac 1);
lcp@848
   159
qed "trans_on_0";
lcp@848
   160
wenzelm@5067
   161
Goalw [part_ord_def] "part_ord(0,r)";
wenzelm@4091
   162
by (simp_tac (simpset() addsimps [irrefl_0, trans_on_0]) 1);
lcp@848
   163
qed "part_ord_0";
lcp@848
   164
wenzelm@5067
   165
Goalw [linear_def] "linear(0,r)";
paulson@2925
   166
by (Blast_tac 1);
lcp@848
   167
qed "linear_0";
lcp@848
   168
wenzelm@5067
   169
Goalw [tot_ord_def] "tot_ord(0,r)";
wenzelm@4091
   170
by (simp_tac (simpset() addsimps [part_ord_0, linear_0]) 1);
lcp@848
   171
qed "tot_ord_0";
lcp@848
   172
wenzelm@5067
   173
Goalw [wf_on_def, wf_def] "wf[0](r)";
paulson@2925
   174
by (Blast_tac 1);
lcp@848
   175
qed "wf_on_0";
lcp@848
   176
wenzelm@5067
   177
Goalw [well_ord_def] "well_ord(0,r)";
wenzelm@4091
   178
by (simp_tac (simpset() addsimps [tot_ord_0, wf_on_0]) 1);
lcp@848
   179
qed "well_ord_0";
lcp@836
   180
lcp@836
   181
paulson@5262
   182
(** The unit set is well-ordered by the empty relation (Grabczewski) **)
paulson@5262
   183
paulson@5262
   184
Goalw [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def]
paulson@5262
   185
        "tot_ord({a},0)";
paulson@5262
   186
by (Simp_tac 1);
paulson@5262
   187
qed "tot_ord_unit";
paulson@5262
   188
paulson@5262
   189
Goalw [wf_on_def, wf_def] "wf[{a}](0)";
paulson@5262
   190
by (Fast_tac 1);
paulson@5262
   191
qed "wf_on_unit";
paulson@5262
   192
paulson@5262
   193
Goalw [well_ord_def] "well_ord({a},0)";
paulson@5262
   194
by (simp_tac (simpset() addsimps [tot_ord_unit, wf_on_unit]) 1);
paulson@5262
   195
qed "well_ord_unit";
paulson@5262
   196
paulson@5262
   197
lcp@789
   198
(** Order-preserving (monotone) maps **)
lcp@789
   199
wenzelm@5067
   200
Goalw [mono_map_def] 
paulson@5147
   201
    "f: mono_map(A,r,B,s) ==> f: A->B";
lcp@789
   202
by (etac CollectD1 1);
lcp@789
   203
qed "mono_map_is_fun";
lcp@789
   204
wenzelm@5067
   205
Goalw [mono_map_def, inj_def] 
paulson@5147
   206
    "[| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)";
paulson@3736
   207
by (Clarify_tac 1);
lcp@789
   208
by (linear_case_tac 1);
lcp@789
   209
by (REPEAT 
lcp@789
   210
    (EVERY [eresolve_tac [wf_on_not_refl RS notE] 1,
clasohm@1461
   211
            etac ssubst 2,
paulson@2469
   212
            Fast_tac 2,
clasohm@1461
   213
            REPEAT (ares_tac [apply_type] 1)]));
lcp@789
   214
qed "mono_map_is_inj";
lcp@789
   215
lcp@789
   216
lcp@789
   217
(** Order-isomorphisms -- or similarities, as Suppes calls them **)
lcp@789
   218
paulson@5268
   219
val prems = Goalw [ord_iso_def]
clasohm@1461
   220
    "[| f: bij(A, B);   \
clasohm@1461
   221
\       !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
lcp@848
   222
\    |] ==> f: ord_iso(A,r,B,s)";
wenzelm@4091
   223
by (blast_tac (claset() addSIs prems) 1);
lcp@848
   224
qed "ord_isoI";
lcp@848
   225
wenzelm@5067
   226
Goalw [ord_iso_def, mono_map_def]
paulson@5147
   227
    "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)";
wenzelm@4091
   228
by (blast_tac (claset() addSDs [bij_is_fun]) 1);
lcp@789
   229
qed "ord_iso_is_mono_map";
lcp@435
   230
wenzelm@5067
   231
Goalw [ord_iso_def] 
paulson@5147
   232
    "f: ord_iso(A,r,B,s) ==> f: bij(A,B)";
lcp@435
   233
by (etac CollectD1 1);
clasohm@760
   234
qed "ord_iso_is_bij";
lcp@435
   235
lcp@789
   236
(*Needed?  But ord_iso_converse is!*)
wenzelm@5067
   237
Goalw [ord_iso_def] 
paulson@5147
   238
    "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> \
lcp@435
   239
\         <f`x, f`y> : s";
paulson@2925
   240
by (Blast_tac 1);
clasohm@760
   241
qed "ord_iso_apply";
lcp@435
   242
paulson@6176
   243
(*Rewriting with bijections and converse (function inverse)*)
paulson@6176
   244
val bij_inverse_ss = 
nipkow@7570
   245
    simpset() setSolver (mk_solver ""
nipkow@7570
   246
      (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
nipkow@7570
   247
				        inj_is_fun, comp_fun, comp_bij])))
paulson@6176
   248
          addsimps [right_inverse_bij];
paulson@6176
   249
wenzelm@5067
   250
Goalw [ord_iso_def] 
paulson@5147
   251
    "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] ==> \
lcp@435
   252
\         <converse(f) ` x, converse(f) ` y> : r";
lcp@437
   253
by (etac CollectE 1);
lcp@437
   254
by (etac (bspec RS bspec RS iffD2) 1);
lcp@435
   255
by (REPEAT (eresolve_tac [asm_rl, 
clasohm@1461
   256
                          bij_converse_bij RS bij_is_fun RS apply_type] 1));
paulson@6176
   257
by (asm_simp_tac bij_inverse_ss 1);
clasohm@760
   258
qed "ord_iso_converse";
lcp@435
   259
lcp@812
   260
lcp@812
   261
(** Symmetry and Transitivity Rules **)
lcp@812
   262
lcp@848
   263
(*Reflexivity of similarity*)
wenzelm@5067
   264
Goal "id(A): ord_iso(A,r,A,r)";
lcp@848
   265
by (resolve_tac [id_bij RS ord_isoI] 1);
paulson@2469
   266
by (Asm_simp_tac 1);
lcp@848
   267
qed "ord_iso_refl";
lcp@848
   268
lcp@848
   269
(*Symmetry of similarity*)
paulson@6153
   270
Goalw [ord_iso_def] "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
paulson@6153
   271
by (force_tac (claset(), bij_inverse_ss) 1);
clasohm@782
   272
qed "ord_iso_sym";
lcp@769
   273
lcp@848
   274
(*Transitivity of similarity*)
wenzelm@5067
   275
Goalw [mono_map_def] 
paulson@5147
   276
    "[| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |] ==> \
lcp@812
   277
\         (f O g): mono_map(A,r,C,t)";
paulson@6153
   278
by (force_tac (claset(), bij_inverse_ss) 1);
lcp@812
   279
qed "mono_map_trans";
lcp@812
   280
lcp@812
   281
(*Transitivity of similarity: the order-isomorphism relation*)
wenzelm@5067
   282
Goalw [ord_iso_def] 
paulson@5147
   283
    "[| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |] ==> \
lcp@789
   284
\         (f O g): ord_iso(A,r,C,t)";
paulson@6153
   285
by (force_tac (claset(), bij_inverse_ss) 1);
lcp@789
   286
qed "ord_iso_trans";
lcp@789
   287
lcp@789
   288
(** Two monotone maps can make an order-isomorphism **)
lcp@789
   289
wenzelm@5067
   290
Goalw [ord_iso_def, mono_map_def]
paulson@5147
   291
    "[| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);     \
lcp@789
   292
\              f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
paulson@4152
   293
by Safe_tac;
lcp@789
   294
by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
paulson@2925
   295
by (Blast_tac 1);
lcp@789
   296
by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
wenzelm@4091
   297
by (blast_tac (claset() addIs [apply_funtype]) 2);
wenzelm@4091
   298
by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1);
lcp@789
   299
qed "mono_ord_isoI";
lcp@789
   300
paulson@5268
   301
Goal "[| well_ord(A,r);  well_ord(B,s);                             \
clasohm@1461
   302
\            f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r)      \
lcp@789
   303
\         |] ==> f: ord_iso(A,r,B,s)";
lcp@789
   304
by (REPEAT (ares_tac [mono_ord_isoI] 1));
lcp@789
   305
by (forward_tac [mono_map_is_fun RS fun_is_rel] 1);
lcp@789
   306
by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1);
lcp@789
   307
by (DEPTH_SOLVE (ares_tac [mono_map_is_inj, left_comp_inverse] 1
lcp@789
   308
          ORELSE eresolve_tac [well_ord_is_linear, well_ord_is_wf] 1));
lcp@789
   309
qed "well_ord_mono_ord_isoI";
lcp@789
   310
lcp@789
   311
lcp@789
   312
(** Order-isomorphisms preserve the ordering's properties **)
lcp@789
   313
wenzelm@5067
   314
Goalw [part_ord_def, irrefl_def, trans_on_def, ord_iso_def]
paulson@5147
   315
    "[| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)";
paulson@2469
   316
by (Asm_simp_tac 1);
wenzelm@4091
   317
by (fast_tac (claset() addIs [bij_is_fun RS apply_type]) 1);
lcp@789
   318
qed "part_ord_ord_iso";
lcp@435
   319
wenzelm@5067
   320
Goalw [linear_def, ord_iso_def]
paulson@5147
   321
    "[| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)";
paulson@2469
   322
by (Asm_simp_tac 1);
paulson@4152
   323
by Safe_tac;
lcp@789
   324
by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1);
wenzelm@4091
   325
by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
lcp@789
   326
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
paulson@6176
   327
by (asm_full_simp_tac bij_inverse_ss 1);
lcp@789
   328
qed "linear_ord_iso";
lcp@789
   329
wenzelm@5067
   330
Goalw [wf_on_def, wf_def, ord_iso_def]
paulson@5147
   331
    "[| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)";
lcp@789
   332
(*reversed &-congruence rule handles context of membership in A*)
wenzelm@4091
   333
by (asm_full_simp_tac (simpset() addcongs [conj_cong2]) 1);
paulson@4152
   334
by Safe_tac;
lcp@789
   335
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
wenzelm@4091
   336
by (safe_tac (claset() addSIs [equalityI]));
paulson@2925
   337
by (ALLGOALS (blast_tac
wenzelm@4091
   338
	      (claset() addSDs [equalityD1] addIs [bij_is_fun RS apply_type])));
lcp@789
   339
qed "wf_on_ord_iso";
lcp@789
   340
wenzelm@5067
   341
Goalw [well_ord_def, tot_ord_def]
paulson@5147
   342
    "[| well_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)";
lcp@789
   343
by (fast_tac
wenzelm@4091
   344
    (claset() addSEs [part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso]) 1);
lcp@789
   345
qed "well_ord_ord_iso";
lcp@789
   346
lcp@789
   347
lcp@789
   348
(*** Main results of Kunen, Chapter 1 section 6 ***)
lcp@435
   349
lcp@812
   350
(*Inductive argument for Kunen's Lemma 6.1, etc. 
lcp@812
   351
  Simple proof from Halmos, page 72*)
wenzelm@5067
   352
Goalw [well_ord_def, ord_iso_def]
paulson@5147
   353
  "[| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |] \
lcp@812
   354
\       ==> ~ <f`y, y>: r";
lcp@812
   355
by (REPEAT (eresolve_tac [conjE, CollectE] 1));
lcp@435
   356
by (wf_on_ind_tac "y" [] 1);
lcp@812
   357
by (dres_inst_tac [("a","y1")] (bij_is_fun RS apply_type) 1);
lcp@812
   358
by (assume_tac 1);
paulson@2925
   359
by (Blast_tac 1);
lcp@812
   360
qed "well_ord_iso_subset_lemma";
lcp@435
   361
lcp@435
   362
(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
lcp@435
   363
                     of a well-ordering*)
paulson@5268
   364
Goal "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P";
lcp@812
   365
by (metacut_tac well_ord_iso_subset_lemma 1);
lcp@812
   366
by (REPEAT_FIRST (ares_tac [pred_subset]));
lcp@812
   367
(*Now we know  f`x < x *)
lcp@435
   368
by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type),
clasohm@1461
   369
             assume_tac]);
lcp@812
   370
(*Now we also know f`x : pred(A,x,r);  contradiction! *)
wenzelm@4091
   371
by (asm_full_simp_tac (simpset() addsimps [well_ord_def, pred_def]) 1);
lcp@789
   372
qed "well_ord_iso_predE";
lcp@789
   373
lcp@789
   374
(*Simple consequence of Lemma 6.1*)
paulson@5268
   375
Goal "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
paulson@6153
   376
\        a:A;  c:A |] ==> a=c";
wenzelm@7499
   377
by (ftac well_ord_is_trans_on 1);
wenzelm@7499
   378
by (ftac well_ord_is_linear 1);
lcp@789
   379
by (linear_case_tac 1);
lcp@789
   380
by (dtac ord_iso_sym 1);
paulson@6153
   381
(*two symmetric cases*)
paulson@6153
   382
by (auto_tac (claset() addSEs [pred_subset RSN (2, well_ord_subset) RS
paulson@6153
   383
			       well_ord_iso_predE]
paulson@6153
   384
	               addSIs [predI], 
paulson@6153
   385
	      simpset() addsimps [trans_pred_pred_eq]));
lcp@789
   386
qed "well_ord_iso_pred_eq";
lcp@789
   387
lcp@789
   388
(*Does not assume r is a wellordering!*)
wenzelm@5067
   389
Goalw [ord_iso_def, pred_def]
paulson@5147
   390
 "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
lcp@789
   391
\      f `` pred(A,a,r) = pred(B, f`a, s)";
lcp@789
   392
by (etac CollectE 1);
lcp@789
   393
by (asm_simp_tac 
wenzelm@4091
   394
    (simpset() addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
paulson@2493
   395
by (rtac equalityI 1);
wenzelm@4091
   396
by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
clasohm@1461
   397
by (rtac RepFun_eqI 1);
wenzelm@4091
   398
by (blast_tac (claset() addSIs [right_inverse_bij RS sym]) 1);
lcp@812
   399
by (asm_simp_tac bij_inverse_ss 1);
lcp@789
   400
qed "ord_iso_image_pred";
lcp@435
   401
lcp@789
   402
(*But in use, A and B may themselves be initial segments.  Then use
lcp@789
   403
  trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
paulson@5268
   404
Goal "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
lcp@789
   405
\      restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
wenzelm@4091
   406
by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
clasohm@1461
   407
by (rewtac ord_iso_def);
lcp@848
   408
by (etac CollectE 1);
lcp@848
   409
by (rtac CollectI 1);
wenzelm@4091
   410
by (asm_full_simp_tac (simpset() addsimps [pred_def]) 2);
lcp@789
   411
by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1);
lcp@789
   412
qed "ord_iso_restrict_pred";
lcp@789
   413
lcp@789
   414
(*Tricky; a lot of forward proof!*)
paulson@5268
   415
Goal "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;     \
clasohm@1461
   416
\         f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);  \
clasohm@1461
   417
\         g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);  \
lcp@789
   418
\         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s";
lcp@789
   419
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
lcp@789
   420
    REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
lcp@789
   421
by (subgoal_tac "b = g`a" 1);
paulson@2469
   422
by (Asm_simp_tac 1);
clasohm@1461
   423
by (rtac well_ord_iso_pred_eq 1);
lcp@789
   424
by (REPEAT_SOME assume_tac);
wenzelm@7499
   425
by (ftac ord_iso_restrict_pred 1  THEN
lcp@789
   426
    REPEAT1 (eresolve_tac [asm_rl, predI] 1));
lcp@789
   427
by (asm_full_simp_tac
wenzelm@4091
   428
    (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
lcp@789
   429
by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1);
lcp@789
   430
by (assume_tac 1);
lcp@789
   431
qed "well_ord_iso_preserving";
lcp@435
   432
wenzelm@4091
   433
val  bij_apply_cs = claset() addSIs [bij_converse_bij]
paulson@2925
   434
                            addIs  [ord_iso_is_bij, bij_is_fun, apply_funtype];
paulson@2469
   435
lcp@812
   436
(*See Halmos, page 72*)
paulson@5268
   437
Goal "[| well_ord(A,r);  \
lcp@435
   438
\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
lcp@812
   439
\         ==> ~ <g`y, f`y> : s";
wenzelm@7499
   440
by (ftac well_ord_iso_subset_lemma 1);
lcp@812
   441
by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
lcp@812
   442
by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
paulson@4152
   443
by Safe_tac;
wenzelm@7499
   444
by (ftac ord_iso_converse 1);
paulson@2925
   445
by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
lcp@435
   446
by (asm_full_simp_tac bij_inverse_ss 1);
clasohm@760
   447
qed "well_ord_iso_unique_lemma";
lcp@435
   448
lcp@435
   449
(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
paulson@5268
   450
Goal "[| well_ord(A,r);  \
lcp@435
   451
\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
lcp@437
   452
by (rtac fun_extension 1);
lcp@812
   453
by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
lcp@812
   454
by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
paulson@2925
   455
by (REPEAT (blast_tac bij_apply_cs 3));
lcp@812
   456
by (dtac well_ord_ord_iso 2 THEN etac ord_iso_sym 2);
wenzelm@4091
   457
by (asm_full_simp_tac (simpset() addsimps [tot_ord_def, well_ord_def]) 2);
lcp@812
   458
by (linear_case_tac 1);
lcp@812
   459
by (DEPTH_SOLVE (eresolve_tac [asm_rl, well_ord_iso_unique_lemma RS notE] 1));
clasohm@760
   460
qed "well_ord_iso_unique";
lcp@435
   461
lcp@435
   462
lcp@789
   463
(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
lcp@789
   464
wenzelm@5067
   465
Goalw [ord_iso_map_def] "ord_iso_map(A,r,B,s) <= A*B";
paulson@2925
   466
by (Blast_tac 1);
lcp@789
   467
qed "ord_iso_map_subset";
lcp@789
   468
wenzelm@5067
   469
Goalw [ord_iso_map_def] "domain(ord_iso_map(A,r,B,s)) <= A";
paulson@2925
   470
by (Blast_tac 1);
lcp@789
   471
qed "domain_ord_iso_map";
lcp@789
   472
wenzelm@5067
   473
Goalw [ord_iso_map_def] "range(ord_iso_map(A,r,B,s)) <= B";
paulson@2925
   474
by (Blast_tac 1);
lcp@789
   475
qed "range_ord_iso_map";
lcp@789
   476
wenzelm@5067
   477
Goalw [ord_iso_map_def]
lcp@789
   478
    "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
wenzelm@4091
   479
by (blast_tac (claset() addIs [ord_iso_sym]) 1);
lcp@789
   480
qed "converse_ord_iso_map";
lcp@789
   481
wenzelm@5067
   482
Goalw [ord_iso_map_def, function_def]
paulson@5147
   483
    "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))";
wenzelm@4091
   484
by (blast_tac (claset() addIs [well_ord_iso_pred_eq, 
paulson@2925
   485
			      ord_iso_sym, ord_iso_trans]) 1);
lcp@789
   486
qed "function_ord_iso_map";
lcp@789
   487
paulson@5268
   488
Goal "well_ord(B,s) ==> ord_iso_map(A,r,B,s)        \
lcp@789
   489
\          : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))";
lcp@789
   490
by (asm_simp_tac 
wenzelm@4091
   491
    (simpset() addsimps [Pi_iff, function_ord_iso_map,
clasohm@1461
   492
                     ord_iso_map_subset RS domain_times_range]) 1);
lcp@789
   493
qed "ord_iso_map_fun";
lcp@435
   494
wenzelm@5067
   495
Goalw [mono_map_def]
paulson@5147
   496
    "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)  \
clasohm@1461
   497
\          : mono_map(domain(ord_iso_map(A,r,B,s)), r,  \
clasohm@1461
   498
\                     range(ord_iso_map(A,r,B,s)), s)";
wenzelm@4091
   499
by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1);
paulson@4152
   500
by Safe_tac;
lcp@789
   501
by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1);
lcp@789
   502
by (REPEAT 
wenzelm@4091
   503
    (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
paulson@2925
   504
by (asm_simp_tac 
wenzelm@4091
   505
    (simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
clasohm@1461
   506
by (rewtac ord_iso_map_def);
paulson@5488
   507
by Safe_tac;
clasohm@1461
   508
by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
lcp@789
   509
qed "ord_iso_map_mono_map";
lcp@435
   510
wenzelm@5067
   511
Goalw [mono_map_def]
paulson@5147
   512
    "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)  \
clasohm@1461
   513
\          : ord_iso(domain(ord_iso_map(A,r,B,s)), r,   \
clasohm@1461
   514
\                     range(ord_iso_map(A,r,B,s)), s)";
clasohm@1461
   515
by (rtac well_ord_mono_ord_isoI 1);
lcp@789
   516
by (resolve_tac [converse_ord_iso_map RS subst] 4);
lcp@789
   517
by (asm_simp_tac 
wenzelm@4091
   518
    (simpset() addsimps [ord_iso_map_subset RS converse_converse]) 4);
lcp@789
   519
by (REPEAT (ares_tac [ord_iso_map_mono_map] 3));
lcp@789
   520
by (ALLGOALS (etac well_ord_subset));
lcp@789
   521
by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map]));
lcp@789
   522
qed "ord_iso_map_ord_iso";
lcp@467
   523
lcp@789
   524
(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
wenzelm@5067
   525
Goalw [ord_iso_map_def]
paulson@5147
   526
  "[| well_ord(A,r);  well_ord(B,s);               \
clasohm@1461
   527
\          a: A;  a ~: domain(ord_iso_map(A,r,B,s))     \
lcp@1015
   528
\       |] ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)";
wenzelm@4091
   529
by (safe_tac (claset() addSIs [predI]));
lcp@1015
   530
(*Case analysis on  xaa vs a in r *)
lcp@789
   531
by (forw_inst_tac [("A","A")] well_ord_is_linear 1);
lcp@789
   532
by (linear_case_tac 1);
lcp@1015
   533
(*Trivial case: a=xa*)
paulson@2925
   534
by (Blast_tac 2);
lcp@1015
   535
(*Harder case: <a, xa>: r*)
lcp@789
   536
by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
lcp@789
   537
    REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
wenzelm@7499
   538
by (ftac ord_iso_restrict_pred 1  THEN
lcp@789
   539
    REPEAT1 (eresolve_tac [asm_rl, predI] 1));
lcp@789
   540
by (asm_full_simp_tac
wenzelm@4091
   541
    (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
paulson@2925
   542
by (Blast_tac 1);
lcp@789
   543
qed "domain_ord_iso_map_subset";
lcp@435
   544
lcp@789
   545
(*For the 4-way case analysis in the main result*)
paulson@5268
   546
Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
clasohm@1461
   547
\       domain(ord_iso_map(A,r,B,s)) = A |      \
lcp@789
   548
\       (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))";
wenzelm@7499
   549
by (ftac well_ord_is_wf 1);
lcp@789
   550
by (rewrite_goals_tac [wf_on_def, wf_def]);
lcp@789
   551
by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1);
paulson@3736
   552
by Safe_tac;
lcp@789
   553
(*The first case: the domain equals A*)
lcp@789
   554
by (rtac (domain_ord_iso_map RS equalityI) 1);
lcp@789
   555
by (etac (Diff_eq_0_iff RS iffD1) 1);
lcp@789
   556
(*The other case: the domain equals an initial segment*)
lcp@789
   557
by (swap_res_tac [bexI] 1);
lcp@789
   558
by (assume_tac 2);
lcp@789
   559
by (rtac equalityI 1);
wenzelm@4091
   560
(*not (claset()) below; that would use rules like domainE!*)
wenzelm@4091
   561
by (blast_tac (claset() addSEs [predE]) 2);
lcp@789
   562
by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1));
lcp@789
   563
qed "domain_ord_iso_map_cases";
lcp@467
   564
lcp@789
   565
(*As above, by duality*)
paulson@5268
   566
Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
clasohm@1461
   567
\       range(ord_iso_map(A,r,B,s)) = B |       \
lcp@789
   568
\       (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))";
lcp@789
   569
by (resolve_tac [converse_ord_iso_map RS subst] 1);
lcp@789
   570
by (asm_simp_tac
wenzelm@4091
   571
    (simpset() addsimps [range_converse, domain_ord_iso_map_cases]) 1);
lcp@789
   572
qed "range_ord_iso_map_cases";
lcp@789
   573
lcp@789
   574
(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
paulson@5268
   575
Goal "[| well_ord(A,r);  well_ord(B,s) |] ==>         \
clasohm@1461
   576
\       ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |    \
lcp@789
   577
\       (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \
lcp@789
   578
\       (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))";
lcp@789
   579
by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1);
lcp@789
   580
by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2);
lcp@789
   581
by (REPEAT_FIRST (eresolve_tac [asm_rl, disjE, bexE]));
clasohm@1461
   582
by (ALLGOALS (dtac ord_iso_map_ord_iso THEN' assume_tac THEN' 
wenzelm@4091
   583
              asm_full_simp_tac (simpset() addsimps [bexI])));
lcp@789
   584
by (resolve_tac [wf_on_not_refl RS notE] 1);
clasohm@1461
   585
by (etac well_ord_is_wf 1);
lcp@789
   586
by (assume_tac 1);
lcp@789
   587
by (subgoal_tac "<x,y>: ord_iso_map(A,r,B,s)" 1);
clasohm@1461
   588
by (dtac rangeI 1);
wenzelm@4091
   589
by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
clasohm@1461
   590
by (rewtac ord_iso_map_def);
paulson@2925
   591
by (Blast_tac 1);
lcp@789
   592
qed "well_ord_trichotomy";
lcp@467
   593
lcp@836
   594
lcp@836
   595
(*** Properties of converse(r), by Krzysztof Grabczewski ***)
lcp@836
   596
wenzelm@5067
   597
Goalw [irrefl_def] 
paulson@5147
   598
            "irrefl(A,r) ==> irrefl(A,converse(r))";
paulson@4311
   599
by (Blast_tac 1);
lcp@836
   600
qed "irrefl_converse";
lcp@836
   601
wenzelm@5067
   602
Goalw [trans_on_def] 
paulson@5147
   603
    "trans[A](r) ==> trans[A](converse(r))";
paulson@4311
   604
by (Blast_tac 1);
lcp@836
   605
qed "trans_on_converse";
lcp@836
   606
wenzelm@5067
   607
Goalw [part_ord_def] 
paulson@5147
   608
    "part_ord(A,r) ==> part_ord(A,converse(r))";
wenzelm@4091
   609
by (blast_tac (claset() addSIs [irrefl_converse, trans_on_converse]) 1);
lcp@836
   610
qed "part_ord_converse";
lcp@836
   611
wenzelm@5067
   612
Goalw [linear_def] 
paulson@5147
   613
    "linear(A,r) ==> linear(A,converse(r))";
paulson@4311
   614
by (Blast_tac 1);
lcp@836
   615
qed "linear_converse";
lcp@836
   616
wenzelm@5067
   617
Goalw [tot_ord_def] 
paulson@5147
   618
    "tot_ord(A,r) ==> tot_ord(A,converse(r))";
wenzelm@4091
   619
by (blast_tac (claset() addSIs [part_ord_converse, linear_converse]) 1);
lcp@836
   620
qed "tot_ord_converse";
paulson@2469
   621
paulson@2469
   622
paulson@2469
   623
(** By Krzysztof Grabczewski.
paulson@2469
   624
    Lemmas involving the first element of a well ordered set **)
paulson@2469
   625
paulson@5137
   626
Goalw [first_def] "first(b,B,r) ==> b:B";
paulson@2925
   627
by (Blast_tac 1);
paulson@2469
   628
qed "first_is_elem";
paulson@2469
   629
wenzelm@5067
   630
Goalw [well_ord_def, wf_on_def, wf_def,     first_def] 
paulson@5147
   631
        "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))";
paulson@2469
   632
by (REPEAT (eresolve_tac [conjE,allE,disjE] 1));
paulson@2469
   633
by (contr_tac 1);
paulson@2469
   634
by (etac bexE 1);
paulson@2469
   635
by (res_inst_tac [("a","x")] ex1I 1);
paulson@2925
   636
by (Blast_tac 2);
paulson@2469
   637
by (rewrite_goals_tac [tot_ord_def, linear_def]);
wenzelm@4091
   638
by (Blast.depth_tac (claset()) 7 1);
paulson@2469
   639
qed "well_ord_imp_ex1_first";
paulson@2469
   640
paulson@5137
   641
Goal "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B";
paulson@2469
   642
by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1));
paulson@2469
   643
by (rtac first_is_elem 1);
paulson@2469
   644
by (etac theI 1);
paulson@2469
   645
qed "the_first_in";