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