author  wenzelm 
Sat, 17 Oct 2009 14:43:18 +0200  
changeset 32960  69916a850301 
parent 21404  eb85850d3eb7 
child 46823  57bf0cecb366 
permissions  rwrr 
13634  1 
(* Title: ZF/Constructible/Rank.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

5 
header {*Absoluteness for Order Types, Rank Functions and WellFounded 

6 
Relations*} 

7 

16417  8 
theory Rank imports WF_absolute begin 
13634  9 

10 
subsection {*Order Types: A Direct Construction by Replacement*} 

11 

12 
locale M_ordertype = M_basic + 

13 
assumes well_ord_iso_separation: 

14 
"[ M(A); M(f); M(r) ] 

15 
==> separation (M, \<lambda>x. x\<in>A > (\<exists>y[M]. (\<exists>p[M]. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

16 
fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))" 
13634  17 
and obase_separation: 
18 
{*part of the order type formalization*} 

19 
"[ M(A); M(r) ] 

20 
==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

21 
ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

22 
order_isomorphism(M,par,r,x,mx,g))" 
13634  23 
and obase_equals_separation: 
24 
"[ M(A); M(r) ] 

25 
==> separation (M, \<lambda>x. x\<in>A > ~(\<exists>y[M]. \<exists>g[M]. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

26 
ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

27 
membership(M,y,my) & pred_set(M,A,x,r,pxr) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

28 
order_isomorphism(M,pxr,r,y,my,g))))" 
13634  29 
and omap_replacement: 
30 
"[ M(A); M(r) ] 

31 
==> strong_replacement(M, 

32 
\<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

33 
ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

34 
pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" 
13634  35 

36 

37 
text{*Inductive argument for Kunen's Lemma I 6.1, etc. 

38 
Simple proof from Halmos, page 72*} 

39 
lemma (in M_ordertype) wellordered_iso_subset_lemma: 

40 
"[ wellordered(M,A,r); f \<in> ord_iso(A,r, A',r); A'<= A; y \<in> A; 

41 
M(A); M(f); M(r) ] ==> ~ <f`y, y> \<in> r" 

42 
apply (unfold wellordered_def ord_iso_def) 

43 
apply (elim conjE CollectE) 

44 
apply (erule wellfounded_on_induct, assumption+) 

45 
apply (insert well_ord_iso_separation [of A f r]) 

46 
apply (simp, clarify) 

47 
apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast) 

48 
done 

49 

50 

51 
text{*Kunen's Lemma I 6.1, page 14: 

52 
there's no orderisomorphism to an initial segment of a wellordering*} 

53 
lemma (in M_ordertype) wellordered_iso_predD: 

54 
"[ wellordered(M,A,r); f \<in> ord_iso(A, r, Order.pred(A,x,r), r); 

55 
M(A); M(f); M(r) ] ==> x \<notin> A" 

56 
apply (rule notI) 

57 
apply (frule wellordered_iso_subset_lemma, assumption) 

58 
apply (auto elim: predE) 

59 
(*Now we know ~ (f`x < x) *) 

60 
apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 

61 
(*Now we also know f`x \<in> pred(A,x,r); contradiction! *) 

62 
apply (simp add: Order.pred_def) 

63 
done 

64 

65 

66 
lemma (in M_ordertype) wellordered_iso_pred_eq_lemma: 

67 
"[ f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>; 

68 
wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) ] ==> <x,y> \<notin> r" 

69 
apply (frule wellordered_is_trans_on, assumption) 

70 
apply (rule notI) 

71 
apply (drule_tac x2=y and x=x and r2=r in 

72 
wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) 

73 
apply (simp add: trans_pred_pred_eq) 

74 
apply (blast intro: predI dest: transM)+ 

75 
done 

76 

77 

78 
text{*Simple consequence of Lemma 6.1*} 

79 
lemma (in M_ordertype) wellordered_iso_pred_eq: 

80 
"[ wellordered(M,A,r); 

81 
f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r); 

82 
M(A); M(f); M(r); a\<in>A; c\<in>A ] ==> a=c" 

83 
apply (frule wellordered_is_trans_on, assumption) 

84 
apply (frule wellordered_is_linear, assumption) 

85 
apply (erule_tac x=a and y=c in linearE, auto) 

86 
apply (drule ord_iso_sym) 

87 
(*two symmetric cases*) 

88 
apply (blast dest: wellordered_iso_pred_eq_lemma)+ 

89 
done 

90 

91 

92 
text{*Following Kunen's Theorem I 7.6, page 17. Note that this material is 

93 
not required elsewhere.*} 

94 

95 
text{*Can't use @{text well_ord_iso_preserving} because it needs the 

96 
strong premise @{term "well_ord(A,r)"}*} 

97 
lemma (in M_ordertype) ord_iso_pred_imp_lt: 

98 
"[ f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i)); 

99 
g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); 

100 
wellordered(M,A,r); x \<in> A; y \<in> A; M(A); M(r); M(f); M(g); M(j); 

101 
Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r ] 

102 
==> i < j" 

103 
apply (frule wellordered_is_trans_on, assumption) 

104 
apply (frule_tac y=y in transM, assumption) 

105 
apply (rule_tac i=i and j=j in Ord_linear_lt, auto) 

106 
txt{*case @{term "i=j"} yields a contradiction*} 

107 
apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in 

108 
wellordered_iso_predD [THEN notE]) 

109 
apply (blast intro: wellordered_subset [OF _ pred_subset]) 

110 
apply (simp add: trans_pred_pred_eq) 

111 
apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 

112 
apply (simp_all add: pred_iff pred_closed converse_closed comp_closed) 

113 
txt{*case @{term "j<i"} also yields a contradiction*} 

114 
apply (frule restrict_ord_iso2, assumption+) 

115 
apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 

116 
apply (frule apply_type, blast intro: ltD) 

117 
{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*} 

118 
apply (simp add: pred_iff) 

119 
apply (subgoal_tac 

120 
"\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r, 

121 
Order.pred(A, converse(f)`j, r), r)") 

122 
apply (clarify, frule wellordered_iso_pred_eq, assumption+) 

123 
apply (blast dest: wellordered_asym) 

124 
apply (intro rexI) 

125 
apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+ 

126 
done 

127 

128 

129 
lemma ord_iso_converse1: 

130 
"[ f: ord_iso(A,r,B,s); <b, f`a>: s; a:A; b:B ] 

13721  131 
==> <converse(f) ` b, a> \<in> r" 
13634  132 
apply (frule ord_iso_converse, assumption+) 
133 
apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) 

134 
apply (simp add: left_inverse_bij [OF ord_iso_is_bij]) 

135 
done 

136 

137 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

138 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

139 
obase :: "[i=>o,i,i] => i" where 
13634  140 
{*the domain of @{text om}, eventually shown to equal @{text A}*} 
141 
"obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 

142 
g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}" 

143 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

144 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

145 
omap :: "[i=>o,i,i,i] => o" where 
13634  146 
{*the function that maps wosets to order types*} 
147 
"omap(M,A,r,f) == 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

148 
\<forall>z[M]. 
13634  149 
z \<in> f <> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
150 
g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" 

151 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

152 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

153 
otype :: "[i=>o,i,i,i] => o" where {*the order types themselves*} 
13634  154 
"otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)" 
155 

156 

157 
text{*Can also be proved with the premise @{term "M(z)"} instead of 

158 
@{term "M(f)"}, but that version is less useful. This lemma 

159 
is also more useful than the definition, @{text omap_def}.*} 

160 
lemma (in M_ordertype) omap_iff: 

161 
"[ omap(M,A,r,f); M(A); M(f) ] 

162 
==> z \<in> f <> 

163 
(\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 

164 
g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" 

165 
apply (simp add: omap_def Memrel_closed pred_closed) 

166 
apply (rule iffI) 

167 
apply (drule_tac [2] x=z in rspec) 

168 
apply (drule_tac x=z in rspec) 

169 
apply (blast dest: transM)+ 

170 
done 

171 

172 
lemma (in M_ordertype) omap_unique: 

173 
"[ omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') ] ==> f' = f" 

174 
apply (rule equality_iffI) 

175 
apply (simp add: omap_iff) 

176 
done 

177 

178 
lemma (in M_ordertype) omap_yields_Ord: 

179 
"[ omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) ] ==> Ord(x)" 

180 
by (simp add: omap_def) 

181 

182 
lemma (in M_ordertype) otype_iff: 

183 
"[ otype(M,A,r,i); M(A); M(r); M(i) ] 

184 
==> x \<in> i <> 

185 
(M(x) & Ord(x) & 

186 
(\<exists>a\<in>A. \<exists>g[M]. g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))" 

187 
apply (auto simp add: omap_iff otype_def) 

188 
apply (blast intro: transM) 

189 
apply (rule rangeI) 

190 
apply (frule transM, assumption) 

191 
apply (simp add: omap_iff, blast) 

192 
done 

193 

194 
lemma (in M_ordertype) otype_eq_range: 

195 
"[ omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) ] 

196 
==> i = range(f)" 

197 
apply (auto simp add: otype_def omap_iff) 

198 
apply (blast dest: omap_unique) 

199 
done 

200 

201 

202 
lemma (in M_ordertype) Ord_otype: 

203 
"[ otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) ] ==> Ord(i)" 

204 
apply (rule OrdI) 

205 
prefer 2 

206 
apply (simp add: Ord_def otype_def omap_def) 

207 
apply clarify 

208 
apply (frule pair_components_in_M, assumption) 

209 
apply blast 

210 
apply (auto simp add: Transset_def otype_iff) 

211 
apply (blast intro: transM) 

212 
apply (blast intro: Ord_in_Ord) 

213 
apply (rename_tac y a g) 

214 
apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

215 
THEN apply_funtype], assumption) 
13634  216 
apply (rule_tac x="converse(g)`y" in bexI) 
217 
apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) 

218 
apply (safe elim!: predE) 

219 
apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM) 

220 
done 

221 

222 
lemma (in M_ordertype) domain_omap: 

223 
"[ omap(M,A,r,f); M(A); M(r); M(B); M(f) ] 

224 
==> domain(f) = obase(M,A,r)" 

225 
apply (simp add: domain_closed obase_def) 

226 
apply (rule equality_iffI) 

227 
apply (simp add: domain_iff omap_iff, blast) 

228 
done 

229 

230 
lemma (in M_ordertype) omap_subset: 

231 
"[ omap(M,A,r,f); otype(M,A,r,i); 

232 
M(A); M(r); M(f); M(B); M(i) ] ==> f \<subseteq> obase(M,A,r) * i" 

233 
apply clarify 

234 
apply (simp add: omap_iff obase_def) 

235 
apply (force simp add: otype_iff) 

236 
done 

237 

238 
lemma (in M_ordertype) omap_funtype: 

239 
"[ omap(M,A,r,f); otype(M,A,r,i); 

240 
M(A); M(r); M(f); M(i) ] ==> f \<in> obase(M,A,r) > i" 

241 
apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) 

242 
apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 

243 
done 

244 

245 

246 
lemma (in M_ordertype) wellordered_omap_bij: 

247 
"[ wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 

248 
M(A); M(r); M(f); M(i) ] ==> f \<in> bij(obase(M,A,r),i)" 

249 
apply (insert omap_funtype [of A r f i]) 

250 
apply (auto simp add: bij_def inj_def) 

251 
prefer 2 apply (blast intro: fun_is_surj dest: otype_eq_range) 

252 
apply (frule_tac a=w in apply_Pair, assumption) 

253 
apply (frule_tac a=x in apply_Pair, assumption) 

254 
apply (simp add: omap_iff) 

255 
apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) 

256 
done 

257 

258 

259 
text{*This is not the final result: we must show @{term "oB(A,r) = A"}*} 

260 
lemma (in M_ordertype) omap_ord_iso: 

261 
"[ wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 

262 
M(A); M(r); M(f); M(i) ] ==> f \<in> ord_iso(obase(M,A,r),r,i,Memrel(i))" 

263 
apply (rule ord_isoI) 

264 
apply (erule wellordered_omap_bij, assumption+) 

265 
apply (insert omap_funtype [of A r f i], simp) 

266 
apply (frule_tac a=x in apply_Pair, assumption) 

267 
apply (frule_tac a=y in apply_Pair, assumption) 

268 
apply (auto simp add: omap_iff) 

269 
txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*} 

270 
apply (blast intro: ltD ord_iso_pred_imp_lt) 

271 
txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*} 

272 
apply (rename_tac x y g ga) 

273 
apply (frule wellordered_is_linear, assumption, 

274 
erule_tac x=x and y=y in linearE, assumption+) 

275 
txt{*the case @{term "x=y"} leads to immediate contradiction*} 

276 
apply (blast elim: mem_irrefl) 

277 
txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*} 

278 
apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) 

279 
done 

280 

281 
lemma (in M_ordertype) Ord_omap_image_pred: 

282 
"[ wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 

283 
M(A); M(r); M(f); M(i); b \<in> A ] ==> Ord(f `` Order.pred(A,b,r))" 

284 
apply (frule wellordered_is_trans_on, assumption) 

285 
apply (rule OrdI) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

286 
prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) 
13634  287 
txt{*Hard part is to show that the image is a transitive set.*} 
288 
apply (simp add: Transset_def, clarify) 

289 
apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f i]]) 

290 
apply (rename_tac c j, clarify) 

291 
apply (frule omap_funtype [of A r f, THEN apply_funtype], assumption+) 

13721  292 
apply (subgoal_tac "j \<in> i") 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

293 
prefer 2 apply (blast intro: Ord_trans Ord_otype) 
13721  294 
apply (subgoal_tac "converse(f) ` j \<in> obase(M,A,r)") 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

295 
prefer 2 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

296 
apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, 
13634  297 
THEN bij_is_fun, THEN apply_funtype]) 
298 
apply (rule_tac x="converse(f) ` j" in bexI) 

299 
apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) 

300 
apply (intro predI conjI) 

301 
apply (erule_tac b=c in trans_onD) 

302 
apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f i]]) 

303 
apply (auto simp add: obase_def) 

304 
done 

305 

306 
lemma (in M_ordertype) restrict_omap_ord_iso: 

307 
"[ wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 

308 
D \<subseteq> obase(M,A,r); M(A); M(r); M(f); M(i) ] 

309 
==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)" 

310 
apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f i]], 

311 
assumption+) 

312 
apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) 

313 
apply (blast dest: subsetD [OF omap_subset]) 

314 
apply (drule ord_iso_sym, simp) 

315 
done 

316 

317 
lemma (in M_ordertype) obase_equals: 

318 
"[ wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 

319 
M(A); M(r); M(f); M(i) ] ==> obase(M,A,r) = A" 

320 
apply (rule equalityI, force simp add: obase_def, clarify) 

321 
apply (unfold obase_def, simp) 

322 
apply (frule wellordered_is_wellfounded_on, assumption) 

323 
apply (erule wellfounded_on_induct, assumption+) 

324 
apply (frule obase_equals_separation [of A r], assumption) 

325 
apply (simp, clarify) 

326 
apply (rename_tac b) 

327 
apply (subgoal_tac "Order.pred(A,b,r) <= obase(M,A,r)") 

328 
apply (blast intro!: restrict_omap_ord_iso Ord_omap_image_pred) 

329 
apply (force simp add: pred_iff obase_def) 

330 
done 

331 

332 

333 

334 
text{*Main result: @{term om} gives the orderisomorphism 

335 
@{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *} 

336 
theorem (in M_ordertype) omap_ord_iso_otype: 

337 
"[ wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 

338 
M(A); M(r); M(f); M(i) ] ==> f \<in> ord_iso(A, r, i, Memrel(i))" 

339 
apply (frule omap_ord_iso, assumption+) 

340 
apply (simp add: obase_equals) 

341 
done 

342 

343 
lemma (in M_ordertype) obase_exists: 

344 
"[ M(A); M(r) ] ==> M(obase(M,A,r))" 

345 
apply (simp add: obase_def) 

346 
apply (insert obase_separation [of A r]) 

347 
apply (simp add: separation_def) 

348 
done 

349 

350 
lemma (in M_ordertype) omap_exists: 

351 
"[ M(A); M(r) ] ==> \<exists>z[M]. omap(M,A,r,z)" 

352 
apply (simp add: omap_def) 

353 
apply (insert omap_replacement [of A r]) 

354 
apply (simp add: strong_replacement_def) 

355 
apply (drule_tac x="obase(M,A,r)" in rspec) 

356 
apply (simp add: obase_exists) 

357 
apply (simp add: Memrel_closed pred_closed obase_def) 

358 
apply (erule impE) 

359 
apply (clarsimp simp add: univalent_def) 

360 
apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify) 

361 
apply (rule_tac x=Y in rexI) 

362 
apply (simp add: Memrel_closed pred_closed obase_def, blast, assumption) 

363 
done 

364 

365 
declare rall_simps [simp] rex_simps [simp] 

366 

367 
lemma (in M_ordertype) otype_exists: 

368 
"[ wellordered(M,A,r); M(A); M(r) ] ==> \<exists>i[M]. otype(M,A,r,i)" 

369 
apply (insert omap_exists [of A r]) 

370 
apply (simp add: otype_def, safe) 

371 
apply (rule_tac x="range(x)" in rexI) 

372 
apply blast+ 

373 
done 

374 

375 
lemma (in M_ordertype) ordertype_exists: 

376 
"[ wellordered(M,A,r); M(A); M(r) ] 

377 
==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))" 

378 
apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) 

379 
apply (rename_tac i) 

380 
apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 

381 
apply (rule Ord_otype) 

382 
apply (force simp add: otype_def range_closed) 

383 
apply (simp_all add: wellordered_is_trans_on) 

384 
done 

385 

386 

387 
lemma (in M_ordertype) relativized_imp_well_ord: 

388 
"[ wellordered(M,A,r); M(A); M(r) ] ==> well_ord(A,r)" 

389 
apply (insert ordertype_exists [of A r], simp) 

390 
apply (blast intro: well_ord_ord_iso well_ord_Memrel) 

391 
done 

392 

393 
subsection {*Kunen's theorem 5.4, page 127*} 

394 

395 
text{*(a) The notion of Wellordering is absolute*} 

396 
theorem (in M_ordertype) well_ord_abs [simp]: 

397 
"[ M(A); M(r) ] ==> wellordered(M,A,r) <> well_ord(A,r)" 

398 
by (blast intro: well_ord_imp_relativized relativized_imp_well_ord) 

399 

400 

401 
text{*(b) Order types are absolute*} 

402 
theorem (in M_ordertype) 

403 
"[ wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i)); 

404 
M(A); M(r); M(f); M(i); Ord(i) ] ==> i = ordertype(A,r)" 

405 
by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso 

406 
Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 

407 

408 

409 
subsection{*Ordinal Arithmetic: Two Examples of Recursion*} 

410 

411 
text{*Note: the remainder of this theory is not needed elsewhere.*} 

412 

413 
subsubsection{*Ordinal Addition*} 

414 

415 
(*FIXME: update to use new techniques!!*) 

416 
(*This expresses ordinal addition in the language of ZF. It also 

417 
provides an abbreviation that can be used in the instance of strong 

418 
replacement below. Here j is used to define the relation, namely 

419 
Memrel(succ(j)), while x determines the domain of f.*) 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

420 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

421 
is_oadd_fun :: "[i=>o,i,i,i,i] => o" where 
13634  422 
"is_oadd_fun(M,i,j,x,f) == 
423 
(\<forall>sj msj. M(sj) > M(msj) > 

424 
successor(M,j,sj) > membership(M,sj,msj) > 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

425 
M_is_recfun(M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

426 
%x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

427 
msj, x, f))" 
13634  428 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

429 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

430 
is_oadd :: "[i=>o,i,i,i] => o" where 
13634  431 
"is_oadd(M,i,j,k) == 
432 
(~ ordinal(M,i) & ~ ordinal(M,j) & k=0)  

433 
(~ ordinal(M,i) & ordinal(M,j) & k=j)  

434 
(ordinal(M,i) & ~ ordinal(M,j) & k=i)  

435 
(ordinal(M,i) & ordinal(M,j) & 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

436 
(\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

437 
successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

438 
fun_apply(M,f,j,fj) & fj = k))" 
13634  439 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

440 
definition 
13634  441 
(*NEEDS RELATIVIZATION*) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

442 
omult_eqns :: "[i,i,i,i] => o" where 
13634  443 
"omult_eqns(i,x,g,z) == 
444 
Ord(x) & 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

445 
(x=0 > z=0) & 
13634  446 
(\<forall>j. x = succ(j) > z = g`j ++ i) & 
447 
(Limit(x) > z = \<Union>(g``x))" 

448 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

449 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

450 
is_omult_fun :: "[i=>o,i,i,i] => o" where 
13634  451 
"is_omult_fun(M,i,j,f) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

452 
(\<exists>df. M(df) & is_function(M,f) & 
13634  453 
is_domain(M,f,df) & subset(M, j, df)) & 
454 
(\<forall>x\<in>j. omult_eqns(i,x,f,f`x))" 

455 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

456 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

457 
is_omult :: "[i=>o,i,i,i] => o" where 
13634  458 
"is_omult(M,i,j,k) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

459 
\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
13634  460 
successor(M,j,sj) & is_omult_fun(M,i,sj,f) & 
461 
fun_apply(M,f,j,fj) & fj = k" 

462 

463 

464 
locale M_ord_arith = M_ordertype + 

465 
assumes oadd_strong_replacement: 

466 
"[ M(i); M(j) ] ==> 

467 
strong_replacement(M, 

468 
\<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & 

469 
(\<exists>f[M]. \<exists>fx[M]. is_oadd_fun(M,i,j,x,f) & 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

470 
image(M,f,x,fx) & y = i Un fx))" 
13634  471 

472 
and omult_strong_replacement': 

473 
"[ M(i); M(j) ] ==> 

474 
strong_replacement(M, 

475 
\<lambda>x z. \<exists>y[M]. z = <x,y> & 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

476 
(\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

477 
y = (THE z. omult_eqns(i, x, g, z))))" 
13634  478 

479 

480 

481 
text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*} 

482 
lemma (in M_ord_arith) is_oadd_fun_iff: 

483 
"[ a\<le>j; M(i); M(j); M(a); M(f) ] 

484 
==> is_oadd_fun(M,i,j,a,f) <> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

485 
f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) > x < a > f`x = i Un f``x)" 
13634  486 
apply (frule lt_Ord) 
487 
apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 

488 
relation2_def is_recfun_abs [of "%x g. i Un g``x"] 

489 
image_closed is_recfun_iff_equation 

490 
Ball_def lt_trans [OF ltI, of _ a] lt_Memrel) 

491 
apply (simp add: lt_def) 

492 
apply (blast dest: transM) 

493 
done 

494 

495 

496 
lemma (in M_ord_arith) oadd_strong_replacement': 

497 
"[ M(i); M(j) ] ==> 

498 
strong_replacement(M, 

499 
\<lambda>x z. \<exists>y[M]. z = <x,y> & 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

500 
(\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

501 
y = i Un g``x))" 
13634  502 
apply (insert oadd_strong_replacement [of i j]) 
503 
apply (simp add: is_oadd_fun_def relation2_def 

504 
is_recfun_abs [of "%x g. i Un g``x"]) 

505 
done 

506 

507 

508 
lemma (in M_ord_arith) exists_oadd: 

509 
"[ Ord(j); M(i); M(j) ] 

510 
==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)" 

511 
apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) 

512 
apply (simp_all add: Memrel_type oadd_strong_replacement') 

513 
done 

514 

515 
lemma (in M_ord_arith) exists_oadd_fun: 

516 
"[ Ord(j); M(i); M(j) ] ==> \<exists>f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)" 

517 
apply (rule exists_oadd [THEN rexE]) 

518 
apply (erule Ord_succ, assumption, simp) 

519 
apply (rename_tac f) 

520 
apply (frule is_recfun_type) 

521 
apply (rule_tac x=f in rexI) 

522 
apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def 

523 
is_oadd_fun_iff Ord_trans [OF _ succI1], assumption) 

524 
done 

525 

526 
lemma (in M_ord_arith) is_oadd_fun_apply: 

527 
"[ x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) ] 

528 
==> f`x = i Un (\<Union>k\<in>x. {f ` k})" 

529 
apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) 

530 
apply (frule lt_closed, simp) 

531 
apply (frule leI [THEN le_imp_subset]) 

532 
apply (simp add: image_fun, blast) 

533 
done 

534 

535 
lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]: 

536 
"[ is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) ] 

537 
==> j<J > f`j = i++j" 

538 
apply (erule_tac i=j in trans_induct, clarify) 

539 
apply (subgoal_tac "\<forall>k\<in>x. k<J") 

540 
apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply) 

541 
apply (blast intro: lt_trans ltI lt_Ord) 

542 
done 

543 

544 
lemma (in M_ord_arith) Ord_oadd_abs: 

545 
"[ M(i); M(j); M(k); Ord(i); Ord(j) ] ==> is_oadd(M,i,j,k) <> k = i++j" 

546 
apply (simp add: is_oadd_def is_oadd_fun_iff_oadd) 

547 
apply (frule exists_oadd_fun [of j i], blast+) 

548 
done 

549 

550 
lemma (in M_ord_arith) oadd_abs: 

551 
"[ M(i); M(j); M(k) ] ==> is_oadd(M,i,j,k) <> k = i++j" 

552 
apply (case_tac "Ord(i) & Ord(j)") 

553 
apply (simp add: Ord_oadd_abs) 

554 
apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd) 

555 
done 

556 

557 
lemma (in M_ord_arith) oadd_closed [intro,simp]: 

558 
"[ M(i); M(j) ] ==> M(i++j)" 

559 
apply (simp add: oadd_eq_if_raw_oadd, clarify) 

560 
apply (simp add: raw_oadd_eq_oadd) 

561 
apply (frule exists_oadd_fun [of j i], auto) 

562 
apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) 

563 
done 

564 

565 

566 
subsubsection{*Ordinal Multiplication*} 

567 

568 
lemma omult_eqns_unique: 

569 
"[ omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') ] ==> z=z'"; 

570 
apply (simp add: omult_eqns_def, clarify) 

571 
apply (erule Ord_cases, simp_all) 

572 
done 

573 

574 
lemma omult_eqns_0: "omult_eqns(i,0,g,z) <> z=0" 

575 
by (simp add: omult_eqns_def) 

576 

577 
lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0" 

578 
by (simp add: omult_eqns_0) 

579 

580 
lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <> Ord(j) & z = g`j ++ i" 

581 
by (simp add: omult_eqns_def) 

582 

583 
lemma the_omult_eqns_succ: 

584 
"Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i" 

585 
by (simp add: omult_eqns_succ) 

586 

587 
lemma omult_eqns_Limit: 

588 
"Limit(x) ==> omult_eqns(i,x,g,z) <> z = \<Union>(g``x)" 

589 
apply (simp add: omult_eqns_def) 

590 
apply (blast intro: Limit_is_Ord) 

591 
done 

592 

593 
lemma the_omult_eqns_Limit: 

594 
"Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)" 

595 
by (simp add: omult_eqns_Limit) 

596 

597 
lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)" 

598 
by (simp add: omult_eqns_def) 

599 

600 

601 
lemma (in M_ord_arith) the_omult_eqns_closed: 

602 
"[ M(i); M(x); M(g); function(g) ] 

603 
==> M(THE z. omult_eqns(i, x, g, z))" 

604 
apply (case_tac "Ord(x)") 

605 
prefer 2 apply (simp add: omult_eqns_Not) {*trivial, nonOrd case*} 

606 
apply (erule Ord_cases) 

607 
apply (simp add: omult_eqns_0) 

608 
apply (simp add: omult_eqns_succ apply_closed oadd_closed) 

609 
apply (simp add: omult_eqns_Limit) 

610 
done 

611 

612 
lemma (in M_ord_arith) exists_omult: 

613 
"[ Ord(j); M(i); M(j) ] 

614 
==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)" 

615 
apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) 

616 
apply (simp_all add: Memrel_type omult_strong_replacement') 

617 
apply (blast intro: the_omult_eqns_closed) 

618 
done 

619 

620 
lemma (in M_ord_arith) exists_omult_fun: 

621 
"[ Ord(j); M(i); M(j) ] ==> \<exists>f[M]. is_omult_fun(M,i,succ(j),f)" 

622 
apply (rule exists_omult [THEN rexE]) 

623 
apply (erule Ord_succ, assumption, simp) 

624 
apply (rename_tac f) 

625 
apply (frule is_recfun_type) 

626 
apply (rule_tac x=f in rexI) 

627 
apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def 

628 
is_omult_fun_def Ord_trans [OF _ succI1]) 

629 
apply (force dest: Ord_in_Ord' 

630 
simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ 

631 
the_omult_eqns_Limit, assumption) 

632 
done 

633 

634 
lemma (in M_ord_arith) is_omult_fun_apply_0: 

635 
"[ 0 < j; is_omult_fun(M,i,j,f) ] ==> f`0 = 0" 

636 
by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib) 

637 

638 
lemma (in M_ord_arith) is_omult_fun_apply_succ: 

639 
"[ succ(x) < j; is_omult_fun(M,i,j,f) ] ==> f`succ(x) = f`x ++ i" 

640 
by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) 

641 

642 
lemma (in M_ord_arith) is_omult_fun_apply_Limit: 

643 
"[ x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) ] 

644 
==> f ` x = (\<Union>y\<in>x. f`y)" 

645 
apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify) 

646 
apply (drule subset_trans [OF OrdmemD], assumption+) 

647 
apply (simp add: ball_conj_distrib omult_Limit image_function) 

648 
done 

649 

650 
lemma (in M_ord_arith) is_omult_fun_eq_omult: 

651 
"[ is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) ] 

652 
==> j<J > f`j = i**j" 

653 
apply (erule_tac i=j in trans_induct3) 

654 
apply (safe del: impCE) 

655 
apply (simp add: is_omult_fun_apply_0) 

656 
apply (subgoal_tac "x<J") 

657 
apply (simp add: is_omult_fun_apply_succ omult_succ) 

658 
apply (blast intro: lt_trans) 

659 
apply (subgoal_tac "\<forall>k\<in>x. k<J") 

660 
apply (simp add: is_omult_fun_apply_Limit omult_Limit) 

661 
apply (blast intro: lt_trans ltI lt_Ord) 

662 
done 

663 

664 
lemma (in M_ord_arith) omult_abs: 

665 
"[ M(i); M(j); M(k); Ord(i); Ord(j) ] ==> is_omult(M,i,j,k) <> k = i**j" 

666 
apply (simp add: is_omult_def is_omult_fun_eq_omult) 

667 
apply (frule exists_omult_fun [of j i], blast+) 

668 
done 

669 

670 

671 

13647  672 
subsection {*Absoluteness of WellFounded Relations*} 
673 

674 
text{*Relativized to @{term M}: Every wellfounded relation is a subset of some 

675 
inverse image of an ordinal. Key step is the construction (in @{term M}) of a 

676 
rank function.*} 

677 

13634  678 
locale M_wfrank = M_trancl + 
679 
assumes wfrank_separation: 

680 
"M(r) ==> 

681 
separation (M, \<lambda>x. 

682 
\<forall>rplus[M]. tran_closure(M,r,rplus) > 

683 
~ (\<exists>f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))" 

684 
and wfrank_strong_replacement: 

685 
"M(r) ==> 

686 
strong_replacement(M, \<lambda>x z. 

687 
\<forall>rplus[M]. tran_closure(M,r,rplus) > 

688 
(\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z) & 

689 
M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) & 

690 
is_range(M,f,y)))" 

691 
and Ord_wfrank_separation: 

692 
"M(r) ==> 

693 
separation (M, \<lambda>x. 

694 
\<forall>rplus[M]. tran_closure(M,r,rplus) > 

695 
~ (\<forall>f[M]. \<forall>rangef[M]. 

696 
is_range(M,f,rangef) > 

697 
M_is_recfun(M, \<lambda>x f y. is_range(M,f,y), rplus, x, f) > 

698 
ordinal(M,rangef)))" 

699 

700 

701 
text{*Proving that the relativized instances of Separation or Replacement 

702 
agree with the "real" ones.*} 

703 

704 
lemma (in M_wfrank) wfrank_separation': 

705 
"M(r) ==> 

706 
separation 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

707 
(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))" 
13634  708 
apply (insert wfrank_separation [of r]) 
709 
apply (simp add: relation2_def is_recfun_abs [of "%x. range"]) 

710 
done 

711 

712 
lemma (in M_wfrank) wfrank_strong_replacement': 

713 
"M(r) ==> 

714 
strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

715 
pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

716 
y = range(f))" 
13634  717 
apply (insert wfrank_strong_replacement [of r]) 
718 
apply (simp add: relation2_def is_recfun_abs [of "%x. range"]) 

719 
done 

720 

721 
lemma (in M_wfrank) Ord_wfrank_separation': 

722 
"M(r) ==> 

723 
separation (M, \<lambda>x. 

724 
~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) > Ord(range(f))))" 

725 
apply (insert Ord_wfrank_separation [of r]) 

726 
apply (simp add: relation2_def is_recfun_abs [of "%x. range"]) 

727 
done 

728 

729 
text{*This function, defined using replacement, is a rank function for 

730 
wellfounded relations within the class M.*} 

21233  731 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

732 
wellfoundedrank :: "[i=>o,i,i] => i" where 
13634  733 
"wellfoundedrank(M,r,A) == 
734 
{p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 

735 
p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) & 

736 
y = range(f)}" 

737 

738 
lemma (in M_wfrank) exists_wfrank: 

739 
"[ wellfounded(M,r); M(a); M(r) ] 

740 
==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)" 

741 
apply (rule wellfounded_exists_is_recfun) 

742 
apply (blast intro: wellfounded_trancl) 

743 
apply (rule trans_trancl) 

744 
apply (erule wfrank_separation') 

745 
apply (erule wfrank_strong_replacement') 

746 
apply (simp_all add: trancl_subset_times) 

747 
done 

748 

749 
lemma (in M_wfrank) M_wellfoundedrank: 

750 
"[ wellfounded(M,r); M(r); M(A) ] ==> M(wellfoundedrank(M,r,A))" 

751 
apply (insert wfrank_strong_replacement' [of r]) 

752 
apply (simp add: wellfoundedrank_def) 

753 
apply (rule strong_replacement_closed) 

754 
apply assumption+ 

755 
apply (rule univalent_is_recfun) 

756 
apply (blast intro: wellfounded_trancl) 

757 
apply (rule trans_trancl) 

758 
apply (simp add: trancl_subset_times) 

759 
apply (blast dest: transM) 

760 
done 

761 

762 
lemma (in M_wfrank) Ord_wfrank_range [rule_format]: 

763 
"[ wellfounded(M,r); a\<in>A; M(r); M(A) ] 

764 
==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) > Ord(range(f))" 

765 
apply (drule wellfounded_trancl, assumption) 

766 
apply (rule wellfounded_induct, assumption, erule (1) transM) 

767 
apply simp 

768 
apply (blast intro: Ord_wfrank_separation', clarify) 

769 
txt{*The reasoning in both cases is that we get @{term y} such that 

770 
@{term "\<langle>y, x\<rangle> \<in> r^+"}. We find that 

771 
@{term "f`y = restrict(f, r^+ `` {y})"}. *} 

772 
apply (rule OrdI [OF _ Ord_is_Transset]) 

773 
txt{*An ordinal is a transitive set...*} 

774 
apply (simp add: Transset_def) 

775 
apply clarify 

776 
apply (frule apply_recfun2, assumption) 

777 
apply (force simp add: restrict_iff) 

778 
txt{*...of ordinals. This second case requires the induction hyp.*} 

779 
apply clarify 

780 
apply (rename_tac i y) 

781 
apply (frule apply_recfun2, assumption) 

782 
apply (frule is_recfun_imp_in_r, assumption) 

783 
apply (frule is_recfun_restrict) 

784 
(*simp_all won't work*) 

785 
apply (simp add: trans_trancl trancl_subset_times)+ 

786 
apply (drule spec [THEN mp], assumption) 

787 
apply (subgoal_tac "M(restrict(f, r^+ `` {y}))") 

788 
apply (drule_tac x="restrict(f, r^+ `` {y})" in rspec) 

789 
apply assumption 

790 
apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) 

791 
apply (blast dest: pair_components_in_M) 

792 
done 

793 

794 
lemma (in M_wfrank) Ord_range_wellfoundedrank: 

795 
"[ wellfounded(M,r); r \<subseteq> A*A; M(r); M(A) ] 

796 
==> Ord (range(wellfoundedrank(M,r,A)))" 

797 
apply (frule wellfounded_trancl, assumption) 

798 
apply (frule trancl_subset_times) 

799 
apply (simp add: wellfoundedrank_def) 

800 
apply (rule OrdI [OF _ Ord_is_Transset]) 

801 
prefer 2 

802 
txt{*by our previous result the range consists of ordinals.*} 

803 
apply (blast intro: Ord_wfrank_range) 

804 
txt{*We still must show that the range is a transitive set.*} 

805 
apply (simp add: Transset_def, clarify, simp) 

806 
apply (rename_tac x i f u) 

807 
apply (frule is_recfun_imp_in_r, assumption) 

808 
apply (subgoal_tac "M(u) & M(i) & M(x)") 

809 
prefer 2 apply (blast dest: transM, clarify) 

810 
apply (rule_tac a=u in rangeI) 

811 
apply (rule_tac x=u in ReplaceI) 

812 
apply simp 

813 
apply (rule_tac x="restrict(f, r^+ `` {u})" in rexI) 

814 
apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) 

815 
apply simp 

816 
apply blast 

817 
txt{*Unicity requirement of Replacement*} 

818 
apply clarify 

819 
apply (frule apply_recfun2, assumption) 

820 
apply (simp add: trans_trancl is_recfun_cut) 

821 
done 

822 

823 
lemma (in M_wfrank) function_wellfoundedrank: 

824 
"[ wellfounded(M,r); M(r); M(A)] 

825 
==> function(wellfoundedrank(M,r,A))" 

826 
apply (simp add: wellfoundedrank_def function_def, clarify) 

827 
txt{*Uniqueness: repeated below!*} 

828 
apply (drule is_recfun_functional, assumption) 

829 
apply (blast intro: wellfounded_trancl) 

830 
apply (simp_all add: trancl_subset_times trans_trancl) 

831 
done 

832 

833 
lemma (in M_wfrank) domain_wellfoundedrank: 

834 
"[ wellfounded(M,r); M(r); M(A)] 

835 
==> domain(wellfoundedrank(M,r,A)) = A" 

836 
apply (simp add: wellfoundedrank_def function_def) 

837 
apply (rule equalityI, auto) 

838 
apply (frule transM, assumption) 

839 
apply (frule_tac a=x in exists_wfrank, assumption+, clarify) 

840 
apply (rule_tac b="range(f)" in domainI) 

841 
apply (rule_tac x=x in ReplaceI) 

842 
apply simp 

843 
apply (rule_tac x=f in rexI, blast, simp_all) 

844 
txt{*Uniqueness (for Replacement): repeated above!*} 

845 
apply clarify 

846 
apply (drule is_recfun_functional, assumption) 

847 
apply (blast intro: wellfounded_trancl) 

848 
apply (simp_all add: trancl_subset_times trans_trancl) 

849 
done 

850 

851 
lemma (in M_wfrank) wellfoundedrank_type: 

852 
"[ wellfounded(M,r); M(r); M(A)] 

853 
==> wellfoundedrank(M,r,A) \<in> A > range(wellfoundedrank(M,r,A))" 

854 
apply (frule function_wellfoundedrank [of r A], assumption+) 

855 
apply (frule function_imp_Pi) 

856 
apply (simp add: wellfoundedrank_def relation_def) 

857 
apply blast 

858 
apply (simp add: domain_wellfoundedrank) 

859 
done 

860 

861 
lemma (in M_wfrank) Ord_wellfoundedrank: 

862 
"[ wellfounded(M,r); a \<in> A; r \<subseteq> A*A; M(r); M(A) ] 

863 
==> Ord(wellfoundedrank(M,r,A) ` a)" 

864 
by (blast intro: apply_funtype [OF wellfoundedrank_type] 

865 
Ord_in_Ord [OF Ord_range_wellfoundedrank]) 

866 

867 
lemma (in M_wfrank) wellfoundedrank_eq: 

868 
"[ is_recfun(r^+, a, %x. range, f); 

869 
wellfounded(M,r); a \<in> A; M(f); M(r); M(A)] 

870 
==> wellfoundedrank(M,r,A) ` a = range(f)" 

871 
apply (rule apply_equality) 

872 
prefer 2 apply (blast intro: wellfoundedrank_type) 

873 
apply (simp add: wellfoundedrank_def) 

874 
apply (rule ReplaceI) 

875 
apply (rule_tac x="range(f)" in rexI) 

876 
apply blast 

877 
apply simp_all 

878 
txt{*Unicity requirement of Replacement*} 

879 
apply clarify 

880 
apply (drule is_recfun_functional, assumption) 

881 
apply (blast intro: wellfounded_trancl) 

882 
apply (simp_all add: trancl_subset_times trans_trancl) 

883 
done 

884 

885 

886 
lemma (in M_wfrank) wellfoundedrank_lt: 

887 
"[ <a,b> \<in> r; 

888 
wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)] 

889 
==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b" 

890 
apply (frule wellfounded_trancl, assumption) 

891 
apply (subgoal_tac "a\<in>A & b\<in>A") 

892 
prefer 2 apply blast 

893 
apply (simp add: lt_def Ord_wellfoundedrank, clarify) 

894 
apply (frule exists_wfrank [of concl: _ b], erule (1) transM, assumption) 

895 
apply clarify 

896 
apply (rename_tac fb) 

897 
apply (frule is_recfun_restrict [of concl: "r^+" a]) 

898 
apply (rule trans_trancl, assumption) 

899 
apply (simp_all add: r_into_trancl trancl_subset_times) 

900 
txt{*Still the same goal, but with new @{text is_recfun} assumptions.*} 

901 
apply (simp add: wellfoundedrank_eq) 

902 
apply (frule_tac a=a in wellfoundedrank_eq, assumption+) 

903 
apply (simp_all add: transM [of a]) 

904 
txt{*We have used equations for wellfoundedrank and now must use some 

905 
for @{text is_recfun}. *} 

906 
apply (rule_tac a=a in rangeI) 

907 
apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff 

908 
r_into_trancl apply_recfun r_into_trancl) 

909 
done 

910 

911 

912 
lemma (in M_wfrank) wellfounded_imp_subset_rvimage: 

913 
"[wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)] 

914 
==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" 

915 
apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI) 

916 
apply (rule_tac x="wellfoundedrank(M,r,A)" in exI) 

917 
apply (simp add: Ord_range_wellfoundedrank, clarify) 

918 
apply (frule subsetD, assumption, clarify) 

919 
apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD]) 

920 
apply (blast intro: apply_rangeI wellfoundedrank_type) 

921 
done 

922 

923 
lemma (in M_wfrank) wellfounded_imp_wf: 

924 
"[wellfounded(M,r); relation(r); M(r)] ==> wf(r)" 

925 
by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage 

926 
intro: wf_rvimage_Ord [THEN wf_subset]) 

927 

928 
lemma (in M_wfrank) wellfounded_on_imp_wf_on: 

929 
"[wellfounded_on(M,A,r); relation(r); M(r); M(A)] ==> wf[A](r)" 

930 
apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) 

931 
apply (rule wellfounded_imp_wf) 

932 
apply (simp_all add: relation_def) 

933 
done 

934 

935 

936 
theorem (in M_wfrank) wf_abs: 

937 
"[relation(r); M(r)] ==> wellfounded(M,r) <> wf(r)" 

938 
by (blast intro: wellfounded_imp_wf wf_imp_relativized) 

939 

940 
theorem (in M_wfrank) wf_on_abs: 

941 
"[relation(r); M(r); M(A)] ==> wellfounded_on(M,A,r) <> wf[A](r)" 

942 
by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) 

943 

944 
end 