author  lcp 
Thu, 23 Jun 1994 17:38:12 +0200  
changeset 437  435875e4b21d 
parent 435  ca5356bd315a 
child 443  10884e64c241 
permissions  rwrr 
0  1 
(* Title: ZF/wf.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow and Lawrence C Paulson 

4 
Copyright 1992 University of Cambridge 

5 

6 
For wf.thy. Wellfounded Recursion 

7 

8 
Derived first for transitive relations, and finally for arbitrary WF relations 

9 
via wf_trancl and trans_trancl. 

10 

11 
It is difficult to derive this general case directly, using r^+ instead of 

12 
r. In is_recfun, the two occurrences of the relation must have the same 

13 
form. Inserting r^+ in the_recfun or wftrec yields a recursion rule with 

14 
r^+ `` {a} instead of r``{a}. This recursion rule is stronger in 

15 
principle, but harder to use, especially to prove wfrec_eclose_eq in 

16 
epsilon.ML. Expanding out the definition of wftrec in wfrec would yield 

17 
a mess. 

18 
*) 

19 

20 
open WF; 

21 

22 

23 
(*** Wellfounded relations ***) 

24 

435  25 
(** Equivalences between wf and wf_on **) 
26 

27 
goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)"; 

28 
by (fast_tac ZF_cs 1); 

29 
val wf_imp_wf_on = result(); 

30 

31 
goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)"; 

32 
by (fast_tac ZF_cs 1); 

33 
val wf_on_field_imp_wf = result(); 

34 

35 
goal WF.thy "wf(r) <> wf[field(r)](r)"; 

36 
by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1); 

37 
val wf_iff_wf_on_field = result(); 

0  38 

435  39 
goalw WF.thy [wf_on_def, wf_def] "!!A B r. [ wf[A](r); B<=A ] ==> wf[B](r)"; 
40 
by (fast_tac ZF_cs 1); 

41 
val wf_on_subset_A = result(); 

42 

43 
goalw WF.thy [wf_on_def, wf_def] "!!A r s. [ wf[A](r); s<=r ] ==> wf[A](s)"; 

44 
by (fast_tac ZF_cs 1); 

45 
val wf_on_subset_r = result(); 

46 

47 
(** Introduction rules for wf_on **) 

48 

49 
(*If every nonempty subset of A has an rminimal element then wf[A](r).*) 

50 
val [prem] = goalw WF.thy [wf_on_def, wf_def] 

51 
"[ !!Z u. [ Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r ] ==> False ] \ 

52 
\ ==> wf[A](r)"; 

0  53 
by (rtac (equals0I RS disjCI RS allI) 1); 
435  54 
by (res_inst_tac [ ("Z", "Z") ] prem 1); 
55 
by (ALLGOALS (fast_tac ZF_cs)); 

56 
val wf_onI = result(); 

0  57 

435  58 
(*If r allows wellfounded induction over A then wf[A](r) 
59 
Premise is equivalent to 

60 
!!B. ALL x:A. (ALL y. <y,x>: r > y:B) > x:B ==> A<=B *) 

61 
val [prem] = goal WF.thy 

62 
"[ !!y B. [ ALL x:A. (ALL y:A. <y,x>:r > y:B) > x:B; y:A \ 

63 
\ ] ==> y:B ] \ 

64 
\ ==> wf[A](r)"; 

437  65 
by (rtac wf_onI 1); 
435  66 
by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1); 
67 
by (contr_tac 3); 

0  68 
by (fast_tac ZF_cs 2); 
69 
by (fast_tac ZF_cs 1); 

435  70 
val wf_onI2 = result(); 
0  71 

72 

73 
(** Wellfounded Induction **) 

74 

75 
(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*) 

76 
val major::prems = goalw WF.thy [wf_def] 

77 
"[ wf(r); \ 

78 
\ !!x.[ ALL y. <y,x>: r > P(y) ] ==> P(x) \ 

79 
\ ] ==> P(a)"; 

80 
by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ] (major RS allE) 1); 

81 
by (etac disjE 1); 

82 
by (rtac classical 1); 

83 
by (etac equals0D 1); 

84 
by (etac (singletonI RS UnI2 RS CollectI) 1); 

85 
by (etac bexE 1); 

86 
by (etac CollectE 1); 

87 
by (etac swap 1); 

88 
by (resolve_tac prems 1); 

89 
by (fast_tac ZF_cs 1); 

90 
val wf_induct = result(); 

91 

92 
(*Perform induction on i, then prove the wf(r) subgoal using prems. *) 

93 
fun wf_ind_tac a prems i = 

94 
EVERY [res_inst_tac [("a",a)] wf_induct i, 

95 
rename_last_tac a ["1"] (i+1), 

96 
ares_tac prems i]; 

97 

98 
(*The form of this rule is designed to match wfI2*) 

99 
val wfr::amem::prems = goal WF.thy 

100 
"[ wf(r); a:A; field(r)<=A; \ 

101 
\ !!x.[ x: A; ALL y. <y,x>: r > P(y) ] ==> P(x) \ 

102 
\ ] ==> P(a)"; 

103 
by (rtac (amem RS rev_mp) 1); 

104 
by (wf_ind_tac "a" [wfr] 1); 

105 
by (rtac impI 1); 

106 
by (eresolve_tac prems 1); 

107 
by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1); 

108 
val wf_induct2 = result(); 

109 

435  110 
goal ZF.thy "!!r A. field(r Int A*A) <= A"; 
111 
by (fast_tac ZF_cs 1); 

112 
val field_Int_square = result(); 

113 

114 
val wfr::amem::prems = goalw WF.thy [wf_on_def] 

115 
"[ wf[A](r); a:A; \ 

116 
\ !!x.[ x: A; ALL y:A. <y,x>: r > P(y) ] ==> P(x) \ 

117 
\ ] ==> P(a)"; 

118 
by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1); 

119 
by (REPEAT (ares_tac prems 1)); 

120 
by (fast_tac ZF_cs 1); 

121 
val wf_on_induct = result(); 

122 

123 
fun wf_on_ind_tac a prems i = 

124 
EVERY [res_inst_tac [("a",a)] wf_on_induct i, 

125 
rename_last_tac a ["1"] (i+2), 

126 
REPEAT (ares_tac prems i)]; 

127 

128 
(*If r allows wellfounded induction then wf(r)*) 

129 
val [subs,indhyp] = goal WF.thy 

130 
"[ field(r)<=A; \ 

131 
\ !!y B. [ ALL x:A. (ALL y:A. <y,x>:r > y:B) > x:B; y:A \ 

132 
\ ] ==> y:B ] \ 

133 
\ ==> wf(r)"; 

437  134 
by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1); 
435  135 
by (REPEAT (ares_tac [indhyp] 1)); 
136 
val wfI2 = result(); 

137 

138 

139 
(*** Properties of wellfounded relations ***) 

140 

141 
goal WF.thy "!!r. wf(r) ==> <a,a> ~: r"; 

142 
by (wf_ind_tac "a" [] 1); 

143 
by (fast_tac ZF_cs 1); 

144 
val wf_not_refl = result(); 

145 

146 
goal WF.thy "!!r. [ wf(r); <a,x>:r; <x,a>:r ] ==> P"; 

147 
by (subgoal_tac "ALL x. <a,x>:r > <x,a>:r > P" 1); 

148 
by (wf_ind_tac "a" [] 2); 

0  149 
by (fast_tac ZF_cs 2); 
435  150 
by (fast_tac FOL_cs 1); 
437  151 
val wf_asym = result(); 
0  152 

435  153 
goal WF.thy "!!r. [ wf[A](r); a: A ] ==> <a,a> ~: r"; 
154 
by (wf_on_ind_tac "a" [] 1); 

155 
by (fast_tac ZF_cs 1); 

156 
val wf_on_not_refl = result(); 

157 

158 
goal WF.thy "!!r. [ wf[A](r); <a,b>:r; <b,a>:r; a:A; b:A ] ==> P"; 

159 
by (subgoal_tac "ALL y:A. <a,y>:r > <y,a>:r > P" 1); 

160 
by (wf_on_ind_tac "a" [] 2); 

161 
by (fast_tac ZF_cs 2); 

162 
by (fast_tac ZF_cs 1); 

437  163 
val wf_on_asym = result(); 
435  164 

165 
(*Needed to prove well_ordI. Could also reason that wf[A](r) means 

166 
wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) 

167 
goal WF.thy 

168 
"!!r. [ wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A ] ==> P"; 

169 
by (subgoal_tac 

170 
"ALL y:A. ALL z:A. <a,y>:r > <y,z>:r > <z,a>:r > P" 1); 

171 
by (wf_on_ind_tac "a" [] 2); 

172 
by (fast_tac ZF_cs 2); 

173 
by (fast_tac ZF_cs 1); 

174 
val wf_on_chain3 = result(); 

175 

176 

177 
(*retains the universal formula for later use!*) 

178 
val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ]; 

179 

180 
(*transitive closure of a WF relation is WF provided A is downwards closed*) 

181 
val [wfr,subs] = goal WF.thy 

182 
"[ wf[A](r); r``A <= A ] ==> wf[A](r^+)"; 

437  183 
by (rtac wf_onI2 1); 
435  184 
by (bchain_tac 1); 
185 
by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1); 

186 
by (rtac (impI RS ballI) 1); 

0  187 
by (etac tranclE 1); 
435  188 
by (etac (bspec RS mp) 1 THEN assume_tac 1); 
0  189 
by (fast_tac ZF_cs 1); 
435  190 
by (cut_facts_tac [subs] 1); 
191 
(*astar_tac is slightly faster*) 

192 
by (best_tac ZF_cs 1); 

193 
val wf_on_trancl = result(); 

194 

195 
goal WF.thy "!!r. wf(r) ==> wf(r^+)"; 

196 
by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1); 

437  197 
by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1); 
198 
by (etac wf_on_trancl 1); 

0  199 
by (fast_tac ZF_cs 1); 
200 
val wf_trancl = result(); 

201 

435  202 

203 

0  204 
(** r``{a} is the set of everything under a in r **) 
205 

206 
val underI = standard (vimage_singleton_iff RS iffD2); 

207 
val underD = standard (vimage_singleton_iff RS iffD1); 

208 

209 
(** is_recfun **) 

210 

211 
val [major] = goalw WF.thy [is_recfun_def] 

212 
"is_recfun(r,a,H,f) ==> f: r``{a} > range(f)"; 

213 
by (rtac (major RS ssubst) 1); 

214 
by (rtac (lamI RS rangeI RS lam_type) 1); 

215 
by (assume_tac 1); 

216 
val is_recfun_type = result(); 

217 

218 
val [isrec,rel] = goalw WF.thy [is_recfun_def] 

219 
"[ is_recfun(r,a,H,f); <x,a>:r ] ==> f`x = H(x, restrict(f,r``{x}))"; 

220 
by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1); 

221 
by (rtac (rel RS underI RS beta) 1); 

222 
val apply_recfun = result(); 

223 

224 
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE 

225 
spec RS mp instantiates induction hypotheses*) 

226 
fun indhyp_tac hyps = 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

227 
resolve_tac (TrueI::refl::hyps) ORELSE' 
0  228 
(cut_facts_tac hyps THEN' 
229 
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE' 

230 
eresolve_tac [underD, transD, spec RS mp])); 

231 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

232 
(*** NOTE! some simplifications need a different solver!! ***) 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

233 
val wf_super_ss = ZF_ss setsolver indhyp_tac; 
0  234 

235 
val prems = goalw WF.thy [is_recfun_def] 

236 
"[ wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) ] ==> \ 

237 
\ <x,a>:r > <x,b>:r > f`x=g`x"; 

238 
by (cut_facts_tac prems 1); 

239 
by (wf_ind_tac "x" prems 1); 

240 
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); 

241 
by (rewtac restrict_def); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

242 
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1); 
0  243 
val is_recfun_equal_lemma = result(); 
244 
val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp); 

245 

246 
val prems as [wfr,transr,recf,recg,_] = goal WF.thy 

247 
"[ wf(r); trans(r); \ 

248 
\ is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r ] ==> \ 

249 
\ restrict(f, r``{b}) = g"; 

250 
by (cut_facts_tac prems 1); 

251 
by (rtac (consI1 RS restrict_type RS fun_extension) 1); 

252 
by (etac is_recfun_type 1); 

253 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

254 
(asm_simp_tac (wf_super_ss addsimps 
0  255 
[ [wfr,transr,recf,recg] MRS is_recfun_equal ]))); 
256 
val is_recfun_cut = result(); 

257 

258 
(*** Main Existence Lemma ***) 

259 

260 
val prems = goal WF.thy 

261 
"[ wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) ] ==> f=g"; 

262 
by (cut_facts_tac prems 1); 

263 
by (rtac fun_extension 1); 

264 
by (REPEAT (ares_tac [is_recfun_equal] 1 

265 
ORELSE eresolve_tac [is_recfun_type,underD] 1)); 

266 
val is_recfun_functional = result(); 

267 

268 
(*If some f satisfies is_recfun(r,a,H,) then so does the_recfun(r,a,H) *) 

269 
val prems = goalw WF.thy [the_recfun_def] 

270 
"[ is_recfun(r,a,H,f); wf(r); trans(r) ] \ 

271 
\ ==> is_recfun(r, a, H, the_recfun(r,a,H))"; 

272 
by (rtac (ex1I RS theI) 1); 

273 
by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1)); 

274 
val is_the_recfun = result(); 

275 

276 
val prems = goal WF.thy 

277 
"[ wf(r); trans(r) ] ==> is_recfun(r, a, H, the_recfun(r,a,H))"; 

278 
by (cut_facts_tac prems 1); 

279 
by (wf_ind_tac "a" prems 1); 

280 
by (res_inst_tac [("f", "lam y: r``{a1}. wftrec(r,y,H)")] is_the_recfun 1); 

281 
by (REPEAT (assume_tac 2)); 

282 
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); 

283 
(*Applying the substitution: must keep the quantified assumption!!*) 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

284 
by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1)); 
0  285 
by (fold_tac [is_recfun_def]); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

286 
by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1); 
0  287 
by (rtac is_recfun_type 1); 
288 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

289 
(asm_simp_tac 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

290 
(wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut]))); 
0  291 
val unfold_the_recfun = result(); 
292 

293 

294 
(*** Unfolding wftrec ***) 

295 

296 
val prems = goal WF.thy 

297 
"[ wf(r); trans(r); <b,a>:r ] ==> \ 

298 
\ restrict(the_recfun(r,a,H), r``{b}) = the_recfun(r,b,H)"; 

299 
by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1)); 

300 
val the_recfun_cut = result(); 

301 

302 
(*NOT SUITABLE FOR REWRITING since it is recursive!*) 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

303 
goalw WF.thy [wftrec_def] 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

304 
"!!r. [ wf(r); trans(r) ] ==> \ 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

305 
\ wftrec(r,a,H) = H(a, lam x: r``{a}. wftrec(r,x,H))"; 
0  306 
by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

307 
by (ALLGOALS (asm_simp_tac 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

308 
(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut]))); 
0  309 
val wftrec = result(); 
310 

311 
(** Removal of the premise trans(r) **) 

312 

313 
(*NOT SUITABLE FOR REWRITING since it is recursive!*) 

314 
val [wfr] = goalw WF.thy [wfrec_def] 

315 
"wf(r) ==> wfrec(r,a,H) = H(a, lam x:r``{a}. wfrec(r,x,H))"; 

316 
by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1); 

317 
by (rtac trans_trancl 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

318 
by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1); 
0  319 
by (etac r_into_trancl 1); 
320 
by (rtac subset_refl 1); 

321 
val wfrec = result(); 

322 

323 
(*This form avoids giant explosions in proofs. NOTE USE OF == *) 

324 
val rew::prems = goal WF.thy 

325 
"[ !!x. h(x)==wfrec(r,x,H); wf(r) ] ==> \ 

326 
\ h(a) = H(a, lam x: r``{a}. h(x))"; 

327 
by (rewtac rew); 

328 
by (REPEAT (resolve_tac (prems@[wfrec]) 1)); 

329 
val def_wfrec = result(); 

330 

331 
val prems = goal WF.thy 

332 
"[ wf(r); a:A; field(r)<=A; \ 

333 
\ !!x u. [ x: A; u: Pi(r``{x}, B) ] ==> H(x,u) : B(x) \ 

334 
\ ] ==> wfrec(r,a,H) : B(a)"; 

335 
by (res_inst_tac [("a","a")] wf_induct2 1); 

336 
by (rtac (wfrec RS ssubst) 4); 

337 
by (REPEAT (ares_tac (prems@[lam_type]) 1 

338 
ORELSE eresolve_tac [spec RS mp, underD] 1)); 

339 
val wfrec_type = result(); 

435  340 

341 

342 
goalw WF.thy [wf_on_def, wfrec_on_def] 

343 
"!!A r. [ wf[A](r); a: A ] ==> \ 

344 
\ wfrec[A](r,a,H) = H(a, lam x: (r``{a}) Int A. wfrec[A](r,x,H))"; 

437  345 
by (etac (wfrec RS trans) 1); 
435  346 
by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1); 
347 
val wfrec_on = result(); 

348 