src/ZF/OrderType.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 16417 9bc16273c2d4
child 24826 78e6a3cea367
permissions -rw-r--r--
added Tools/lin_arith.ML;
clasohm@1478
     1
(*  Title:      ZF/OrderType.thy
lcp@435
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@435
     4
    Copyright   1994  University of Cambridge
lcp@435
     5
lcp@435
     6
*)
lcp@435
     7
paulson@13356
     8
header{*Order Types and Ordinal Arithmetic*}
paulson@13356
     9
haftmann@16417
    10
theory OrderType imports OrderArith OrdQuant Nat begin
paulson@13221
    11
paulson@13356
    12
text{*The order type of a well-ordering is the least ordinal isomorphic to it.
paulson@13356
    13
Ordinal arithmetic is traditionally defined in terms of order types, as it is
paulson@13356
    14
here.  But a definition by transfinite recursion would be much simpler!*}
paulson@13356
    15
paulson@13125
    16
constdefs
paulson@13125
    17
  
paulson@13140
    18
  ordermap  :: "[i,i]=>i"
paulson@13125
    19
   "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
lcp@435
    20
paulson@13140
    21
  ordertype :: "[i,i]=>i"
paulson@13125
    22
   "ordertype(A,r) == ordermap(A,r)``A"
lcp@850
    23
paulson@13125
    24
  (*alternative definition of ordinal numbers*)
paulson@13140
    25
  Ord_alt   :: "i => o"
paulson@13125
    26
   "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
lcp@435
    27
paulson@13125
    28
  (*coercion to ordinal: if not, just 0*)
paulson@13140
    29
  ordify    :: "i=>i"
paulson@13125
    30
    "ordify(x) == if Ord(x) then x else 0"
paulson@13125
    31
lcp@850
    32
  (*ordinal multiplication*)
paulson@13140
    33
  omult      :: "[i,i]=>i"           (infixl "**" 70)
paulson@13125
    34
   "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
lcp@850
    35
lcp@850
    36
  (*ordinal addition*)
paulson@13140
    37
  raw_oadd   :: "[i,i]=>i"
paulson@13125
    38
    "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
paulson@13125
    39
paulson@13140
    40
  oadd      :: "[i,i]=>i"           (infixl "++" 65)
paulson@13125
    41
    "i ++ j == raw_oadd(ordify(i),ordify(j))"
lcp@850
    42
lcp@1033
    43
  (*ordinal subtraction*)
paulson@13140
    44
  odiff      :: "[i,i]=>i"           (infixl "--" 65)
paulson@13125
    45
    "i -- j == ordertype(i-j, Memrel(i))"
lcp@1033
    46
paulson@13125
    47
  
wenzelm@12114
    48
syntax (xsymbols)
paulson@13140
    49
  "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
wenzelm@9964
    50
wenzelm@9964
    51
syntax (HTML output)
paulson@13140
    52
  "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
paulson@13140
    53
paulson@13140
    54
paulson@13269
    55
subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
paulson@13140
    56
paulson@13140
    57
lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
paulson@13140
    58
apply (rule well_ordI)
paulson@13140
    59
apply (rule wf_Memrel [THEN wf_imp_wf_on])
paulson@13140
    60
apply (simp add: ltD lt_Ord linear_def
paulson@13140
    61
                 ltI [THEN lt_trans2 [of _ j i]])
paulson@13140
    62
apply (intro ballI Ord_linear)
paulson@13140
    63
apply (blast intro: Ord_in_Ord lt_Ord)+
paulson@13140
    64
done
paulson@13140
    65
paulson@13140
    66
(*"Ord(i) ==> well_ord(i, Memrel(i))"*)
paulson@13140
    67
lemmas well_ord_Memrel = le_refl [THEN le_well_ord_Memrel]
paulson@13140
    68
paulson@13140
    69
(*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord
paulson@13140
    70
  The smaller ordinal is an initial segment of the larger *)
paulson@13140
    71
lemma lt_pred_Memrel: 
paulson@13140
    72
    "j<i ==> pred(i, j, Memrel(i)) = j"
paulson@13140
    73
apply (unfold pred_def lt_def)
paulson@13140
    74
apply (simp (no_asm_simp))
paulson@13140
    75
apply (blast intro: Ord_trans)
paulson@13140
    76
done
paulson@13140
    77
paulson@13140
    78
lemma pred_Memrel: 
paulson@13140
    79
      "x:A ==> pred(A, x, Memrel(A)) = A Int x"
paulson@13140
    80
by (unfold pred_def Memrel_def, blast)
paulson@13140
    81
paulson@13140
    82
lemma Ord_iso_implies_eq_lemma:
paulson@13140
    83
     "[| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"
paulson@13140
    84
apply (frule lt_pred_Memrel)
paulson@13140
    85
apply (erule ltE)
paulson@13140
    86
apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto) 
paulson@13140
    87
apply (unfold ord_iso_def)
paulson@13140
    88
(*Combining the two simplifications causes looping*)
paulson@13140
    89
apply (simp (no_asm_simp))
paulson@13140
    90
apply (blast intro: bij_is_fun [THEN apply_type] Ord_trans)
paulson@13140
    91
done
paulson@13140
    92
paulson@13140
    93
(*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
paulson@13140
    94
lemma Ord_iso_implies_eq:
paulson@13140
    95
     "[| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j)) |]     
paulson@13140
    96
      ==> i=j"
paulson@13140
    97
apply (rule_tac i = i and j = j in Ord_linear_lt)
paulson@13140
    98
apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+
paulson@13140
    99
done
paulson@13140
   100
paulson@13140
   101
paulson@13269
   102
subsection{*Ordermap and ordertype*}
paulson@13140
   103
paulson@13140
   104
lemma ordermap_type: 
paulson@13140
   105
    "ordermap(A,r) : A -> ordertype(A,r)"
paulson@13140
   106
apply (unfold ordermap_def ordertype_def)
paulson@13140
   107
apply (rule lam_type)
paulson@13140
   108
apply (rule lamI [THEN imageI], assumption+)
paulson@13140
   109
done
paulson@13140
   110
paulson@13356
   111
subsubsection{*Unfolding of ordermap *}
paulson@13140
   112
paulson@13140
   113
(*Useful for cardinality reasoning; see CardinalArith.ML*)
paulson@13140
   114
lemma ordermap_eq_image: 
paulson@13140
   115
    "[| wf[A](r);  x:A |]
paulson@13140
   116
     ==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
paulson@13140
   117
apply (unfold ordermap_def pred_def)
paulson@13140
   118
apply (simp (no_asm_simp))
paulson@13140
   119
apply (erule wfrec_on [THEN trans], assumption)
paulson@13140
   120
apply (simp (no_asm_simp) add: subset_iff image_lam vimage_singleton_iff)
paulson@13140
   121
done
paulson@13140
   122
paulson@13140
   123
(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
paulson@13140
   124
lemma ordermap_pred_unfold:
paulson@13140
   125
     "[| wf[A](r);  x:A |]
paulson@13140
   126
      ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"
paulson@13140
   127
by (simp add: ordermap_eq_image pred_subset ordermap_type [THEN image_fun])
paulson@13140
   128
paulson@13140
   129
(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
paulson@13140
   130
lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def] 
paulson@13140
   131
paulson@13140
   132
(*The theorem above is 
paulson@13140
   133
paulson@13140
   134
[| wf[A](r); x : A |]
paulson@13140
   135
==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
paulson@13140
   136
paulson@13140
   137
NOTE: the definition of ordermap used here delivers ordinals only if r is
paulson@13140
   138
transitive.  If r is the predecessor relation on the naturals then
paulson@13140
   139
ordermap(nat,predr) ` n equals {n-1} and not n.  A more complicated definition,
paulson@13140
   140
like
paulson@13140
   141
paulson@13140
   142
  ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
paulson@13140
   143
paulson@13140
   144
might eliminate the need for r to be transitive.
paulson@13140
   145
*)
paulson@13140
   146
paulson@13140
   147
paulson@13356
   148
subsubsection{*Showing that ordermap, ordertype yield ordinals *}
paulson@13140
   149
paulson@13140
   150
lemma Ord_ordermap: 
paulson@13140
   151
    "[| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)"
paulson@13140
   152
apply (unfold well_ord_def tot_ord_def part_ord_def, safe)
paulson@13140
   153
apply (rule_tac a=x in wf_on_induct, assumption+)
paulson@13140
   154
apply (simp (no_asm_simp) add: ordermap_pred_unfold)
paulson@13140
   155
apply (rule OrdI [OF _ Ord_is_Transset])
paulson@13140
   156
apply (unfold pred_def Transset_def)
paulson@13140
   157
apply (blast intro: trans_onD
paulson@13140
   158
	     dest!: ordermap_unfold [THEN equalityD1])+ 
paulson@13140
   159
done
paulson@13140
   160
paulson@13140
   161
lemma Ord_ordertype: 
paulson@13140
   162
    "well_ord(A,r) ==> Ord(ordertype(A,r))"
paulson@13140
   163
apply (unfold ordertype_def)
paulson@13140
   164
apply (subst image_fun [OF ordermap_type subset_refl])
paulson@13140
   165
apply (rule OrdI [OF _ Ord_is_Transset])
paulson@13140
   166
prefer 2 apply (blast intro: Ord_ordermap)
paulson@13140
   167
apply (unfold Transset_def well_ord_def)
paulson@13140
   168
apply (blast intro: trans_onD
paulson@13140
   169
	     dest!: ordermap_unfold [THEN equalityD1])
paulson@13140
   170
done
paulson@13140
   171
paulson@13140
   172
paulson@13356
   173
subsubsection{*ordermap preserves the orderings in both directions *}
paulson@13140
   174
paulson@13140
   175
lemma ordermap_mono:
paulson@13140
   176
     "[| <w,x>: r;  wf[A](r);  w: A; x: A |]
paulson@13140
   177
      ==> ordermap(A,r)`w : ordermap(A,r)`x"
paulson@13163
   178
apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast)
paulson@13140
   179
done
paulson@13140
   180
paulson@13140
   181
(*linearity of r is crucial here*)
paulson@13140
   182
lemma converse_ordermap_mono: 
paulson@13140
   183
    "[| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r); w: A; x: A |]
paulson@13140
   184
     ==> <w,x>: r"
paulson@13140
   185
apply (unfold well_ord_def tot_ord_def, safe)
paulson@13140
   186
apply (erule_tac x=w and y=x in linearE, assumption+) 
paulson@13140
   187
apply (blast elim!: mem_not_refl [THEN notE])
paulson@13140
   188
apply (blast dest: ordermap_mono intro: mem_asym) 
paulson@13140
   189
done
paulson@13140
   190
paulson@13140
   191
lemmas ordermap_surj = 
paulson@13140
   192
    ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]
paulson@13140
   193
paulson@13140
   194
lemma ordermap_bij: 
paulson@13140
   195
    "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"
paulson@13140
   196
apply (unfold well_ord_def tot_ord_def bij_def inj_def)
paulson@13140
   197
apply (force intro!: ordermap_type ordermap_surj 
paulson@13140
   198
             elim: linearE dest: ordermap_mono 
paulson@13140
   199
             simp add: mem_not_refl)
paulson@13140
   200
done
paulson@13140
   201
paulson@13356
   202
subsubsection{*Isomorphisms involving ordertype *}
paulson@13140
   203
paulson@13140
   204
lemma ordertype_ord_iso: 
paulson@13140
   205
 "well_ord(A,r)
paulson@13140
   206
  ==> ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
paulson@13140
   207
apply (unfold ord_iso_def)
paulson@13140
   208
apply (safe elim!: well_ord_is_wf 
paulson@13140
   209
            intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
paulson@13140
   210
apply (blast dest!: converse_ordermap_mono)
paulson@13140
   211
done
paulson@13140
   212
paulson@13140
   213
lemma ordertype_eq:
paulson@13140
   214
     "[| f: ord_iso(A,r,B,s);  well_ord(B,s) |]
paulson@13140
   215
      ==> ordertype(A,r) = ordertype(B,s)"
paulson@13140
   216
apply (frule well_ord_ord_iso, assumption)
paulson@13140
   217
apply (rule Ord_iso_implies_eq, (erule Ord_ordertype)+)
paulson@13140
   218
apply (blast intro: ord_iso_trans ord_iso_sym ordertype_ord_iso)
paulson@13140
   219
done
paulson@13140
   220
paulson@13140
   221
lemma ordertype_eq_imp_ord_iso:
paulson@13140
   222
     "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r);  well_ord(B,s) |] 
paulson@13140
   223
      ==> EX f. f: ord_iso(A,r,B,s)"
paulson@13140
   224
apply (rule exI)
paulson@13140
   225
apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
paulson@13140
   226
apply (erule ssubst)
paulson@13140
   227
apply (erule ordertype_ord_iso [THEN ord_iso_sym])
paulson@13140
   228
done
paulson@13140
   229
paulson@13356
   230
subsubsection{*Basic equalities for ordertype *}
paulson@13140
   231
paulson@13140
   232
(*Ordertype of Memrel*)
paulson@13140
   233
lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j"
paulson@13140
   234
apply (rule Ord_iso_implies_eq [symmetric])
paulson@13140
   235
apply (erule ltE, assumption)
paulson@13140
   236
apply (blast intro: le_well_ord_Memrel Ord_ordertype)
paulson@13140
   237
apply (rule ord_iso_trans)
paulson@13140
   238
apply (erule_tac [2] le_well_ord_Memrel [THEN ordertype_ord_iso])
paulson@13140
   239
apply (rule id_bij [THEN ord_isoI])
paulson@13140
   240
apply (simp (no_asm_simp))
paulson@13140
   241
apply (fast elim: ltE Ord_in_Ord Ord_trans)
paulson@13140
   242
done
paulson@13140
   243
paulson@13140
   244
(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
paulson@13140
   245
lemmas ordertype_Memrel = le_refl [THEN le_ordertype_Memrel]
paulson@13140
   246
paulson@13140
   247
lemma ordertype_0 [simp]: "ordertype(0,r) = 0"
paulson@13140
   248
apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq, THEN trans])
paulson@13140
   249
apply (erule emptyE)
paulson@13140
   250
apply (rule well_ord_0)
paulson@13140
   251
apply (rule Ord_0 [THEN ordertype_Memrel])
paulson@13140
   252
done
paulson@13140
   253
paulson@13140
   254
(*Ordertype of rvimage:  [| f: bij(A,B);  well_ord(B,s) |] ==>
paulson@13140
   255
                         ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
paulson@13140
   256
lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq]
paulson@13140
   257
paulson@13356
   258
subsubsection{*A fundamental unfolding law for ordertype. *}
paulson@13140
   259
paulson@13140
   260
(*Ordermap returns the same result if applied to an initial segment*)
paulson@13140
   261
lemma ordermap_pred_eq_ordermap:
paulson@13140
   262
     "[| well_ord(A,r);  y:A;  z: pred(A,y,r) |]
paulson@13140
   263
      ==> ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"
paulson@13140
   264
apply (frule wf_on_subset_A [OF well_ord_is_wf pred_subset])
paulson@13140
   265
apply (rule_tac a=z in wf_on_induct, assumption+)
paulson@13140
   266
apply (safe elim!: predE)
paulson@13140
   267
apply (simp (no_asm_simp) add: ordermap_pred_unfold well_ord_is_wf pred_iff)
paulson@13140
   268
(*combining these two simplifications LOOPS! *)
paulson@13140
   269
apply (simp (no_asm_simp) add: pred_pred_eq)
paulson@13140
   270
apply (simp add: pred_def)
paulson@13140
   271
apply (rule RepFun_cong [OF _ refl])
paulson@13140
   272
apply (drule well_ord_is_trans_on)
paulson@13140
   273
apply (fast elim!: trans_onD)
paulson@13140
   274
done
paulson@13140
   275
paulson@13140
   276
lemma ordertype_unfold: 
paulson@13140
   277
    "ordertype(A,r) = {ordermap(A,r)`y . y : A}"
paulson@13140
   278
apply (unfold ordertype_def)
paulson@13140
   279
apply (rule image_fun [OF ordermap_type subset_refl])
paulson@13140
   280
done
paulson@13140
   281
paulson@14046
   282
text{*Theorems by Krzysztof Grabczewski; proofs simplified by lcp *}
paulson@13140
   283
paulson@13140
   284
lemma ordertype_pred_subset: "[| well_ord(A,r);  x:A |] ==>              
paulson@13140
   285
          ordertype(pred(A,x,r),r) <= ordertype(A,r)"
paulson@13140
   286
apply (simp add: ordertype_unfold well_ord_subset [OF _ pred_subset])
paulson@13140
   287
apply (fast intro: ordermap_pred_eq_ordermap elim: predE)
paulson@13140
   288
done
paulson@13140
   289
paulson@13140
   290
lemma ordertype_pred_lt:
paulson@13140
   291
     "[| well_ord(A,r);  x:A |]
paulson@13140
   292
      ==> ordertype(pred(A,x,r),r) < ordertype(A,r)"
paulson@13140
   293
apply (rule ordertype_pred_subset [THEN subset_imp_le, THEN leE])
paulson@13140
   294
apply (simp_all add: Ord_ordertype well_ord_subset [OF _ pred_subset])
paulson@13140
   295
apply (erule sym [THEN ordertype_eq_imp_ord_iso, THEN exE])
paulson@13140
   296
apply (erule_tac [3] well_ord_iso_predE)
paulson@13140
   297
apply (simp_all add: well_ord_subset [OF _ pred_subset])
paulson@13140
   298
done
paulson@13140
   299
paulson@13140
   300
(*May rewrite with this -- provided no rules are supplied for proving that
paulson@13140
   301
        well_ord(pred(A,x,r), r) *)
paulson@13140
   302
lemma ordertype_pred_unfold:
paulson@13140
   303
     "well_ord(A,r)
paulson@13140
   304
      ==> ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"
paulson@13140
   305
apply (rule equalityI)
paulson@13140
   306
apply (safe intro!: ordertype_pred_lt [THEN ltD])
paulson@13140
   307
apply (auto simp add: ordertype_def well_ord_is_wf [THEN ordermap_eq_image]
paulson@13140
   308
                      ordermap_type [THEN image_fun]
paulson@13140
   309
                      ordermap_pred_eq_ordermap pred_subset)
paulson@13140
   310
done
paulson@13140
   311
paulson@13140
   312
paulson@13269
   313
subsection{*Alternative definition of ordinal*}
paulson@13140
   314
paulson@13140
   315
(*proof by Krzysztof Grabczewski*)
paulson@13140
   316
lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
paulson@13140
   317
apply (unfold Ord_alt_def)
paulson@13140
   318
apply (rule conjI)
paulson@13140
   319
apply (erule well_ord_Memrel)
paulson@13140
   320
apply (unfold Ord_def Transset_def pred_def Memrel_def, blast) 
paulson@13140
   321
done
paulson@13140
   322
paulson@13140
   323
(*proof by lcp*)
paulson@13140
   324
lemma Ord_alt_is_Ord: 
paulson@13140
   325
    "Ord_alt(i) ==> Ord(i)"
paulson@13140
   326
apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def 
paulson@13140
   327
                     tot_ord_def part_ord_def trans_on_def)
paulson@13140
   328
apply (simp add: pred_Memrel)
paulson@13140
   329
apply (blast elim!: equalityE)
paulson@13140
   330
done
paulson@13140
   331
paulson@13140
   332
paulson@13269
   333
subsection{*Ordinal Addition*}
paulson@13140
   334
paulson@13356
   335
subsubsection{*Order Type calculations for radd *}
paulson@13140
   336
paulson@14046
   337
text{*Addition with 0 *}
paulson@13140
   338
paulson@13140
   339
lemma bij_sum_0: "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"
paulson@13140
   340
apply (rule_tac d = Inl in lam_bijective, safe)
paulson@13140
   341
apply (simp_all (no_asm_simp))
paulson@13140
   342
done
paulson@13140
   343
paulson@13140
   344
lemma ordertype_sum_0_eq:
paulson@13140
   345
     "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"
paulson@13140
   346
apply (rule bij_sum_0 [THEN ord_isoI, THEN ordertype_eq])
paulson@13140
   347
prefer 2 apply assumption
paulson@13140
   348
apply force
paulson@13140
   349
done
paulson@13140
   350
paulson@13140
   351
lemma bij_0_sum: "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)"
paulson@13140
   352
apply (rule_tac d = Inr in lam_bijective, safe)
paulson@13140
   353
apply (simp_all (no_asm_simp))
paulson@13140
   354
done
paulson@13140
   355
paulson@13140
   356
lemma ordertype_0_sum_eq:
paulson@13140
   357
     "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"
paulson@13140
   358
apply (rule bij_0_sum [THEN ord_isoI, THEN ordertype_eq])
paulson@13140
   359
prefer 2 apply assumption
paulson@13140
   360
apply force
paulson@13140
   361
done
paulson@13140
   362
paulson@14046
   363
text{*Initial segments of radd.  Statements by Grabczewski *}
paulson@13140
   364
paulson@13140
   365
(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
paulson@13140
   366
lemma pred_Inl_bij: 
paulson@13140
   367
 "a:A ==> (lam x:pred(A,a,r). Inl(x))     
paulson@13140
   368
          : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
paulson@13140
   369
apply (unfold pred_def)
paulson@13140
   370
apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
paulson@13140
   371
apply auto
paulson@13140
   372
done
paulson@13140
   373
paulson@13140
   374
lemma ordertype_pred_Inl_eq:
paulson@13140
   375
     "[| a:A;  well_ord(A,r) |]
paulson@13140
   376
      ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =  
paulson@13140
   377
          ordertype(pred(A,a,r), r)"
paulson@13140
   378
apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
paulson@13140
   379
apply (simp_all add: well_ord_subset [OF _ pred_subset])
paulson@13140
   380
apply (simp add: pred_def)
paulson@13140
   381
done
paulson@13140
   382
paulson@13140
   383
lemma pred_Inr_bij: 
paulson@13140
   384
 "b:B ==>   
paulson@13140
   385
         id(A+pred(B,b,s))       
paulson@13140
   386
         : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
paulson@13140
   387
apply (unfold pred_def id_def)
paulson@13140
   388
apply (rule_tac d = "%z. z" in lam_bijective, auto) 
paulson@13140
   389
done
paulson@13140
   390
paulson@13140
   391
lemma ordertype_pred_Inr_eq:
paulson@13140
   392
     "[| b:B;  well_ord(A,r);  well_ord(B,s) |]
paulson@13140
   393
      ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =  
paulson@13140
   394
          ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"
paulson@13140
   395
apply (rule pred_Inr_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
paulson@13140
   396
prefer 2 apply (force simp add: pred_def id_def, assumption)
paulson@13140
   397
apply (blast intro: well_ord_radd well_ord_subset [OF _ pred_subset])
paulson@13140
   398
done
paulson@13140
   399
paulson@13140
   400
paulson@13356
   401
subsubsection{*ordify: trivial coercion to an ordinal *}
paulson@13140
   402
paulson@13140
   403
lemma Ord_ordify [iff, TC]: "Ord(ordify(x))"
paulson@13140
   404
by (simp add: ordify_def)
paulson@13140
   405
paulson@13140
   406
(*Collapsing*)
paulson@13140
   407
lemma ordify_idem [simp]: "ordify(ordify(x)) = ordify(x)"
paulson@13140
   408
by (simp add: ordify_def)
paulson@13140
   409
paulson@13140
   410
paulson@13356
   411
subsubsection{*Basic laws for ordinal addition *}
paulson@13140
   412
paulson@13140
   413
lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"
paulson@13140
   414
by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd
paulson@13140
   415
              well_ord_Memrel)
paulson@13140
   416
paulson@13140
   417
lemma Ord_oadd [iff,TC]: "Ord(i++j)"
paulson@13140
   418
by (simp add: oadd_def Ord_raw_oadd)
paulson@13140
   419
paulson@13140
   420
paulson@14046
   421
text{*Ordinal addition with zero *}
paulson@13140
   422
paulson@13140
   423
lemma raw_oadd_0: "Ord(i) ==> raw_oadd(i,0) = i"
paulson@13140
   424
by (simp add: raw_oadd_def ordify_def ordertype_sum_0_eq
paulson@13140
   425
              ordertype_Memrel well_ord_Memrel)
paulson@13140
   426
paulson@13140
   427
lemma oadd_0 [simp]: "Ord(i) ==> i++0 = i"
paulson@13140
   428
apply (simp (no_asm_simp) add: oadd_def raw_oadd_0 ordify_def)
paulson@13140
   429
done
paulson@13140
   430
paulson@13140
   431
lemma raw_oadd_0_left: "Ord(i) ==> raw_oadd(0,i) = i"
paulson@13140
   432
by (simp add: raw_oadd_def ordify_def ordertype_0_sum_eq ordertype_Memrel
paulson@13140
   433
              well_ord_Memrel)
paulson@13140
   434
paulson@13140
   435
lemma oadd_0_left [simp]: "Ord(i) ==> 0++i = i"
paulson@13140
   436
by (simp add: oadd_def raw_oadd_0_left ordify_def)
paulson@13140
   437
paulson@13140
   438
paulson@13140
   439
lemma oadd_eq_if_raw_oadd:
paulson@13140
   440
     "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)  
paulson@13140
   441
              else (if Ord(j) then j else 0))"
paulson@13140
   442
by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)
paulson@13140
   443
paulson@13140
   444
lemma raw_oadd_eq_oadd: "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"
paulson@13140
   445
by (simp add: oadd_def ordify_def)
paulson@13140
   446
paulson@13140
   447
(*** Further properties of ordinal addition.  Statements by Grabczewski,
paulson@13140
   448
    proofs by lcp. ***)
paulson@13140
   449
paulson@13140
   450
(*Surely also provable by transfinite induction on j?*)
paulson@13140
   451
lemma lt_oadd1: "k<i ==> k < i++j"
paulson@13140
   452
apply (simp add: oadd_def ordify_def lt_Ord2 raw_oadd_0, clarify)
paulson@13140
   453
apply (simp add: raw_oadd_def)
paulson@13140
   454
apply (rule ltE, assumption)
paulson@13140
   455
apply (rule ltI)
paulson@13140
   456
apply (force simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel
paulson@13140
   457
          ordertype_pred_Inl_eq lt_pred_Memrel leI [THEN le_ordertype_Memrel])
paulson@13140
   458
apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)
paulson@13140
   459
done
paulson@13140
   460
paulson@13140
   461
(*Thus also we obtain the rule  i++j = k ==> i le k *)
paulson@13140
   462
lemma oadd_le_self: "Ord(i) ==> i le i++j"
paulson@13140
   463
apply (rule all_lt_imp_le)
paulson@13140
   464
apply (auto simp add: Ord_oadd lt_oadd1) 
paulson@13140
   465
done
paulson@13140
   466
paulson@14046
   467
text{*Various other results *}
paulson@13140
   468
paulson@13140
   469
lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
paulson@13140
   470
apply (rule id_bij [THEN ord_isoI])
paulson@13140
   471
apply (simp (no_asm_simp))
paulson@13140
   472
apply blast
paulson@13140
   473
done
paulson@13140
   474
paulson@13221
   475
lemma subset_ord_iso_Memrel:
paulson@13221
   476
     "[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: ord_iso(A,Memrel(A),C,r)"
paulson@13221
   477
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 
paulson@13221
   478
apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 
paulson@13221
   479
apply (simp add: right_comp_id) 
paulson@13221
   480
done
paulson@13221
   481
paulson@13221
   482
lemma restrict_ord_iso:
paulson@13221
   483
     "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
paulson@13221
   484
       trans[A](r) |]
paulson@13221
   485
      ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
paulson@13221
   486
apply (frule ltD) 
paulson@13221
   487
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 
paulson@13221
   488
apply (frule ord_iso_restrict_pred, assumption) 
paulson@13221
   489
apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
paulson@13221
   490
apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI]) 
paulson@13221
   491
done
paulson@13221
   492
paulson@13221
   493
lemma restrict_ord_iso2:
paulson@13221
   494
     "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A; 
paulson@13221
   495
       j < i; trans[A](r) |]
paulson@13221
   496
      ==> converse(restrict(converse(f), j)) 
paulson@13221
   497
          \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
paulson@13221
   498
by (blast intro: restrict_ord_iso ord_iso_sym ltI)
paulson@13221
   499
paulson@13140
   500
lemma ordertype_sum_Memrel:
paulson@13140
   501
     "[| well_ord(A,r);  k<j |]
paulson@13140
   502
      ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =  
paulson@13140
   503
          ordertype(A+k, radd(A, r, k, Memrel(k)))"
paulson@13140
   504
apply (erule ltE)
paulson@13140
   505
apply (rule ord_iso_refl [THEN sum_ord_iso_cong, THEN ordertype_eq])
paulson@13140
   506
apply (erule OrdmemD [THEN id_ord_iso_Memrel, THEN ord_iso_sym])
paulson@13140
   507
apply (simp_all add: well_ord_radd well_ord_Memrel)
paulson@13140
   508
done
paulson@13140
   509
paulson@13140
   510
lemma oadd_lt_mono2: "k<j ==> i++k < i++j"
paulson@13140
   511
apply (simp add: oadd_def ordify_def raw_oadd_0_left lt_Ord lt_Ord2, clarify)
paulson@13140
   512
apply (simp add: raw_oadd_def)
paulson@13140
   513
apply (rule ltE, assumption)
paulson@13140
   514
apply (rule ordertype_pred_unfold [THEN equalityD2, THEN subsetD, THEN ltI])
paulson@13140
   515
apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
paulson@13140
   516
apply (rule bexI)
paulson@13140
   517
apply (erule_tac [2] InrI)
paulson@13140
   518
apply (simp add: ordertype_pred_Inr_eq well_ord_Memrel lt_pred_Memrel
paulson@13140
   519
                 leI [THEN le_ordertype_Memrel] ordertype_sum_Memrel)
paulson@13140
   520
done
paulson@13140
   521
paulson@13140
   522
lemma oadd_lt_cancel2: "[| i++j < i++k;  Ord(j) |] ==> j<k"
berghofe@13611
   523
apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split add: split_if_asm)
paulson@13140
   524
 prefer 2
paulson@13140
   525
 apply (frule_tac i = i and j = j in oadd_le_self)
berghofe@13611
   526
 apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
paulson@13140
   527
apply (rule Ord_linear_lt, auto) 
paulson@13140
   528
apply (simp_all add: raw_oadd_eq_oadd)
paulson@13140
   529
apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
paulson@13140
   530
done
paulson@13140
   531
paulson@13140
   532
lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
paulson@13140
   533
by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
paulson@13140
   534
paulson@13140
   535
lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
paulson@13140
   536
apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
paulson@13140
   537
apply (simp add: raw_oadd_eq_oadd)
paulson@13140
   538
apply (rule Ord_linear_lt, auto) 
paulson@13140
   539
apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
paulson@13140
   540
done
paulson@13140
   541
paulson@13140
   542
lemma lt_oadd_disj: "k < i++j ==> k<i | (EX l:j. k = i++l )"
paulson@13140
   543
apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
paulson@13140
   544
            split add: split_if_asm)
paulson@13140
   545
 prefer 2
paulson@13140
   546
 apply (simp add: Ord_in_Ord' [of _ j] lt_def)
paulson@13140
   547
apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
paulson@13140
   548
apply (erule ltD [THEN RepFunE])
paulson@13140
   549
apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI 
paulson@13140
   550
                       lt_pred_Memrel le_ordertype_Memrel leI
paulson@13140
   551
                       ordertype_pred_Inr_eq ordertype_sum_Memrel)
paulson@13140
   552
done
paulson@13140
   553
paulson@13140
   554
paulson@13356
   555
subsubsection{*Ordinal addition with successor -- via associativity! *}
paulson@13140
   556
paulson@13140
   557
lemma oadd_assoc: "(i++j)++k = i++(j++k)"
paulson@13140
   558
apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)
paulson@13140
   559
apply (simp add: raw_oadd_def)
paulson@13140
   560
apply (rule ordertype_eq [THEN trans])
paulson@13140
   561
apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym] 
paulson@13140
   562
                                 ord_iso_refl])
paulson@13140
   563
apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
paulson@13140
   564
apply (rule sum_assoc_ord_iso [THEN ordertype_eq, THEN trans])
paulson@13140
   565
apply (rule_tac [2] ordertype_eq)
paulson@13140
   566
apply (rule_tac [2] sum_ord_iso_cong [OF ord_iso_refl ordertype_ord_iso])
paulson@13140
   567
apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
paulson@13140
   568
done
paulson@13140
   569
paulson@13615
   570
lemma oadd_unfold: "[| Ord(i);  Ord(j) |] ==> i++j = i Un (\<Union>k\<in>j. {i++k})"
paulson@13140
   571
apply (rule subsetI [THEN equalityI])
paulson@13140
   572
apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
paulson@13140
   573
apply (blast intro: Ord_oadd) 
paulson@13140
   574
apply (blast elim!: ltE, blast) 
paulson@13140
   575
apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)
paulson@13140
   576
done
paulson@13140
   577
paulson@13140
   578
lemma oadd_1: "Ord(i) ==> i++1 = succ(i)"
paulson@13140
   579
apply (simp (no_asm_simp) add: oadd_unfold Ord_1 oadd_0)
paulson@13140
   580
apply blast
paulson@13140
   581
done
paulson@13140
   582
paulson@13140
   583
lemma oadd_succ [simp]: "Ord(j) ==> i++succ(j) = succ(i++j)"
paulson@13140
   584
apply (simp add: oadd_eq_if_raw_oadd, clarify)
paulson@13140
   585
apply (simp add: raw_oadd_eq_oadd)
paulson@13140
   586
apply (simp add: oadd_1 [of j, symmetric] oadd_1 [of "i++j", symmetric]
paulson@13140
   587
                 oadd_assoc)
paulson@13140
   588
done
paulson@13140
   589
paulson@13140
   590
paulson@14046
   591
text{*Ordinal addition with limit ordinals *}
paulson@13140
   592
paulson@13140
   593
lemma oadd_UN:
paulson@13140
   594
     "[| !!x. x:A ==> Ord(j(x));  a:A |]
paulson@13615
   595
      ==> i ++ (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i++j(x))"
paulson@13140
   596
by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD] 
paulson@13140
   597
                 oadd_lt_mono2 [THEN ltD] 
paulson@13140
   598
          elim!: ltE dest!: ltI [THEN lt_oadd_disj])
paulson@13140
   599
paulson@13615
   600
lemma oadd_Limit: "Limit(j) ==> i++j = (\<Union>k\<in>j. i++k)"
paulson@13140
   601
apply (frule Limit_has_0 [THEN ltD])
paulson@13356
   602
apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] 
paulson@13356
   603
                 Union_eq_UN [symmetric] Limit_Union_eq)
paulson@13140
   604
done
paulson@13140
   605
paulson@13221
   606
lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
paulson@13221
   607
apply (erule trans_induct3 [of j])
paulson@13221
   608
apply (simp_all add: oadd_Limit)
paulson@13221
   609
apply (simp add: Union_empty_iff Limit_def lt_def, blast)
paulson@13221
   610
done
paulson@13221
   611
paulson@13221
   612
lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
paulson@13221
   613
by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
paulson@13221
   614
paulson@13221
   615
lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
paulson@13221
   616
apply (simp add: oadd_Limit)
paulson@13221
   617
apply (frule Limit_has_1 [THEN ltD])
paulson@13221
   618
apply (rule increasing_LimitI)
paulson@13221
   619
 apply (rule Ord_0_lt)
paulson@13221
   620
  apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
paulson@13221
   621
 apply (force simp add: Union_empty_iff oadd_eq_0_iff
paulson@13221
   622
                        Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
paulson@13339
   623
apply (rule_tac x="succ(y)" in bexI)
paulson@13221
   624
 apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
paulson@13221
   625
apply (simp add: Limit_def lt_def) 
paulson@13221
   626
done
paulson@13221
   627
paulson@14046
   628
text{*Order/monotonicity properties of ordinal addition *}
paulson@13140
   629
paulson@13140
   630
lemma oadd_le_self2: "Ord(i) ==> i le j++i"
paulson@13140
   631
apply (erule_tac i = i in trans_induct3)
paulson@13140
   632
apply (simp (no_asm_simp) add: Ord_0_le)
paulson@13140
   633
apply (simp (no_asm_simp) add: oadd_succ succ_leI)
paulson@13140
   634
apply (simp (no_asm_simp) add: oadd_Limit)
paulson@13140
   635
apply (rule le_trans)
paulson@13140
   636
apply (rule_tac [2] le_implies_UN_le_UN)
paulson@13140
   637
apply (erule_tac [2] bspec)
paulson@13356
   638
 prefer 2 apply assumption
paulson@13356
   639
apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
paulson@13140
   640
done
paulson@13140
   641
paulson@13140
   642
lemma oadd_le_mono1: "k le j ==> k++i le j++i"
paulson@13140
   643
apply (frule lt_Ord)
paulson@13140
   644
apply (frule le_Ord2)
paulson@13140
   645
apply (simp add: oadd_eq_if_raw_oadd, clarify)
paulson@13140
   646
apply (simp add: raw_oadd_eq_oadd)
paulson@13140
   647
apply (erule_tac i = i in trans_induct3)
paulson@13140
   648
apply (simp (no_asm_simp))
paulson@13140
   649
apply (simp (no_asm_simp) add: oadd_succ succ_le_iff)
paulson@13140
   650
apply (simp (no_asm_simp) add: oadd_Limit)
paulson@13140
   651
apply (rule le_implies_UN_le_UN, blast)
paulson@13140
   652
done
paulson@13140
   653
paulson@13140
   654
lemma oadd_lt_mono: "[| i' le i;  j'<j |] ==> i'++j' < i++j"
paulson@13140
   655
by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)
paulson@13140
   656
paulson@13140
   657
lemma oadd_le_mono: "[| i' le i;  j' le j |] ==> i'++j' le i++j"
paulson@13140
   658
by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
paulson@13140
   659
paulson@13140
   660
lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"
paulson@13140
   661
by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
paulson@13140
   662
paulson@13221
   663
lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
paulson@13221
   664
apply (rule lt_trans2) 
paulson@13221
   665
apply (erule le_refl) 
paulson@13221
   666
apply (simp only: lt_Ord2  oadd_1 [of i, symmetric]) 
paulson@13221
   667
apply (blast intro: succ_leI oadd_le_mono)
paulson@13221
   668
done
paulson@13221
   669
paulson@13269
   670
text{*Every ordinal is exceeded by some limit ordinal.*}
paulson@13269
   671
lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
paulson@13269
   672
apply (rule_tac x="i ++ nat" in exI) 
paulson@13269
   673
apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
paulson@13269
   674
done
paulson@13269
   675
paulson@13269
   676
lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
paulson@13269
   677
apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit]) 
paulson@13269
   678
apply (simp add: Un_least_lt_iff) 
paulson@13269
   679
done
paulson@13269
   680
paulson@13140
   681
paulson@14046
   682
subsection{*Ordinal Subtraction*}
paulson@14046
   683
paulson@14046
   684
text{*The difference is @{term "ordertype(j-i, Memrel(j))"}.
paulson@14046
   685
    It's probably simpler to define the difference recursively!*}
paulson@13140
   686
paulson@13140
   687
lemma bij_sum_Diff:
paulson@13140
   688
     "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"
paulson@13140
   689
apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
paulson@13140
   690
apply (blast intro!: if_type)
paulson@13140
   691
apply (fast intro!: case_type)
paulson@13140
   692
apply (erule_tac [2] sumE)
paulson@13140
   693
apply (simp_all (no_asm_simp))
paulson@13140
   694
done
paulson@13140
   695
paulson@13140
   696
lemma ordertype_sum_Diff:
paulson@13140
   697
     "i le j ==>   
paulson@13140
   698
            ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =        
paulson@13140
   699
            ordertype(j, Memrel(j))"
paulson@13140
   700
apply (safe dest!: le_subset_iff [THEN iffD1])
paulson@13140
   701
apply (rule bij_sum_Diff [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
paulson@13140
   702
apply (erule_tac [3] well_ord_Memrel, assumption)
paulson@13140
   703
apply (simp (no_asm_simp))
paulson@13140
   704
apply (frule_tac j = y in Ord_in_Ord, assumption)
paulson@13140
   705
apply (frule_tac j = x in Ord_in_Ord, assumption)
paulson@13140
   706
apply (simp (no_asm_simp) add: Ord_mem_iff_lt lt_Ord not_lt_iff_le)
paulson@13140
   707
apply (blast intro: lt_trans2 lt_trans)
paulson@13140
   708
done
paulson@13140
   709
paulson@13140
   710
lemma Ord_odiff [simp,TC]: 
paulson@13140
   711
    "[| Ord(i);  Ord(j) |] ==> Ord(i--j)"
paulson@13140
   712
apply (unfold odiff_def)
paulson@13140
   713
apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
paulson@13140
   714
done
paulson@13140
   715
paulson@13140
   716
paulson@13140
   717
lemma raw_oadd_ordertype_Diff: 
paulson@13140
   718
   "i le j   
paulson@13140
   719
    ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
paulson@13140
   720
apply (simp add: raw_oadd_def odiff_def)
paulson@13140
   721
apply (safe dest!: le_subset_iff [THEN iffD1])
paulson@13140
   722
apply (rule sum_ord_iso_cong [THEN ordertype_eq])
paulson@13140
   723
apply (erule id_ord_iso_Memrel)
paulson@13140
   724
apply (rule ordertype_ord_iso [THEN ord_iso_sym])
paulson@13140
   725
apply (blast intro: well_ord_radd Diff_subset well_ord_subset well_ord_Memrel)+
paulson@13140
   726
done
paulson@13140
   727
paulson@13140
   728
lemma oadd_odiff_inverse: "i le j ==> i ++ (j--i) = j"
paulson@13140
   729
by (simp add: lt_Ord le_Ord2 oadd_def ordify_def raw_oadd_ordertype_Diff
paulson@13140
   730
              ordertype_sum_Diff ordertype_Memrel lt_Ord2 [THEN Ord_succD])
paulson@13140
   731
paulson@13140
   732
(*By oadd_inject, the difference between i and j is unique.  Note that we get
paulson@13140
   733
  i++j = k  ==>  j = k--i.  *)
paulson@13140
   734
lemma odiff_oadd_inverse: "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"
paulson@13140
   735
apply (rule oadd_inject)
paulson@13140
   736
apply (blast intro: oadd_odiff_inverse oadd_le_self)
paulson@13140
   737
apply (blast intro: Ord_ordertype Ord_oadd Ord_odiff)+
paulson@13140
   738
done
paulson@13140
   739
paulson@13140
   740
lemma odiff_lt_mono2: "[| i<j;  k le i |] ==> i--k < j--k"
paulson@13140
   741
apply (rule_tac i = k in oadd_lt_cancel2)
paulson@13140
   742
apply (simp add: oadd_odiff_inverse)
paulson@13140
   743
apply (subst oadd_odiff_inverse)
paulson@13140
   744
apply (blast intro: le_trans leI, assumption)
paulson@13140
   745
apply (simp (no_asm_simp) add: lt_Ord le_Ord2)
paulson@13140
   746
done
paulson@13140
   747
paulson@13140
   748
paulson@13269
   749
subsection{*Ordinal Multiplication*}
paulson@13140
   750
paulson@13140
   751
lemma Ord_omult [simp,TC]: 
paulson@13140
   752
    "[| Ord(i);  Ord(j) |] ==> Ord(i**j)"
paulson@13140
   753
apply (unfold omult_def)
paulson@13140
   754
apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
paulson@13140
   755
done
paulson@13140
   756
paulson@13356
   757
subsubsection{*A useful unfolding law *}
paulson@13140
   758
paulson@13140
   759
lemma pred_Pair_eq: 
paulson@13140
   760
 "[| a:A;  b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =      
paulson@13140
   761
                      pred(A,a,r)*B Un ({a} * pred(B,b,s))"
paulson@13140
   762
apply (unfold pred_def, blast)
paulson@13140
   763
done
paulson@13140
   764
paulson@13140
   765
lemma ordertype_pred_Pair_eq:
paulson@13140
   766
     "[| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>            
paulson@13140
   767
         ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =  
paulson@13140
   768
         ordertype(pred(A,a,r)*B + pred(B,b,s),                         
paulson@13140
   769
                  radd(A*B, rmult(A,r,B,s), B, s))"
paulson@13140
   770
apply (simp (no_asm_simp) add: pred_Pair_eq)
paulson@13140
   771
apply (rule ordertype_eq [symmetric])
paulson@13140
   772
apply (rule prod_sum_singleton_ord_iso)
paulson@13140
   773
apply (simp_all add: pred_subset well_ord_rmult [THEN well_ord_subset])
paulson@13140
   774
apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset] 
paulson@13140
   775
             elim!: predE)
paulson@13140
   776
done
paulson@13140
   777
paulson@13140
   778
lemma ordertype_pred_Pair_lemma: 
paulson@13140
   779
    "[| i'<i;  j'<j |]
paulson@13140
   780
     ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),  
paulson@13140
   781
                   rmult(i,Memrel(i),j,Memrel(j))) =                    
paulson@13140
   782
         raw_oadd (j**i', j')"
paulson@13140
   783
apply (unfold raw_oadd_def omult_def)
paulson@13356
   784
apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 
paulson@13356
   785
                 well_ord_Memrel)
paulson@13140
   786
apply (rule trans)
paulson@13356
   787
 apply (rule_tac [2] ordertype_ord_iso 
paulson@13356
   788
                      [THEN sum_ord_iso_cong, THEN ordertype_eq])
paulson@13356
   789
  apply (rule_tac [3] ord_iso_refl)
paulson@13140
   790
apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])
paulson@13140
   791
apply (elim SigmaE sumE ltE ssubst)
paulson@13140
   792
apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
paulson@13140
   793
                     Ord_ordertype lt_Ord lt_Ord2) 
paulson@13140
   794
apply (blast intro: Ord_trans)+
paulson@13140
   795
done
paulson@13140
   796
paulson@13140
   797
lemma lt_omult: 
paulson@13140
   798
 "[| Ord(i);  Ord(j);  k<j**i |]
paulson@13140
   799
  ==> EX j' i'. k = j**i' ++ j' & j'<j & i'<i"
paulson@13140
   800
apply (unfold omult_def)
paulson@13140
   801
apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
paulson@13140
   802
apply (safe elim!: ltE)
paulson@13140
   803
apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd 
paulson@13140
   804
            omult_def [symmetric] Ord_in_Ord' [of _ i] Ord_in_Ord' [of _ j])
paulson@13140
   805
apply (blast intro: ltI)
paulson@13140
   806
done
paulson@13140
   807
paulson@13140
   808
lemma omult_oadd_lt: 
paulson@13140
   809
     "[| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i"
paulson@13140
   810
apply (unfold omult_def)
paulson@13140
   811
apply (rule ltI)
paulson@13140
   812
 prefer 2
paulson@13140
   813
 apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
paulson@13356
   814
apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
paulson@14864
   815
apply (rule bexI [of _ i']) 
paulson@14864
   816
apply (rule bexI [of _ j']) 
paulson@13140
   817
apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
paulson@13140
   818
apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
paulson@14864
   819
apply (simp_all add: lt_def) 
paulson@13140
   820
done
paulson@13140
   821
paulson@13140
   822
lemma omult_unfold:
paulson@13615
   823
     "[| Ord(i);  Ord(j) |] ==> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})"
paulson@13140
   824
apply (rule subsetI [THEN equalityI])
paulson@13140
   825
apply (rule lt_omult [THEN exE])
paulson@13140
   826
apply (erule_tac [3] ltI)
paulson@13140
   827
apply (simp_all add: Ord_omult) 
paulson@13140
   828
apply (blast elim!: ltE)
paulson@13140
   829
apply (blast intro: omult_oadd_lt [THEN ltD] ltI)
paulson@13140
   830
done
paulson@13140
   831
paulson@13356
   832
subsubsection{*Basic laws for ordinal multiplication *}
paulson@13140
   833
paulson@14046
   834
text{*Ordinal multiplication by zero *}
paulson@13140
   835
paulson@13140
   836
lemma omult_0 [simp]: "i**0 = 0"
paulson@13140
   837
apply (unfold omult_def)
paulson@13140
   838
apply (simp (no_asm_simp))
paulson@13140
   839
done
paulson@13140
   840
paulson@13140
   841
lemma omult_0_left [simp]: "0**i = 0"
paulson@13140
   842
apply (unfold omult_def)
paulson@13140
   843
apply (simp (no_asm_simp))
paulson@13140
   844
done
paulson@13140
   845
paulson@14046
   846
text{*Ordinal multiplication by 1 *}
paulson@13140
   847
paulson@13140
   848
lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
paulson@13140
   849
apply (unfold omult_def)
paulson@13140
   850
apply (rule_tac s1="Memrel(i)" 
paulson@13140
   851
       in ord_isoI [THEN ordertype_eq, THEN trans])
paulson@13140
   852
apply (rule_tac c = snd and d = "%z.<0,z>"  in lam_bijective)
paulson@13140
   853
apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)
paulson@13140
   854
done
paulson@13140
   855
paulson@13140
   856
lemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"
paulson@13140
   857
apply (unfold omult_def)
paulson@13140
   858
apply (rule_tac s1="Memrel(i)" 
paulson@13140
   859
       in ord_isoI [THEN ordertype_eq, THEN trans])
paulson@13140
   860
apply (rule_tac c = fst and d = "%z.<z,0>" in lam_bijective)
paulson@13140
   861
apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)
paulson@13140
   862
done
paulson@13140
   863
paulson@14046
   864
text{*Distributive law for ordinal multiplication and addition *}
paulson@13140
   865
paulson@13140
   866
lemma oadd_omult_distrib:
paulson@13140
   867
     "[| Ord(i);  Ord(j);  Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"
paulson@13140
   868
apply (simp add: oadd_eq_if_raw_oadd)
paulson@13140
   869
apply (simp add: omult_def raw_oadd_def)
paulson@13140
   870
apply (rule ordertype_eq [THEN trans])
paulson@13140
   871
apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym] 
paulson@13140
   872
                                  ord_iso_refl])
paulson@13140
   873
apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel 
paulson@13140
   874
                     Ord_ordertype)
paulson@13140
   875
apply (rule sum_prod_distrib_ord_iso [THEN ordertype_eq, THEN trans])
paulson@13140
   876
apply (rule_tac [2] ordertype_eq)
paulson@13140
   877
apply (rule_tac [2] sum_ord_iso_cong [OF ordertype_ord_iso ordertype_ord_iso])
paulson@13140
   878
apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel 
paulson@13140
   879
                     Ord_ordertype)
paulson@13140
   880
done
paulson@13140
   881
paulson@13140
   882
lemma omult_succ: "[| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i"
paulson@13140
   883
by (simp del: oadd_succ add: oadd_1 [of j, symmetric] oadd_omult_distrib)
paulson@13140
   884
paulson@14046
   885
text{*Associative law *}
paulson@13140
   886
paulson@13140
   887
lemma omult_assoc: 
paulson@13140
   888
    "[| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)"
paulson@13140
   889
apply (unfold omult_def)
paulson@13140
   890
apply (rule ordertype_eq [THEN trans])
paulson@13140
   891
apply (rule prod_ord_iso_cong [OF ord_iso_refl 
paulson@13140
   892
                                  ordertype_ord_iso [THEN ord_iso_sym]])
paulson@13140
   893
apply (blast intro: well_ord_rmult well_ord_Memrel)+
paulson@13356
   894
apply (rule prod_assoc_ord_iso 
paulson@13356
   895
             [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
paulson@13140
   896
apply (rule_tac [2] ordertype_eq)
paulson@13140
   897
apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])
paulson@13140
   898
apply (blast intro: well_ord_rmult well_ord_Memrel Ord_ordertype)+
paulson@13140
   899
done
paulson@13140
   900
paulson@13140
   901
paulson@14046
   902
text{*Ordinal multiplication with limit ordinals *}
paulson@13140
   903
paulson@13140
   904
lemma omult_UN: 
paulson@13140
   905
     "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |]
paulson@13615
   906
      ==> i ** (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i**j(x))"
paulson@13140
   907
by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
paulson@13140
   908
paulson@13615
   909
lemma omult_Limit: "[| Ord(i);  Limit(j) |] ==> i**j = (\<Union>k\<in>j. i**k)"
paulson@13140
   910
by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric] 
paulson@13140
   911
              Union_eq_UN [symmetric] Limit_Union_eq)
paulson@13140
   912
paulson@13140
   913
paulson@13356
   914
subsubsection{*Ordering/monotonicity properties of ordinal multiplication *}
paulson@13140
   915
paulson@13140
   916
(*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
paulson@13140
   917
lemma lt_omult1: "[| k<i;  0<j |] ==> k < i**j"
paulson@13140
   918
apply (safe elim!: ltE intro!: ltI Ord_omult)
paulson@13140
   919
apply (force simp add: omult_unfold)
paulson@13140
   920
done
paulson@13140
   921
paulson@13140
   922
lemma omult_le_self: "[| Ord(i);  0<j |] ==> i le i**j"
paulson@13140
   923
by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
paulson@13140
   924
paulson@13140
   925
lemma omult_le_mono1: "[| k le j;  Ord(i) |] ==> k**i le j**i"
paulson@13140
   926
apply (frule lt_Ord)
paulson@13140
   927
apply (frule le_Ord2)
paulson@13140
   928
apply (erule trans_induct3)
paulson@13140
   929
apply (simp (no_asm_simp) add: le_refl Ord_0)
paulson@13140
   930
apply (simp (no_asm_simp) add: omult_succ oadd_le_mono)
paulson@13140
   931
apply (simp (no_asm_simp) add: omult_Limit)
paulson@13140
   932
apply (rule le_implies_UN_le_UN, blast)
paulson@13140
   933
done
paulson@13140
   934
paulson@13140
   935
lemma omult_lt_mono2: "[| k<j;  0<i |] ==> i**k < i**j"
paulson@13140
   936
apply (rule ltI)
paulson@13140
   937
apply (simp (no_asm_simp) add: omult_unfold lt_Ord2)
paulson@13140
   938
apply (safe elim!: ltE intro!: Ord_omult)
paulson@13140
   939
apply (force simp add: Ord_omult)
paulson@13140
   940
done
paulson@13140
   941
paulson@13140
   942
lemma omult_le_mono2: "[| k le j;  Ord(i) |] ==> i**k le i**j"
paulson@13140
   943
apply (rule subset_imp_le)
paulson@13140
   944
apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)
paulson@13140
   945
apply (simp add: omult_unfold)
paulson@13140
   946
apply (blast intro: Ord_trans) 
paulson@13140
   947
done
paulson@13140
   948
paulson@13140
   949
lemma omult_le_mono: "[| i' le i;  j' le j |] ==> i'**j' le i**j"
paulson@13140
   950
by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)
paulson@13140
   951
paulson@13140
   952
lemma omult_lt_mono: "[| i' le i;  j'<j;  0<i |] ==> i'**j' < i**j"
paulson@13140
   953
by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
paulson@13140
   954
paulson@13140
   955
lemma omult_le_self2: "[| Ord(i);  0<j |] ==> i le j**i"
paulson@13140
   956
apply (frule lt_Ord2)
paulson@13140
   957
apply (erule_tac i = i in trans_induct3)
paulson@13140
   958
apply (simp (no_asm_simp))
paulson@13140
   959
apply (simp (no_asm_simp) add: omult_succ)
paulson@13140
   960
apply (erule lt_trans1)
paulson@13140
   961
apply (rule_tac b = "j**x" in oadd_0 [THEN subst], rule_tac [2] oadd_lt_mono2)
paulson@13140
   962
apply (blast intro: Ord_omult, assumption)
paulson@13140
   963
apply (simp (no_asm_simp) add: omult_Limit)
paulson@13140
   964
apply (rule le_trans)
paulson@13140
   965
apply (rule_tac [2] le_implies_UN_le_UN)
paulson@13140
   966
prefer 2 apply blast
paulson@13140
   967
apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq Limit_is_Ord)
paulson@13140
   968
done
paulson@13140
   969
paulson@13140
   970
paulson@14046
   971
text{*Further properties of ordinal multiplication *}
paulson@13140
   972
paulson@13140
   973
lemma omult_inject: "[| i**j = i**k;  0<i;  Ord(j);  Ord(k) |] ==> j=k"
paulson@13140
   974
apply (rule Ord_linear_lt)
paulson@13140
   975
prefer 4 apply assumption
paulson@13140
   976
apply auto 
paulson@13140
   977
apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
paulson@13140
   978
done
paulson@13140
   979
paulson@14046
   980
subsection{*The Relation @{term Lt}*}
paulson@14046
   981
paulson@14046
   982
lemma wf_Lt: "wf(Lt)"
paulson@14046
   983
apply (rule wf_subset) 
paulson@14046
   984
apply (rule wf_Memrel) 
paulson@14046
   985
apply (auto simp add: Lt_def Memrel_def lt_def) 
paulson@14046
   986
done
paulson@14046
   987
paulson@14046
   988
lemma irrefl_Lt: "irrefl(A,Lt)"
paulson@14046
   989
by (auto simp add: Lt_def irrefl_def)
paulson@14046
   990
paulson@14046
   991
lemma trans_Lt: "trans[A](Lt)"
paulson@14046
   992
apply (simp add: Lt_def trans_on_def) 
paulson@14046
   993
apply (blast intro: lt_trans) 
paulson@14046
   994
done
paulson@14046
   995
paulson@14046
   996
lemma part_ord_Lt: "part_ord(A,Lt)"
paulson@14046
   997
by (simp add: part_ord_def irrefl_Lt trans_Lt)
paulson@14046
   998
paulson@14046
   999
lemma linear_Lt: "linear(nat,Lt)"
paulson@14046
  1000
apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff) 
paulson@14046
  1001
apply (drule lt_asym, auto) 
paulson@14046
  1002
done
paulson@14046
  1003
paulson@14046
  1004
lemma tot_ord_Lt: "tot_ord(nat,Lt)"
paulson@14046
  1005
by (simp add: tot_ord_def linear_Lt part_ord_Lt)
paulson@14046
  1006
paulson@14052
  1007
lemma well_ord_Lt: "well_ord(nat,Lt)"
paulson@14052
  1008
by (simp add: well_ord_def wf_Lt wf_imp_wf_on tot_ord_Lt)
paulson@14052
  1009
paulson@14046
  1010
paulson@14046
  1011
paulson@13140
  1012
ML {*
paulson@13140
  1013
val ordermap_def = thm "ordermap_def";
paulson@13140
  1014
val ordertype_def = thm "ordertype_def";
paulson@13140
  1015
val Ord_alt_def = thm "Ord_alt_def";
paulson@13140
  1016
val ordify_def = thm "ordify_def";
paulson@13140
  1017
paulson@13140
  1018
val Ord_in_Ord' = thm "Ord_in_Ord'";
paulson@13140
  1019
val le_well_ord_Memrel = thm "le_well_ord_Memrel";
paulson@13140
  1020
val well_ord_Memrel = thm "well_ord_Memrel";
paulson@13140
  1021
val lt_pred_Memrel = thm "lt_pred_Memrel";
paulson@13140
  1022
val pred_Memrel = thm "pred_Memrel";
paulson@13140
  1023
val Ord_iso_implies_eq = thm "Ord_iso_implies_eq";
paulson@13140
  1024
val ordermap_type = thm "ordermap_type";
paulson@13140
  1025
val ordermap_eq_image = thm "ordermap_eq_image";
paulson@13140
  1026
val ordermap_pred_unfold = thm "ordermap_pred_unfold";
paulson@13140
  1027
val ordermap_unfold = thm "ordermap_unfold";
paulson@13140
  1028
val Ord_ordermap = thm "Ord_ordermap";
paulson@13140
  1029
val Ord_ordertype = thm "Ord_ordertype";
paulson@13140
  1030
val ordermap_mono = thm "ordermap_mono";
paulson@13140
  1031
val converse_ordermap_mono = thm "converse_ordermap_mono";
paulson@13140
  1032
val ordermap_surj = thm "ordermap_surj";
paulson@13140
  1033
val ordermap_bij = thm "ordermap_bij";
paulson@13140
  1034
val ordertype_ord_iso = thm "ordertype_ord_iso";
paulson@13140
  1035
val ordertype_eq = thm "ordertype_eq";
paulson@13140
  1036
val ordertype_eq_imp_ord_iso = thm "ordertype_eq_imp_ord_iso";
paulson@13140
  1037
val le_ordertype_Memrel = thm "le_ordertype_Memrel";
paulson@13140
  1038
val ordertype_Memrel = thm "ordertype_Memrel";
paulson@13140
  1039
val ordertype_0 = thm "ordertype_0";
paulson@13140
  1040
val bij_ordertype_vimage = thm "bij_ordertype_vimage";
paulson@13140
  1041
val ordermap_pred_eq_ordermap = thm "ordermap_pred_eq_ordermap";
paulson@13140
  1042
val ordertype_unfold = thm "ordertype_unfold";
paulson@13140
  1043
val ordertype_pred_subset = thm "ordertype_pred_subset";
paulson@13140
  1044
val ordertype_pred_lt = thm "ordertype_pred_lt";
paulson@13140
  1045
val ordertype_pred_unfold = thm "ordertype_pred_unfold";
paulson@13140
  1046
val Ord_is_Ord_alt = thm "Ord_is_Ord_alt";
paulson@13140
  1047
val Ord_alt_is_Ord = thm "Ord_alt_is_Ord";
paulson@13140
  1048
val bij_sum_0 = thm "bij_sum_0";
paulson@13140
  1049
val ordertype_sum_0_eq = thm "ordertype_sum_0_eq";
paulson@13140
  1050
val bij_0_sum = thm "bij_0_sum";
paulson@13140
  1051
val ordertype_0_sum_eq = thm "ordertype_0_sum_eq";
paulson@13140
  1052
val pred_Inl_bij = thm "pred_Inl_bij";
paulson@13140
  1053
val ordertype_pred_Inl_eq = thm "ordertype_pred_Inl_eq";
paulson@13140
  1054
val pred_Inr_bij = thm "pred_Inr_bij";
paulson@13140
  1055
val ordertype_pred_Inr_eq = thm "ordertype_pred_Inr_eq";
paulson@13140
  1056
val Ord_ordify = thm "Ord_ordify";
paulson@13140
  1057
val ordify_idem = thm "ordify_idem";
paulson@13140
  1058
val Ord_raw_oadd = thm "Ord_raw_oadd";
paulson@13140
  1059
val Ord_oadd = thm "Ord_oadd";
paulson@13140
  1060
val raw_oadd_0 = thm "raw_oadd_0";
paulson@13140
  1061
val oadd_0 = thm "oadd_0";
paulson@13140
  1062
val raw_oadd_0_left = thm "raw_oadd_0_left";
paulson@13140
  1063
val oadd_0_left = thm "oadd_0_left";
paulson@13140
  1064
val oadd_eq_if_raw_oadd = thm "oadd_eq_if_raw_oadd";
paulson@13140
  1065
val raw_oadd_eq_oadd = thm "raw_oadd_eq_oadd";
paulson@13140
  1066
val lt_oadd1 = thm "lt_oadd1";
paulson@13140
  1067
val oadd_le_self = thm "oadd_le_self";
paulson@13140
  1068
val id_ord_iso_Memrel = thm "id_ord_iso_Memrel";
paulson@13140
  1069
val ordertype_sum_Memrel = thm "ordertype_sum_Memrel";
paulson@13140
  1070
val oadd_lt_mono2 = thm "oadd_lt_mono2";
paulson@13140
  1071
val oadd_lt_cancel2 = thm "oadd_lt_cancel2";
paulson@13140
  1072
val oadd_lt_iff2 = thm "oadd_lt_iff2";
paulson@13140
  1073
val oadd_inject = thm "oadd_inject";
paulson@13140
  1074
val lt_oadd_disj = thm "lt_oadd_disj";
paulson@13140
  1075
val oadd_assoc = thm "oadd_assoc";
paulson@13140
  1076
val oadd_unfold = thm "oadd_unfold";
paulson@13140
  1077
val oadd_1 = thm "oadd_1";
paulson@13140
  1078
val oadd_succ = thm "oadd_succ";
paulson@13140
  1079
val oadd_UN = thm "oadd_UN";
paulson@13140
  1080
val oadd_Limit = thm "oadd_Limit";
paulson@13140
  1081
val oadd_le_self2 = thm "oadd_le_self2";
paulson@13140
  1082
val oadd_le_mono1 = thm "oadd_le_mono1";
paulson@13140
  1083
val oadd_lt_mono = thm "oadd_lt_mono";
paulson@13140
  1084
val oadd_le_mono = thm "oadd_le_mono";
paulson@13140
  1085
val oadd_le_iff2 = thm "oadd_le_iff2";
paulson@13140
  1086
val bij_sum_Diff = thm "bij_sum_Diff";
paulson@13140
  1087
val ordertype_sum_Diff = thm "ordertype_sum_Diff";
paulson@13140
  1088
val Ord_odiff = thm "Ord_odiff";
paulson@13140
  1089
val raw_oadd_ordertype_Diff = thm "raw_oadd_ordertype_Diff";
paulson@13140
  1090
val oadd_odiff_inverse = thm "oadd_odiff_inverse";
paulson@13140
  1091
val odiff_oadd_inverse = thm "odiff_oadd_inverse";
paulson@13140
  1092
val odiff_lt_mono2 = thm "odiff_lt_mono2";
paulson@13140
  1093
val Ord_omult = thm "Ord_omult";
paulson@13140
  1094
val pred_Pair_eq = thm "pred_Pair_eq";
paulson@13140
  1095
val ordertype_pred_Pair_eq = thm "ordertype_pred_Pair_eq";
paulson@13140
  1096
val lt_omult = thm "lt_omult";
paulson@13140
  1097
val omult_oadd_lt = thm "omult_oadd_lt";
paulson@13140
  1098
val omult_unfold = thm "omult_unfold";
paulson@13140
  1099
val omult_0 = thm "omult_0";
paulson@13140
  1100
val omult_0_left = thm "omult_0_left";
paulson@13140
  1101
val omult_1 = thm "omult_1";
paulson@13140
  1102
val omult_1_left = thm "omult_1_left";
paulson@13140
  1103
val oadd_omult_distrib = thm "oadd_omult_distrib";
paulson@13140
  1104
val omult_succ = thm "omult_succ";
paulson@13140
  1105
val omult_assoc = thm "omult_assoc";
paulson@13140
  1106
val omult_UN = thm "omult_UN";
paulson@13140
  1107
val omult_Limit = thm "omult_Limit";
paulson@13140
  1108
val lt_omult1 = thm "lt_omult1";
paulson@13140
  1109
val omult_le_self = thm "omult_le_self";
paulson@13140
  1110
val omult_le_mono1 = thm "omult_le_mono1";
paulson@13140
  1111
val omult_lt_mono2 = thm "omult_lt_mono2";
paulson@13140
  1112
val omult_le_mono2 = thm "omult_le_mono2";
paulson@13140
  1113
val omult_le_mono = thm "omult_le_mono";
paulson@13140
  1114
val omult_lt_mono = thm "omult_lt_mono";
paulson@13140
  1115
val omult_le_self2 = thm "omult_le_self2";
paulson@13140
  1116
val omult_inject = thm "omult_inject";
paulson@14046
  1117
paulson@14046
  1118
val wf_Lt = thm "wf_Lt";
paulson@14046
  1119
val irrefl_Lt = thm "irrefl_Lt";
paulson@14046
  1120
val trans_Lt = thm "trans_Lt";
paulson@14046
  1121
val part_ord_Lt = thm "part_ord_Lt";
paulson@14046
  1122
val linear_Lt = thm "linear_Lt";
paulson@14046
  1123
val tot_ord_Lt = thm "tot_ord_Lt";
paulson@14052
  1124
val well_ord_Lt = thm "well_ord_Lt";
paulson@13140
  1125
*}
paulson@9654
  1126
lcp@435
  1127
end