author  lcp 
Thu, 12 Jan 1995 03:00:38 +0100  
changeset 849  013a16d3addb 
parent 831  60d850cc5fe6 
child 984  4fb1d099ba45 
permissions  rwrr 
435  1 
(* Title: ZF/OrderType.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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, 

22 
[ltI, prem] MRS lt_trans2 RS ltD]) 1); 

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 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

57 
"!!i. [ Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \ 
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, 
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, 

101 
assume_tac (i+1), 

102 
assume_tac i]; 

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 

131 
"!!r. [ <w,x>: r; wf[A](r); w: A; x: A ] ==> \ 

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", 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset

152 
rewrite_rule [symmetric ordertype_def] 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset

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))"; 

157 
by (safe_tac ZF_cs); 

437  158 
by (rtac ordermap_type 1); 
159 
by (rtac ordermap_surj 2); 

435  160 
by (linear_case_tac 1); 
161 
(*The two cases yield similar contradictions*) 

467  162 
by (ALLGOALS (dtac ordermap_mono)); 
435  163 
by (REPEAT_SOME assume_tac); 
164 
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl]))); 

760  165 
qed "ordermap_bij"; 
435  166 

849  167 
(*** Isomorphisms involving ordertype ***) 
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

168 

435  169 
goalw OrderType.thy [ord_iso_def] 
170 
"!!r. well_ord(A,r) ==> \ 

171 
\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; 

172 
by (safe_tac ZF_cs); 

467  173 
by (rtac ordermap_bij 1); 
437  174 
by (assume_tac 1); 
467  175 
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2); 
437  176 
by (rewtac well_ord_def); 
467  177 
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono, 
435  178 
ordermap_type RS apply_type]) 1); 
760  179 
qed "ordertype_ord_iso"; 
435  180 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

181 
goal OrderType.thy 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

182 
"!!f. [ f: ord_iso(A,r,B,s); well_ord(B,s) ] ==> \ 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

183 
\ ordertype(A,r) = ordertype(B,s)"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

184 
by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1); 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

185 
by (resolve_tac [Ord_iso_implies_eq] 1 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

186 
THEN REPEAT (eresolve_tac [Ord_ordertype] 1)); 
831  187 
by (deepen_tac (ZF_cs addIs [ord_iso_trans, ord_iso_sym] 
188 
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

189 
qed "ordertype_eq"; 
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

190 

849  191 
goal OrderType.thy 
192 
"!!A B. [ ordertype(A,r) = ordertype(B,s); \ 

193 
\ well_ord(A,r); well_ord(B,s) \ 

194 
\ ] ==> EX f. f: ord_iso(A,r,B,s)"; 

195 
by (resolve_tac [exI] 1); 

196 
by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1); 

197 
by (assume_tac 1); 

198 
by (eresolve_tac [ssubst] 1); 

199 
by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); 

200 
qed "ordertype_eq_imp_ord_iso"; 

435  201 

849  202 
(*** Basic equalities for ordertype ***) 
467  203 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

204 
(*Ordertype of Memrel*) 
849  205 
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

206 
by (resolve_tac [Ord_iso_implies_eq RS sym] 1); 
849  207 
by (eresolve_tac [ltE] 1); 
208 
by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1)); 

209 
by (resolve_tac [ord_iso_trans] 1); 

210 
by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2); 

211 
by (resolve_tac [id_bij RS ord_isoI] 1); 

212 
by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1); 

213 
by (fast_tac (ZF_cs addEs [ltE, Ord_in_Ord, Ord_trans]) 1); 

214 
qed "le_ordertype_Memrel"; 

215 

216 
(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*) 

217 
bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel); 

467  218 

849  219 
goal OrderType.thy "ordertype(0,r) = 0"; 
220 
by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1); 

221 
by (etac emptyE 1); 

222 
by (resolve_tac [well_ord_0] 1); 

223 
by (resolve_tac [Ord_0 RS ordertype_Memrel] 1); 

224 
qed "ordertype_0"; 

225 

226 
(*Ordertype of rvimage: [ f: bij(A,B); well_ord(B,s) ] ==> 

227 
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

228 
bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq); 
467  229 

849  230 
(*** A fundamental unfolding law for ordertype. ***) 
231 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

232 
(*Ordermap returns the same result if applied to an initial segment*) 
467  233 
goal OrderType.thy 
234 
"!!r. [ well_ord(A,r); y:A; z: pred(A,y,r) ] ==> \ 

235 
\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"; 

236 
by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1); 

237 
by (wf_on_ind_tac "z" [] 1); 

238 
by (safe_tac (ZF_cs addSEs [predE])); 

239 
by (asm_simp_tac 

240 
(ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); 

241 
(*combining these two simplifications LOOPS! *) 

242 
by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1); 

243 
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); 

807  244 
by (rtac (refl RSN (2,RepFun_cong)) 1); 
245 
by (dtac well_ord_is_trans_on 1); 

467  246 
by (fast_tac (eq_cs addSEs [trans_onD]) 1); 
760  247 
qed "ordermap_pred_eq_ordermap"; 
467  248 

849  249 
goalw OrderType.thy [ordertype_def] 
250 
"ordertype(A,r) = {ordermap(A,r)`y . y : A}"; 

251 
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1); 

252 
qed "ordertype_unfold"; 

253 

254 
(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **) 

255 

256 
goal OrderType.thy 

257 
"!!r. [ well_ord(A,r); x:A ] ==> \ 

258 
\ ordertype(pred(A,x,r),r) <= ordertype(A,r)"; 

259 
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, 

260 
pred_subset RSN (2, well_ord_subset)]) 1); 

261 
by (fast_tac (ZF_cs addIs [ordermap_pred_eq_ordermap, RepFun_eqI] 

262 
addEs [predE]) 1); 

263 
qed "ordertype_pred_subset"; 

264 

265 
goal OrderType.thy 

266 
"!!r. [ well_ord(A,r); x:A ] ==> \ 

267 
\ ordertype(pred(A,x,r),r) < ordertype(A,r)"; 

268 
by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1); 

269 
by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1)); 

270 
by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1); 

271 
by (eresolve_tac [well_ord_iso_predE] 3); 

272 
by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1)); 

273 
qed "ordertype_pred_lt"; 

274 

275 
(*May rewrite with this  provided no rules are supplied for proving that 

276 
well_ord(pred(A,x,r), r) *) 

277 
goal OrderType.thy 

278 
"!!A r. well_ord(A,r) ==> \ 

279 
\ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"; 

280 
by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD])); 

281 
by (asm_full_simp_tac 

282 
(ZF_ss addsimps [ordertype_def, 

283 
ordermap_bij RS bij_is_fun RS image_fun]) 1); 

284 
by (eresolve_tac [RepFunE] 1); 

285 
by (asm_full_simp_tac 

286 
(ZF_ss addsimps [well_ord_is_wf, ordermap_eq_image, 

287 
ordermap_type RS image_fun, 

288 
ordermap_pred_eq_ordermap, 

289 
pred_subset, subset_refl]) 1); 

290 
by (eresolve_tac [RepFunI] 1); 

291 
qed "ordertype_pred_unfold"; 

292 

293 

294 
(**** Alternative definition of ordinal ****) 

295 

296 
(*proof by Krzysztof Grabczewski*) 

297 
goalw OrderType.thy [Ord_alt_def] "!!i. Ord(i) ==> Ord_alt(i)"; 

298 
by (resolve_tac [conjI] 1); 

299 
by (eresolve_tac [well_ord_Memrel] 1); 

300 
by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]); 

301 
by (fast_tac eq_cs 1); 

302 
qed "Ord_is_Ord_alt"; 

303 

304 
(*proof by lcp*) 

305 
goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, 

306 
tot_ord_def, part_ord_def, trans_on_def] 

307 
"!!i. Ord_alt(i) ==> Ord(i)"; 

308 
by (asm_full_simp_tac (ZF_ss addsimps [Memrel_iff, pred_Memrel]) 1); 

309 
by (safe_tac ZF_cs); 

310 
by (fast_tac (ZF_cs addSDs [equalityD1]) 1); 

311 
by (subgoal_tac "xa: i" 1); 

312 
by (fast_tac (ZF_cs addSDs [equalityD1]) 2); 

313 
by (fast_tac (ZF_cs addSDs [equalityD1] 

314 
addSEs [bspec RS bspec RS bspec RS mp RS mp]) 1); 

315 
qed "Ord_alt_is_Ord"; 

316 

317 

318 
(**** Ordinal Addition ****) 

319 

320 
(*** Order Type calculations for radd ***) 

321 

322 
(** Addition with 0 **) 

323 

324 
goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)"; 

325 
by (res_inst_tac [("d", "Inl")] lam_bijective 1); 

326 
by (safe_tac sum_cs); 

327 
by (ALLGOALS (asm_simp_tac sum_ss)); 

328 
qed "bij_sum_0"; 

329 

330 
goal OrderType.thy 

331 
"!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"; 

332 
by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1); 

333 
by (assume_tac 2); 

334 
by (asm_simp_tac ZF_ss 1); 

335 
by (REPEAT_FIRST (eresolve_tac [sumE, emptyE])); 

336 
by (asm_simp_tac (sum_ss addsimps [radd_Inl_iff, Memrel_iff]) 1); 

337 
qed "ordertype_sum_0_eq"; 

338 

339 
goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)"; 

340 
by (res_inst_tac [("d", "Inr")] lam_bijective 1); 

341 
by (safe_tac sum_cs); 

342 
by (ALLGOALS (asm_simp_tac sum_ss)); 

343 
qed "bij_0_sum"; 

344 

345 
goal OrderType.thy 

346 
"!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"; 

347 
by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1); 

348 
by (assume_tac 2); 

349 
by (asm_simp_tac ZF_ss 1); 

350 
by (REPEAT_FIRST (eresolve_tac [sumE, emptyE])); 

351 
by (asm_simp_tac (sum_ss addsimps [radd_Inr_iff, Memrel_iff]) 1); 

352 
qed "ordertype_0_sum_eq"; 

353 

354 
(** Initial segments of radd. Statements by Grabczewski **) 

355 

356 
(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *) 

357 
goalw OrderType.thy [pred_def] 

358 
"!!A B. a:A ==> \ 

359 
\ (lam x:pred(A,a,r). Inl(x)) \ 

360 
\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"; 

361 
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1); 

362 
by (safe_tac sum_cs); 

363 
by (ALLGOALS 

364 
(asm_full_simp_tac 

365 
(sum_ss addsimps [radd_Inl_iff, radd_Inr_Inl_iff]))); 

366 
qed "pred_Inl_bij"; 

367 

368 
goal OrderType.thy 

369 
"!!A B. [ a:A; well_ord(A,r) ] ==> \ 

370 
\ ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \ 

371 
\ ordertype(pred(A,a,r), r)"; 

372 
by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); 

373 
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset])); 

374 
by (asm_full_simp_tac (ZF_ss addsimps [radd_Inl_iff, pred_def]) 1); 

375 
qed "ordertype_pred_Inl_eq"; 

376 

377 
goalw OrderType.thy [pred_def, id_def] 

378 
"!!A B. b:B ==> \ 

379 
\ id(A+pred(B,b,s)) \ 

380 
\ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"; 

381 
by (res_inst_tac [("d", "%z.z")] lam_bijective 1); 

382 
by (safe_tac sum_cs); 

383 
by (ALLGOALS (asm_full_simp_tac radd_ss)); 

384 
qed "pred_Inr_bij"; 

385 

386 
goal OrderType.thy 

387 
"!!A B. [ b:B; well_ord(A,r); well_ord(B,s) ] ==> \ 

388 
\ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \ 

389 
\ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"; 

390 
by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); 

391 
by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset])); 

392 
by (asm_full_simp_tac (ZF_ss addsimps [pred_def, id_def]) 1); 

393 
by (REPEAT_FIRST (eresolve_tac [sumE])); 

394 
by (ALLGOALS (asm_simp_tac radd_ss)); 

395 
qed "ordertype_pred_Inr_eq"; 

396 

397 
(*** Basic laws for ordinal addition ***) 

398 

399 
goalw OrderType.thy [oadd_def] 

400 
"!!i j. [ Ord(i); Ord(j) ] ==> Ord(i++j)"; 

401 
by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1)); 

402 
qed "Ord_oadd"; 

403 

404 
(** Ordinal addition with zero **) 

405 

406 
goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> i++0 = i"; 

407 
by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_sum_0_eq, 

408 
ordertype_Memrel, well_ord_Memrel]) 1); 

409 
qed "oadd_0"; 

410 

411 
goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> 0++i = i"; 

412 
by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_0_sum_eq, 

413 
ordertype_Memrel, well_ord_Memrel]) 1); 

414 
qed "oadd_0_left"; 

415 

416 

417 
(*** Further properties of ordinal addition. Statements by Grabczewski, 

418 
proofs by lcp. ***) 

419 

420 
goalw OrderType.thy [oadd_def] "!!i j k. [ k<i; Ord(j) ] ==> k < i++j"; 

421 
by (resolve_tac [ltE] 1 THEN assume_tac 1); 

422 
by (resolve_tac [ltI] 1); 

423 
by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2)); 

424 
by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_unfold, 

425 
well_ord_radd, well_ord_Memrel]) 1); 

426 
by (resolve_tac [RepFun_eqI] 1); 

427 
by (eresolve_tac [InlI] 2); 

428 
by (asm_simp_tac 

429 
(ZF_ss addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 

430 
lt_pred_Memrel, leI RS le_ordertype_Memrel]) 1); 

431 
qed "lt_oadd1"; 

432 

433 
goal OrderType.thy "!!i j. [ Ord(i); Ord(j) ] ==> i le i++j"; 

434 
by (resolve_tac [all_lt_imp_le] 1); 

435 
by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1)); 

436 
qed "oadd_le_self"; 

437 

438 
(** A couple of strange but necessary results! **) 

439 

440 
goal OrderType.thy 

441 
"!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"; 

442 
by (resolve_tac [id_bij RS ord_isoI] 1); 

443 
by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1); 

444 
by (fast_tac ZF_cs 1); 

445 
qed "id_ord_iso_Memrel"; 

446 

447 
goal OrderType.thy 

448 
"!!k. [ well_ord(A,r); k<j ] ==> \ 

449 
\ ordertype(A+k, radd(A, r, k, Memrel(j))) = \ 

450 
\ ordertype(A+k, radd(A, r, k, Memrel(k)))"; 

451 
by (eresolve_tac [ltE] 1); 

452 
by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1); 

453 
by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1); 

454 
by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel])); 

455 
qed "ordertype_sum_Memrel"; 

456 

457 
goalw OrderType.thy [oadd_def] "!!i j k. [ k<j; Ord(i) ] ==> i++k < i++j"; 

458 
by (resolve_tac [ltE] 1 THEN assume_tac 1); 

459 
by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1); 

460 
by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel])); 

461 
by (resolve_tac [RepFun_eqI] 1); 

462 
by (eresolve_tac [InrI] 2); 

463 
by (asm_simp_tac 

464 
(ZF_ss addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 

465 
lt_pred_Memrel, leI RS le_ordertype_Memrel, 

466 
ordertype_sum_Memrel]) 1); 

467 
qed "oadd_lt_mono2"; 

468 

469 
goal OrderType.thy "!!i j. [ i++j = i++k; Ord(i); Ord(j); Ord(k) ] ==> j=k"; 

470 
by (rtac Ord_linear_lt 1); 

471 
by (REPEAT_SOME assume_tac); 

472 
by (ALLGOALS 

473 
(dresolve_tac [oadd_lt_mono2] THEN' assume_tac THEN' 

474 
asm_full_simp_tac (ZF_ss addsimps [lt_not_refl]))); 

475 
qed "oadd_inject"; 

476 

477 
goalw OrderType.thy [oadd_def] 

478 
"!!i j k. [ k < i++j; Ord(i); Ord(j) ] ==> k<i  (EX l:j. k = i++l )"; 

479 
(*Rotate the hypotheses so that simplification will work*) 

480 
by (etac revcut_rl 1); 

481 
by (asm_full_simp_tac 

482 
(ZF_ss addsimps [ordertype_pred_unfold, well_ord_radd, 

483 
well_ord_Memrel]) 1); 

484 
by (eresolve_tac [ltD RS RepFunE] 1); 

485 
by (eresolve_tac [sumE] 1); 

486 
by (asm_simp_tac 

487 
(ZF_ss addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 

488 
ltI, lt_pred_Memrel, le_ordertype_Memrel, leI]) 1); 

489 
by (asm_simp_tac 

490 
(ZF_ss addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 

491 
ltI, lt_pred_Memrel, ordertype_sum_Memrel]) 1); 

492 
by (fast_tac ZF_cs 1); 

493 
qed "lt_oadd_disj"; 

494 

495 

496 
(*** Ordinal addition with successor  via associativity! ***) 

497 

498 
goalw OrderType.thy [oadd_def] 

499 
"!!i j k. [ Ord(i); Ord(j); Ord(k) ] ==> (i++j)++k = i++(j++k)"; 

500 
by (resolve_tac [ordertype_eq RS trans] 1); 

501 
by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 

502 
sum_ord_iso_cong) 1); 

503 
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); 

504 
by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1); 

505 
by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS 

506 
ordertype_eq) 2); 

507 
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); 

508 
qed "oadd_assoc"; 

509 

510 
goal OrderType.thy 

511 
"!!i j. [ Ord(i); Ord(j) ] ==> i++j = i Un (UN k:j. {i++k})"; 

512 
by (rtac (subsetI RS equalityI) 1); 

513 
by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1); 

514 
by (REPEAT (ares_tac [Ord_oadd] 1)); 

515 
by (fast_tac (ZF_cs addSEs [ltE]) 1); 

516 
by (fast_tac ZF_cs 1); 

517 
by (safe_tac ZF_cs); 

518 
by (ALLGOALS 

519 
(asm_full_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, Ord_oadd]))); 

520 
by (fast_tac (ZF_cs addIs [lt_oadd1]) 1); 

521 
by (fast_tac (ZF_cs addIs [oadd_lt_mono2]) 1); 

522 
qed "oadd_unfold"; 

523 

524 
goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)"; 

525 
by (asm_simp_tac (ZF_ss addsimps [oadd_unfold, Ord_1, oadd_0]) 1); 

526 
by (fast_tac eq_cs 1); 

527 
qed "oadd_1"; 

528 

467  529 
goal OrderType.thy 
849  530 
"!!i. [ Ord(i); Ord(j) ] ==> i++succ(j) = succ(i++j)"; 
531 
by (asm_simp_tac 

532 
(ZF_ss addsimps [oadd_1 RS sym, Ord_oadd, oadd_assoc, Ord_1]) 1); 

533 
qed "oadd_succ"; 

534 

535 

536 
(** Ordinal addition with limit ordinals **) 

537 

538 
val prems = goal OrderType.thy 

539 
"[ Ord(i); !!x. x:A ==> Ord(j(x)); a:A ] ==> \ 

540 
\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; 

541 
by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, 

542 
lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]) 

543 
addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1); 

544 
qed "oadd_UN"; 

545 

546 
goal OrderType.thy 

547 
"!!i j. [ Ord(i); Limit(j) ] ==> i++j = (UN k:j. i++k)"; 

548 
by (forward_tac [Limit_has_0 RS ltD] 1); 

549 
by (asm_simp_tac (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, 

550 
oadd_UN RS sym, Union_eq_UN RS sym, 

551 
Limit_Union_eq]) 1); 

552 
qed "oadd_Limit"; 

553 

554 
(** Order/monotonicity properties of ordinal addition **) 

555 

556 
goal OrderType.thy "!!i j. [ Ord(i); Ord(j) ] ==> i le j++i"; 

557 
by (eres_inst_tac [("i","i")] trans_induct3 1); 

558 
by (asm_simp_tac (ZF_ss addsimps [oadd_0, Ord_0_le]) 1); 

559 
by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_leI]) 1); 

560 
by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1); 

561 
by (resolve_tac [le_trans] 1); 

562 
by (resolve_tac [le_implies_UN_le_UN] 2); 

563 
by (fast_tac ZF_cs 2); 

564 
by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 

565 
le_refl, Limit_is_Ord]) 1); 

566 
qed "oadd_le_self2"; 

567 

568 
goal OrderType.thy "!!i j k. [ k le j; Ord(i) ] ==> k++i le j++i"; 

569 
by (forward_tac [lt_Ord] 1); 

570 
by (forward_tac [le_Ord2] 1); 

571 
by (eresolve_tac [trans_induct3] 1); 

572 
by (asm_simp_tac (ZF_ss addsimps [oadd_0]) 1); 

573 
by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_le_iff]) 1); 

574 
by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1); 

575 
by (resolve_tac [le_implies_UN_le_UN] 1); 

576 
by (fast_tac ZF_cs 1); 

577 
qed "oadd_le_mono1"; 

578 

579 
goal OrderType.thy "!!i j. [ i' le i; j'<j ] ==> i'++j' < i++j"; 

580 
by (resolve_tac [lt_trans1] 1); 

581 
by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE, 

582 
Ord_succD] 1)); 

583 
qed "oadd_lt_mono"; 

584 

585 
goal OrderType.thy "!!i j. [ i' le i; j' le j ] ==> i'++j' le i++j"; 

586 
by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); 

587 
qed "oadd_le_mono"; 

588 

589 

590 
(** Ordinal subtraction; the difference is ordertype(ji, Memrel(j)). 

591 
Probably simpler to define the difference recursively! 

592 
**) 

593 

594 
goal OrderType.thy 

595 
"!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(BA))"; 

596 
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1); 

597 
by (fast_tac (sum_cs addSIs [if_type]) 1); 

598 
by (fast_tac (ZF_cs addSIs [case_type]) 1); 

599 
by (eresolve_tac [sumE] 2); 

600 
by (ALLGOALS (asm_simp_tac (sum_ss setloop split_tac [expand_if]))); 

601 
qed "bij_sum_Diff"; 

602 

603 
goal OrderType.thy 

604 
"!!i j. i le j ==> \ 

605 
\ ordertype(i+(ji), radd(i,Memrel(j),ji,Memrel(j))) = \ 

606 
\ ordertype(j, Memrel(j))"; 

607 
by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); 

608 
by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); 

609 
by (eresolve_tac [well_ord_Memrel] 3); 

610 
by (assume_tac 1); 

611 
by (asm_simp_tac 

612 
(radd_ss setloop split_tac [expand_if] addsimps [Memrel_iff]) 1); 

613 
by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1); 

614 
by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1); 

615 
by (asm_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1); 

616 
by (fast_tac (ZF_cs addEs [lt_trans2, lt_trans]) 1); 

617 
qed "ordertype_sum_Diff"; 

618 

619 
goalw OrderType.thy [oadd_def] 

620 
"!!i j. i le j ==> \ 

621 
\ i ++ ordertype(ji, Memrel(j)) = \ 

622 
\ ordertype(i+(ji), radd(i,Memrel(j),ji,Memrel(j)))"; 

623 
by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); 

624 
by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1); 

625 
by (eresolve_tac [id_ord_iso_Memrel] 1); 

626 
by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); 

627 
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset, 

628 
Diff_subset] 1)); 

629 
qed "oadd_ordertype_Diff"; 

630 

631 
goal OrderType.thy 

632 
"!!i j. i le j ==> i ++ ordertype(ji, Memrel(j)) = j"; 

633 
by (asm_simp_tac (ZF_ss addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, 

634 
ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1); 

635 
qed "oadd_inverse"; 

636 

637 
(*By oadd_inject, the difference between i and j is unique.*) 

638 

639 

640 
(**** Ordinal Multiplication ****) 

641 

642 
goalw OrderType.thy [omult_def] 

643 
"!!i j. [ Ord(i); Ord(j) ] ==> Ord(i**j)"; 

644 
by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1)); 

645 
qed "Ord_omult"; 

646 

647 
(*** A useful unfolding law ***) 

648 

649 
goalw OrderType.thy [pred_def] 

650 
"!!A B. [ a:A; b:B ] ==> \ 

651 
\ pred(A*B, <a,b>, rmult(A,r,B,s)) = \ 

652 
\ pred(A,a,r)*B Un ({a} * pred(B,b,s))"; 

653 
by (safe_tac eq_cs); 

654 
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [rmult_iff]))); 

655 
by (ALLGOALS (fast_tac ZF_cs)); 

656 
qed "pred_Pair_eq"; 

657 

658 
goal OrderType.thy 

659 
"!!A B. [ a:A; b:B; well_ord(A,r); well_ord(B,s) ] ==> \ 

660 
\ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \ 

661 
\ ordertype(pred(A,a,r)*B + pred(B,b,s), \ 

662 
\ radd(A*B, rmult(A,r,B,s), B, s))"; 

663 
by (asm_simp_tac (ZF_ss addsimps [pred_Pair_eq]) 1); 

664 
by (resolve_tac [ordertype_eq RS sym] 1); 

665 
by (resolve_tac [prod_sum_singleton_ord_iso] 1); 

666 
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset])); 

667 
by (fast_tac (ZF_cs addSEs [predE]) 1); 

668 
qed "ordertype_pred_Pair_eq"; 

669 

670 
goalw OrderType.thy [oadd_def, omult_def] 

671 
"!!i j. [ i'<i; j'<j ] ==> \ 

672 
\ ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \ 

673 
\ rmult(i,Memrel(i),j,Memrel(j))) = \ 

674 
\ j**i' ++ j'"; 

675 
by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, ltD, lt_Ord2, well_ord_Memrel]) 1); 

676 
by (resolve_tac [trans] 1); 

677 
by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2); 

678 
by (resolve_tac [ord_iso_refl] 3); 

679 
by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1); 

680 
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst])); 

681 
by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 

682 
Ord_ordertype])); 

683 
by (ALLGOALS 

684 
(asm_simp_tac (radd_ss addsimps [rmult_iff, id_conv, Memrel_iff]))); 

685 
by (safe_tac ZF_cs); 

686 
by (ALLGOALS (fast_tac (ZF_cs addEs [Ord_trans]))); 

687 
qed "ordertype_pred_Pair_lemma"; 

688 

689 
goalw OrderType.thy [omult_def] 

690 
"!!i j. [ Ord(i); Ord(j); k<j**i ] ==> \ 

691 
\ EX j' i'. k = j**i' ++ j' & j'<j & i'<i"; 

692 
by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold, 

693 
well_ord_rmult, well_ord_Memrel]) 1); 

694 
by (step_tac (ZF_cs addSEs [ltE]) 1); 

695 
by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, 

696 
symmetric omult_def]) 1); 

697 
by (fast_tac (ZF_cs addIs [ltI]) 1); 

698 
qed "lt_omult"; 

699 

700 
goalw OrderType.thy [omult_def] 

701 
"!!i j. [ j'<j; i'<i ] ==> j**i' ++ j' < j**i"; 

702 
by (resolve_tac [ltI] 1); 

703 
by (asm_full_simp_tac 

704 
(ZF_ss addsimps [ordertype_pred_unfold, 

705 
well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1); 

706 
by (resolve_tac [RepFun_eqI] 1); 

707 
by (fast_tac (ZF_cs addSEs [ltE]) 2); 

708 
by (asm_simp_tac 

709 
(ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, symmetric omult_def]) 1); 

814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset

710 
by (asm_simp_tac 
849  711 
(ZF_ss addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
712 
lt_Ord2]) 1); 

713 
qed "omult_oadd_lt"; 

714 

715 
goal OrderType.thy 

716 
"!!i j. [ Ord(i); Ord(j) ] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"; 

717 
by (rtac (subsetI RS equalityI) 1); 

718 
by (resolve_tac [lt_omult RS exE] 1); 

719 
by (eresolve_tac [ltI] 3); 

720 
by (REPEAT (ares_tac [Ord_omult] 1)); 

721 
by (fast_tac (ZF_cs addSEs [ltE]) 1); 

722 
by (fast_tac (ZF_cs addIs [omult_oadd_lt RS ltD, ltI]) 1); 

723 
qed "omult_unfold"; 

724 

725 
(*** Basic laws for ordinal multiplication ***) 

726 

727 
(** Ordinal multiplication by zero **) 

728 

729 
goalw OrderType.thy [omult_def] "i**0 = 0"; 

730 
by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1); 

731 
qed "omult_0"; 

732 

733 
goalw OrderType.thy [omult_def] "0**i = 0"; 

734 
by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1); 

735 
qed "omult_0_left"; 

736 

737 
(** Ordinal multiplication by 1 **) 

738 

739 
goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> i**1 = i"; 

740 
by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); 

741 
by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1); 

742 
by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, 

743 
well_ord_Memrel, ordertype_Memrel])); 

744 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff]))); 

745 
qed "omult_1"; 

746 

747 
goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> 1**i = i"; 

748 
by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); 

749 
by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1); 

750 
by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, 

751 
well_ord_Memrel, ordertype_Memrel])); 

752 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff]))); 

753 
qed "omult_1_left"; 

754 

755 
(** Distributive law for ordinal multiplication and addition **) 

756 

757 
goalw OrderType.thy [omult_def, oadd_def] 

758 
"!!i. [ Ord(i); Ord(j); Ord(k) ] ==> i**(j++k) = (i**j)++(i**k)"; 

759 
by (resolve_tac [ordertype_eq RS trans] 1); 

760 
by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 

761 
prod_ord_iso_cong) 1); 

762 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 

763 
Ord_ordertype] 1)); 

764 
by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1); 

765 
by (rtac ordertype_eq 2); 

766 
by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2); 

767 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 

768 
Ord_ordertype] 1)); 

769 
qed "oadd_omult_distrib"; 

770 

771 
goal OrderType.thy "!!i. [ Ord(i); Ord(j) ] ==> i**succ(j) = (i**j)++i"; 

772 
by (asm_simp_tac 

773 
(ZF_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, Ord_1]) 1); 

774 
qed "omult_succ"; 

775 

776 
(** Associative law **) 

777 

778 
goalw OrderType.thy [omult_def] 

779 
"!!i j k. [ Ord(i); Ord(j); Ord(k) ] ==> (i**j)**k = i**(j**k)"; 

780 
by (resolve_tac [ordertype_eq RS trans] 1); 

781 
by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS 

782 
prod_ord_iso_cong) 1); 

783 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); 

784 
by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS 

785 
ordertype_eq RS trans] 1); 

786 
by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS 

787 
ordertype_eq) 2); 

788 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1)); 

789 
qed "omult_assoc"; 

790 

791 

792 
(** Ordinal multiplication with limit ordinals **) 

793 

794 
val prems = goal OrderType.thy 

795 
"[ Ord(i); !!x. x:A ==> Ord(j(x)) ] ==> \ 

796 
\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"; 

797 
by (asm_simp_tac (ZF_ss addsimps (prems@[Ord_UN, omult_unfold])) 1); 

798 
by (fast_tac eq_cs 1); 

799 
qed "omult_UN"; 

467  800 

849  801 
goal OrderType.thy 
802 
"!!i j. [ Ord(i); Limit(j) ] ==> i**j = (UN k:j. i**k)"; 

803 
by (asm_simp_tac 

804 
(ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 

805 
Union_eq_UN RS sym, Limit_Union_eq]) 1); 

806 
qed "omult_Limit"; 

807 

808 

809 
(*** Ordering/monotonicity properties of ordinal multiplication ***) 

810 

811 
(*As a special case we have "[ 0<i; 0<j ] ==> 0 < i**j" *) 

812 
goal OrderType.thy "!!i j. [ k<i; 0<j ] ==> k < i**j"; 

813 
by (safe_tac (ZF_cs addSEs [ltE] addSIs [ltI, Ord_omult])); 

814 
by (asm_simp_tac (ZF_ss addsimps [omult_unfold]) 1); 

815 
by (REPEAT (eresolve_tac [UN_I] 1)); 

816 
by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0_left]) 1); 

817 
qed "lt_omult1"; 

818 

819 
goal OrderType.thy "!!i j. [ Ord(i); 0<j ] ==> i le i**j"; 

820 
by (resolve_tac [all_lt_imp_le] 1); 

821 
by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1)); 

822 
qed "omult_le_self"; 

823 

824 
goal OrderType.thy "!!i j k. [ k le j; Ord(i) ] ==> k**i le j**i"; 

825 
by (forward_tac [lt_Ord] 1); 

826 
by (forward_tac [le_Ord2] 1); 

827 
by (eresolve_tac [trans_induct3] 1); 

828 
by (asm_simp_tac (ZF_ss addsimps [omult_0, le_refl, Ord_0]) 1); 

829 
by (asm_simp_tac (ZF_ss addsimps [omult_succ, oadd_le_mono]) 1); 

830 
by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1); 

831 
by (resolve_tac [le_implies_UN_le_UN] 1); 

832 
by (fast_tac ZF_cs 1); 

833 
qed "omult_le_mono1"; 

834 

835 
goal OrderType.thy "!!i j k. [ k<j; 0<i ] ==> i**k < i**j"; 

836 
by (resolve_tac [ltI] 1); 

837 
by (asm_simp_tac (ZF_ss addsimps [omult_unfold, lt_Ord2]) 1); 

838 
by (safe_tac (ZF_cs addSEs [ltE] addSIs [Ord_omult])); 

839 
by (REPEAT (eresolve_tac [UN_I] 1)); 

840 
by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0, Ord_omult]) 1); 

841 
qed "omult_lt_mono2"; 

842 

843 
goal OrderType.thy "!!i j k. [ k le j; Ord(i) ] ==> i**k le i**j"; 

844 
by (resolve_tac [subset_imp_le] 1); 

845 
by (safe_tac (ZF_cs addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult])); 

846 
by (asm_full_simp_tac (ZF_ss addsimps [omult_unfold]) 1); 

847 
by (safe_tac ZF_cs); 

848 
by (eresolve_tac [UN_I] 1); 

849 
by (deepen_tac (ZF_cs addEs [Ord_trans]) 0 1); 

850 
qed "omult_le_mono2"; 

851 

852 
goal OrderType.thy "!!i j. [ i' le i; j' le j ] ==> i'**j' le i**j"; 

853 
by (resolve_tac [le_trans] 1); 

854 
by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE, 

855 
Ord_succD] 1)); 

856 
qed "omult_le_mono"; 

857 

858 
goal OrderType.thy 

859 
"!!i j. [ i' le i; j'<j; 0<i ] ==> i'**j' < i**j"; 

860 
by (resolve_tac [lt_trans1] 1); 

861 
by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE, 

862 
Ord_succD] 1)); 

863 
qed "omult_lt_mono"; 

864 

865 
goal OrderType.thy 

866 
"!!i j. [ i' le i; j' le j ] ==> i'++j' le i++j"; 

867 
by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); 

868 
qed "oadd_le_mono"; 

869 

870 
goal OrderType.thy "!!i j. [ Ord(i); 0<j ] ==> i le j**i"; 

871 
by (forward_tac [lt_Ord2] 1); 

872 
by (eres_inst_tac [("i","i")] trans_induct3 1); 

873 
by (asm_simp_tac (ZF_ss addsimps [omult_0, Ord_0 RS le_refl]) 1); 

874 
by (asm_simp_tac (ZF_ss addsimps [omult_succ, succ_le_iff]) 1); 

875 
by (eresolve_tac [lt_trans1] 1); 

876 
by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 

877 
rtac oadd_lt_mono2 2); 

878 
by (REPEAT (ares_tac [Ord_omult] 1)); 

879 
by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1); 

880 
by (resolve_tac [le_trans] 1); 

881 
by (resolve_tac [le_implies_UN_le_UN] 2); 

882 
by (fast_tac ZF_cs 2); 

883 
by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, 

884 
Limit_is_Ord RS le_refl]) 1); 

885 
qed "omult_le_self2"; 

886 

887 

888 
(** Further properties of ordinal multiplication **) 

889 

890 
goal OrderType.thy "!!i j. [ i**j = i**k; 0<i; Ord(j); Ord(k) ] ==> j=k"; 

891 
by (rtac Ord_linear_lt 1); 

892 
by (REPEAT_SOME assume_tac); 

893 
by (ALLGOALS 

894 
(dresolve_tac [omult_lt_mono2] THEN' assume_tac THEN' 

895 
asm_full_simp_tac (ZF_ss addsimps [lt_not_refl]))); 

896 
qed "omult_inject"; 

897 

898 