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