src/ZF/OrderType.thy
changeset 46820 c656222c4dc1
parent 32960 69916a850301
child 46821 ff6b0c1087f2
     1.1 --- a/src/ZF/OrderType.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/OrderType.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -11,44 +11,44 @@
     1.4  Ordinal arithmetic is traditionally defined in terms of order types, as it is
     1.5  here.  But a definition by transfinite recursion would be much simpler!*}
     1.6  
     1.7 -definition  
     1.8 +definition
     1.9    ordermap  :: "[i,i]=>i"  where
    1.10 -   "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
    1.11 +   "ordermap(A,r) == \<lambda>x\<in>A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
    1.12  
    1.13 -definition  
    1.14 +definition
    1.15    ordertype :: "[i,i]=>i"  where
    1.16     "ordertype(A,r) == ordermap(A,r)``A"
    1.17  
    1.18 -definition  
    1.19 +definition
    1.20    (*alternative definition of ordinal numbers*)
    1.21    Ord_alt   :: "i => o"  where
    1.22 -   "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
    1.23 +   "Ord_alt(X) == well_ord(X, Memrel(X)) & (\<forall>u\<in>X. u=pred(X, u, Memrel(X)))"
    1.24  
    1.25 -definition  
    1.26 +definition
    1.27    (*coercion to ordinal: if not, just 0*)
    1.28    ordify    :: "i=>i"  where
    1.29      "ordify(x) == if Ord(x) then x else 0"
    1.30  
    1.31 -definition  
    1.32 +definition
    1.33    (*ordinal multiplication*)
    1.34    omult      :: "[i,i]=>i"           (infixl "**" 70)  where
    1.35     "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
    1.36  
    1.37 -definition  
    1.38 +definition
    1.39    (*ordinal addition*)
    1.40    raw_oadd   :: "[i,i]=>i"  where
    1.41      "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
    1.42  
    1.43 -definition  
    1.44 +definition
    1.45    oadd      :: "[i,i]=>i"           (infixl "++" 65)  where
    1.46      "i ++ j == raw_oadd(ordify(i),ordify(j))"
    1.47  
    1.48 -definition  
    1.49 +definition
    1.50    (*ordinal subtraction*)
    1.51    odiff      :: "[i,i]=>i"           (infixl "--" 65)  where
    1.52      "i -- j == ordertype(i-j, Memrel(i))"
    1.53  
    1.54 -  
    1.55 +
    1.56  notation (xsymbols)
    1.57    omult  (infixl "\<times>\<times>" 70)
    1.58  
    1.59 @@ -58,7 +58,7 @@
    1.60  
    1.61  subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
    1.62  
    1.63 -lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
    1.64 +lemma le_well_ord_Memrel: "j \<le> i ==> well_ord(j, Memrel(i))"
    1.65  apply (rule well_ordI)
    1.66  apply (rule wf_Memrel [THEN wf_imp_wf_on])
    1.67  apply (simp add: ltD lt_Ord linear_def
    1.68 @@ -72,22 +72,22 @@
    1.69  
    1.70  (*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord
    1.71    The smaller ordinal is an initial segment of the larger *)
    1.72 -lemma lt_pred_Memrel: 
    1.73 +lemma lt_pred_Memrel:
    1.74      "j<i ==> pred(i, j, Memrel(i)) = j"
    1.75  apply (unfold pred_def lt_def)
    1.76  apply (simp (no_asm_simp))
    1.77  apply (blast intro: Ord_trans)
    1.78  done
    1.79  
    1.80 -lemma pred_Memrel: 
    1.81 -      "x:A ==> pred(A, x, Memrel(A)) = A Int x"
    1.82 +lemma pred_Memrel:
    1.83 +      "x:A ==> pred(A, x, Memrel(A)) = A \<inter> x"
    1.84  by (unfold pred_def Memrel_def, blast)
    1.85  
    1.86  lemma Ord_iso_implies_eq_lemma:
    1.87       "[| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"
    1.88  apply (frule lt_pred_Memrel)
    1.89  apply (erule ltE)
    1.90 -apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto) 
    1.91 +apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
    1.92  apply (unfold ord_iso_def)
    1.93  (*Combining the two simplifications causes looping*)
    1.94  apply (simp (no_asm_simp))
    1.95 @@ -96,7 +96,7 @@
    1.96  
    1.97  (*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
    1.98  lemma Ord_iso_implies_eq:
    1.99 -     "[| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j)) |]     
   1.100 +     "[| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j)) |]
   1.101        ==> i=j"
   1.102  apply (rule_tac i = i and j = j in Ord_linear_lt)
   1.103  apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+
   1.104 @@ -105,8 +105,8 @@
   1.105  
   1.106  subsection{*Ordermap and ordertype*}
   1.107  
   1.108 -lemma ordermap_type: 
   1.109 -    "ordermap(A,r) : A -> ordertype(A,r)"
   1.110 +lemma ordermap_type:
   1.111 +    "ordermap(A,r) \<in> A -> ordertype(A,r)"
   1.112  apply (unfold ordermap_def ordertype_def)
   1.113  apply (rule lam_type)
   1.114  apply (rule lamI [THEN imageI], assumption+)
   1.115 @@ -115,7 +115,7 @@
   1.116  subsubsection{*Unfolding of ordermap *}
   1.117  
   1.118  (*Useful for cardinality reasoning; see CardinalArith.ML*)
   1.119 -lemma ordermap_eq_image: 
   1.120 +lemma ordermap_eq_image:
   1.121      "[| wf[A](r);  x:A |]
   1.122       ==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
   1.123  apply (unfold ordermap_def pred_def)
   1.124 @@ -127,23 +127,23 @@
   1.125  (*Useful for rewriting PROVIDED pred is not unfolded until later!*)
   1.126  lemma ordermap_pred_unfold:
   1.127       "[| wf[A](r);  x:A |]
   1.128 -      ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"
   1.129 +      ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y \<in> pred(A,x,r)}"
   1.130  by (simp add: ordermap_eq_image pred_subset ordermap_type [THEN image_fun])
   1.131  
   1.132  (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
   1.133 -lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def] 
   1.134 +lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def]
   1.135  
   1.136 -(*The theorem above is 
   1.137 +(*The theorem above is
   1.138  
   1.139 -[| wf[A](r); x : A |]
   1.140 -==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
   1.141 +[| wf[A](r); x \<in> A |]
   1.142 +==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> \<in> r}}
   1.143  
   1.144  NOTE: the definition of ordermap used here delivers ordinals only if r is
   1.145  transitive.  If r is the predecessor relation on the naturals then
   1.146  ordermap(nat,predr) ` n equals {n-1} and not n.  A more complicated definition,
   1.147  like
   1.148  
   1.149 -  ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
   1.150 +  ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> \<in> r}},
   1.151  
   1.152  might eliminate the need for r to be transitive.
   1.153  *)
   1.154 @@ -151,7 +151,7 @@
   1.155  
   1.156  subsubsection{*Showing that ordermap, ordertype yield ordinals *}
   1.157  
   1.158 -lemma Ord_ordermap: 
   1.159 +lemma Ord_ordermap:
   1.160      "[| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)"
   1.161  apply (unfold well_ord_def tot_ord_def part_ord_def, safe)
   1.162  apply (rule_tac a=x in wf_on_induct, assumption+)
   1.163 @@ -159,10 +159,10 @@
   1.164  apply (rule OrdI [OF _ Ord_is_Transset])
   1.165  apply (unfold pred_def Transset_def)
   1.166  apply (blast intro: trans_onD
   1.167 -             dest!: ordermap_unfold [THEN equalityD1])+ 
   1.168 +             dest!: ordermap_unfold [THEN equalityD1])+
   1.169  done
   1.170  
   1.171 -lemma Ord_ordertype: 
   1.172 +lemma Ord_ordertype:
   1.173      "well_ord(A,r) ==> Ord(ordertype(A,r))"
   1.174  apply (unfold ordertype_def)
   1.175  apply (subst image_fun [OF ordermap_type subset_refl])
   1.176 @@ -178,38 +178,38 @@
   1.177  
   1.178  lemma ordermap_mono:
   1.179       "[| <w,x>: r;  wf[A](r);  w: A; x: A |]
   1.180 -      ==> ordermap(A,r)`w : ordermap(A,r)`x"
   1.181 +      ==> ordermap(A,r)`w \<in> ordermap(A,r)`x"
   1.182  apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast)
   1.183  done
   1.184  
   1.185  (*linearity of r is crucial here*)
   1.186 -lemma converse_ordermap_mono: 
   1.187 -    "[| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r); w: A; x: A |]
   1.188 +lemma converse_ordermap_mono:
   1.189 +    "[| ordermap(A,r)`w \<in> ordermap(A,r)`x;  well_ord(A,r); w: A; x: A |]
   1.190       ==> <w,x>: r"
   1.191  apply (unfold well_ord_def tot_ord_def, safe)
   1.192 -apply (erule_tac x=w and y=x in linearE, assumption+) 
   1.193 +apply (erule_tac x=w and y=x in linearE, assumption+)
   1.194  apply (blast elim!: mem_not_refl [THEN notE])
   1.195 -apply (blast dest: ordermap_mono intro: mem_asym) 
   1.196 +apply (blast dest: ordermap_mono intro: mem_asym)
   1.197  done
   1.198  
   1.199 -lemmas ordermap_surj = 
   1.200 +lemmas ordermap_surj =
   1.201      ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]
   1.202  
   1.203 -lemma ordermap_bij: 
   1.204 -    "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"
   1.205 +lemma ordermap_bij:
   1.206 +    "well_ord(A,r) ==> ordermap(A,r) \<in> bij(A, ordertype(A,r))"
   1.207  apply (unfold well_ord_def tot_ord_def bij_def inj_def)
   1.208 -apply (force intro!: ordermap_type ordermap_surj 
   1.209 -             elim: linearE dest: ordermap_mono 
   1.210 +apply (force intro!: ordermap_type ordermap_surj
   1.211 +             elim: linearE dest: ordermap_mono
   1.212               simp add: mem_not_refl)
   1.213  done
   1.214  
   1.215  subsubsection{*Isomorphisms involving ordertype *}
   1.216  
   1.217 -lemma ordertype_ord_iso: 
   1.218 +lemma ordertype_ord_iso:
   1.219   "well_ord(A,r)
   1.220 -  ==> ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
   1.221 +  ==> ordermap(A,r) \<in> ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
   1.222  apply (unfold ord_iso_def)
   1.223 -apply (safe elim!: well_ord_is_wf 
   1.224 +apply (safe elim!: well_ord_is_wf
   1.225              intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
   1.226  apply (blast dest!: converse_ordermap_mono)
   1.227  done
   1.228 @@ -223,8 +223,8 @@
   1.229  done
   1.230  
   1.231  lemma ordertype_eq_imp_ord_iso:
   1.232 -     "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r);  well_ord(B,s) |] 
   1.233 -      ==> EX f. f: ord_iso(A,r,B,s)"
   1.234 +     "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r);  well_ord(B,s) |]
   1.235 +      ==> \<exists>f. f: ord_iso(A,r,B,s)"
   1.236  apply (rule exI)
   1.237  apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
   1.238  apply (erule ssubst)
   1.239 @@ -234,7 +234,7 @@
   1.240  subsubsection{*Basic equalities for ordertype *}
   1.241  
   1.242  (*Ordertype of Memrel*)
   1.243 -lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j"
   1.244 +lemma le_ordertype_Memrel: "j \<le> i ==> ordertype(j,Memrel(i)) = j"
   1.245  apply (rule Ord_iso_implies_eq [symmetric])
   1.246  apply (erule ltE, assumption)
   1.247  apply (blast intro: le_well_ord_Memrel Ord_ordertype)
   1.248 @@ -277,16 +277,16 @@
   1.249  apply (fast elim!: trans_onD)
   1.250  done
   1.251  
   1.252 -lemma ordertype_unfold: 
   1.253 -    "ordertype(A,r) = {ordermap(A,r)`y . y : A}"
   1.254 +lemma ordertype_unfold:
   1.255 +    "ordertype(A,r) = {ordermap(A,r)`y . y \<in> A}"
   1.256  apply (unfold ordertype_def)
   1.257  apply (rule image_fun [OF ordermap_type subset_refl])
   1.258  done
   1.259  
   1.260  text{*Theorems by Krzysztof Grabczewski; proofs simplified by lcp *}
   1.261  
   1.262 -lemma ordertype_pred_subset: "[| well_ord(A,r);  x:A |] ==>              
   1.263 -          ordertype(pred(A,x,r),r) <= ordertype(A,r)"
   1.264 +lemma ordertype_pred_subset: "[| well_ord(A,r);  x:A |] ==>
   1.265 +          ordertype(pred(A,x,r),r) \<subseteq> ordertype(A,r)"
   1.266  apply (simp add: ordertype_unfold well_ord_subset [OF _ pred_subset])
   1.267  apply (fast intro: ordermap_pred_eq_ordermap elim: predE)
   1.268  done
   1.269 @@ -321,13 +321,13 @@
   1.270  apply (unfold Ord_alt_def)
   1.271  apply (rule conjI)
   1.272  apply (erule well_ord_Memrel)
   1.273 -apply (unfold Ord_def Transset_def pred_def Memrel_def, blast) 
   1.274 +apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)
   1.275  done
   1.276  
   1.277  (*proof by lcp*)
   1.278 -lemma Ord_alt_is_Ord: 
   1.279 +lemma Ord_alt_is_Ord:
   1.280      "Ord_alt(i) ==> Ord(i)"
   1.281 -apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def 
   1.282 +apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def
   1.283                       tot_ord_def part_ord_def trans_on_def)
   1.284  apply (simp add: pred_Memrel)
   1.285  apply (blast elim!: equalityE)
   1.286 @@ -340,7 +340,7 @@
   1.287  
   1.288  text{*Addition with 0 *}
   1.289  
   1.290 -lemma bij_sum_0: "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"
   1.291 +lemma bij_sum_0: "(\<lambda>z\<in>A+0. case(%x. x, %y. y, z)) \<in> bij(A+0, A)"
   1.292  apply (rule_tac d = Inl in lam_bijective, safe)
   1.293  apply (simp_all (no_asm_simp))
   1.294  done
   1.295 @@ -352,7 +352,7 @@
   1.296  apply force
   1.297  done
   1.298  
   1.299 -lemma bij_0_sum: "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)"
   1.300 +lemma bij_0_sum: "(\<lambda>z\<in>0+A. case(%x. x, %y. y, z)) \<in> bij(0+A, A)"
   1.301  apply (rule_tac d = Inr in lam_bijective, safe)
   1.302  apply (simp_all (no_asm_simp))
   1.303  done
   1.304 @@ -367,9 +367,9 @@
   1.305  text{*Initial segments of radd.  Statements by Grabczewski *}
   1.306  
   1.307  (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
   1.308 -lemma pred_Inl_bij: 
   1.309 - "a:A ==> (lam x:pred(A,a,r). Inl(x))     
   1.310 -          : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
   1.311 +lemma pred_Inl_bij:
   1.312 + "a:A ==> (\<lambda>x\<in>pred(A,a,r). Inl(x))
   1.313 +          \<in> bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
   1.314  apply (unfold pred_def)
   1.315  apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
   1.316  apply auto
   1.317 @@ -377,24 +377,24 @@
   1.318  
   1.319  lemma ordertype_pred_Inl_eq:
   1.320       "[| a:A;  well_ord(A,r) |]
   1.321 -      ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =  
   1.322 +      ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =
   1.323            ordertype(pred(A,a,r), r)"
   1.324  apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
   1.325  apply (simp_all add: well_ord_subset [OF _ pred_subset])
   1.326  apply (simp add: pred_def)
   1.327  done
   1.328  
   1.329 -lemma pred_Inr_bij: 
   1.330 - "b:B ==>   
   1.331 -         id(A+pred(B,b,s))       
   1.332 -         : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
   1.333 +lemma pred_Inr_bij:
   1.334 + "b:B ==>
   1.335 +         id(A+pred(B,b,s))
   1.336 +         \<in> bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
   1.337  apply (unfold pred_def id_def)
   1.338 -apply (rule_tac d = "%z. z" in lam_bijective, auto) 
   1.339 +apply (rule_tac d = "%z. z" in lam_bijective, auto)
   1.340  done
   1.341  
   1.342  lemma ordertype_pred_Inr_eq:
   1.343       "[| b:B;  well_ord(A,r);  well_ord(B,s) |]
   1.344 -      ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =  
   1.345 +      ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =
   1.346            ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"
   1.347  apply (rule pred_Inr_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
   1.348  prefer 2 apply (force simp add: pred_def id_def, assumption)
   1.349 @@ -441,7 +441,7 @@
   1.350  
   1.351  
   1.352  lemma oadd_eq_if_raw_oadd:
   1.353 -     "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)  
   1.354 +     "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)
   1.355                else (if Ord(j) then j else 0))"
   1.356  by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)
   1.357  
   1.358 @@ -462,15 +462,15 @@
   1.359  apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)
   1.360  done
   1.361  
   1.362 -(*Thus also we obtain the rule  i++j = k ==> i le k *)
   1.363 -lemma oadd_le_self: "Ord(i) ==> i le i++j"
   1.364 +(*Thus also we obtain the rule  @{term"i++j = k ==> i \<le> k"} *)
   1.365 +lemma oadd_le_self: "Ord(i) ==> i \<le> i++j"
   1.366  apply (rule all_lt_imp_le)
   1.367 -apply (auto simp add: Ord_oadd lt_oadd1) 
   1.368 +apply (auto simp add: Ord_oadd lt_oadd1)
   1.369  done
   1.370  
   1.371  text{*Various other results *}
   1.372  
   1.373 -lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
   1.374 +lemma id_ord_iso_Memrel: "A<=B ==> id(A) \<in> ord_iso(A, Memrel(A), A, Memrel(B))"
   1.375  apply (rule id_bij [THEN ord_isoI])
   1.376  apply (simp (no_asm_simp))
   1.377  apply blast
   1.378 @@ -478,32 +478,32 @@
   1.379  
   1.380  lemma subset_ord_iso_Memrel:
   1.381       "[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: ord_iso(A,Memrel(A),C,r)"
   1.382 -apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 
   1.383 -apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 
   1.384 -apply (simp add: right_comp_id) 
   1.385 +apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel])
   1.386 +apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption)
   1.387 +apply (simp add: right_comp_id)
   1.388  done
   1.389  
   1.390  lemma restrict_ord_iso:
   1.391 -     "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
   1.392 +     "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i;
   1.393         trans[A](r) |]
   1.394        ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
   1.395 -apply (frule ltD) 
   1.396 -apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 
   1.397 -apply (frule ord_iso_restrict_pred, assumption) 
   1.398 +apply (frule ltD)
   1.399 +apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
   1.400 +apply (frule ord_iso_restrict_pred, assumption)
   1.401  apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
   1.402 -apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI]) 
   1.403 +apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])
   1.404  done
   1.405  
   1.406  lemma restrict_ord_iso2:
   1.407 -     "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A; 
   1.408 +     "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A;
   1.409         j < i; trans[A](r) |]
   1.410 -      ==> converse(restrict(converse(f), j)) 
   1.411 +      ==> converse(restrict(converse(f), j))
   1.412            \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
   1.413  by (blast intro: restrict_ord_iso ord_iso_sym ltI)
   1.414  
   1.415  lemma ordertype_sum_Memrel:
   1.416       "[| well_ord(A,r);  k<j |]
   1.417 -      ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =  
   1.418 +      ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =
   1.419            ordertype(A+k, radd(A, r, k, Memrel(k)))"
   1.420  apply (erule ltE)
   1.421  apply (rule ord_iso_refl [THEN sum_ord_iso_cong, THEN ordertype_eq])
   1.422 @@ -528,7 +528,7 @@
   1.423   prefer 2
   1.424   apply (frule_tac i = i and j = j in oadd_le_self)
   1.425   apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
   1.426 -apply (rule Ord_linear_lt, auto) 
   1.427 +apply (rule Ord_linear_lt, auto)
   1.428  apply (simp_all add: raw_oadd_eq_oadd)
   1.429  apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
   1.430  done
   1.431 @@ -539,18 +539,18 @@
   1.432  lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
   1.433  apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
   1.434  apply (simp add: raw_oadd_eq_oadd)
   1.435 -apply (rule Ord_linear_lt, auto) 
   1.436 +apply (rule Ord_linear_lt, auto)
   1.437  apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
   1.438  done
   1.439  
   1.440 -lemma lt_oadd_disj: "k < i++j ==> k<i | (EX l:j. k = i++l )"
   1.441 +lemma lt_oadd_disj: "k < i++j ==> k<i | (\<exists>l\<in>j. k = i++l )"
   1.442  apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
   1.443              split add: split_if_asm)
   1.444   prefer 2
   1.445   apply (simp add: Ord_in_Ord' [of _ j] lt_def)
   1.446  apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
   1.447  apply (erule ltD [THEN RepFunE])
   1.448 -apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI 
   1.449 +apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI
   1.450                         lt_pred_Memrel le_ordertype_Memrel leI
   1.451                         ordertype_pred_Inr_eq ordertype_sum_Memrel)
   1.452  done
   1.453 @@ -562,7 +562,7 @@
   1.454  apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)
   1.455  apply (simp add: raw_oadd_def)
   1.456  apply (rule ordertype_eq [THEN trans])
   1.457 -apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym] 
   1.458 +apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
   1.459                                   ord_iso_refl])
   1.460  apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
   1.461  apply (rule sum_assoc_ord_iso [THEN ordertype_eq, THEN trans])
   1.462 @@ -571,11 +571,11 @@
   1.463  apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
   1.464  done
   1.465  
   1.466 -lemma oadd_unfold: "[| Ord(i);  Ord(j) |] ==> i++j = i Un (\<Union>k\<in>j. {i++k})"
   1.467 +lemma oadd_unfold: "[| Ord(i);  Ord(j) |] ==> i++j = i \<union> (\<Union>k\<in>j. {i++k})"
   1.468  apply (rule subsetI [THEN equalityI])
   1.469  apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
   1.470 -apply (blast intro: Ord_oadd) 
   1.471 -apply (blast elim!: ltE, blast) 
   1.472 +apply (blast intro: Ord_oadd)
   1.473 +apply (blast elim!: ltE, blast)
   1.474  apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)
   1.475  done
   1.476  
   1.477 @@ -597,13 +597,13 @@
   1.478  lemma oadd_UN:
   1.479       "[| !!x. x:A ==> Ord(j(x));  a:A |]
   1.480        ==> i ++ (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i++j(x))"
   1.481 -by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD] 
   1.482 -                 oadd_lt_mono2 [THEN ltD] 
   1.483 +by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD]
   1.484 +                 oadd_lt_mono2 [THEN ltD]
   1.485            elim!: ltE dest!: ltI [THEN lt_oadd_disj])
   1.486  
   1.487  lemma oadd_Limit: "Limit(j) ==> i++j = (\<Union>k\<in>j. i++k)"
   1.488  apply (frule Limit_has_0 [THEN ltD])
   1.489 -apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] 
   1.490 +apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric]
   1.491                   Union_eq_UN [symmetric] Limit_Union_eq)
   1.492  done
   1.493  
   1.494 @@ -626,12 +626,12 @@
   1.495                          Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
   1.496  apply (rule_tac x="succ(y)" in bexI)
   1.497   apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
   1.498 -apply (simp add: Limit_def lt_def) 
   1.499 +apply (simp add: Limit_def lt_def)
   1.500  done
   1.501  
   1.502  text{*Order/monotonicity properties of ordinal addition *}
   1.503  
   1.504 -lemma oadd_le_self2: "Ord(i) ==> i le j++i"
   1.505 +lemma oadd_le_self2: "Ord(i) ==> i \<le> j++i"
   1.506  apply (erule_tac i = i in trans_induct3)
   1.507  apply (simp (no_asm_simp) add: Ord_0_le)
   1.508  apply (simp (no_asm_simp) add: oadd_succ succ_leI)
   1.509 @@ -643,7 +643,7 @@
   1.510  apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
   1.511  done
   1.512  
   1.513 -lemma oadd_le_mono1: "k le j ==> k++i le j++i"
   1.514 +lemma oadd_le_mono1: "k \<le> j ==> k++i \<le> j++i"
   1.515  apply (frule lt_Ord)
   1.516  apply (frule le_Ord2)
   1.517  apply (simp add: oadd_eq_if_raw_oadd, clarify)
   1.518 @@ -655,31 +655,31 @@
   1.519  apply (rule le_implies_UN_le_UN, blast)
   1.520  done
   1.521  
   1.522 -lemma oadd_lt_mono: "[| i' le i;  j'<j |] ==> i'++j' < i++j"
   1.523 +lemma oadd_lt_mono: "[| i' \<le> i;  j'<j |] ==> i'++j' < i++j"
   1.524  by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)
   1.525  
   1.526 -lemma oadd_le_mono: "[| i' le i;  j' le j |] ==> i'++j' le i++j"
   1.527 +lemma oadd_le_mono: "[| i' \<le> i;  j' \<le> j |] ==> i'++j' \<le> i++j"
   1.528  by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
   1.529  
   1.530 -lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"
   1.531 +lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k <-> j \<le> k"
   1.532  by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
   1.533  
   1.534  lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
   1.535 -apply (rule lt_trans2) 
   1.536 -apply (erule le_refl) 
   1.537 -apply (simp only: lt_Ord2  oadd_1 [of i, symmetric]) 
   1.538 +apply (rule lt_trans2)
   1.539 +apply (erule le_refl)
   1.540 +apply (simp only: lt_Ord2  oadd_1 [of i, symmetric])
   1.541  apply (blast intro: succ_leI oadd_le_mono)
   1.542  done
   1.543  
   1.544  text{*Every ordinal is exceeded by some limit ordinal.*}
   1.545  lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
   1.546 -apply (rule_tac x="i ++ nat" in exI) 
   1.547 +apply (rule_tac x="i ++ nat" in exI)
   1.548  apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
   1.549  done
   1.550  
   1.551  lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
   1.552 -apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit]) 
   1.553 -apply (simp add: Un_least_lt_iff) 
   1.554 +apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
   1.555 +apply (simp add: Un_least_lt_iff)
   1.556  done
   1.557  
   1.558  
   1.559 @@ -689,7 +689,7 @@
   1.560      It's probably simpler to define the difference recursively!*}
   1.561  
   1.562  lemma bij_sum_Diff:
   1.563 -     "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"
   1.564 +     "A<=B ==> (\<lambda>y\<in>B. if(y:A, Inl(y), Inr(y))) \<in> bij(B, A+(B-A))"
   1.565  apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
   1.566  apply (blast intro!: if_type)
   1.567  apply (fast intro!: case_type)
   1.568 @@ -698,8 +698,8 @@
   1.569  done
   1.570  
   1.571  lemma ordertype_sum_Diff:
   1.572 -     "i le j ==>   
   1.573 -            ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =        
   1.574 +     "i \<le> j ==>
   1.575 +            ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =
   1.576              ordertype(j, Memrel(j))"
   1.577  apply (safe dest!: le_subset_iff [THEN iffD1])
   1.578  apply (rule bij_sum_Diff [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
   1.579 @@ -711,15 +711,15 @@
   1.580  apply (blast intro: lt_trans2 lt_trans)
   1.581  done
   1.582  
   1.583 -lemma Ord_odiff [simp,TC]: 
   1.584 +lemma Ord_odiff [simp,TC]:
   1.585      "[| Ord(i);  Ord(j) |] ==> Ord(i--j)"
   1.586  apply (unfold odiff_def)
   1.587  apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
   1.588  done
   1.589  
   1.590  
   1.591 -lemma raw_oadd_ordertype_Diff: 
   1.592 -   "i le j   
   1.593 +lemma raw_oadd_ordertype_Diff:
   1.594 +   "i \<le> j
   1.595      ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
   1.596  apply (simp add: raw_oadd_def odiff_def)
   1.597  apply (safe dest!: le_subset_iff [THEN iffD1])
   1.598 @@ -729,7 +729,7 @@
   1.599  apply (blast intro: well_ord_radd Diff_subset well_ord_subset well_ord_Memrel)+
   1.600  done
   1.601  
   1.602 -lemma oadd_odiff_inverse: "i le j ==> i ++ (j--i) = j"
   1.603 +lemma oadd_odiff_inverse: "i \<le> j ==> i ++ (j--i) = j"
   1.604  by (simp add: lt_Ord le_Ord2 oadd_def ordify_def raw_oadd_ordertype_Diff
   1.605                ordertype_sum_Diff ordertype_Memrel lt_Ord2 [THEN Ord_succD])
   1.606  
   1.607 @@ -741,7 +741,7 @@
   1.608  apply (blast intro: Ord_ordertype Ord_oadd Ord_odiff)+
   1.609  done
   1.610  
   1.611 -lemma odiff_lt_mono2: "[| i<j;  k le i |] ==> i--k < j--k"
   1.612 +lemma odiff_lt_mono2: "[| i<j;  k \<le> i |] ==> i--k < j--k"
   1.613  apply (rule_tac i = k in oadd_lt_cancel2)
   1.614  apply (simp add: oadd_odiff_inverse)
   1.615  apply (subst oadd_odiff_inverse)
   1.616 @@ -752,7 +752,7 @@
   1.617  
   1.618  subsection{*Ordinal Multiplication*}
   1.619  
   1.620 -lemma Ord_omult [simp,TC]: 
   1.621 +lemma Ord_omult [simp,TC]:
   1.622      "[| Ord(i);  Ord(j) |] ==> Ord(i**j)"
   1.623  apply (unfold omult_def)
   1.624  apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
   1.625 @@ -760,67 +760,67 @@
   1.626  
   1.627  subsubsection{*A useful unfolding law *}
   1.628  
   1.629 -lemma pred_Pair_eq: 
   1.630 - "[| a:A;  b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =      
   1.631 -                      pred(A,a,r)*B Un ({a} * pred(B,b,s))"
   1.632 +lemma pred_Pair_eq:
   1.633 + "[| a:A;  b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =
   1.634 +                      pred(A,a,r)*B \<union> ({a} * pred(B,b,s))"
   1.635  apply (unfold pred_def, blast)
   1.636  done
   1.637  
   1.638  lemma ordertype_pred_Pair_eq:
   1.639 -     "[| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>            
   1.640 -         ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =  
   1.641 -         ordertype(pred(A,a,r)*B + pred(B,b,s),                         
   1.642 +     "[| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>
   1.643 +         ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =
   1.644 +         ordertype(pred(A,a,r)*B + pred(B,b,s),
   1.645                    radd(A*B, rmult(A,r,B,s), B, s))"
   1.646  apply (simp (no_asm_simp) add: pred_Pair_eq)
   1.647  apply (rule ordertype_eq [symmetric])
   1.648  apply (rule prod_sum_singleton_ord_iso)
   1.649  apply (simp_all add: pred_subset well_ord_rmult [THEN well_ord_subset])
   1.650 -apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset] 
   1.651 +apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset]
   1.652               elim!: predE)
   1.653  done
   1.654  
   1.655 -lemma ordertype_pred_Pair_lemma: 
   1.656 +lemma ordertype_pred_Pair_lemma:
   1.657      "[| i'<i;  j'<j |]
   1.658 -     ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),  
   1.659 -                   rmult(i,Memrel(i),j,Memrel(j))) =                    
   1.660 +     ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
   1.661 +                   rmult(i,Memrel(i),j,Memrel(j))) =
   1.662           raw_oadd (j**i', j')"
   1.663  apply (unfold raw_oadd_def omult_def)
   1.664 -apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 
   1.665 +apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2
   1.666                   well_ord_Memrel)
   1.667  apply (rule trans)
   1.668 - apply (rule_tac [2] ordertype_ord_iso 
   1.669 + apply (rule_tac [2] ordertype_ord_iso
   1.670                        [THEN sum_ord_iso_cong, THEN ordertype_eq])
   1.671    apply (rule_tac [3] ord_iso_refl)
   1.672  apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])
   1.673  apply (elim SigmaE sumE ltE ssubst)
   1.674  apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
   1.675 -                     Ord_ordertype lt_Ord lt_Ord2) 
   1.676 +                     Ord_ordertype lt_Ord lt_Ord2)
   1.677  apply (blast intro: Ord_trans)+
   1.678  done
   1.679  
   1.680 -lemma lt_omult: 
   1.681 +lemma lt_omult:
   1.682   "[| Ord(i);  Ord(j);  k<j**i |]
   1.683 -  ==> EX j' i'. k = j**i' ++ j' & j'<j & i'<i"
   1.684 +  ==> \<exists>j' i'. k = j**i' ++ j' & j'<j & i'<i"
   1.685  apply (unfold omult_def)
   1.686  apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
   1.687  apply (safe elim!: ltE)
   1.688 -apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd 
   1.689 +apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd
   1.690              omult_def [symmetric] Ord_in_Ord' [of _ i] Ord_in_Ord' [of _ j])
   1.691  apply (blast intro: ltI)
   1.692  done
   1.693  
   1.694 -lemma omult_oadd_lt: 
   1.695 +lemma omult_oadd_lt:
   1.696       "[| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i"
   1.697  apply (unfold omult_def)
   1.698  apply (rule ltI)
   1.699   prefer 2
   1.700   apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
   1.701  apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
   1.702 -apply (rule bexI [of _ i']) 
   1.703 -apply (rule bexI [of _ j']) 
   1.704 +apply (rule bexI [of _ i'])
   1.705 +apply (rule bexI [of _ j'])
   1.706  apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
   1.707  apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
   1.708 -apply (simp_all add: lt_def) 
   1.709 +apply (simp_all add: lt_def)
   1.710  done
   1.711  
   1.712  lemma omult_unfold:
   1.713 @@ -828,7 +828,7 @@
   1.714  apply (rule subsetI [THEN equalityI])
   1.715  apply (rule lt_omult [THEN exE])
   1.716  apply (erule_tac [3] ltI)
   1.717 -apply (simp_all add: Ord_omult) 
   1.718 +apply (simp_all add: Ord_omult)
   1.719  apply (blast elim!: ltE)
   1.720  apply (blast intro: omult_oadd_lt [THEN ltD] ltI)
   1.721  done
   1.722 @@ -851,7 +851,7 @@
   1.723  
   1.724  lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
   1.725  apply (unfold omult_def)
   1.726 -apply (rule_tac s1="Memrel(i)" 
   1.727 +apply (rule_tac s1="Memrel(i)"
   1.728         in ord_isoI [THEN ordertype_eq, THEN trans])
   1.729  apply (rule_tac c = snd and d = "%z.<0,z>"  in lam_bijective)
   1.730  apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)
   1.731 @@ -859,7 +859,7 @@
   1.732  
   1.733  lemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"
   1.734  apply (unfold omult_def)
   1.735 -apply (rule_tac s1="Memrel(i)" 
   1.736 +apply (rule_tac s1="Memrel(i)"
   1.737         in ord_isoI [THEN ordertype_eq, THEN trans])
   1.738  apply (rule_tac c = fst and d = "%z.<z,0>" in lam_bijective)
   1.739  apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)
   1.740 @@ -872,14 +872,14 @@
   1.741  apply (simp add: oadd_eq_if_raw_oadd)
   1.742  apply (simp add: omult_def raw_oadd_def)
   1.743  apply (rule ordertype_eq [THEN trans])
   1.744 -apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym] 
   1.745 +apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
   1.746                                    ord_iso_refl])
   1.747 -apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel 
   1.748 +apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
   1.749                       Ord_ordertype)
   1.750  apply (rule sum_prod_distrib_ord_iso [THEN ordertype_eq, THEN trans])
   1.751  apply (rule_tac [2] ordertype_eq)
   1.752  apply (rule_tac [2] sum_ord_iso_cong [OF ordertype_ord_iso ordertype_ord_iso])
   1.753 -apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel 
   1.754 +apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
   1.755                       Ord_ordertype)
   1.756  done
   1.757  
   1.758 @@ -888,14 +888,14 @@
   1.759  
   1.760  text{*Associative law *}
   1.761  
   1.762 -lemma omult_assoc: 
   1.763 +lemma omult_assoc:
   1.764      "[| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)"
   1.765  apply (unfold omult_def)
   1.766  apply (rule ordertype_eq [THEN trans])
   1.767 -apply (rule prod_ord_iso_cong [OF ord_iso_refl 
   1.768 +apply (rule prod_ord_iso_cong [OF ord_iso_refl
   1.769                                    ordertype_ord_iso [THEN ord_iso_sym]])
   1.770  apply (blast intro: well_ord_rmult well_ord_Memrel)+
   1.771 -apply (rule prod_assoc_ord_iso 
   1.772 +apply (rule prod_assoc_ord_iso
   1.773               [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
   1.774  apply (rule_tac [2] ordertype_eq)
   1.775  apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])
   1.776 @@ -905,13 +905,13 @@
   1.777  
   1.778  text{*Ordinal multiplication with limit ordinals *}
   1.779  
   1.780 -lemma omult_UN: 
   1.781 +lemma omult_UN:
   1.782       "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |]
   1.783        ==> i ** (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i**j(x))"
   1.784  by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
   1.785  
   1.786  lemma omult_Limit: "[| Ord(i);  Limit(j) |] ==> i**j = (\<Union>k\<in>j. i**k)"
   1.787 -by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric] 
   1.788 +by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]
   1.789                Union_eq_UN [symmetric] Limit_Union_eq)
   1.790  
   1.791  
   1.792 @@ -923,10 +923,10 @@
   1.793  apply (force simp add: omult_unfold)
   1.794  done
   1.795  
   1.796 -lemma omult_le_self: "[| Ord(i);  0<j |] ==> i le i**j"
   1.797 +lemma omult_le_self: "[| Ord(i);  0<j |] ==> i \<le> i**j"
   1.798  by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
   1.799  
   1.800 -lemma omult_le_mono1: "[| k le j;  Ord(i) |] ==> k**i le j**i"
   1.801 +lemma omult_le_mono1: "[| k \<le> j;  Ord(i) |] ==> k**i \<le> j**i"
   1.802  apply (frule lt_Ord)
   1.803  apply (frule le_Ord2)
   1.804  apply (erule trans_induct3)
   1.805 @@ -943,20 +943,20 @@
   1.806  apply (force simp add: Ord_omult)
   1.807  done
   1.808  
   1.809 -lemma omult_le_mono2: "[| k le j;  Ord(i) |] ==> i**k le i**j"
   1.810 +lemma omult_le_mono2: "[| k \<le> j;  Ord(i) |] ==> i**k \<le> i**j"
   1.811  apply (rule subset_imp_le)
   1.812  apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)
   1.813  apply (simp add: omult_unfold)
   1.814 -apply (blast intro: Ord_trans) 
   1.815 +apply (blast intro: Ord_trans)
   1.816  done
   1.817  
   1.818 -lemma omult_le_mono: "[| i' le i;  j' le j |] ==> i'**j' le i**j"
   1.819 +lemma omult_le_mono: "[| i' \<le> i;  j' \<le> j |] ==> i'**j' \<le> i**j"
   1.820  by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)
   1.821  
   1.822 -lemma omult_lt_mono: "[| i' le i;  j'<j;  0<i |] ==> i'**j' < i**j"
   1.823 +lemma omult_lt_mono: "[| i' \<le> i;  j'<j;  0<i |] ==> i'**j' < i**j"
   1.824  by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
   1.825  
   1.826 -lemma omult_le_self2: "[| Ord(i);  0<j |] ==> i le j**i"
   1.827 +lemma omult_le_self2: "[| Ord(i);  0<j |] ==> i \<le> j**i"
   1.828  apply (frule lt_Ord2)
   1.829  apply (erule_tac i = i in trans_induct3)
   1.830  apply (simp (no_asm_simp))
   1.831 @@ -977,32 +977,32 @@
   1.832  lemma omult_inject: "[| i**j = i**k;  0<i;  Ord(j);  Ord(k) |] ==> j=k"
   1.833  apply (rule Ord_linear_lt)
   1.834  prefer 4 apply assumption
   1.835 -apply auto 
   1.836 +apply auto
   1.837  apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
   1.838  done
   1.839  
   1.840  subsection{*The Relation @{term Lt}*}
   1.841  
   1.842  lemma wf_Lt: "wf(Lt)"
   1.843 -apply (rule wf_subset) 
   1.844 -apply (rule wf_Memrel) 
   1.845 -apply (auto simp add: Lt_def Memrel_def lt_def) 
   1.846 +apply (rule wf_subset)
   1.847 +apply (rule wf_Memrel)
   1.848 +apply (auto simp add: Lt_def Memrel_def lt_def)
   1.849  done
   1.850  
   1.851  lemma irrefl_Lt: "irrefl(A,Lt)"
   1.852  by (auto simp add: Lt_def irrefl_def)
   1.853  
   1.854  lemma trans_Lt: "trans[A](Lt)"
   1.855 -apply (simp add: Lt_def trans_on_def) 
   1.856 -apply (blast intro: lt_trans) 
   1.857 +apply (simp add: Lt_def trans_on_def)
   1.858 +apply (blast intro: lt_trans)
   1.859  done
   1.860  
   1.861  lemma part_ord_Lt: "part_ord(A,Lt)"
   1.862  by (simp add: part_ord_def irrefl_Lt trans_Lt)
   1.863  
   1.864  lemma linear_Lt: "linear(nat,Lt)"
   1.865 -apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff) 
   1.866 -apply (drule lt_asym, auto) 
   1.867 +apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff)
   1.868 +apply (drule lt_asym, auto)
   1.869  done
   1.870  
   1.871  lemma tot_ord_Lt: "tot_ord(nat,Lt)"