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