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