author | paulson |
Wed, 09 Oct 1996 13:32:33 +0200 | |
changeset 2073 | fb0655539d05 |
parent 2033 | 639de962ded4 |
child 2469 | b50b8c0eec01 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/OrderType.ML |
435 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
435 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
849 | 6 |
Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory |
7 |
||
8 |
Ordinal arithmetic is traditionally defined in terms of order types, as here. |
|
9 |
But a definition by transfinite recursion would be much simpler! |
|
435 | 10 |
*) |
11 |
||
12 |
||
13 |
open OrderType; |
|
14 |
||
849 | 15 |
(**** Proofs needing the combination of Ordinal.thy and Order.thy ****) |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
16 |
|
849 | 17 |
val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))"; |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
18 |
by (rtac well_ordI 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
19 |
by (rtac (wf_Memrel RS wf_imp_wf_on) 1); |
849 | 20 |
by (resolve_tac [prem RS ltE] 1); |
21 |
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff, |
|
1461 | 22 |
[ltI, prem] MRS lt_trans2 RS ltD]) 1); |
849 | 23 |
by (REPEAT (resolve_tac [ballI, Ord_linear] 1)); |
24 |
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); |
|
25 |
qed "le_well_ord_Memrel"; |
|
26 |
||
27 |
(*"Ord(i) ==> well_ord(i, Memrel(i))"*) |
|
28 |
bind_thm ("well_ord_Memrel", le_refl RS le_well_ord_Memrel); |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
29 |
|
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
30 |
(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
31 |
The smaller ordinal is an initial segment of the larger *) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
32 |
goalw OrderType.thy [pred_def, lt_def] |
849 | 33 |
"!!i j. j<i ==> pred(i, j, Memrel(i)) = j"; |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
34 |
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
35 |
by (fast_tac (eq_cs addEs [Ord_trans]) 1); |
849 | 36 |
qed "lt_pred_Memrel"; |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
37 |
|
831 | 38 |
goalw OrderType.thy [pred_def,Memrel_def] |
849 | 39 |
"!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x"; |
831 | 40 |
by (fast_tac eq_cs 1); |
41 |
qed "pred_Memrel"; |
|
42 |
||
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
43 |
goal OrderType.thy |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
44 |
"!!i. [| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"; |
849 | 45 |
by (forward_tac [lt_pred_Memrel] 1); |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
46 |
by (etac ltE 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
47 |
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
48 |
assume_tac 3 THEN assume_tac 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
49 |
by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
50 |
(*Combining the two simplifications causes looping*) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
51 |
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
52 |
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
53 |
qed "Ord_iso_implies_eq_lemma"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
54 |
|
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
55 |
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
56 |
goal OrderType.thy |
1461 | 57 |
"!!i. [| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \ |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
58 |
\ |] ==> i=j"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
59 |
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
60 |
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1)); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
61 |
qed "Ord_iso_implies_eq"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
62 |
|
849 | 63 |
|
64 |
(**** Ordermap and ordertype ****) |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
65 |
|
437 | 66 |
goalw OrderType.thy [ordermap_def,ordertype_def] |
67 |
"ordermap(A,r) : A -> ordertype(A,r)"; |
|
68 |
by (rtac lam_type 1); |
|
69 |
by (rtac (lamI RS imageI) 1); |
|
70 |
by (REPEAT (assume_tac 1)); |
|
760 | 71 |
qed "ordermap_type"; |
437 | 72 |
|
849 | 73 |
(*** Unfolding of ordermap ***) |
435 | 74 |
|
437 | 75 |
(*Useful for cardinality reasoning; see CardinalArith.ML*) |
435 | 76 |
goalw OrderType.thy [ordermap_def, pred_def] |
77 |
"!!r. [| wf[A](r); x:A |] ==> \ |
|
437 | 78 |
\ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"; |
79 |
by (asm_simp_tac ZF_ss 1); |
|
80 |
by (etac (wfrec_on RS trans) 1); |
|
81 |
by (assume_tac 1); |
|
82 |
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam, |
|
83 |
vimage_singleton_iff]) 1); |
|
760 | 84 |
qed "ordermap_eq_image"; |
437 | 85 |
|
467 | 86 |
(*Useful for rewriting PROVIDED pred is not unfolded until later!*) |
437 | 87 |
goal OrderType.thy |
88 |
"!!r. [| wf[A](r); x:A |] ==> \ |
|
435 | 89 |
\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"; |
437 | 90 |
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, |
1461 | 91 |
ordermap_type RS image_fun]) 1); |
760 | 92 |
qed "ordermap_pred_unfold"; |
435 | 93 |
|
94 |
(*pred-unfolded version. NOT suitable for rewriting -- loops!*) |
|
95 |
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold; |
|
96 |
||
849 | 97 |
(*** Showing that ordermap, ordertype yield ordinals ***) |
435 | 98 |
|
99 |
fun ordermap_elim_tac i = |
|
100 |
EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i, |
|
1461 | 101 |
assume_tac (i+1), |
102 |
assume_tac i]; |
|
435 | 103 |
|
104 |
goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def] |
|
105 |
"!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"; |
|
106 |
by (safe_tac ZF_cs); |
|
107 |
by (wf_on_ind_tac "x" [] 1); |
|
108 |
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1); |
|
109 |
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
|
437 | 110 |
by (rewrite_goals_tac [pred_def,Transset_def]); |
435 | 111 |
by (fast_tac ZF_cs 2); |
112 |
by (safe_tac ZF_cs); |
|
113 |
by (ordermap_elim_tac 1); |
|
114 |
by (fast_tac (ZF_cs addSEs [trans_onD]) 1); |
|
760 | 115 |
qed "Ord_ordermap"; |
435 | 116 |
|
117 |
goalw OrderType.thy [ordertype_def] |
|
118 |
"!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; |
|
2033 | 119 |
by (stac ([ordermap_type, subset_refl] MRS image_fun) 1); |
435 | 120 |
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
121 |
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2); |
|
437 | 122 |
by (rewrite_goals_tac [Transset_def,well_ord_def]); |
435 | 123 |
by (safe_tac ZF_cs); |
124 |
by (ordermap_elim_tac 1); |
|
125 |
by (fast_tac ZF_cs 1); |
|
760 | 126 |
qed "Ord_ordertype"; |
435 | 127 |
|
849 | 128 |
(*** ordermap preserves the orderings in both directions ***) |
435 | 129 |
|
130 |
goal OrderType.thy |
|
1461 | 131 |
"!!r. [| <w,x>: r; wf[A](r); w: A; x: A |] ==> \ |
435 | 132 |
\ ordermap(A,r)`w : ordermap(A,r)`x"; |
133 |
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1); |
|
437 | 134 |
by (assume_tac 1); |
435 | 135 |
by (fast_tac ZF_cs 1); |
760 | 136 |
qed "ordermap_mono"; |
435 | 137 |
|
138 |
(*linearity of r is crucial here*) |
|
139 |
goalw OrderType.thy [well_ord_def, tot_ord_def] |
|
140 |
"!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ |
|
141 |
\ w: A; x: A |] ==> <w,x>: r"; |
|
142 |
by (safe_tac ZF_cs); |
|
143 |
by (linear_case_tac 1); |
|
144 |
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1); |
|
467 | 145 |
by (dtac ordermap_mono 1); |
435 | 146 |
by (REPEAT_SOME assume_tac); |
437 | 147 |
by (etac mem_asym 1); |
148 |
by (assume_tac 1); |
|
760 | 149 |
qed "converse_ordermap_mono"; |
435 | 150 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset
|
151 |
bind_thm ("ordermap_surj", |
1461 | 152 |
rewrite_rule [symmetric ordertype_def] |
153 |
(ordermap_type RS surj_image)); |
|
435 | 154 |
|
155 |
goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def] |
|
156 |
"!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; |
|
984 | 157 |
by (fast_tac (ZF_cs addSIs [ordermap_type, ordermap_surj] |
1461 | 158 |
addEs [linearE] |
159 |
addDs [ordermap_mono] |
|
984 | 160 |
addss (ZF_ss addsimps [mem_not_refl])) 1); |
760 | 161 |
qed "ordermap_bij"; |
435 | 162 |
|
849 | 163 |
(*** Isomorphisms involving ordertype ***) |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
164 |
|
435 | 165 |
goalw OrderType.thy [ord_iso_def] |
166 |
"!!r. well_ord(A,r) ==> \ |
|
167 |
\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; |
|
168 |
by (safe_tac ZF_cs); |
|
467 | 169 |
by (rtac ordermap_bij 1); |
437 | 170 |
by (assume_tac 1); |
467 | 171 |
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2); |
437 | 172 |
by (rewtac well_ord_def); |
467 | 173 |
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono, |
1461 | 174 |
ordermap_type RS apply_type]) 1); |
760 | 175 |
qed "ordertype_ord_iso"; |
435 | 176 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
177 |
goal OrderType.thy |
1461 | 178 |
"!!f. [| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \ |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
179 |
\ ordertype(A,r) = ordertype(B,s)"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
180 |
by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1); |
1461 | 181 |
by (rtac Ord_iso_implies_eq 1 |
182 |
THEN REPEAT (etac Ord_ordertype 1)); |
|
831 | 183 |
by (deepen_tac (ZF_cs addIs [ord_iso_trans, ord_iso_sym] |
184 |
addSEs [ordertype_ord_iso]) 0 1); |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
185 |
qed "ordertype_eq"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
186 |
|
849 | 187 |
goal OrderType.thy |
1461 | 188 |
"!!A B. [| ordertype(A,r) = ordertype(B,s); \ |
849 | 189 |
\ well_ord(A,r); well_ord(B,s) \ |
190 |
\ |] ==> EX f. f: ord_iso(A,r,B,s)"; |
|
1461 | 191 |
by (rtac exI 1); |
849 | 192 |
by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1); |
193 |
by (assume_tac 1); |
|
1461 | 194 |
by (etac ssubst 1); |
849 | 195 |
by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); |
196 |
qed "ordertype_eq_imp_ord_iso"; |
|
435 | 197 |
|
849 | 198 |
(*** Basic equalities for ordertype ***) |
467 | 199 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
200 |
(*Ordertype of Memrel*) |
849 | 201 |
goal OrderType.thy "!!i. j le i ==> ordertype(j,Memrel(i)) = j"; |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
202 |
by (resolve_tac [Ord_iso_implies_eq RS sym] 1); |
1461 | 203 |
by (etac ltE 1); |
849 | 204 |
by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1)); |
1461 | 205 |
by (rtac ord_iso_trans 1); |
849 | 206 |
by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2); |
207 |
by (resolve_tac [id_bij RS ord_isoI] 1); |
|
208 |
by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1); |
|
209 |
by (fast_tac (ZF_cs addEs [ltE, Ord_in_Ord, Ord_trans]) 1); |
|
210 |
qed "le_ordertype_Memrel"; |
|
211 |
||
212 |
(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*) |
|
213 |
bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel); |
|
467 | 214 |
|
849 | 215 |
goal OrderType.thy "ordertype(0,r) = 0"; |
216 |
by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1); |
|
217 |
by (etac emptyE 1); |
|
1461 | 218 |
by (rtac well_ord_0 1); |
849 | 219 |
by (resolve_tac [Ord_0 RS ordertype_Memrel] 1); |
220 |
qed "ordertype_0"; |
|
221 |
||
222 |
(*Ordertype of rvimage: [| f: bij(A,B); well_ord(B,s) |] ==> |
|
223 |
ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *) |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
224 |
bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq); |
467 | 225 |
|
849 | 226 |
(*** A fundamental unfolding law for ordertype. ***) |
227 |
||
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
228 |
(*Ordermap returns the same result if applied to an initial segment*) |
467 | 229 |
goal OrderType.thy |
1461 | 230 |
"!!r. [| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \ |
231 |
\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"; |
|
467 | 232 |
by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1); |
233 |
by (wf_on_ind_tac "z" [] 1); |
|
234 |
by (safe_tac (ZF_cs addSEs [predE])); |
|
235 |
by (asm_simp_tac |
|
236 |
(ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); |
|
237 |
(*combining these two simplifications LOOPS! *) |
|
238 |
by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1); |
|
239 |
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); |
|
807 | 240 |
by (rtac (refl RSN (2,RepFun_cong)) 1); |
241 |
by (dtac well_ord_is_trans_on 1); |
|
467 | 242 |
by (fast_tac (eq_cs addSEs [trans_onD]) 1); |
760 | 243 |
qed "ordermap_pred_eq_ordermap"; |
467 | 244 |
|
849 | 245 |
goalw OrderType.thy [ordertype_def] |
246 |
"ordertype(A,r) = {ordermap(A,r)`y . y : A}"; |
|
247 |
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1); |
|
248 |
qed "ordertype_unfold"; |
|
249 |
||
250 |
(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **) |
|
251 |
||
252 |
goal OrderType.thy |
|
253 |
"!!r. [| well_ord(A,r); x:A |] ==> \ |
|
254 |
\ ordertype(pred(A,x,r),r) <= ordertype(A,r)"; |
|
255 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, |
|
256 |
pred_subset RSN (2, well_ord_subset)]) 1); |
|
257 |
by (fast_tac (ZF_cs addIs [ordermap_pred_eq_ordermap, RepFun_eqI] |
|
1461 | 258 |
addEs [predE]) 1); |
849 | 259 |
qed "ordertype_pred_subset"; |
260 |
||
261 |
goal OrderType.thy |
|
262 |
"!!r. [| well_ord(A,r); x:A |] ==> \ |
|
263 |
\ ordertype(pred(A,x,r),r) < ordertype(A,r)"; |
|
264 |
by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1); |
|
265 |
by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1)); |
|
266 |
by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1); |
|
1461 | 267 |
by (etac well_ord_iso_predE 3); |
849 | 268 |
by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1)); |
269 |
qed "ordertype_pred_lt"; |
|
270 |
||
271 |
(*May rewrite with this -- provided no rules are supplied for proving that |
|
1461 | 272 |
well_ord(pred(A,x,r), r) *) |
849 | 273 |
goal OrderType.thy |
274 |
"!!A r. well_ord(A,r) ==> \ |
|
275 |
\ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"; |
|
276 |
by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD])); |
|
984 | 277 |
by (fast_tac |
278 |
(ZF_cs addss |
|
279 |
(ZF_ss addsimps [ordertype_def, |
|
1461 | 280 |
well_ord_is_wf RS ordermap_eq_image, |
281 |
ordermap_type RS image_fun, |
|
282 |
ordermap_pred_eq_ordermap, |
|
283 |
pred_subset])) |
|
984 | 284 |
1); |
849 | 285 |
qed "ordertype_pred_unfold"; |
286 |
||
287 |
||
288 |
(**** Alternative definition of ordinal ****) |
|
289 |
||
290 |
(*proof by Krzysztof Grabczewski*) |
|
291 |
goalw OrderType.thy [Ord_alt_def] "!!i. Ord(i) ==> Ord_alt(i)"; |
|
1461 | 292 |
by (rtac conjI 1); |
293 |
by (etac well_ord_Memrel 1); |
|
849 | 294 |
by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]); |
295 |
by (fast_tac eq_cs 1); |
|
296 |
qed "Ord_is_Ord_alt"; |
|
297 |
||
298 |
(*proof by lcp*) |
|
299 |
goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, |
|
1461 | 300 |
tot_ord_def, part_ord_def, trans_on_def] |
849 | 301 |
"!!i. Ord_alt(i) ==> Ord(i)"; |
302 |
by (asm_full_simp_tac (ZF_ss addsimps [Memrel_iff, pred_Memrel]) 1); |
|
303 |
by (safe_tac ZF_cs); |
|
304 |
by (fast_tac (ZF_cs addSDs [equalityD1]) 1); |
|
305 |
by (subgoal_tac "xa: i" 1); |
|
306 |
by (fast_tac (ZF_cs addSDs [equalityD1]) 2); |
|
307 |
by (fast_tac (ZF_cs addSDs [equalityD1] |
|
308 |
addSEs [bspec RS bspec RS bspec RS mp RS mp]) 1); |
|
309 |
qed "Ord_alt_is_Ord"; |
|
310 |
||
311 |
||
312 |
(**** Ordinal Addition ****) |
|
313 |
||
314 |
(*** Order Type calculations for radd ***) |
|
315 |
||
316 |
(** Addition with 0 **) |
|
317 |
||
318 |
goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)"; |
|
319 |
by (res_inst_tac [("d", "Inl")] lam_bijective 1); |
|
320 |
by (safe_tac sum_cs); |
|
321 |
by (ALLGOALS (asm_simp_tac sum_ss)); |
|
322 |
qed "bij_sum_0"; |
|
323 |
||
324 |
goal OrderType.thy |
|
325 |
"!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"; |
|
326 |
by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1); |
|
327 |
by (assume_tac 2); |
|
984 | 328 |
by (fast_tac (sum_cs addss (sum_ss addsimps [radd_Inl_iff, Memrel_iff])) 1); |
849 | 329 |
qed "ordertype_sum_0_eq"; |
330 |
||
331 |
goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)"; |
|
332 |
by (res_inst_tac [("d", "Inr")] lam_bijective 1); |
|
333 |
by (safe_tac sum_cs); |
|
334 |
by (ALLGOALS (asm_simp_tac sum_ss)); |
|
335 |
qed "bij_0_sum"; |
|
336 |
||
337 |
goal OrderType.thy |
|
338 |
"!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"; |
|
339 |
by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1); |
|
340 |
by (assume_tac 2); |
|
984 | 341 |
by (fast_tac (sum_cs addss (sum_ss addsimps [radd_Inr_iff, Memrel_iff])) 1); |
849 | 342 |
qed "ordertype_0_sum_eq"; |
343 |
||
344 |
(** Initial segments of radd. Statements by Grabczewski **) |
|
345 |
||
346 |
(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *) |
|
347 |
goalw OrderType.thy [pred_def] |
|
348 |
"!!A B. a:A ==> \ |
|
1461 | 349 |
\ (lam x:pred(A,a,r). Inl(x)) \ |
849 | 350 |
\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"; |
351 |
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1); |
|
352 |
by (safe_tac sum_cs); |
|
353 |
by (ALLGOALS |
|
354 |
(asm_full_simp_tac |
|
355 |
(sum_ss addsimps [radd_Inl_iff, radd_Inr_Inl_iff]))); |
|
356 |
qed "pred_Inl_bij"; |
|
357 |
||
358 |
goal OrderType.thy |
|
359 |
"!!A B. [| a:A; well_ord(A,r) |] ==> \ |
|
360 |
\ ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \ |
|
361 |
\ ordertype(pred(A,a,r), r)"; |
|
362 |
by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); |
|
363 |
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset])); |
|
364 |
by (asm_full_simp_tac (ZF_ss addsimps [radd_Inl_iff, pred_def]) 1); |
|
365 |
qed "ordertype_pred_Inl_eq"; |
|
366 |
||
367 |
goalw OrderType.thy [pred_def, id_def] |
|
368 |
"!!A B. b:B ==> \ |
|
1461 | 369 |
\ id(A+pred(B,b,s)) \ |
849 | 370 |
\ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"; |
371 |
by (res_inst_tac [("d", "%z.z")] lam_bijective 1); |
|
372 |
by (safe_tac sum_cs); |
|
373 |
by (ALLGOALS (asm_full_simp_tac radd_ss)); |
|
374 |
qed "pred_Inr_bij"; |
|
375 |
||
376 |
goal OrderType.thy |
|
377 |
"!!A B. [| b:B; well_ord(A,r); well_ord(B,s) |] ==> \ |
|
378 |
\ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \ |
|
379 |
\ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"; |
|
380 |
by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); |
|
984 | 381 |
by (fast_tac (sum_cs addss (radd_ss addsimps [pred_def, id_def])) 2); |
849 | 382 |
by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset])); |
383 |
qed "ordertype_pred_Inr_eq"; |
|
384 |
||
385 |
(*** Basic laws for ordinal addition ***) |
|
386 |
||
387 |
goalw OrderType.thy [oadd_def] |
|
388 |
"!!i j. [| Ord(i); Ord(j) |] ==> Ord(i++j)"; |
|
389 |
by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1)); |
|
390 |
qed "Ord_oadd"; |
|
391 |
||
392 |
(** Ordinal addition with zero **) |
|
393 |
||
394 |
goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> i++0 = i"; |
|
395 |
by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_sum_0_eq, |
|
1461 | 396 |
ordertype_Memrel, well_ord_Memrel]) 1); |
849 | 397 |
qed "oadd_0"; |
398 |
||
399 |
goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> 0++i = i"; |
|
400 |
by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_0_sum_eq, |
|
1461 | 401 |
ordertype_Memrel, well_ord_Memrel]) 1); |
849 | 402 |
qed "oadd_0_left"; |
403 |
||
404 |
||
405 |
(*** Further properties of ordinal addition. Statements by Grabczewski, |
|
406 |
proofs by lcp. ***) |
|
407 |
||
408 |
goalw OrderType.thy [oadd_def] "!!i j k. [| k<i; Ord(j) |] ==> k < i++j"; |
|
1461 | 409 |
by (rtac ltE 1 THEN assume_tac 1); |
410 |
by (rtac ltI 1); |
|
849 | 411 |
by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2)); |
412 |
by (asm_simp_tac |
|
984 | 413 |
(ZF_ss addsimps [ordertype_pred_unfold, |
1461 | 414 |
well_ord_radd, well_ord_Memrel, |
415 |
ordertype_pred_Inl_eq, |
|
416 |
lt_pred_Memrel, leI RS le_ordertype_Memrel] |
|
417 |
setloop rtac (InlI RSN (2,RepFun_eqI))) 1); |
|
849 | 418 |
qed "lt_oadd1"; |
419 |
||
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
420 |
(*Thus also we obtain the rule i++j = k ==> i le k *) |
849 | 421 |
goal OrderType.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i++j"; |
1461 | 422 |
by (rtac all_lt_imp_le 1); |
849 | 423 |
by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1)); |
424 |
qed "oadd_le_self"; |
|
425 |
||
426 |
(** A couple of strange but necessary results! **) |
|
427 |
||
428 |
goal OrderType.thy |
|
429 |
"!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"; |
|
430 |
by (resolve_tac [id_bij RS ord_isoI] 1); |
|
431 |
by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1); |
|
432 |
by (fast_tac ZF_cs 1); |
|
433 |
qed "id_ord_iso_Memrel"; |
|
434 |
||
435 |
goal OrderType.thy |
|
1461 | 436 |
"!!k. [| well_ord(A,r); k<j |] ==> \ |
437 |
\ ordertype(A+k, radd(A, r, k, Memrel(j))) = \ |
|
849 | 438 |
\ ordertype(A+k, radd(A, r, k, Memrel(k)))"; |
1461 | 439 |
by (etac ltE 1); |
849 | 440 |
by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1); |
441 |
by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1); |
|
442 |
by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel])); |
|
443 |
qed "ordertype_sum_Memrel"; |
|
444 |
||
445 |
goalw OrderType.thy [oadd_def] "!!i j k. [| k<j; Ord(i) |] ==> i++k < i++j"; |
|
1461 | 446 |
by (rtac ltE 1 THEN assume_tac 1); |
849 | 447 |
by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1); |
448 |
by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel])); |
|
1461 | 449 |
by (rtac RepFun_eqI 1); |
450 |
by (etac InrI 2); |
|
849 | 451 |
by (asm_simp_tac |
452 |
(ZF_ss addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, |
|
1461 | 453 |
lt_pred_Memrel, leI RS le_ordertype_Memrel, |
454 |
ordertype_sum_Memrel]) 1); |
|
849 | 455 |
qed "oadd_lt_mono2"; |
456 |
||
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
457 |
goal OrderType.thy |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
458 |
"!!i j k. [| i++j < i++k; Ord(i); Ord(j); Ord(k) |] ==> j<k"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
459 |
by (rtac Ord_linear_lt 1); |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
460 |
by (REPEAT_SOME assume_tac); |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
461 |
by (ALLGOALS |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
462 |
(fast_tac (ZF_cs addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym]))); |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
463 |
qed "oadd_lt_cancel2"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
464 |
|
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
465 |
goal OrderType.thy |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
466 |
"!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
467 |
by (fast_tac (ZF_cs addSIs [oadd_lt_mono2] addSEs [oadd_lt_cancel2]) 1); |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
468 |
qed "oadd_lt_iff2"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
469 |
|
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
470 |
goal OrderType.thy |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
471 |
"!!i j k. [| i++j = i++k; Ord(i); Ord(j); Ord(k) |] ==> j=k"; |
849 | 472 |
by (rtac Ord_linear_lt 1); |
473 |
by (REPEAT_SOME assume_tac); |
|
474 |
by (ALLGOALS |
|
984 | 475 |
(fast_tac (ZF_cs addDs [oadd_lt_mono2] |
476 |
addss (ZF_ss addsimps [lt_not_refl])))); |
|
849 | 477 |
qed "oadd_inject"; |
478 |
||
479 |
goalw OrderType.thy [oadd_def] |
|
480 |
"!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> k<i | (EX l:j. k = i++l )"; |
|
481 |
(*Rotate the hypotheses so that simplification will work*) |
|
482 |
by (etac revcut_rl 1); |
|
483 |
by (asm_full_simp_tac |
|
484 |
(ZF_ss addsimps [ordertype_pred_unfold, well_ord_radd, |
|
1461 | 485 |
well_ord_Memrel]) 1); |
849 | 486 |
by (eresolve_tac [ltD RS RepFunE] 1); |
984 | 487 |
by (fast_tac (sum_cs addss |
1461 | 488 |
(ZF_ss addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, |
489 |
ltI, lt_pred_Memrel, le_ordertype_Memrel, leI, |
|
490 |
ordertype_pred_Inr_eq, |
|
491 |
ordertype_sum_Memrel])) 1); |
|
849 | 492 |
qed "lt_oadd_disj"; |
493 |
||
494 |
||
495 |
(*** Ordinal addition with successor -- via associativity! ***) |
|
496 |
||
497 |
goalw OrderType.thy [oadd_def] |
|
498 |
"!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> (i++j)++k = i++(j++k)"; |
|
499 |
by (resolve_tac [ordertype_eq RS trans] 1); |
|
500 |
by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS |
|
1461 | 501 |
sum_ord_iso_cong) 1); |
849 | 502 |
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); |
503 |
by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1); |
|
504 |
by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS |
|
1461 | 505 |
ordertype_eq) 2); |
849 | 506 |
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); |
507 |
qed "oadd_assoc"; |
|
508 |
||
509 |
goal OrderType.thy |
|
510 |
"!!i j. [| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"; |
|
511 |
by (rtac (subsetI RS equalityI) 1); |
|
512 |
by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1); |
|
513 |
by (REPEAT (ares_tac [Ord_oadd] 1)); |
|
984 | 514 |
by (fast_tac (ZF_cs addIs [lt_oadd1, oadd_lt_mono2] |
1461 | 515 |
addss (ZF_ss addsimps [Ord_mem_iff_lt, Ord_oadd])) 3); |
984 | 516 |
by (fast_tac ZF_cs 2); |
849 | 517 |
by (fast_tac (ZF_cs addSEs [ltE]) 1); |
518 |
qed "oadd_unfold"; |
|
519 |
||
520 |
goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)"; |
|
521 |
by (asm_simp_tac (ZF_ss addsimps [oadd_unfold, Ord_1, oadd_0]) 1); |
|
522 |
by (fast_tac eq_cs 1); |
|
523 |
qed "oadd_1"; |
|
524 |
||
467 | 525 |
goal OrderType.thy |
849 | 526 |
"!!i. [| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)"; |
527 |
by (asm_simp_tac |
|
528 |
(ZF_ss addsimps [oadd_1 RS sym, Ord_oadd, oadd_assoc, Ord_1]) 1); |
|
529 |
qed "oadd_succ"; |
|
530 |
||
531 |
||
532 |
(** Ordinal addition with limit ordinals **) |
|
533 |
||
534 |
val prems = goal OrderType.thy |
|
535 |
"[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \ |
|
536 |
\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; |
|
537 |
by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, |
|
1461 | 538 |
lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]) |
849 | 539 |
addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1); |
540 |
qed "oadd_UN"; |
|
541 |
||
542 |
goal OrderType.thy |
|
543 |
"!!i j. [| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)"; |
|
544 |
by (forward_tac [Limit_has_0 RS ltD] 1); |
|
545 |
by (asm_simp_tac (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, |
|
1461 | 546 |
oadd_UN RS sym, Union_eq_UN RS sym, |
547 |
Limit_Union_eq]) 1); |
|
849 | 548 |
qed "oadd_Limit"; |
549 |
||
550 |
(** Order/monotonicity properties of ordinal addition **) |
|
551 |
||
552 |
goal OrderType.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le j++i"; |
|
553 |
by (eres_inst_tac [("i","i")] trans_induct3 1); |
|
554 |
by (asm_simp_tac (ZF_ss addsimps [oadd_0, Ord_0_le]) 1); |
|
555 |
by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_leI]) 1); |
|
556 |
by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1); |
|
1461 | 557 |
by (rtac le_trans 1); |
558 |
by (rtac le_implies_UN_le_UN 2); |
|
849 | 559 |
by (fast_tac ZF_cs 2); |
560 |
by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, |
|
1461 | 561 |
le_refl, Limit_is_Ord]) 1); |
849 | 562 |
qed "oadd_le_self2"; |
563 |
||
564 |
goal OrderType.thy "!!i j k. [| k le j; Ord(i) |] ==> k++i le j++i"; |
|
565 |
by (forward_tac [lt_Ord] 1); |
|
566 |
by (forward_tac [le_Ord2] 1); |
|
1461 | 567 |
by (etac trans_induct3 1); |
849 | 568 |
by (asm_simp_tac (ZF_ss addsimps [oadd_0]) 1); |
569 |
by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_le_iff]) 1); |
|
570 |
by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1); |
|
1461 | 571 |
by (rtac le_implies_UN_le_UN 1); |
849 | 572 |
by (fast_tac ZF_cs 1); |
573 |
qed "oadd_le_mono1"; |
|
574 |
||
575 |
goal OrderType.thy "!!i j. [| i' le i; j'<j |] ==> i'++j' < i++j"; |
|
1461 | 576 |
by (rtac lt_trans1 1); |
849 | 577 |
by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE, |
1461 | 578 |
Ord_succD] 1)); |
849 | 579 |
qed "oadd_lt_mono"; |
580 |
||
581 |
goal OrderType.thy "!!i j. [| i' le i; j' le j |] ==> i'++j' le i++j"; |
|
582 |
by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); |
|
583 |
qed "oadd_le_mono"; |
|
584 |
||
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
585 |
goal OrderType.thy |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
586 |
"!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
587 |
by (asm_simp_tac (ZF_ss addsimps [oadd_lt_iff2, oadd_succ RS sym, |
1461 | 588 |
Ord_succ]) 1); |
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
589 |
qed "oadd_le_iff2"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
590 |
|
849 | 591 |
|
592 |
(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). |
|
593 |
Probably simpler to define the difference recursively! |
|
594 |
**) |
|
595 |
||
596 |
goal OrderType.thy |
|
597 |
"!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"; |
|
598 |
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1); |
|
599 |
by (fast_tac (sum_cs addSIs [if_type]) 1); |
|
600 |
by (fast_tac (ZF_cs addSIs [case_type]) 1); |
|
1461 | 601 |
by (etac sumE 2); |
849 | 602 |
by (ALLGOALS (asm_simp_tac (sum_ss setloop split_tac [expand_if]))); |
603 |
qed "bij_sum_Diff"; |
|
604 |
||
605 |
goal OrderType.thy |
|
1461 | 606 |
"!!i j. i le j ==> \ |
607 |
\ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) = \ |
|
849 | 608 |
\ ordertype(j, Memrel(j))"; |
609 |
by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); |
|
610 |
by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); |
|
1461 | 611 |
by (etac well_ord_Memrel 3); |
849 | 612 |
by (assume_tac 1); |
613 |
by (asm_simp_tac |
|
614 |
(radd_ss setloop split_tac [expand_if] addsimps [Memrel_iff]) 1); |
|
615 |
by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1); |
|
616 |
by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1); |
|
617 |
by (asm_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1); |
|
618 |
by (fast_tac (ZF_cs addEs [lt_trans2, lt_trans]) 1); |
|
619 |
qed "ordertype_sum_Diff"; |
|
620 |
||
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
621 |
goalw OrderType.thy [oadd_def, odiff_def] |
1461 | 622 |
"!!i j. i le j ==> \ |
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
623 |
\ i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"; |
849 | 624 |
by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); |
625 |
by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1); |
|
1461 | 626 |
by (etac id_ord_iso_Memrel 1); |
849 | 627 |
by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); |
628 |
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset, |
|
1461 | 629 |
Diff_subset] 1)); |
849 | 630 |
qed "oadd_ordertype_Diff"; |
631 |
||
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
632 |
goal OrderType.thy "!!i j. i le j ==> i ++ (j--i) = j"; |
849 | 633 |
by (asm_simp_tac (ZF_ss addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, |
1461 | 634 |
ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1); |
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
635 |
qed "oadd_odiff_inverse"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
636 |
|
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
637 |
goalw OrderType.thy [odiff_def] |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
638 |
"!!i j. [| Ord(i); Ord(j) |] ==> Ord(i--j)"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
639 |
by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, |
1461 | 640 |
Diff_subset] 1)); |
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
641 |
qed "Ord_odiff"; |
849 | 642 |
|
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
643 |
(*By oadd_inject, the difference between i and j is unique. Note that we get |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
644 |
i++j = k ==> j = k--i. *) |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
645 |
goal OrderType.thy |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
646 |
"!!i j. [| Ord(i); Ord(j) |] ==> (i++j) -- i = j"; |
1461 | 647 |
by (rtac oadd_inject 1); |
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
648 |
by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2)); |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
649 |
by (asm_simp_tac (ZF_ss addsimps [oadd_odiff_inverse, oadd_le_self]) 1); |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
650 |
qed "odiff_oadd_inverse"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
651 |
|
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
652 |
val [i_lt_j, k_le_i] = goal OrderType.thy |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
653 |
"[| i<j; k le i |] ==> i--k < j--k"; |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
654 |
by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1); |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
655 |
by (simp_tac |
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
656 |
(ZF_ss addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans, |
1461 | 657 |
oadd_odiff_inverse]) 1); |
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
658 |
by (REPEAT (resolve_tac (Ord_odiff :: |
1461 | 659 |
([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1)); |
1032
54b9f670c67e
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp
parents:
984
diff
changeset
|
660 |
qed "odiff_lt_mono2"; |
849 | 661 |
|
662 |
||
663 |
(**** Ordinal Multiplication ****) |
|
664 |
||
665 |
goalw OrderType.thy [omult_def] |
|
666 |
"!!i j. [| Ord(i); Ord(j) |] ==> Ord(i**j)"; |
|
667 |
by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1)); |
|
668 |
qed "Ord_omult"; |
|
669 |
||
670 |
(*** A useful unfolding law ***) |
|
671 |
||
672 |
goalw OrderType.thy [pred_def] |
|
673 |
"!!A B. [| a:A; b:B |] ==> \ |
|
1461 | 674 |
\ pred(A*B, <a,b>, rmult(A,r,B,s)) = \ |
849 | 675 |
\ pred(A,a,r)*B Un ({a} * pred(B,b,s))"; |
676 |
by (safe_tac eq_cs); |
|
677 |
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [rmult_iff]))); |
|
678 |
by (ALLGOALS (fast_tac ZF_cs)); |
|
679 |
qed "pred_Pair_eq"; |
|
680 |
||
681 |
goal OrderType.thy |
|
682 |
"!!A B. [| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \ |
|
683 |
\ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \ |
|
1461 | 684 |
\ ordertype(pred(A,a,r)*B + pred(B,b,s), \ |
849 | 685 |
\ radd(A*B, rmult(A,r,B,s), B, s))"; |
686 |
by (asm_simp_tac (ZF_ss addsimps [pred_Pair_eq]) 1); |
|
687 |
by (resolve_tac [ordertype_eq RS sym] 1); |
|
1461 | 688 |
by (rtac prod_sum_singleton_ord_iso 1); |
984 | 689 |
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset])); |
849 | 690 |
by (fast_tac (ZF_cs addSEs [predE]) 1); |
691 |
qed "ordertype_pred_Pair_eq"; |
|
692 |
||
693 |
goalw OrderType.thy [oadd_def, omult_def] |
|
694 |
"!!i j. [| i'<i; j'<j |] ==> \ |
|
695 |
\ ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \ |
|
696 |
\ rmult(i,Memrel(i),j,Memrel(j))) = \ |
|
697 |
\ j**i' ++ j'"; |
|
984 | 698 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, |
1461 | 699 |
ltD, lt_Ord2, well_ord_Memrel]) 1); |
700 |
by (rtac trans 1); |
|
849 | 701 |
by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2); |
1461 | 702 |
by (rtac ord_iso_refl 3); |
849 | 703 |
by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1); |
704 |
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst])); |
|
705 |
by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, |
|
1461 | 706 |
Ord_ordertype])); |
849 | 707 |
by (ALLGOALS |
708 |
(asm_simp_tac (radd_ss addsimps [rmult_iff, id_conv, Memrel_iff]))); |
|
709 |
by (safe_tac ZF_cs); |
|
710 |
by (ALLGOALS (fast_tac (ZF_cs addEs [Ord_trans]))); |
|
711 |
qed "ordertype_pred_Pair_lemma"; |
|
712 |
||
713 |
goalw OrderType.thy [omult_def] |
|
714 |
"!!i j. [| Ord(i); Ord(j); k<j**i |] ==> \ |
|
715 |
\ EX j' i'. k = j**i' ++ j' & j'<j & i'<i"; |
|
716 |
by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold, |
|
1461 | 717 |
well_ord_rmult, well_ord_Memrel]) 1); |
849 | 718 |
by (step_tac (ZF_cs addSEs [ltE]) 1); |
719 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, |
|
1461 | 720 |
symmetric omult_def]) 1); |
849 | 721 |
by (fast_tac (ZF_cs addIs [ltI]) 1); |
722 |
qed "lt_omult"; |
|
723 |
||
724 |
goalw OrderType.thy [omult_def] |
|
725 |
"!!i j. [| j'<j; i'<i |] ==> j**i' ++ j' < j**i"; |
|
1461 | 726 |
by (rtac ltI 1); |
984 | 727 |
by (asm_simp_tac |
728 |
(ZF_ss addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, |
|
1461 | 729 |
lt_Ord2]) 2); |
984 | 730 |
by (asm_simp_tac |
849 | 731 |
(ZF_ss addsimps [ordertype_pred_unfold, |
1461 | 732 |
well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1); |
733 |
by (rtac RepFun_eqI 1); |
|
849 | 734 |
by (fast_tac (ZF_cs addSEs [ltE]) 2); |
735 |
by (asm_simp_tac |
|
736 |
(ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, symmetric omult_def]) 1); |
|
737 |
qed "omult_oadd_lt"; |
|
738 |
||
739 |
goal OrderType.thy |
|
740 |
"!!i j. [| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"; |
|
741 |
by (rtac (subsetI RS equalityI) 1); |
|
742 |
by (resolve_tac [lt_omult RS exE] 1); |
|
1461 | 743 |
by (etac ltI 3); |
849 | 744 |
by (REPEAT (ares_tac [Ord_omult] 1)); |
745 |
by (fast_tac (ZF_cs addSEs [ltE]) 1); |
|
746 |
by (fast_tac (ZF_cs addIs [omult_oadd_lt RS ltD, ltI]) 1); |
|
747 |
qed "omult_unfold"; |
|
748 |
||
749 |
(*** Basic laws for ordinal multiplication ***) |
|
750 |
||
751 |
(** Ordinal multiplication by zero **) |
|
752 |
||
753 |
goalw OrderType.thy [omult_def] "i**0 = 0"; |
|
754 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1); |
|
755 |
qed "omult_0"; |
|
756 |
||
757 |
goalw OrderType.thy [omult_def] "0**i = 0"; |
|
758 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1); |
|
759 |
qed "omult_0_left"; |
|
760 |
||
761 |
(** Ordinal multiplication by 1 **) |
|
762 |
||
763 |
goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> i**1 = i"; |
|
764 |
by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); |
|
765 |
by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1); |
|
766 |
by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, |
|
1461 | 767 |
well_ord_Memrel, ordertype_Memrel])); |
849 | 768 |
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff]))); |
769 |
qed "omult_1"; |
|
770 |
||
771 |
goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> 1**i = i"; |
|
772 |
by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); |
|
773 |
by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1); |
|
774 |
by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, |
|
1461 | 775 |
well_ord_Memrel, ordertype_Memrel])); |
849 | 776 |
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff]))); |
777 |
qed "omult_1_left"; |
|
778 |
||
779 |
(** Distributive law for ordinal multiplication and addition **) |
|
780 |
||
781 |
goalw OrderType.thy [omult_def, oadd_def] |
|
782 |
"!!i. [| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"; |
|
783 |
by (resolve_tac [ordertype_eq RS trans] 1); |
|
784 |
by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS |
|
1461 | 785 |
prod_ord_iso_cong) 1); |
849 | 786 |
by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, |
1461 | 787 |
Ord_ordertype] 1)); |
849 | 788 |
by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1); |
789 |
by (rtac ordertype_eq 2); |
|
790 |
by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2); |
|
791 |
by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, |
|
1461 | 792 |
Ord_ordertype] 1)); |
849 | 793 |
qed "oadd_omult_distrib"; |
794 |
||
795 |
goal OrderType.thy "!!i. [| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"; |
|
796 |
by (asm_simp_tac |
|
797 |
(ZF_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, Ord_1]) 1); |
|
798 |
qed "omult_succ"; |
|
799 |
||
800 |
(** Associative law **) |
|
801 |
||
802 |
goalw OrderType.thy [omult_def] |
|
803 |
"!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"; |
|
804 |
by (resolve_tac [ordertype_eq RS trans] 1); |
|
805 |
by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS |
|
1461 | 806 |
prod_ord_iso_cong) 1); |
849 | 807 |
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); |
808 |
by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS |
|
1461 | 809 |
ordertype_eq RS trans] 1); |
849 | 810 |
by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS |
1461 | 811 |
ordertype_eq) 2); |
849 | 812 |
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1)); |
813 |
qed "omult_assoc"; |
|
814 |
||
815 |
||
816 |
(** Ordinal multiplication with limit ordinals **) |
|
817 |
||
818 |
val prems = goal OrderType.thy |
|
819 |
"[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \ |
|
820 |
\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"; |
|
821 |
by (asm_simp_tac (ZF_ss addsimps (prems@[Ord_UN, omult_unfold])) 1); |
|
822 |
by (fast_tac eq_cs 1); |
|
823 |
qed "omult_UN"; |
|
467 | 824 |
|
849 | 825 |
goal OrderType.thy |
826 |
"!!i j. [| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)"; |
|
827 |
by (asm_simp_tac |
|
828 |
(ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, |
|
1461 | 829 |
Union_eq_UN RS sym, Limit_Union_eq]) 1); |
849 | 830 |
qed "omult_Limit"; |
831 |
||
832 |
||
833 |
(*** Ordering/monotonicity properties of ordinal multiplication ***) |
|
834 |
||
835 |
(*As a special case we have "[| 0<i; 0<j |] ==> 0 < i**j" *) |
|
836 |
goal OrderType.thy "!!i j. [| k<i; 0<j |] ==> k < i**j"; |
|
837 |
by (safe_tac (ZF_cs addSEs [ltE] addSIs [ltI, Ord_omult])); |
|
838 |
by (asm_simp_tac (ZF_ss addsimps [omult_unfold]) 1); |
|
1461 | 839 |
by (REPEAT (etac UN_I 1)); |
849 | 840 |
by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0_left]) 1); |
841 |
qed "lt_omult1"; |
|
842 |
||
843 |
goal OrderType.thy "!!i j. [| Ord(i); 0<j |] ==> i le i**j"; |
|
1461 | 844 |
by (rtac all_lt_imp_le 1); |
849 | 845 |
by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1)); |
846 |
qed "omult_le_self"; |
|
847 |
||
848 |
goal OrderType.thy "!!i j k. [| k le j; Ord(i) |] ==> k**i le j**i"; |
|
849 |
by (forward_tac [lt_Ord] 1); |
|
850 |
by (forward_tac [le_Ord2] 1); |
|
1461 | 851 |
by (etac trans_induct3 1); |
849 | 852 |
by (asm_simp_tac (ZF_ss addsimps [omult_0, le_refl, Ord_0]) 1); |
853 |
by (asm_simp_tac (ZF_ss addsimps [omult_succ, oadd_le_mono]) 1); |
|
854 |
by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1); |
|
1461 | 855 |
by (rtac le_implies_UN_le_UN 1); |
849 | 856 |
by (fast_tac ZF_cs 1); |
857 |
qed "omult_le_mono1"; |
|
858 |
||
859 |
goal OrderType.thy "!!i j k. [| k<j; 0<i |] ==> i**k < i**j"; |
|
1461 | 860 |
by (rtac ltI 1); |
849 | 861 |
by (asm_simp_tac (ZF_ss addsimps [omult_unfold, lt_Ord2]) 1); |
862 |
by (safe_tac (ZF_cs addSEs [ltE] addSIs [Ord_omult])); |
|
1461 | 863 |
by (REPEAT (etac UN_I 1)); |
849 | 864 |
by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0, Ord_omult]) 1); |
865 |
qed "omult_lt_mono2"; |
|
866 |
||
867 |
goal OrderType.thy "!!i j k. [| k le j; Ord(i) |] ==> i**k le i**j"; |
|
1461 | 868 |
by (rtac subset_imp_le 1); |
849 | 869 |
by (safe_tac (ZF_cs addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult])); |
870 |
by (asm_full_simp_tac (ZF_ss addsimps [omult_unfold]) 1); |
|
984 | 871 |
by (deepen_tac (ZF_cs addEs [Ord_trans, UN_I]) 0 1); |
849 | 872 |
qed "omult_le_mono2"; |
873 |
||
874 |
goal OrderType.thy "!!i j. [| i' le i; j' le j |] ==> i'**j' le i**j"; |
|
1461 | 875 |
by (rtac le_trans 1); |
849 | 876 |
by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE, |
1461 | 877 |
Ord_succD] 1)); |
849 | 878 |
qed "omult_le_mono"; |
879 |
||
880 |
goal OrderType.thy |
|
881 |
"!!i j. [| i' le i; j'<j; 0<i |] ==> i'**j' < i**j"; |
|
1461 | 882 |
by (rtac lt_trans1 1); |
849 | 883 |
by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE, |
1461 | 884 |
Ord_succD] 1)); |
849 | 885 |
qed "omult_lt_mono"; |
886 |
||
887 |
goal OrderType.thy "!!i j. [| Ord(i); 0<j |] ==> i le j**i"; |
|
888 |
by (forward_tac [lt_Ord2] 1); |
|
889 |
by (eres_inst_tac [("i","i")] trans_induct3 1); |
|
890 |
by (asm_simp_tac (ZF_ss addsimps [omult_0, Ord_0 RS le_refl]) 1); |
|
891 |
by (asm_simp_tac (ZF_ss addsimps [omult_succ, succ_le_iff]) 1); |
|
1461 | 892 |
by (etac lt_trans1 1); |
849 | 893 |
by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN |
894 |
rtac oadd_lt_mono2 2); |
|
895 |
by (REPEAT (ares_tac [Ord_omult] 1)); |
|
896 |
by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1); |
|
1461 | 897 |
by (rtac le_trans 1); |
898 |
by (rtac le_implies_UN_le_UN 2); |
|
849 | 899 |
by (fast_tac ZF_cs 2); |
900 |
by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, |
|
1461 | 901 |
Limit_is_Ord RS le_refl]) 1); |
849 | 902 |
qed "omult_le_self2"; |
903 |
||
904 |
||
905 |
(** Further properties of ordinal multiplication **) |
|
906 |
||
907 |
goal OrderType.thy "!!i j. [| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k"; |
|
908 |
by (rtac Ord_linear_lt 1); |
|
909 |
by (REPEAT_SOME assume_tac); |
|
910 |
by (ALLGOALS |
|
984 | 911 |
(fast_tac (ZF_cs addDs [omult_lt_mono2] |
912 |
addss (ZF_ss addsimps [lt_not_refl])))); |
|
849 | 913 |
qed "omult_inject"; |
914 |
||
915 |