src/ZF/OrderType.ML
 changeset 1461 6bcb44e4d6e5 parent 1032 54b9f670c67e child 2033 639de962ded4
equal 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 `