src/ZF/OrderType.ML
changeset 1461 6bcb44e4d6e5
parent 1032 54b9f670c67e
child 2033 639de962ded4
equal deleted inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
     1 (*  Title: 	ZF/OrderType.ML
     1 (*  Title:      ZF/OrderType.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory 
     6 Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory 
     7 
     7 
     8 Ordinal arithmetic is traditionally defined in terms of order types, as here.
     8 Ordinal arithmetic is traditionally defined in terms of order types, as here.
    17 val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))";
    17 val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))";
    18 by (rtac well_ordI 1);
    18 by (rtac well_ordI 1);
    19 by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
    19 by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
    20 by (resolve_tac [prem RS ltE] 1);
    20 by (resolve_tac [prem RS ltE] 1);
    21 by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff,
    21 by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff,
    22 				  [ltI, prem] MRS lt_trans2 RS ltD]) 1);
    22                                   [ltI, prem] MRS lt_trans2 RS ltD]) 1);
    23 by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
    23 by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
    24 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
    24 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
    25 qed "le_well_ord_Memrel";
    25 qed "le_well_ord_Memrel";
    26 
    26 
    27 (*"Ord(i) ==> well_ord(i, Memrel(i))"*)
    27 (*"Ord(i) ==> well_ord(i, Memrel(i))"*)
    52 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1);
    52 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1);
    53 qed "Ord_iso_implies_eq_lemma";
    53 qed "Ord_iso_implies_eq_lemma";
    54 
    54 
    55 (*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
    55 (*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
    56 goal OrderType.thy
    56 goal OrderType.thy
    57     "!!i. [| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j))	\
    57     "!!i. [| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j))     \
    58 \         |] ==> i=j";
    58 \         |] ==> i=j";
    59 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
    59 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
    60 by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
    60 by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
    61 qed "Ord_iso_implies_eq";
    61 qed "Ord_iso_implies_eq";
    62 
    62 
    86 (*Useful for rewriting PROVIDED pred is not unfolded until later!*)
    86 (*Useful for rewriting PROVIDED pred is not unfolded until later!*)
    87 goal OrderType.thy 
    87 goal OrderType.thy 
    88     "!!r. [| wf[A](r);  x:A |] ==> \
    88     "!!r. [| wf[A](r);  x:A |] ==> \
    89 \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
    89 \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
    90 by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
    90 by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
    91 				  ordermap_type RS image_fun]) 1);
    91                                   ordermap_type RS image_fun]) 1);
    92 qed "ordermap_pred_unfold";
    92 qed "ordermap_pred_unfold";
    93 
    93 
    94 (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
    94 (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
    95 val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
    95 val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
    96 
    96 
    97 (*** Showing that ordermap, ordertype yield ordinals ***)
    97 (*** Showing that ordermap, ordertype yield ordinals ***)
    98 
    98 
    99 fun ordermap_elim_tac i =
    99 fun ordermap_elim_tac i =
   100     EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
   100     EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
   101 	   assume_tac (i+1),
   101            assume_tac (i+1),
   102 	   assume_tac i];
   102            assume_tac i];
   103 
   103 
   104 goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
   104 goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
   105     "!!r. [| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)";
   105     "!!r. [| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)";
   106 by (safe_tac ZF_cs);
   106 by (safe_tac ZF_cs);
   107 by (wf_on_ind_tac "x" [] 1);
   107 by (wf_on_ind_tac "x" [] 1);
   126 qed "Ord_ordertype";
   126 qed "Ord_ordertype";
   127 
   127 
   128 (*** ordermap preserves the orderings in both directions ***)
   128 (*** ordermap preserves the orderings in both directions ***)
   129 
   129 
   130 goal OrderType.thy
   130 goal OrderType.thy
   131     "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>	\
   131     "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>    \
   132 \         ordermap(A,r)`w : ordermap(A,r)`x";
   132 \         ordermap(A,r)`w : ordermap(A,r)`x";
   133 by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
   133 by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
   134 by (assume_tac 1);
   134 by (assume_tac 1);
   135 by (fast_tac ZF_cs 1);
   135 by (fast_tac ZF_cs 1);
   136 qed "ordermap_mono";
   136 qed "ordermap_mono";
   147 by (etac mem_asym 1);
   147 by (etac mem_asym 1);
   148 by (assume_tac 1);
   148 by (assume_tac 1);
   149 qed "converse_ordermap_mono";
   149 qed "converse_ordermap_mono";
   150 
   150 
   151 bind_thm ("ordermap_surj", 
   151 bind_thm ("ordermap_surj", 
   152 	  rewrite_rule [symmetric ordertype_def] 
   152           rewrite_rule [symmetric ordertype_def] 
   153 	      (ordermap_type RS surj_image));
   153               (ordermap_type RS surj_image));
   154 
   154 
   155 goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
   155 goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
   156     "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
   156     "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
   157 by (fast_tac (ZF_cs addSIs [ordermap_type, ordermap_surj]
   157 by (fast_tac (ZF_cs addSIs [ordermap_type, ordermap_surj]
   158 		    addEs [linearE]
   158                     addEs [linearE]
   159 		    addDs [ordermap_mono]
   159                     addDs [ordermap_mono]
   160                     addss (ZF_ss addsimps [mem_not_refl])) 1);
   160                     addss (ZF_ss addsimps [mem_not_refl])) 1);
   161 qed "ordermap_bij";
   161 qed "ordermap_bij";
   162 
   162 
   163 (*** Isomorphisms involving ordertype ***)
   163 (*** Isomorphisms involving ordertype ***)
   164 
   164 
   169 by (rtac ordermap_bij 1);
   169 by (rtac ordermap_bij 1);
   170 by (assume_tac 1);
   170 by (assume_tac 1);
   171 by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
   171 by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
   172 by (rewtac well_ord_def);
   172 by (rewtac well_ord_def);
   173 by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
   173 by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
   174 			    ordermap_type RS apply_type]) 1);
   174                             ordermap_type RS apply_type]) 1);
   175 qed "ordertype_ord_iso";
   175 qed "ordertype_ord_iso";
   176 
   176 
   177 goal OrderType.thy
   177 goal OrderType.thy
   178     "!!f. [| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==>	\
   178     "!!f. [| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==> \
   179 \    ordertype(A,r) = ordertype(B,s)";
   179 \    ordertype(A,r) = ordertype(B,s)";
   180 by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
   180 by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
   181 by (resolve_tac [Ord_iso_implies_eq] 1
   181 by (rtac Ord_iso_implies_eq 1
   182     THEN REPEAT (eresolve_tac [Ord_ordertype] 1));
   182     THEN REPEAT (etac Ord_ordertype 1));
   183 by (deepen_tac (ZF_cs addIs  [ord_iso_trans, ord_iso_sym]
   183 by (deepen_tac (ZF_cs addIs  [ord_iso_trans, ord_iso_sym]
   184                       addSEs [ordertype_ord_iso]) 0 1);
   184                       addSEs [ordertype_ord_iso]) 0 1);
   185 qed "ordertype_eq";
   185 qed "ordertype_eq";
   186 
   186 
   187 goal OrderType.thy
   187 goal OrderType.thy
   188     "!!A B. [| ordertype(A,r) = ordertype(B,s);	\
   188     "!!A B. [| ordertype(A,r) = ordertype(B,s); \
   189 \              well_ord(A,r);  well_ord(B,s) \
   189 \              well_ord(A,r);  well_ord(B,s) \
   190 \           |] ==> EX f. f: ord_iso(A,r,B,s)";
   190 \           |] ==> EX f. f: ord_iso(A,r,B,s)";
   191 by (resolve_tac [exI] 1);
   191 by (rtac exI 1);
   192 by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1);
   192 by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1);
   193 by (assume_tac 1);
   193 by (assume_tac 1);
   194 by (eresolve_tac [ssubst] 1);
   194 by (etac ssubst 1);
   195 by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
   195 by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
   196 qed "ordertype_eq_imp_ord_iso";
   196 qed "ordertype_eq_imp_ord_iso";
   197 
   197 
   198 (*** Basic equalities for ordertype ***)
   198 (*** Basic equalities for ordertype ***)
   199 
   199 
   200 (*Ordertype of Memrel*)
   200 (*Ordertype of Memrel*)
   201 goal OrderType.thy "!!i. j le i ==> ordertype(j,Memrel(i)) = j";
   201 goal OrderType.thy "!!i. j le i ==> ordertype(j,Memrel(i)) = j";
   202 by (resolve_tac [Ord_iso_implies_eq RS sym] 1);
   202 by (resolve_tac [Ord_iso_implies_eq RS sym] 1);
   203 by (eresolve_tac [ltE] 1);
   203 by (etac ltE 1);
   204 by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1));
   204 by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1));
   205 by (resolve_tac [ord_iso_trans] 1);
   205 by (rtac ord_iso_trans 1);
   206 by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2);
   206 by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2);
   207 by (resolve_tac [id_bij RS ord_isoI] 1);
   207 by (resolve_tac [id_bij RS ord_isoI] 1);
   208 by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1);
   208 by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1);
   209 by (fast_tac (ZF_cs addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
   209 by (fast_tac (ZF_cs addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
   210 qed "le_ordertype_Memrel";
   210 qed "le_ordertype_Memrel";
   213 bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel);
   213 bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel);
   214 
   214 
   215 goal OrderType.thy "ordertype(0,r) = 0";
   215 goal OrderType.thy "ordertype(0,r) = 0";
   216 by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1);
   216 by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1);
   217 by (etac emptyE 1);
   217 by (etac emptyE 1);
   218 by (resolve_tac [well_ord_0] 1);
   218 by (rtac well_ord_0 1);
   219 by (resolve_tac [Ord_0 RS ordertype_Memrel] 1);
   219 by (resolve_tac [Ord_0 RS ordertype_Memrel] 1);
   220 qed "ordertype_0";
   220 qed "ordertype_0";
   221 
   221 
   222 (*Ordertype of rvimage:  [| f: bij(A,B);  well_ord(B,s) |] ==>
   222 (*Ordertype of rvimage:  [| f: bij(A,B);  well_ord(B,s) |] ==>
   223                          ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
   223                          ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
   225 
   225 
   226 (*** A fundamental unfolding law for ordertype. ***)
   226 (*** A fundamental unfolding law for ordertype. ***)
   227 
   227 
   228 (*Ordermap returns the same result if applied to an initial segment*)
   228 (*Ordermap returns the same result if applied to an initial segment*)
   229 goal OrderType.thy
   229 goal OrderType.thy
   230     "!!r. [| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>	\
   230     "!!r. [| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>        \
   231 \	  ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
   231 \         ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
   232 by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
   232 by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
   233 by (wf_on_ind_tac "z" [] 1);
   233 by (wf_on_ind_tac "z" [] 1);
   234 by (safe_tac (ZF_cs addSEs [predE]));
   234 by (safe_tac (ZF_cs addSEs [predE]));
   235 by (asm_simp_tac
   235 by (asm_simp_tac
   236     (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
   236     (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
   253     "!!r. [| well_ord(A,r);  x:A |] ==>  \
   253     "!!r. [| well_ord(A,r);  x:A |] ==>  \
   254 \         ordertype(pred(A,x,r),r) <= ordertype(A,r)";
   254 \         ordertype(pred(A,x,r),r) <= ordertype(A,r)";
   255 by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, 
   255 by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, 
   256                   pred_subset RSN (2, well_ord_subset)]) 1);
   256                   pred_subset RSN (2, well_ord_subset)]) 1);
   257 by (fast_tac (ZF_cs addIs [ordermap_pred_eq_ordermap, RepFun_eqI]
   257 by (fast_tac (ZF_cs addIs [ordermap_pred_eq_ordermap, RepFun_eqI]
   258 	            addEs [predE]) 1);
   258                     addEs [predE]) 1);
   259 qed "ordertype_pred_subset";
   259 qed "ordertype_pred_subset";
   260 
   260 
   261 goal OrderType.thy
   261 goal OrderType.thy
   262     "!!r. [| well_ord(A,r);  x:A |] ==>  \
   262     "!!r. [| well_ord(A,r);  x:A |] ==>  \
   263 \         ordertype(pred(A,x,r),r) < ordertype(A,r)";
   263 \         ordertype(pred(A,x,r),r) < ordertype(A,r)";
   264 by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1);
   264 by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1);
   265 by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1));
   265 by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1));
   266 by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1);
   266 by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1);
   267 by (eresolve_tac [well_ord_iso_predE] 3);
   267 by (etac well_ord_iso_predE 3);
   268 by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1));
   268 by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1));
   269 qed "ordertype_pred_lt";
   269 qed "ordertype_pred_lt";
   270 
   270 
   271 (*May rewrite with this -- provided no rules are supplied for proving that
   271 (*May rewrite with this -- provided no rules are supplied for proving that
   272  	well_ord(pred(A,x,r), r) *)
   272         well_ord(pred(A,x,r), r) *)
   273 goal OrderType.thy
   273 goal OrderType.thy
   274     "!!A r. well_ord(A,r) ==>  \
   274     "!!A r. well_ord(A,r) ==>  \
   275 \           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
   275 \           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
   276 by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD]));
   276 by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD]));
   277 by (fast_tac
   277 by (fast_tac
   278     (ZF_cs addss
   278     (ZF_cs addss
   279      (ZF_ss addsimps [ordertype_def, 
   279      (ZF_ss addsimps [ordertype_def, 
   280 		      well_ord_is_wf RS ordermap_eq_image, 
   280                       well_ord_is_wf RS ordermap_eq_image, 
   281 		      ordermap_type RS image_fun, 
   281                       ordermap_type RS image_fun, 
   282 		      ordermap_pred_eq_ordermap, 
   282                       ordermap_pred_eq_ordermap, 
   283 		      pred_subset]))
   283                       pred_subset]))
   284     1);
   284     1);
   285 qed "ordertype_pred_unfold";
   285 qed "ordertype_pred_unfold";
   286 
   286 
   287 
   287 
   288 (**** Alternative definition of ordinal ****)
   288 (**** Alternative definition of ordinal ****)
   289 
   289 
   290 (*proof by Krzysztof Grabczewski*)
   290 (*proof by Krzysztof Grabczewski*)
   291 goalw OrderType.thy [Ord_alt_def] "!!i. Ord(i) ==> Ord_alt(i)";
   291 goalw OrderType.thy [Ord_alt_def] "!!i. Ord(i) ==> Ord_alt(i)";
   292 by (resolve_tac [conjI] 1);
   292 by (rtac conjI 1);
   293 by (eresolve_tac [well_ord_Memrel] 1);
   293 by (etac well_ord_Memrel 1);
   294 by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
   294 by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
   295 by (fast_tac eq_cs 1);
   295 by (fast_tac eq_cs 1);
   296 qed "Ord_is_Ord_alt";
   296 qed "Ord_is_Ord_alt";
   297 
   297 
   298 (*proof by lcp*)
   298 (*proof by lcp*)
   299 goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, 
   299 goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, 
   300 		     tot_ord_def, part_ord_def, trans_on_def] 
   300                      tot_ord_def, part_ord_def, trans_on_def] 
   301     "!!i. Ord_alt(i) ==> Ord(i)";
   301     "!!i. Ord_alt(i) ==> Ord(i)";
   302 by (asm_full_simp_tac (ZF_ss addsimps [Memrel_iff, pred_Memrel]) 1);
   302 by (asm_full_simp_tac (ZF_ss addsimps [Memrel_iff, pred_Memrel]) 1);
   303 by (safe_tac ZF_cs);
   303 by (safe_tac ZF_cs);
   304 by (fast_tac (ZF_cs addSDs [equalityD1]) 1);
   304 by (fast_tac (ZF_cs addSDs [equalityD1]) 1);
   305 by (subgoal_tac "xa: i" 1);
   305 by (subgoal_tac "xa: i" 1);
   344 (** Initial segments of radd.  Statements by Grabczewski **)
   344 (** Initial segments of radd.  Statements by Grabczewski **)
   345 
   345 
   346 (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
   346 (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
   347 goalw OrderType.thy [pred_def]
   347 goalw OrderType.thy [pred_def]
   348  "!!A B. a:A ==>  \
   348  "!!A B. a:A ==>  \
   349 \        (lam x:pred(A,a,r). Inl(x))	\
   349 \        (lam x:pred(A,a,r). Inl(x))    \
   350 \        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
   350 \        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
   351 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
   351 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
   352 by (safe_tac sum_cs);
   352 by (safe_tac sum_cs);
   353 by (ALLGOALS
   353 by (ALLGOALS
   354     (asm_full_simp_tac 
   354     (asm_full_simp_tac 
   364 by (asm_full_simp_tac (ZF_ss addsimps [radd_Inl_iff, pred_def]) 1);
   364 by (asm_full_simp_tac (ZF_ss addsimps [radd_Inl_iff, pred_def]) 1);
   365 qed "ordertype_pred_Inl_eq";
   365 qed "ordertype_pred_Inl_eq";
   366 
   366 
   367 goalw OrderType.thy [pred_def, id_def]
   367 goalw OrderType.thy [pred_def, id_def]
   368  "!!A B. b:B ==>  \
   368  "!!A B. b:B ==>  \
   369 \        id(A+pred(B,b,s))	\
   369 \        id(A+pred(B,b,s))      \
   370 \        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
   370 \        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
   371 by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
   371 by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
   372 by (safe_tac sum_cs);
   372 by (safe_tac sum_cs);
   373 by (ALLGOALS (asm_full_simp_tac radd_ss));
   373 by (ALLGOALS (asm_full_simp_tac radd_ss));
   374 qed "pred_Inr_bij";
   374 qed "pred_Inr_bij";
   391 
   391 
   392 (** Ordinal addition with zero **)
   392 (** Ordinal addition with zero **)
   393 
   393 
   394 goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> i++0 = i";
   394 goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> i++0 = i";
   395 by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_sum_0_eq, 
   395 by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_sum_0_eq, 
   396 				  ordertype_Memrel, well_ord_Memrel]) 1);
   396                                   ordertype_Memrel, well_ord_Memrel]) 1);
   397 qed "oadd_0";
   397 qed "oadd_0";
   398 
   398 
   399 goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> 0++i = i";
   399 goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> 0++i = i";
   400 by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_0_sum_eq, 
   400 by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_0_sum_eq, 
   401 				  ordertype_Memrel, well_ord_Memrel]) 1);
   401                                   ordertype_Memrel, well_ord_Memrel]) 1);
   402 qed "oadd_0_left";
   402 qed "oadd_0_left";
   403 
   403 
   404 
   404 
   405 (*** Further properties of ordinal addition.  Statements by Grabczewski,
   405 (*** Further properties of ordinal addition.  Statements by Grabczewski,
   406     proofs by lcp. ***)
   406     proofs by lcp. ***)
   407 
   407 
   408 goalw OrderType.thy [oadd_def] "!!i j k. [| k<i;  Ord(j) |] ==> k < i++j";
   408 goalw OrderType.thy [oadd_def] "!!i j k. [| k<i;  Ord(j) |] ==> k < i++j";
   409 by (resolve_tac [ltE] 1 THEN assume_tac 1);
   409 by (rtac ltE 1 THEN assume_tac 1);
   410 by (resolve_tac [ltI] 1);
   410 by (rtac ltI 1);
   411 by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
   411 by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
   412 by (asm_simp_tac 
   412 by (asm_simp_tac 
   413     (ZF_ss addsimps [ordertype_pred_unfold, 
   413     (ZF_ss addsimps [ordertype_pred_unfold, 
   414 		     well_ord_radd, well_ord_Memrel,
   414                      well_ord_radd, well_ord_Memrel,
   415 		     ordertype_pred_Inl_eq, 
   415                      ordertype_pred_Inl_eq, 
   416 		     lt_pred_Memrel, leI RS le_ordertype_Memrel]
   416                      lt_pred_Memrel, leI RS le_ordertype_Memrel]
   417 	   setloop rtac (InlI RSN (2,RepFun_eqI))) 1);
   417            setloop rtac (InlI RSN (2,RepFun_eqI))) 1);
   418 qed "lt_oadd1";
   418 qed "lt_oadd1";
   419 
   419 
   420 (*Thus also we obtain the rule  i++j = k ==> i le k *)
   420 (*Thus also we obtain the rule  i++j = k ==> i le k *)
   421 goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le i++j";
   421 goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le i++j";
   422 by (resolve_tac [all_lt_imp_le] 1);
   422 by (rtac all_lt_imp_le 1);
   423 by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1));
   423 by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1));
   424 qed "oadd_le_self";
   424 qed "oadd_le_self";
   425 
   425 
   426 (** A couple of strange but necessary results! **)
   426 (** A couple of strange but necessary results! **)
   427 
   427 
   431 by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1);
   431 by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1);
   432 by (fast_tac ZF_cs 1);
   432 by (fast_tac ZF_cs 1);
   433 qed "id_ord_iso_Memrel";
   433 qed "id_ord_iso_Memrel";
   434 
   434 
   435 goal OrderType.thy
   435 goal OrderType.thy
   436     "!!k. [| well_ord(A,r);  k<j |] ==>			\
   436     "!!k. [| well_ord(A,r);  k<j |] ==>                 \
   437 \            ordertype(A+k, radd(A, r, k, Memrel(j))) =	\
   437 \            ordertype(A+k, radd(A, r, k, Memrel(j))) = \
   438 \            ordertype(A+k, radd(A, r, k, Memrel(k)))";
   438 \            ordertype(A+k, radd(A, r, k, Memrel(k)))";
   439 by (eresolve_tac [ltE] 1);
   439 by (etac ltE 1);
   440 by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1);
   440 by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1);
   441 by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1);
   441 by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1);
   442 by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel]));
   442 by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel]));
   443 qed "ordertype_sum_Memrel";
   443 qed "ordertype_sum_Memrel";
   444 
   444 
   445 goalw OrderType.thy [oadd_def] "!!i j k. [| k<j;  Ord(i) |] ==> i++k < i++j";
   445 goalw OrderType.thy [oadd_def] "!!i j k. [| k<j;  Ord(i) |] ==> i++k < i++j";
   446 by (resolve_tac [ltE] 1 THEN assume_tac 1);
   446 by (rtac ltE 1 THEN assume_tac 1);
   447 by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1);
   447 by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1);
   448 by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel]));
   448 by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel]));
   449 by (resolve_tac [RepFun_eqI] 1);
   449 by (rtac RepFun_eqI 1);
   450 by (eresolve_tac [InrI] 2);
   450 by (etac InrI 2);
   451 by (asm_simp_tac 
   451 by (asm_simp_tac 
   452     (ZF_ss addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 
   452     (ZF_ss addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 
   453 		     lt_pred_Memrel, leI RS le_ordertype_Memrel,
   453                      lt_pred_Memrel, leI RS le_ordertype_Memrel,
   454 		     ordertype_sum_Memrel]) 1);
   454                      ordertype_sum_Memrel]) 1);
   455 qed "oadd_lt_mono2";
   455 qed "oadd_lt_mono2";
   456 
   456 
   457 goal OrderType.thy
   457 goal OrderType.thy
   458     "!!i j k. [| i++j < i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j<k";
   458     "!!i j k. [| i++j < i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j<k";
   459 by (rtac Ord_linear_lt 1);
   459 by (rtac Ord_linear_lt 1);
   480     "!!i j k. [| k < i++j;  Ord(i);  Ord(j) |] ==> k<i | (EX l:j. k = i++l )";
   480     "!!i j k. [| k < i++j;  Ord(i);  Ord(j) |] ==> k<i | (EX l:j. k = i++l )";
   481 (*Rotate the hypotheses so that simplification will work*)
   481 (*Rotate the hypotheses so that simplification will work*)
   482 by (etac revcut_rl 1);
   482 by (etac revcut_rl 1);
   483 by (asm_full_simp_tac 
   483 by (asm_full_simp_tac 
   484     (ZF_ss addsimps [ordertype_pred_unfold, well_ord_radd,
   484     (ZF_ss addsimps [ordertype_pred_unfold, well_ord_radd,
   485 		     well_ord_Memrel]) 1);
   485                      well_ord_Memrel]) 1);
   486 by (eresolve_tac [ltD RS RepFunE] 1);
   486 by (eresolve_tac [ltD RS RepFunE] 1);
   487 by (fast_tac (sum_cs addss 
   487 by (fast_tac (sum_cs addss 
   488 	      (ZF_ss addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
   488               (ZF_ss addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
   489 			       ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
   489                                ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
   490 			       ordertype_pred_Inr_eq, 
   490                                ordertype_pred_Inr_eq, 
   491 			       ordertype_sum_Memrel])) 1);
   491                                ordertype_sum_Memrel])) 1);
   492 qed "lt_oadd_disj";
   492 qed "lt_oadd_disj";
   493 
   493 
   494 
   494 
   495 (*** Ordinal addition with successor -- via associativity! ***)
   495 (*** Ordinal addition with successor -- via associativity! ***)
   496 
   496 
   497 goalw OrderType.thy [oadd_def]
   497 goalw OrderType.thy [oadd_def]
   498     "!!i j k. [| Ord(i);  Ord(j);  Ord(k) |] ==> (i++j)++k = i++(j++k)";
   498     "!!i j k. [| Ord(i);  Ord(j);  Ord(k) |] ==> (i++j)++k = i++(j++k)";
   499 by (resolve_tac [ordertype_eq RS trans] 1);
   499 by (resolve_tac [ordertype_eq RS trans] 1);
   500 by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
   500 by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
   501 	  sum_ord_iso_cong) 1);
   501           sum_ord_iso_cong) 1);
   502 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
   502 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
   503 by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1);
   503 by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1);
   504 by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS 
   504 by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS 
   505 	  ordertype_eq) 2);
   505           ordertype_eq) 2);
   506 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
   506 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
   507 qed "oadd_assoc";
   507 qed "oadd_assoc";
   508 
   508 
   509 goal OrderType.thy
   509 goal OrderType.thy
   510     "!!i j. [| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
   510     "!!i j. [| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
   511 by (rtac (subsetI RS equalityI) 1);
   511 by (rtac (subsetI RS equalityI) 1);
   512 by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
   512 by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
   513 by (REPEAT (ares_tac [Ord_oadd] 1));
   513 by (REPEAT (ares_tac [Ord_oadd] 1));
   514 by (fast_tac (ZF_cs addIs [lt_oadd1, oadd_lt_mono2]
   514 by (fast_tac (ZF_cs addIs [lt_oadd1, oadd_lt_mono2]
   515 	            addss (ZF_ss addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
   515                     addss (ZF_ss addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
   516 by (fast_tac ZF_cs 2);
   516 by (fast_tac ZF_cs 2);
   517 by (fast_tac (ZF_cs addSEs [ltE]) 1);
   517 by (fast_tac (ZF_cs addSEs [ltE]) 1);
   518 qed "oadd_unfold";
   518 qed "oadd_unfold";
   519 
   519 
   520 goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
   520 goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
   533 
   533 
   534 val prems = goal OrderType.thy
   534 val prems = goal OrderType.thy
   535     "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
   535     "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
   536 \    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
   536 \    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
   537 by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
   537 by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
   538 				    lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
   538                                     lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
   539                      addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
   539                      addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
   540 qed "oadd_UN";
   540 qed "oadd_UN";
   541 
   541 
   542 goal OrderType.thy 
   542 goal OrderType.thy 
   543     "!!i j. [| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
   543     "!!i j. [| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
   544 by (forward_tac [Limit_has_0 RS ltD] 1);
   544 by (forward_tac [Limit_has_0 RS ltD] 1);
   545 by (asm_simp_tac (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord,
   545 by (asm_simp_tac (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord,
   546 				  oadd_UN RS sym, Union_eq_UN RS sym, 
   546                                   oadd_UN RS sym, Union_eq_UN RS sym, 
   547 				  Limit_Union_eq]) 1);
   547                                   Limit_Union_eq]) 1);
   548 qed "oadd_Limit";
   548 qed "oadd_Limit";
   549 
   549 
   550 (** Order/monotonicity properties of ordinal addition **)
   550 (** Order/monotonicity properties of ordinal addition **)
   551 
   551 
   552 goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le j++i";
   552 goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le j++i";
   553 by (eres_inst_tac [("i","i")] trans_induct3 1);
   553 by (eres_inst_tac [("i","i")] trans_induct3 1);
   554 by (asm_simp_tac (ZF_ss addsimps [oadd_0, Ord_0_le]) 1);
   554 by (asm_simp_tac (ZF_ss addsimps [oadd_0, Ord_0_le]) 1);
   555 by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_leI]) 1);
   555 by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_leI]) 1);
   556 by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1);
   556 by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1);
   557 by (resolve_tac [le_trans] 1);
   557 by (rtac le_trans 1);
   558 by (resolve_tac [le_implies_UN_le_UN] 2);
   558 by (rtac le_implies_UN_le_UN 2);
   559 by (fast_tac ZF_cs 2);
   559 by (fast_tac ZF_cs 2);
   560 by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
   560 by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
   561 				  le_refl, Limit_is_Ord]) 1);
   561                                   le_refl, Limit_is_Ord]) 1);
   562 qed "oadd_le_self2";
   562 qed "oadd_le_self2";
   563 
   563 
   564 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k++i le j++i";
   564 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k++i le j++i";
   565 by (forward_tac [lt_Ord] 1);
   565 by (forward_tac [lt_Ord] 1);
   566 by (forward_tac [le_Ord2] 1);
   566 by (forward_tac [le_Ord2] 1);
   567 by (eresolve_tac [trans_induct3] 1);
   567 by (etac trans_induct3 1);
   568 by (asm_simp_tac (ZF_ss addsimps [oadd_0]) 1);
   568 by (asm_simp_tac (ZF_ss addsimps [oadd_0]) 1);
   569 by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_le_iff]) 1);
   569 by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_le_iff]) 1);
   570 by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1);
   570 by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1);
   571 by (resolve_tac [le_implies_UN_le_UN] 1);
   571 by (rtac le_implies_UN_le_UN 1);
   572 by (fast_tac ZF_cs 1);
   572 by (fast_tac ZF_cs 1);
   573 qed "oadd_le_mono1";
   573 qed "oadd_le_mono1";
   574 
   574 
   575 goal OrderType.thy "!!i j. [| i' le i;  j'<j |] ==> i'++j' < i++j";
   575 goal OrderType.thy "!!i j. [| i' le i;  j'<j |] ==> i'++j' < i++j";
   576 by (resolve_tac [lt_trans1] 1);
   576 by (rtac lt_trans1 1);
   577 by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE,
   577 by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE,
   578 			  Ord_succD] 1));
   578                           Ord_succD] 1));
   579 qed "oadd_lt_mono";
   579 qed "oadd_lt_mono";
   580 
   580 
   581 goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'++j' le i++j";
   581 goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'++j' le i++j";
   582 by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
   582 by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
   583 qed "oadd_le_mono";
   583 qed "oadd_le_mono";
   584 
   584 
   585 goal OrderType.thy
   585 goal OrderType.thy
   586     "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
   586     "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
   587 by (asm_simp_tac (ZF_ss addsimps [oadd_lt_iff2, oadd_succ RS sym, 
   587 by (asm_simp_tac (ZF_ss addsimps [oadd_lt_iff2, oadd_succ RS sym, 
   588 				  Ord_succ]) 1);
   588                                   Ord_succ]) 1);
   589 qed "oadd_le_iff2";
   589 qed "oadd_le_iff2";
   590 
   590 
   591 
   591 
   592 (** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
   592 (** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
   593     Probably simpler to define the difference recursively!
   593     Probably simpler to define the difference recursively!
   596 goal OrderType.thy
   596 goal OrderType.thy
   597     "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
   597     "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
   598 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
   598 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
   599 by (fast_tac (sum_cs addSIs [if_type]) 1);
   599 by (fast_tac (sum_cs addSIs [if_type]) 1);
   600 by (fast_tac (ZF_cs addSIs [case_type]) 1);
   600 by (fast_tac (ZF_cs addSIs [case_type]) 1);
   601 by (eresolve_tac [sumE] 2);
   601 by (etac sumE 2);
   602 by (ALLGOALS (asm_simp_tac (sum_ss setloop split_tac [expand_if])));
   602 by (ALLGOALS (asm_simp_tac (sum_ss setloop split_tac [expand_if])));
   603 qed "bij_sum_Diff";
   603 qed "bij_sum_Diff";
   604 
   604 
   605 goal OrderType.thy
   605 goal OrderType.thy
   606     "!!i j. i le j ==>	\
   606     "!!i j. i le j ==>  \
   607 \           ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) = 	\
   607 \           ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =       \
   608 \           ordertype(j, Memrel(j))";
   608 \           ordertype(j, Memrel(j))";
   609 by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1]));
   609 by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1]));
   610 by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
   610 by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
   611 by (eresolve_tac [well_ord_Memrel] 3);
   611 by (etac well_ord_Memrel 3);
   612 by (assume_tac 1);
   612 by (assume_tac 1);
   613 by (asm_simp_tac 
   613 by (asm_simp_tac 
   614      (radd_ss setloop split_tac [expand_if] addsimps [Memrel_iff]) 1);
   614      (radd_ss setloop split_tac [expand_if] addsimps [Memrel_iff]) 1);
   615 by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
   615 by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
   616 by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
   616 by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
   617 by (asm_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
   617 by (asm_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
   618 by (fast_tac (ZF_cs addEs [lt_trans2, lt_trans]) 1);
   618 by (fast_tac (ZF_cs addEs [lt_trans2, lt_trans]) 1);
   619 qed "ordertype_sum_Diff";
   619 qed "ordertype_sum_Diff";
   620 
   620 
   621 goalw OrderType.thy [oadd_def, odiff_def]
   621 goalw OrderType.thy [oadd_def, odiff_def]
   622     "!!i j. i le j ==> 	\
   622     "!!i j. i le j ==>  \
   623 \           i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
   623 \           i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
   624 by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1]));
   624 by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1]));
   625 by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
   625 by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
   626 by (eresolve_tac [id_ord_iso_Memrel] 1);
   626 by (etac id_ord_iso_Memrel 1);
   627 by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
   627 by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
   628 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset,
   628 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset,
   629 		      Diff_subset] 1));
   629                       Diff_subset] 1));
   630 qed "oadd_ordertype_Diff";
   630 qed "oadd_ordertype_Diff";
   631 
   631 
   632 goal OrderType.thy "!!i j. i le j ==> i ++ (j--i) = j";
   632 goal OrderType.thy "!!i j. i le j ==> i ++ (j--i) = j";
   633 by (asm_simp_tac (ZF_ss addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, 
   633 by (asm_simp_tac (ZF_ss addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, 
   634 				  ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1);
   634                                   ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1);
   635 qed "oadd_odiff_inverse";
   635 qed "oadd_odiff_inverse";
   636 
   636 
   637 goalw OrderType.thy [odiff_def] 
   637 goalw OrderType.thy [odiff_def] 
   638     "!!i j. [| Ord(i);  Ord(j) |] ==> Ord(i--j)";
   638     "!!i j. [| Ord(i);  Ord(j) |] ==> Ord(i--j)";
   639 by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, 
   639 by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, 
   640 		      Diff_subset] 1));
   640                       Diff_subset] 1));
   641 qed "Ord_odiff";
   641 qed "Ord_odiff";
   642 
   642 
   643 (*By oadd_inject, the difference between i and j is unique.  Note that we get
   643 (*By oadd_inject, the difference between i and j is unique.  Note that we get
   644   i++j = k  ==>  j = k--i.  *)
   644   i++j = k  ==>  j = k--i.  *)
   645 goal OrderType.thy
   645 goal OrderType.thy
   646     "!!i j. [| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
   646     "!!i j. [| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
   647 br oadd_inject 1;
   647 by (rtac oadd_inject 1);
   648 by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
   648 by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
   649 by (asm_simp_tac (ZF_ss addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
   649 by (asm_simp_tac (ZF_ss addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
   650 qed "odiff_oadd_inverse";
   650 qed "odiff_oadd_inverse";
   651 
   651 
   652 val [i_lt_j, k_le_i] = goal OrderType.thy
   652 val [i_lt_j, k_le_i] = goal OrderType.thy
   653     "[| i<j;  k le i |] ==> i--k < j--k";
   653     "[| i<j;  k le i |] ==> i--k < j--k";
   654 by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
   654 by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
   655 by (simp_tac
   655 by (simp_tac
   656     (ZF_ss addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
   656     (ZF_ss addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
   657 		     oadd_odiff_inverse]) 1);
   657                      oadd_odiff_inverse]) 1);
   658 by (REPEAT (resolve_tac (Ord_odiff :: 
   658 by (REPEAT (resolve_tac (Ord_odiff :: 
   659 			 ([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1));
   659                          ([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1));
   660 qed "odiff_lt_mono2";
   660 qed "odiff_lt_mono2";
   661 
   661 
   662 
   662 
   663 (**** Ordinal Multiplication ****)
   663 (**** Ordinal Multiplication ****)
   664 
   664 
   669 
   669 
   670 (*** A useful unfolding law ***)
   670 (*** A useful unfolding law ***)
   671 
   671 
   672 goalw OrderType.thy [pred_def]
   672 goalw OrderType.thy [pred_def]
   673  "!!A B. [| a:A;  b:B |] ==>  \
   673  "!!A B. [| a:A;  b:B |] ==>  \
   674 \        pred(A*B, <a,b>, rmult(A,r,B,s)) =	\
   674 \        pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
   675 \        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
   675 \        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
   676 by (safe_tac eq_cs);
   676 by (safe_tac eq_cs);
   677 by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [rmult_iff])));
   677 by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [rmult_iff])));
   678 by (ALLGOALS (fast_tac ZF_cs));
   678 by (ALLGOALS (fast_tac ZF_cs));
   679 qed "pred_Pair_eq";
   679 qed "pred_Pair_eq";
   680 
   680 
   681 goal OrderType.thy
   681 goal OrderType.thy
   682  "!!A B. [| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
   682  "!!A B. [| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
   683 \        ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
   683 \        ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
   684 \        ordertype(pred(A,a,r)*B + pred(B,b,s), 		\
   684 \        ordertype(pred(A,a,r)*B + pred(B,b,s),                 \
   685 \                 radd(A*B, rmult(A,r,B,s), B, s))";
   685 \                 radd(A*B, rmult(A,r,B,s), B, s))";
   686 by (asm_simp_tac (ZF_ss addsimps [pred_Pair_eq]) 1);
   686 by (asm_simp_tac (ZF_ss addsimps [pred_Pair_eq]) 1);
   687 by (resolve_tac [ordertype_eq RS sym] 1);
   687 by (resolve_tac [ordertype_eq RS sym] 1);
   688 by (resolve_tac [prod_sum_singleton_ord_iso] 1);
   688 by (rtac prod_sum_singleton_ord_iso 1);
   689 by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
   689 by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
   690 by (fast_tac (ZF_cs addSEs [predE]) 1);
   690 by (fast_tac (ZF_cs addSEs [predE]) 1);
   691 qed "ordertype_pred_Pair_eq";
   691 qed "ordertype_pred_Pair_eq";
   692 
   692 
   693 goalw OrderType.thy [oadd_def, omult_def]
   693 goalw OrderType.thy [oadd_def, omult_def]
   694  "!!i j. [| i'<i;  j'<j |] ==>  \
   694  "!!i j. [| i'<i;  j'<j |] ==>  \
   695 \        ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
   695 \        ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
   696 \                  rmult(i,Memrel(i),j,Memrel(j))) = \
   696 \                  rmult(i,Memrel(i),j,Memrel(j))) = \
   697 \        j**i' ++ j'";
   697 \        j**i' ++ j'";
   698 by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, 
   698 by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, 
   699 				  ltD, lt_Ord2, well_ord_Memrel]) 1);
   699                                   ltD, lt_Ord2, well_ord_Memrel]) 1);
   700 by (resolve_tac [trans] 1);
   700 by (rtac trans 1);
   701 by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
   701 by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
   702 by (resolve_tac [ord_iso_refl] 3);
   702 by (rtac ord_iso_refl 3);
   703 by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1);
   703 by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1);
   704 by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
   704 by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
   705 by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
   705 by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
   706 			    Ord_ordertype]));
   706                             Ord_ordertype]));
   707 by (ALLGOALS 
   707 by (ALLGOALS 
   708     (asm_simp_tac (radd_ss addsimps [rmult_iff, id_conv, Memrel_iff])));
   708     (asm_simp_tac (radd_ss addsimps [rmult_iff, id_conv, Memrel_iff])));
   709 by (safe_tac ZF_cs);
   709 by (safe_tac ZF_cs);
   710 by (ALLGOALS (fast_tac (ZF_cs addEs [Ord_trans])));
   710 by (ALLGOALS (fast_tac (ZF_cs addEs [Ord_trans])));
   711 qed "ordertype_pred_Pair_lemma";
   711 qed "ordertype_pred_Pair_lemma";
   712 
   712 
   713 goalw OrderType.thy [omult_def]
   713 goalw OrderType.thy [omult_def]
   714  "!!i j. [| Ord(i);  Ord(j);  k<j**i |] ==>  \
   714  "!!i j. [| Ord(i);  Ord(j);  k<j**i |] ==>  \
   715 \        EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
   715 \        EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
   716 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold, 
   716 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold, 
   717 				       well_ord_rmult, well_ord_Memrel]) 1);
   717                                        well_ord_rmult, well_ord_Memrel]) 1);
   718 by (step_tac (ZF_cs addSEs [ltE]) 1);
   718 by (step_tac (ZF_cs addSEs [ltE]) 1);
   719 by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI,
   719 by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI,
   720 				  symmetric omult_def]) 1);
   720                                   symmetric omult_def]) 1);
   721 by (fast_tac (ZF_cs addIs [ltI]) 1);
   721 by (fast_tac (ZF_cs addIs [ltI]) 1);
   722 qed "lt_omult";
   722 qed "lt_omult";
   723 
   723 
   724 goalw OrderType.thy [omult_def]
   724 goalw OrderType.thy [omult_def]
   725  "!!i j. [| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i";
   725  "!!i j. [| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i";
   726 by (resolve_tac [ltI] 1);
   726 by (rtac ltI 1);
   727 by (asm_simp_tac
   727 by (asm_simp_tac
   728     (ZF_ss addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
   728     (ZF_ss addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
   729 		     lt_Ord2]) 2);
   729                      lt_Ord2]) 2);
   730 by (asm_simp_tac 
   730 by (asm_simp_tac 
   731     (ZF_ss addsimps [ordertype_pred_unfold, 
   731     (ZF_ss addsimps [ordertype_pred_unfold, 
   732 		     well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
   732                      well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
   733 by (resolve_tac [RepFun_eqI] 1);
   733 by (rtac RepFun_eqI 1);
   734 by (fast_tac (ZF_cs addSEs [ltE]) 2);
   734 by (fast_tac (ZF_cs addSEs [ltE]) 2);
   735 by (asm_simp_tac 
   735 by (asm_simp_tac 
   736     (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, symmetric omult_def]) 1);
   736     (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, symmetric omult_def]) 1);
   737 qed "omult_oadd_lt";
   737 qed "omult_oadd_lt";
   738 
   738 
   739 goal OrderType.thy
   739 goal OrderType.thy
   740  "!!i j. [| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
   740  "!!i j. [| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
   741 by (rtac (subsetI RS equalityI) 1);
   741 by (rtac (subsetI RS equalityI) 1);
   742 by (resolve_tac [lt_omult RS exE] 1);
   742 by (resolve_tac [lt_omult RS exE] 1);
   743 by (eresolve_tac [ltI] 3);
   743 by (etac ltI 3);
   744 by (REPEAT (ares_tac [Ord_omult] 1));
   744 by (REPEAT (ares_tac [Ord_omult] 1));
   745 by (fast_tac (ZF_cs addSEs [ltE]) 1);
   745 by (fast_tac (ZF_cs addSEs [ltE]) 1);
   746 by (fast_tac (ZF_cs addIs [omult_oadd_lt RS ltD, ltI]) 1);
   746 by (fast_tac (ZF_cs addIs [omult_oadd_lt RS ltD, ltI]) 1);
   747 qed "omult_unfold";
   747 qed "omult_unfold";
   748 
   748 
   762 
   762 
   763 goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> i**1 = i";
   763 goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> i**1 = i";
   764 by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
   764 by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
   765 by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1);
   765 by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1);
   766 by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, 
   766 by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, 
   767 				well_ord_Memrel, ordertype_Memrel]));
   767                                 well_ord_Memrel, ordertype_Memrel]));
   768 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff])));
   768 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff])));
   769 qed "omult_1";
   769 qed "omult_1";
   770 
   770 
   771 goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> 1**i = i";
   771 goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> 1**i = i";
   772 by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
   772 by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
   773 by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1);
   773 by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1);
   774 by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, 
   774 by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, 
   775 				well_ord_Memrel, ordertype_Memrel]));
   775                                 well_ord_Memrel, ordertype_Memrel]));
   776 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff])));
   776 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff])));
   777 qed "omult_1_left";
   777 qed "omult_1_left";
   778 
   778 
   779 (** Distributive law for ordinal multiplication and addition **)
   779 (** Distributive law for ordinal multiplication and addition **)
   780 
   780 
   781 goalw OrderType.thy [omult_def, oadd_def]
   781 goalw OrderType.thy [omult_def, oadd_def]
   782     "!!i. [| Ord(i);  Ord(j);  Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)";
   782     "!!i. [| Ord(i);  Ord(j);  Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)";
   783 by (resolve_tac [ordertype_eq RS trans] 1);
   783 by (resolve_tac [ordertype_eq RS trans] 1);
   784 by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
   784 by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
   785 	  prod_ord_iso_cong) 1);
   785           prod_ord_iso_cong) 1);
   786 by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
   786 by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
   787 		      Ord_ordertype] 1));
   787                       Ord_ordertype] 1));
   788 by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1);
   788 by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1);
   789 by (rtac ordertype_eq 2);
   789 by (rtac ordertype_eq 2);
   790 by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2);
   790 by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2);
   791 by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
   791 by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
   792 		      Ord_ordertype] 1));
   792                       Ord_ordertype] 1));
   793 qed "oadd_omult_distrib";
   793 qed "oadd_omult_distrib";
   794 
   794 
   795 goal OrderType.thy "!!i. [| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
   795 goal OrderType.thy "!!i. [| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
   796 by (asm_simp_tac 
   796 by (asm_simp_tac 
   797     (ZF_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, Ord_1]) 1);
   797     (ZF_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, Ord_1]) 1);
   801 
   801 
   802 goalw OrderType.thy [omult_def]
   802 goalw OrderType.thy [omult_def]
   803     "!!i j k. [| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)";
   803     "!!i j k. [| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)";
   804 by (resolve_tac [ordertype_eq RS trans] 1);
   804 by (resolve_tac [ordertype_eq RS trans] 1);
   805 by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS 
   805 by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS 
   806 	  prod_ord_iso_cong) 1);
   806           prod_ord_iso_cong) 1);
   807 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
   807 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
   808 by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS 
   808 by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS 
   809 		 ordertype_eq RS trans] 1);
   809                  ordertype_eq RS trans] 1);
   810 by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS
   810 by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS
   811 	  ordertype_eq) 2);
   811           ordertype_eq) 2);
   812 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1));
   812 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1));
   813 qed "omult_assoc";
   813 qed "omult_assoc";
   814 
   814 
   815 
   815 
   816 (** Ordinal multiplication with limit ordinals **)
   816 (** Ordinal multiplication with limit ordinals **)
   824 
   824 
   825 goal OrderType.thy 
   825 goal OrderType.thy 
   826     "!!i j. [| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
   826     "!!i j. [| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
   827 by (asm_simp_tac 
   827 by (asm_simp_tac 
   828     (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 
   828     (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 
   829 		     Union_eq_UN RS sym, Limit_Union_eq]) 1);
   829                      Union_eq_UN RS sym, Limit_Union_eq]) 1);
   830 qed "omult_Limit";
   830 qed "omult_Limit";
   831 
   831 
   832 
   832 
   833 (*** Ordering/monotonicity properties of ordinal multiplication ***)
   833 (*** Ordering/monotonicity properties of ordinal multiplication ***)
   834 
   834 
   835 (*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
   835 (*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
   836 goal OrderType.thy "!!i j. [| k<i;  0<j |] ==> k < i**j";
   836 goal OrderType.thy "!!i j. [| k<i;  0<j |] ==> k < i**j";
   837 by (safe_tac (ZF_cs addSEs [ltE] addSIs [ltI, Ord_omult]));
   837 by (safe_tac (ZF_cs addSEs [ltE] addSIs [ltI, Ord_omult]));
   838 by (asm_simp_tac (ZF_ss addsimps [omult_unfold]) 1);
   838 by (asm_simp_tac (ZF_ss addsimps [omult_unfold]) 1);
   839 by (REPEAT (eresolve_tac [UN_I] 1));
   839 by (REPEAT (etac UN_I 1));
   840 by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0_left]) 1);
   840 by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0_left]) 1);
   841 qed "lt_omult1";
   841 qed "lt_omult1";
   842 
   842 
   843 goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le i**j";
   843 goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le i**j";
   844 by (resolve_tac [all_lt_imp_le] 1);
   844 by (rtac all_lt_imp_le 1);
   845 by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1));
   845 by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1));
   846 qed "omult_le_self";
   846 qed "omult_le_self";
   847 
   847 
   848 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k**i le j**i";
   848 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k**i le j**i";
   849 by (forward_tac [lt_Ord] 1);
   849 by (forward_tac [lt_Ord] 1);
   850 by (forward_tac [le_Ord2] 1);
   850 by (forward_tac [le_Ord2] 1);
   851 by (eresolve_tac [trans_induct3] 1);
   851 by (etac trans_induct3 1);
   852 by (asm_simp_tac (ZF_ss addsimps [omult_0, le_refl, Ord_0]) 1);
   852 by (asm_simp_tac (ZF_ss addsimps [omult_0, le_refl, Ord_0]) 1);
   853 by (asm_simp_tac (ZF_ss addsimps [omult_succ, oadd_le_mono]) 1);
   853 by (asm_simp_tac (ZF_ss addsimps [omult_succ, oadd_le_mono]) 1);
   854 by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1);
   854 by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1);
   855 by (resolve_tac [le_implies_UN_le_UN] 1);
   855 by (rtac le_implies_UN_le_UN 1);
   856 by (fast_tac ZF_cs 1);
   856 by (fast_tac ZF_cs 1);
   857 qed "omult_le_mono1";
   857 qed "omult_le_mono1";
   858 
   858 
   859 goal OrderType.thy "!!i j k. [| k<j;  0<i |] ==> i**k < i**j";
   859 goal OrderType.thy "!!i j k. [| k<j;  0<i |] ==> i**k < i**j";
   860 by (resolve_tac [ltI] 1);
   860 by (rtac ltI 1);
   861 by (asm_simp_tac (ZF_ss addsimps [omult_unfold, lt_Ord2]) 1);
   861 by (asm_simp_tac (ZF_ss addsimps [omult_unfold, lt_Ord2]) 1);
   862 by (safe_tac (ZF_cs addSEs [ltE] addSIs [Ord_omult]));
   862 by (safe_tac (ZF_cs addSEs [ltE] addSIs [Ord_omult]));
   863 by (REPEAT (eresolve_tac [UN_I] 1));
   863 by (REPEAT (etac UN_I 1));
   864 by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0, Ord_omult]) 1);
   864 by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0, Ord_omult]) 1);
   865 qed "omult_lt_mono2";
   865 qed "omult_lt_mono2";
   866 
   866 
   867 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> i**k le i**j";
   867 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> i**k le i**j";
   868 by (resolve_tac [subset_imp_le] 1);
   868 by (rtac subset_imp_le 1);
   869 by (safe_tac (ZF_cs addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult]));
   869 by (safe_tac (ZF_cs addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult]));
   870 by (asm_full_simp_tac (ZF_ss addsimps [omult_unfold]) 1);
   870 by (asm_full_simp_tac (ZF_ss addsimps [omult_unfold]) 1);
   871 by (deepen_tac (ZF_cs addEs [Ord_trans, UN_I]) 0 1);
   871 by (deepen_tac (ZF_cs addEs [Ord_trans, UN_I]) 0 1);
   872 qed "omult_le_mono2";
   872 qed "omult_le_mono2";
   873 
   873 
   874 goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'**j' le i**j";
   874 goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'**j' le i**j";
   875 by (resolve_tac [le_trans] 1);
   875 by (rtac le_trans 1);
   876 by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE,
   876 by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE,
   877 			  Ord_succD] 1));
   877                           Ord_succD] 1));
   878 qed "omult_le_mono";
   878 qed "omult_le_mono";
   879 
   879 
   880 goal OrderType.thy
   880 goal OrderType.thy
   881       "!!i j. [| i' le i;  j'<j;  0<i |] ==> i'**j' < i**j";
   881       "!!i j. [| i' le i;  j'<j;  0<i |] ==> i'**j' < i**j";
   882 by (resolve_tac [lt_trans1] 1);
   882 by (rtac lt_trans1 1);
   883 by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE,
   883 by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE,
   884 			  Ord_succD] 1));
   884                           Ord_succD] 1));
   885 qed "omult_lt_mono";
   885 qed "omult_lt_mono";
   886 
   886 
   887 goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le j**i";
   887 goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le j**i";
   888 by (forward_tac [lt_Ord2] 1);
   888 by (forward_tac [lt_Ord2] 1);
   889 by (eres_inst_tac [("i","i")] trans_induct3 1);
   889 by (eres_inst_tac [("i","i")] trans_induct3 1);
   890 by (asm_simp_tac (ZF_ss addsimps [omult_0, Ord_0 RS le_refl]) 1);
   890 by (asm_simp_tac (ZF_ss addsimps [omult_0, Ord_0 RS le_refl]) 1);
   891 by (asm_simp_tac (ZF_ss addsimps [omult_succ, succ_le_iff]) 1);
   891 by (asm_simp_tac (ZF_ss addsimps [omult_succ, succ_le_iff]) 1);
   892 by (eresolve_tac [lt_trans1] 1);
   892 by (etac lt_trans1 1);
   893 by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 
   893 by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 
   894     rtac oadd_lt_mono2 2);
   894     rtac oadd_lt_mono2 2);
   895 by (REPEAT (ares_tac [Ord_omult] 1));
   895 by (REPEAT (ares_tac [Ord_omult] 1));
   896 by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1);
   896 by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1);
   897 by (resolve_tac [le_trans] 1);
   897 by (rtac le_trans 1);
   898 by (resolve_tac [le_implies_UN_le_UN] 2);
   898 by (rtac le_implies_UN_le_UN 2);
   899 by (fast_tac ZF_cs 2);
   899 by (fast_tac ZF_cs 2);
   900 by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
   900 by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
   901 				  Limit_is_Ord RS le_refl]) 1);
   901                                   Limit_is_Ord RS le_refl]) 1);
   902 qed "omult_le_self2";
   902 qed "omult_le_self2";
   903 
   903 
   904 
   904 
   905 (** Further properties of ordinal multiplication **)
   905 (** Further properties of ordinal multiplication **)
   906 
   906