author  lcp 
Fri, 16 Dec 1994 18:07:12 +0100  
changeset 803  4c8333ab3eae 
parent 788  8acbe6f3de2b 
child 807  3abd026e68a4 
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 

6 
For OrderType.thy. Order types in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 

10 
open OrderType; 

11 

437  12 
goalw OrderType.thy [ordermap_def,ordertype_def] 
13 
"ordermap(A,r) : A > ordertype(A,r)"; 

14 
by (rtac lam_type 1); 

15 
by (rtac (lamI RS imageI) 1); 

16 
by (REPEAT (assume_tac 1)); 

760  17 
qed "ordermap_type"; 
437  18 

435  19 
(** Unfolding of ordermap **) 
20 

437  21 
(*Useful for cardinality reasoning; see CardinalArith.ML*) 
435  22 
goalw OrderType.thy [ordermap_def, pred_def] 
23 
"!!r. [ wf[A](r); x:A ] ==> \ 

437  24 
\ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"; 
25 
by (asm_simp_tac ZF_ss 1); 

26 
by (etac (wfrec_on RS trans) 1); 

27 
by (assume_tac 1); 

28 
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam, 

29 
vimage_singleton_iff]) 1); 

760  30 
qed "ordermap_eq_image"; 
437  31 

467  32 
(*Useful for rewriting PROVIDED pred is not unfolded until later!*) 
437  33 
goal OrderType.thy 
34 
"!!r. [ wf[A](r); x:A ] ==> \ 

435  35 
\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"; 
437  36 
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
37 
ordermap_type RS image_fun]) 1); 

760  38 
qed "ordermap_pred_unfold"; 
435  39 

40 
(*predunfolded version. NOT suitable for rewriting  loops!*) 

41 
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold; 

42 

43 
(** Showing that ordermap, ordertype yield ordinals **) 

44 

45 
fun ordermap_elim_tac i = 

46 
EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i, 

47 
assume_tac (i+1), 

48 
assume_tac i]; 

49 

50 
goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def] 

51 
"!!r. [ well_ord(A,r); x:A ] ==> Ord(ordermap(A,r) ` x)"; 

52 
by (safe_tac ZF_cs); 

53 
by (wf_on_ind_tac "x" [] 1); 

54 
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1); 

55 
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); 

437  56 
by (rewrite_goals_tac [pred_def,Transset_def]); 
435  57 
by (fast_tac ZF_cs 2); 
58 
by (safe_tac ZF_cs); 

59 
by (ordermap_elim_tac 1); 

60 
by (fast_tac (ZF_cs addSEs [trans_onD]) 1); 

760  61 
qed "Ord_ordermap"; 
435  62 

63 
goalw OrderType.thy [ordertype_def] 

64 
"!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; 

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

66 
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); 

67 
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2); 

437  68 
by (rewrite_goals_tac [Transset_def,well_ord_def]); 
435  69 
by (safe_tac ZF_cs); 
70 
by (ordermap_elim_tac 1); 

71 
by (fast_tac ZF_cs 1); 

760  72 
qed "Ord_ordertype"; 
435  73 

74 
(** ordermap preserves the orderings in both directions **) 

75 

76 
goal OrderType.thy 

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

78 
\ ordermap(A,r)`w : ordermap(A,r)`x"; 

79 
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1); 

437  80 
by (assume_tac 1); 
435  81 
by (fast_tac ZF_cs 1); 
760  82 
qed "ordermap_mono"; 
435  83 

84 
(*linearity of r is crucial here*) 

85 
goalw OrderType.thy [well_ord_def, tot_ord_def] 

86 
"!!r. [ ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ 

87 
\ w: A; x: A ] ==> <w,x>: r"; 

88 
by (safe_tac ZF_cs); 

89 
by (linear_case_tac 1); 

90 
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1); 

467  91 
by (dtac ordermap_mono 1); 
435  92 
by (REPEAT_SOME assume_tac); 
437  93 
by (etac mem_asym 1); 
94 
by (assume_tac 1); 

760  95 
qed "converse_ordermap_mono"; 
435  96 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset

97 
bind_thm ("ordermap_surj", 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset

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

99 
(ordermap_type RS surj_image)); 
435  100 

101 
goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def] 

102 
"!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; 

103 
by (safe_tac ZF_cs); 

437  104 
by (rtac ordermap_type 1); 
105 
by (rtac ordermap_surj 2); 

435  106 
by (linear_case_tac 1); 
107 
(*The two cases yield similar contradictions*) 

467  108 
by (ALLGOALS (dtac ordermap_mono)); 
435  109 
by (REPEAT_SOME assume_tac); 
110 
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl]))); 

760  111 
qed "ordermap_bij"; 
435  112 

113 
goalw OrderType.thy [ord_iso_def] 

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

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

116 
by (safe_tac ZF_cs); 

467  117 
by (rtac ordermap_bij 1); 
437  118 
by (assume_tac 1); 
467  119 
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2); 
437  120 
by (rewtac well_ord_def); 
467  121 
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono, 
435  122 
ordermap_type RS apply_type]) 1); 
760  123 
qed "ordertype_ord_iso"; 
435  124 

125 

126 
(** Unfolding of ordertype **) 

127 

128 
goalw OrderType.thy [ordertype_def] 

129 
"ordertype(A,r) = {ordermap(A,r)`y . y : A}"; 

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

760  131 
qed "ordertype_unfold"; 
467  132 

133 

134 
(** Ordertype of Memrel **) 

135 

136 
(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*) 

137 
goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))"; 

138 
by (rtac well_ordI 1); 

139 
by (rtac (wf_Memrel RS wf_imp_wf_on) 1); 

140 
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1); 

141 
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));; 

142 
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));; 

760  143 
qed "well_ord_Memrel"; 
467  144 

145 
goal OrderType.thy "!!i. [ Ord(i); j:i ] ==> ordermap(i,Memrel(i)) ` j = j"; 

146 
by (eresolve_tac [Ord_induct] 1); 

147 
ba 1; 

148 
by (asm_simp_tac (ZF_ss addsimps 

149 
[well_ord_Memrel RS well_ord_is_wf RS ordermap_pred_unfold]) 1); 

150 
by (asm_simp_tac (ZF_ss addsimps [pred_def, Memrel_iff]) 1); 

151 
by (dresolve_tac [OrdmemD] 1); 

152 
by (assume_tac 1); 

153 
by (fast_tac eq_cs 1); 

760  154 
qed "ordermap_Memrel"; 
467  155 

156 
goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i"; 

157 
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, ordermap_Memrel]) 1); 

760  158 
qed "ordertype_Memrel"; 
467  159 

160 
(** Ordertype of rvimage **) 

161 

162 
goal OrderType.thy 

163 
"!!f. [ f: bij(A,B); well_ord(B,r); x:A ] ==> \ 

164 
\ ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)"; 

165 
by (metacut_tac well_ord_rvimage 1 THEN 

166 
etac bij_is_inj 2 THEN assume_tac 2); 

167 
by (res_inst_tac [("A","A"), ("a","x")] wf_on_induct 1 THEN 

168 
REPEAT (ares_tac [well_ord_is_wf] 1)); 

169 
by (asm_simp_tac 

170 
(bij_inverse_ss addsimps [ordermap_pred_unfold, well_ord_is_wf]) 1); 

171 
by (asm_simp_tac (ZF_ss addsimps [pred_def, rvimage_iff]) 1); 

172 
by (safe_tac eq_cs); 

173 
by (fast_tac bij_apply_cs 1); 

174 
by (res_inst_tac [("a", "converse(f)`xb")] RepFun_eqI 1); 

175 
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); 

760  176 
qed "bij_ordermap_vimage"; 
467  177 

178 
goal OrderType.thy 

179 
"!!f. [ f: bij(A,B); well_ord(B,r) ] ==> \ 

180 
\ ordertype(A,rvimage(A,f,r)) = ordertype(B,r)"; 

181 
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, bij_ordermap_vimage]) 1); 

182 
by (safe_tac eq_cs); 

183 
by (fast_tac bij_apply_cs 1); 

184 
by (res_inst_tac [("a", "converse(f)`xa")] RepFun_eqI 1); 

185 
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); 

760  186 
qed "bij_ordertype_vimage"; 
467  187 

188 

189 
goal OrderType.thy 

190 
"!!r. [ well_ord(A,r); y:A; z: pred(A,y,r) ] ==> \ 

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

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

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

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

195 
by (asm_simp_tac 

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

197 
(*combining these two simplifications LOOPS! *) 

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

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

200 
br (refl RSN (2,RepFun_cong)) 1; 

201 
bd well_ord_is_trans_on 1; 

202 
by (fast_tac (eq_cs addSEs [trans_onD]) 1); 

760  203 
qed "ordermap_pred_eq_ordermap"; 
467  204 

205 

206 
goal OrderType.thy 

207 
"!!r. [ well_ord(A,r); i: ordertype(A,r) ] ==> \ 

208 
\ EX B. B<=A & i = ordertype(B,r)"; 

209 
by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1); 

210 
by (res_inst_tac [("x", "pred(A, converse(ordermap(A,r))`i, r)")] exI 1); 

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

212 
by (asm_simp_tac (ZF_ss addsimps [ordermap_bij RS left_inverse_bij]) 1); 

213 
by (asm_simp_tac (ZF_ss addsimps 

214 
[well_ord_is_wf RS ordermap_pred_unfold]) 1); 

215 
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, 

216 
ordermap_pred_eq_ordermap]) 1); 

760  217 
qed "ordertype_subset"; 
467  218 

771
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

219 

067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

220 
(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

221 
The smaller ordinal is an initial segment of the larger *) 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

222 
goalw OrderType.thy [pred_def, lt_def] 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

223 
"!!i j. j<i ==> j = pred(i, j, Memrel(i))"; 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

224 
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

225 
by (fast_tac (eq_cs addEs [Ord_trans]) 1); 
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
771
diff
changeset

226 
qed "lt_eq_pred"; 
771
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

227 

067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

228 
goal OrderType.thy 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

229 
"!!i. [ j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) \ 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

230 
\ ] ==> R"; 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

231 
by (forward_tac [lt_eq_pred] 1); 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

232 
be ltE 1; 
788
8acbe6f3de2b
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of
lcp
parents:
782
diff
changeset

233 
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN 
8acbe6f3de2b
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of
lcp
parents:
782
diff
changeset

234 
assume_tac 3 THEN assume_tac 1); 
771
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

235 
be subst 1; 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

236 
by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1); 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

237 
(*Combining the two simplifications causes looping*) 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

238 
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

239 
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

240 
addEs [Ord_trans]) 1); 
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
771
diff
changeset

241 
qed "Ord_iso_implies_eq_lemma"; 
771
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

242 

067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

243 
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*) 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

244 
goal OrderType.thy 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

245 
"!!i. [ Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \ 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

246 
\ ] ==> i=j"; 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

247 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); 
067767b0b35e
lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
lcp
parents:
760
diff
changeset

248 
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1)); 
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
771
diff
changeset

249 
qed "Ord_iso_implies_eq"; 