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