src/ZF/Ord.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
clasohm@0
     1
(*  Title: 	ZF/ordinal.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For ordinal.thy.  Ordinals in Zermelo-Fraenkel Set Theory 
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open Ord;
clasohm@0
    10
clasohm@0
    11
(*** Rules for Transset ***)
clasohm@0
    12
clasohm@0
    13
(** Two neat characterisations of Transset **)
clasohm@0
    14
clasohm@0
    15
goalw Ord.thy [Transset_def] "Transset(A) <-> A<=Pow(A)";
clasohm@0
    16
by (fast_tac ZF_cs 1);
clasohm@0
    17
val Transset_iff_Pow = result();
clasohm@0
    18
clasohm@0
    19
goalw Ord.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
clasohm@0
    20
by (fast_tac (eq_cs addSEs [equalityE]) 1);
clasohm@0
    21
val Transset_iff_Union_succ = result();
clasohm@0
    22
clasohm@0
    23
(** Consequences of downwards closure **)
clasohm@0
    24
clasohm@0
    25
goalw Ord.thy [Transset_def]
clasohm@0
    26
    "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C";
clasohm@0
    27
by (fast_tac ZF_cs 1);
clasohm@0
    28
val Transset_doubleton_D = result();
clasohm@0
    29
clasohm@0
    30
val [prem1,prem2] = goalw Ord.thy [Pair_def]
clasohm@0
    31
    "[| Transset(C); <a,b>: C |] ==> a:C & b: C";
clasohm@0
    32
by (cut_facts_tac [prem2] 1);	
clasohm@0
    33
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1);
clasohm@0
    34
val Transset_Pair_D = result();
clasohm@0
    35
clasohm@0
    36
val prem1::prems = goal Ord.thy
clasohm@0
    37
    "[| Transset(C); A*B <= C; b: B |] ==> A <= C";
clasohm@0
    38
by (cut_facts_tac prems 1);
clasohm@0
    39
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
clasohm@0
    40
val Transset_includes_domain = result();
clasohm@0
    41
clasohm@0
    42
val prem1::prems = goal Ord.thy
clasohm@0
    43
    "[| Transset(C); A*B <= C; a: A |] ==> B <= C";
clasohm@0
    44
by (cut_facts_tac prems 1);
clasohm@0
    45
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
clasohm@0
    46
val Transset_includes_range = result();
clasohm@0
    47
clasohm@0
    48
val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
clasohm@0
    49
    "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
clasohm@0
    50
br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1;
clasohm@0
    51
by (REPEAT (etac (prem1 RS Transset_includes_range) 1
clasohm@0
    52
     ORELSE resolve_tac [conjI, singletonI] 1));
clasohm@0
    53
val Transset_includes_summands = result();
clasohm@0
    54
clasohm@0
    55
val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
clasohm@0
    56
    "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
clasohm@0
    57
br (Int_Un_distrib RS ssubst) 1;
clasohm@0
    58
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
clasohm@0
    59
val Transset_sum_Int_subset = result();
clasohm@0
    60
clasohm@0
    61
(** Closure properties **)
clasohm@0
    62
clasohm@0
    63
goalw Ord.thy [Transset_def] "Transset(0)";
clasohm@0
    64
by (fast_tac ZF_cs 1);
clasohm@0
    65
val Transset_0 = result();
clasohm@0
    66
clasohm@0
    67
goalw Ord.thy [Transset_def]
clasohm@0
    68
    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Un j)";
clasohm@0
    69
by (fast_tac ZF_cs 1);
clasohm@0
    70
val Transset_Un = result();
clasohm@0
    71
clasohm@0
    72
goalw Ord.thy [Transset_def]
clasohm@0
    73
    "!!i j. [| Transset(i);  Transset(j) |] ==> Transset(i Int j)";
clasohm@0
    74
by (fast_tac ZF_cs 1);
clasohm@0
    75
val Transset_Int = result();
clasohm@0
    76
clasohm@0
    77
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))";
clasohm@0
    78
by (fast_tac ZF_cs 1);
clasohm@0
    79
val Transset_succ = result();
clasohm@0
    80
clasohm@0
    81
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))";
clasohm@0
    82
by (fast_tac ZF_cs 1);
clasohm@0
    83
val Transset_Pow = result();
clasohm@0
    84
clasohm@0
    85
goalw Ord.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))";
clasohm@0
    86
by (fast_tac ZF_cs 1);
clasohm@0
    87
val Transset_Union = result();
clasohm@0
    88
clasohm@0
    89
val [Transprem] = goalw Ord.thy [Transset_def]
clasohm@0
    90
    "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
clasohm@0
    91
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
clasohm@0
    92
val Transset_Union_family = result();
clasohm@0
    93
clasohm@0
    94
val [prem,Transprem] = goalw Ord.thy [Transset_def]
clasohm@0
    95
    "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
clasohm@0
    96
by (cut_facts_tac [prem] 1);
clasohm@0
    97
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
clasohm@0
    98
val Transset_Inter_family = result();
clasohm@0
    99
clasohm@0
   100
(*** Natural Deduction rules for Ord ***)
clasohm@0
   101
clasohm@0
   102
val prems = goalw Ord.thy [Ord_def]
clasohm@0
   103
    "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i) ";
clasohm@0
   104
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
clasohm@0
   105
val OrdI = result();
clasohm@0
   106
clasohm@0
   107
val [major] = goalw Ord.thy [Ord_def]
clasohm@0
   108
    "Ord(i) ==> Transset(i)";
clasohm@0
   109
by (rtac (major RS conjunct1) 1);
clasohm@0
   110
val Ord_is_Transset = result();
clasohm@0
   111
clasohm@0
   112
val [major,minor] = goalw Ord.thy [Ord_def]
clasohm@0
   113
    "[| Ord(i);  j:i |] ==> Transset(j) ";
clasohm@0
   114
by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
clasohm@0
   115
val Ord_contains_Transset = result();
clasohm@0
   116
clasohm@0
   117
(*** Lemmas for ordinals ***)
clasohm@0
   118
clasohm@0
   119
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [| Ord(i);  j:i |] ==> Ord(j) ";
clasohm@0
   120
by (fast_tac ZF_cs 1);
clasohm@0
   121
val Ord_in_Ord = result();
clasohm@0
   122
clasohm@0
   123
goal Ord.thy "!!i j. [| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)";
clasohm@0
   124
by (REPEAT (ares_tac [OrdI] 1
clasohm@0
   125
     ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
clasohm@0
   126
val Ord_subset_Ord = result();
clasohm@0
   127
clasohm@0
   128
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [| j:i;  Ord(i) |] ==> j<=i";
clasohm@0
   129
by (fast_tac ZF_cs 1);
clasohm@0
   130
val OrdmemD = result();
clasohm@0
   131
clasohm@0
   132
goal Ord.thy "!!i j k. [| i:j;  j:k;  Ord(k) |] ==> i:k";
clasohm@0
   133
by (REPEAT (ares_tac [OrdmemD RS subsetD] 1));
clasohm@0
   134
val Ord_trans = result();
clasohm@0
   135
clasohm@0
   136
goal Ord.thy "!!i j. [| i:j;  Ord(j) |] ==> succ(i) <= j";
clasohm@0
   137
by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1));
clasohm@0
   138
val Ord_succ_subsetI = result();
clasohm@0
   139
clasohm@0
   140
clasohm@0
   141
(*** The construction of ordinals: 0, succ, Union ***)
clasohm@0
   142
clasohm@0
   143
goal Ord.thy "Ord(0)";
clasohm@0
   144
by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1));
clasohm@0
   145
val Ord_0 = result();
clasohm@0
   146
clasohm@0
   147
goal Ord.thy "!!i. Ord(i) ==> Ord(succ(i))";
clasohm@0
   148
by (REPEAT (ares_tac [OrdI,Transset_succ] 1
clasohm@0
   149
     ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset,
clasohm@0
   150
			  Ord_contains_Transset] 1));
clasohm@0
   151
val Ord_succ = result();
clasohm@0
   152
clasohm@0
   153
val nonempty::prems = goal Ord.thy
clasohm@0
   154
    "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
clasohm@0
   155
by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
clasohm@0
   156
by (rtac Ord_is_Transset 1);
clasohm@0
   157
by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1
clasohm@0
   158
     ORELSE etac InterD 1));
clasohm@0
   159
val Ord_Inter = result();
clasohm@0
   160
clasohm@0
   161
val jmemA::prems = goal Ord.thy
clasohm@0
   162
    "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))";
clasohm@0
   163
by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);
clasohm@0
   164
by (etac RepFunE 1);
clasohm@0
   165
by (etac ssubst 1);
clasohm@0
   166
by (eresolve_tac prems 1);
clasohm@0
   167
val Ord_INT = result();
clasohm@0
   168
clasohm@0
   169
clasohm@0
   170
(*** Natural Deduction rules for Memrel ***)
clasohm@0
   171
clasohm@0
   172
goalw Ord.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A";
clasohm@0
   173
by (fast_tac ZF_cs 1);
clasohm@0
   174
val Memrel_iff = result();
clasohm@0
   175
clasohm@0
   176
val prems = goal Ord.thy "[| a: b;  a: A;  b: A |]  ==>  <a,b> : Memrel(A)";
clasohm@0
   177
by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1));
clasohm@0
   178
val MemrelI = result();
clasohm@0
   179
clasohm@0
   180
val [major,minor] = goal Ord.thy
clasohm@0
   181
    "[| <a,b> : Memrel(A);  \
clasohm@0
   182
\       [| a: A;  b: A;  a:b |]  ==> P \
clasohm@0
   183
\    |]  ==> P";
clasohm@0
   184
by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1);
clasohm@0
   185
by (etac conjE 1);
clasohm@0
   186
by (rtac minor 1);
clasohm@0
   187
by (REPEAT (assume_tac 1));
clasohm@0
   188
val MemrelE = result();
clasohm@0
   189
clasohm@0
   190
(*The membership relation (as a set) is well-founded.
clasohm@0
   191
  Proof idea: show A<=B by applying the foundation axiom to A-B *)
clasohm@0
   192
goalw Ord.thy [wf_def] "wf(Memrel(A))";
clasohm@0
   193
by (EVERY1 [rtac (foundation RS disjE RS allI),
clasohm@0
   194
	    etac disjI1,
clasohm@0
   195
	    etac bexE, 
clasohm@0
   196
	    rtac (impI RS allI RS bexI RS disjI2),
clasohm@0
   197
	    etac MemrelE,
clasohm@0
   198
	    etac bspec,
clasohm@0
   199
	    REPEAT o assume_tac]);
clasohm@0
   200
val wf_Memrel = result();
clasohm@0
   201
clasohm@0
   202
(*** Transfinite induction ***)
clasohm@0
   203
clasohm@0
   204
(*Epsilon induction over a transitive set*)
clasohm@0
   205
val major::prems = goalw Ord.thy [Transset_def]
clasohm@0
   206
    "[| i: k;  Transset(k);                          \
clasohm@0
   207
\       !!x.[| x: k;  ALL y:x. P(y) |] ==> P(x) \
clasohm@0
   208
\    |]  ==>  P(i)";
clasohm@0
   209
by (rtac (major RS (wf_Memrel RS wf_induct2)) 1);
clasohm@0
   210
by (fast_tac (ZF_cs addEs [MemrelE]) 1);
clasohm@0
   211
by (resolve_tac prems 1);
clasohm@0
   212
by (assume_tac 1);
clasohm@0
   213
by (cut_facts_tac prems 1);
clasohm@0
   214
by (fast_tac (ZF_cs addIs [MemrelI]) 1);
clasohm@0
   215
val Transset_induct = result();
clasohm@0
   216
clasohm@0
   217
(*Induction over an ordinal*)
clasohm@0
   218
val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
clasohm@0
   219
clasohm@0
   220
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
clasohm@0
   221
val [major,indhyp] = goal Ord.thy
clasohm@0
   222
    "[| Ord(i); \
clasohm@0
   223
\       !!x.[| Ord(x);  ALL y:x. P(y) |] ==> P(x) \
clasohm@0
   224
\    |]  ==>  P(i)";
clasohm@0
   225
by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1);
clasohm@0
   226
by (rtac indhyp 1);
clasohm@0
   227
by (rtac (major RS Ord_succ RS Ord_in_Ord) 1);
clasohm@0
   228
by (REPEAT (assume_tac 1));
clasohm@0
   229
val trans_induct = result();
clasohm@0
   230
clasohm@0
   231
(*Perform induction on i, then prove the Ord(i) subgoal using prems. *)
clasohm@0
   232
fun trans_ind_tac a prems i = 
clasohm@0
   233
    EVERY [res_inst_tac [("i",a)] trans_induct i,
clasohm@0
   234
	   rename_last_tac a ["1"] (i+1),
clasohm@0
   235
	   ares_tac prems i];
clasohm@0
   236
clasohm@0
   237
clasohm@0
   238
(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
clasohm@0
   239
clasohm@0
   240
(*Finds contradictions for the following proof*)
clasohm@0
   241
val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac];
clasohm@0
   242
clasohm@0
   243
(** Proving that "member" is a linear ordering on the ordinals **)
clasohm@0
   244
clasohm@0
   245
val prems = goal Ord.thy
clasohm@0
   246
    "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
clasohm@0
   247
by (trans_ind_tac "i" prems 1);
clasohm@0
   248
by (rtac (impI RS allI) 1);
clasohm@0
   249
by (trans_ind_tac "j" [] 1);
clasohm@0
   250
by (DEPTH_SOLVE (swap_res_tac [disjCI,equalityI,subsetI] 1
clasohm@0
   251
     ORELSE ball_tac 1
clasohm@0
   252
     ORELSE eresolve_tac [impE,disjE,allE] 1 
clasohm@0
   253
     ORELSE hyp_subst_tac 1
clasohm@0
   254
     ORELSE Ord_trans_tac 1));
clasohm@0
   255
val Ord_linear_lemma = result();
clasohm@0
   256
clasohm@0
   257
val ordi::ordj::prems = goal Ord.thy
clasohm@0
   258
    "[| Ord(i);  Ord(j);  i:j ==> P;  i=j ==> P;  j:i ==> P |] \
clasohm@0
   259
\    ==> P";
clasohm@0
   260
by (rtac (ordi RS Ord_linear_lemma RS spec RS impE) 1);
clasohm@0
   261
by (rtac ordj 1);
clasohm@0
   262
by (REPEAT (eresolve_tac (prems@[asm_rl,disjE]) 1)); 
clasohm@0
   263
val Ord_linear = result();
clasohm@0
   264
clasohm@0
   265
val prems = goal Ord.thy
clasohm@0
   266
    "[| Ord(i);  Ord(j);  i<=j ==> P;  j<=i ==> P |] \
clasohm@0
   267
\    ==> P";
clasohm@0
   268
by (res_inst_tac [("i","i"),("j","j")] Ord_linear 1);
clasohm@0
   269
by (DEPTH_SOLVE (ares_tac (prems@[subset_refl]) 1
clasohm@0
   270
          ORELSE eresolve_tac [asm_rl,OrdmemD,ssubst] 1));
clasohm@0
   271
val Ord_subset = result();
clasohm@0
   272
clasohm@0
   273
goal Ord.thy "!!i j. [| j<=i;  ~ i<=j;  Ord(i);  Ord(j) |] ==> j:i";
clasohm@0
   274
by (etac Ord_linear 1);
clasohm@0
   275
by (REPEAT (ares_tac [subset_refl] 1
clasohm@0
   276
     ORELSE eresolve_tac [notE,OrdmemD,ssubst] 1));
clasohm@0
   277
val Ord_member = result();
clasohm@0
   278
clasohm@0
   279
val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)";
clasohm@0
   280
by (rtac (empty_subsetI RS Ord_member) 1);
clasohm@0
   281
by (fast_tac ZF_cs 1);
clasohm@0
   282
by (rtac (prem RS Ord_succ) 1);
clasohm@0
   283
by (rtac Ord_0 1);
clasohm@0
   284
val Ord_0_mem_succ = result();
clasohm@0
   285
clasohm@0
   286
goal Ord.thy "!!i j. [| Ord(i);  Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)";
clasohm@0
   287
by (rtac iffI 1);
clasohm@0
   288
by (rtac conjI 1);
clasohm@0
   289
by (etac OrdmemD 1);
clasohm@0
   290
by (rtac (mem_anti_refl RS notI) 2);
clasohm@0
   291
by (etac subsetD 2);
clasohm@0
   292
by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1));
clasohm@0
   293
val Ord_member_iff = result();
clasohm@0
   294
clasohm@0
   295
goal Ord.thy "!!i. Ord(i) ==> 0:i  <-> ~ i=0";
clasohm@0
   296
be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1;
clasohm@0
   297
by (fast_tac eq_cs 1);
clasohm@0
   298
val Ord_0_member_iff = result();
clasohm@0
   299
clasohm@0
   300
(** For ordinals, i: succ(j) means 'less-than or equals' **)
clasohm@0
   301
clasohm@0
   302
goal Ord.thy "!!i j. [| j<=i;  Ord(i);  Ord(j) |] ==> j : succ(i)";
clasohm@0
   303
by (rtac Ord_member 1);
clasohm@0
   304
by (REPEAT (ares_tac [Ord_succ] 3));
clasohm@0
   305
by (rtac (mem_anti_refl RS notI) 2);
clasohm@0
   306
by (etac subsetD 2);
clasohm@0
   307
by (ALLGOALS (fast_tac ZF_cs));
clasohm@0
   308
val member_succI = result();
clasohm@0
   309
clasohm@0
   310
goalw Ord.thy [Transset_def,Ord_def]
clasohm@0
   311
    "!!i j. [| i : succ(j);  Ord(j) |] ==> i<=j";
clasohm@0
   312
by (fast_tac ZF_cs 1);
clasohm@0
   313
val member_succD = result();
clasohm@0
   314
clasohm@0
   315
goal Ord.thy "!!i j. [| Ord(i);  Ord(j) |] ==> j:succ(i) <-> j<=i";
clasohm@0
   316
by (fast_tac (subset_cs addSEs [member_succI, member_succD]) 1);
clasohm@0
   317
val member_succ_iff = result();
clasohm@0
   318
clasohm@0
   319
goal Ord.thy
clasohm@0
   320
    "!!i j. [| Ord(i);  Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
lcp@6
   321
by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
clasohm@0
   322
by (fast_tac ZF_cs 1);
clasohm@0
   323
val subset_succ_iff = result();
clasohm@0
   324
clasohm@0
   325
goal Ord.thy "!!i j. [| i:succ(j);  j:k;  Ord(k) |] ==> i:k";
clasohm@0
   326
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);
clasohm@0
   327
val Ord_trans1 = result();
clasohm@0
   328
clasohm@0
   329
goal Ord.thy "!!i j. [| i:j;  j:succ(k);  Ord(k) |] ==> i:k";
clasohm@0
   330
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);
clasohm@0
   331
val Ord_trans2 = result();
clasohm@0
   332
clasohm@0
   333
goal Ord.thy "!!i jk. [| i:j;  j<=k;  Ord(k) |] ==> i:k";
clasohm@0
   334
by (fast_tac (ZF_cs addEs [Ord_trans]) 1);
clasohm@0
   335
val Ord_transsub2 = result();
clasohm@0
   336
clasohm@0
   337
goal Ord.thy "!!i j. [| i:j;  Ord(j) |] ==> succ(i) : succ(j)";
clasohm@0
   338
by (rtac member_succI 1);
clasohm@0
   339
by (REPEAT (ares_tac [subsetI,Ord_succ,Ord_in_Ord] 1   
clasohm@0
   340
     ORELSE eresolve_tac [succE,Ord_trans,ssubst] 1));
clasohm@0
   341
val succ_mem_succI = result();
clasohm@0
   342
clasohm@0
   343
goal Ord.thy "!!i j. [| succ(i) : succ(j);  Ord(j) |] ==> i:j";
clasohm@0
   344
by (REPEAT (eresolve_tac [asm_rl, make_elim member_succD, succ_subsetE] 1));
clasohm@0
   345
val succ_mem_succE = result();
clasohm@0
   346
clasohm@0
   347
goal Ord.thy "!!i j. Ord(j) ==> succ(i) : succ(j) <-> i:j";
clasohm@0
   348
by (REPEAT (ares_tac [iffI,succ_mem_succI,succ_mem_succE] 1));
clasohm@0
   349
val succ_mem_succ_iff = result();
clasohm@0
   350
clasohm@0
   351
goal Ord.thy "!!i j. [| i<=j;  Ord(i);  Ord(j) |] ==> succ(i) <= succ(j)";
clasohm@0
   352
by (rtac (member_succI RS succ_mem_succI RS member_succD) 1);
clasohm@0
   353
by (REPEAT (ares_tac [Ord_succ] 1));
clasohm@0
   354
val Ord_succ_mono = result();
clasohm@0
   355
clasohm@0
   356
goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
clasohm@0
   357
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
clasohm@0
   358
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
lcp@6
   359
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
clasohm@0
   360
by (rtac (Un_commute RS ssubst) 1);
lcp@6
   361
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
clasohm@0
   362
val Ord_member_UnI = result();
clasohm@0
   363
clasohm@0
   364
goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Int j : k";
clasohm@0
   365
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
clasohm@0
   366
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
lcp@6
   367
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
clasohm@0
   368
by (rtac (Int_commute RS ssubst) 1);
lcp@6
   369
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
clasohm@0
   370
val Ord_member_IntI = result();
clasohm@0
   371
clasohm@0
   372
clasohm@0
   373
(*** Results about limits ***)
clasohm@0
   374
clasohm@0
   375
val prems = goal Ord.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
clasohm@0
   376
by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);
clasohm@0
   377
by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));
clasohm@0
   378
val Ord_Union = result();
clasohm@0
   379
clasohm@0
   380
val prems = goal Ord.thy "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))";
clasohm@0
   381
by (rtac Ord_Union 1);
clasohm@0
   382
by (etac RepFunE 1);
clasohm@0
   383
by (etac ssubst 1);
clasohm@0
   384
by (eresolve_tac prems 1);
clasohm@0
   385
val Ord_UN = result();
clasohm@0
   386
clasohm@0
   387
(*The upper bound must be a successor ordinal --
clasohm@0
   388
  consider that (UN i:nat.i)=nat although nat is an upper bound of each i*)
clasohm@0
   389
val [ordi,limit] = goal Ord.thy
clasohm@0
   390
    "[| Ord(i);  !!y. y:A ==> f(y): succ(i) |] ==> (UN y:A. f(y)) : succ(i)";
clasohm@0
   391
by (rtac (member_succD RS UN_least RS member_succI) 1);
clasohm@0
   392
by (REPEAT (ares_tac [ordi, Ord_UN, ordi RS Ord_succ RS Ord_in_Ord,
clasohm@0
   393
		      limit] 1));
clasohm@0
   394
val sup_least = result();
clasohm@0
   395
clasohm@0
   396
val [jmemi,ordi,limit] = goal Ord.thy
clasohm@0
   397
    "[| j: i;  Ord(i);  !!y. y:A ==> f(y): j |] ==> (UN y:A. succ(f(y))) : i";
clasohm@0
   398
by (cut_facts_tac [jmemi RS (ordi RS Ord_in_Ord)] 1);
clasohm@0
   399
by (rtac (sup_least RS Ord_trans2) 1);
clasohm@0
   400
by (REPEAT (ares_tac [jmemi, ordi, succ_mem_succI, limit] 1));
clasohm@0
   401
val sup_least2 = result();
clasohm@0
   402
clasohm@0
   403
goal Ord.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
clasohm@0
   404
by (fast_tac (eq_cs addSEs [Ord_trans1]) 1);
clasohm@0
   405
val Ord_equality = result();
clasohm@0
   406
clasohm@0
   407
(*Holds for all transitive sets, not just ordinals*)
clasohm@0
   408
goal Ord.thy "!!i. Ord(i) ==> Union(i) <= i";
clasohm@0
   409
by (fast_tac (ZF_cs addSEs [Ord_trans]) 1);
clasohm@0
   410
val Ord_Union_subset = result();