author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2033  639de962ded4 
permissions  rwrr 
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 ZermeloFraenkel 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 
(*predunfolded 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))"; 

119 
by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1); 

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(ji, 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+(BA))"; 

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+(ji), radd(i,Memrel(j),ji,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 ++ (ji) = ordertype(i+(ji), radd(i,Memrel(j),ji,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 ++ (ji) = 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(ij)"; 
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 = ki. *) 
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 ] ==> ik < jk"; 
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 