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