author  clasohm 
Wed, 14 Dec 1994 11:41:49 +0100  
changeset 782  200a16083201 
parent 760  f0200e91b272 
child 1461  6bcb44e4d6e5 
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); 

760  29 
qed "wf_imp_wf_on"; 
435  30 

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

32 
by (fast_tac ZF_cs 1); 

760  33 
qed "wf_on_field_imp_wf"; 
435  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); 

760  37 
qed "wf_iff_wf_on_field"; 
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); 

760  41 
qed "wf_on_subset_A"; 
435  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); 

760  45 
qed "wf_on_subset_r"; 
435  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)); 

760  56 
qed "wf_onI"; 
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); 

760  70 
qed "wf_onI2"; 
0  71 

72 

73 
(** Wellfounded Induction **) 

74 

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

494  76 
val [major,minor] = goalw WF.thy [wf_def] 
0  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); 

494  82 
by (fast_tac (ZF_cs addEs [equalityE]) 1); 
83 
by (asm_full_simp_tac (ZF_ss addsimps [domainI]) 1); 

0  84 
by (etac bexE 1); 
494  85 
by (dtac minor 1); 
0  86 
by (fast_tac ZF_cs 1); 
760  87 
qed "wf_induct"; 
0  88 

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

90 
fun wf_ind_tac a prems i = 

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

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

93 
ares_tac prems i]; 

94 

485  95 
(*The form of this rule is designed to match wfI*) 
0  96 
val wfr::amem::prems = goal WF.thy 
97 
"[ wf(r); a:A; field(r)<=A; \ 

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

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

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

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

102 
by (rtac impI 1); 

103 
by (eresolve_tac prems 1); 

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

760  105 
qed "wf_induct2"; 
0  106 

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

760  109 
qed "field_Int_square"; 
435  110 

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

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

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

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

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

116 
by (REPEAT (ares_tac prems 1)); 

117 
by (fast_tac ZF_cs 1); 

760  118 
qed "wf_on_induct"; 
435  119 

120 
fun wf_on_ind_tac a prems i = 

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

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

123 
REPEAT (ares_tac prems i)]; 

124 

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

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

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

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

129 
\ ] ==> y:B ] \ 

130 
\ ==> wf(r)"; 

437  131 
by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1); 
435  132 
by (REPEAT (ares_tac [indhyp] 1)); 
760  133 
qed "wfI"; 
435  134 

135 

136 
(*** Properties of wellfounded relations ***) 

137 

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

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

140 
by (fast_tac ZF_cs 1); 

760  141 
qed "wf_not_refl"; 
435  142 

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

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

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

0  146 
by (fast_tac ZF_cs 2); 
435  147 
by (fast_tac FOL_cs 1); 
760  148 
qed "wf_asym"; 
0  149 

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

152 
by (fast_tac ZF_cs 1); 

760  153 
qed "wf_on_not_refl"; 
435  154 

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

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

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

158 
by (fast_tac ZF_cs 2); 

159 
by (fast_tac ZF_cs 1); 

760  160 
qed "wf_on_asym"; 
435  161 

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

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

164 
goal WF.thy 

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

166 
by (subgoal_tac 

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

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

169 
by (fast_tac ZF_cs 2); 

170 
by (fast_tac ZF_cs 1); 

760  171 
qed "wf_on_chain3"; 
435  172 

173 

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

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

176 

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

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

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

437  180 
by (rtac wf_onI2 1); 
435  181 
by (bchain_tac 1); 
182 
by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1); 

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

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

189 
by (best_tac ZF_cs 1); 

760  190 
qed "wf_on_trancl"; 
435  191 

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

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

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

0  196 
by (fast_tac ZF_cs 1); 
760  197 
qed "wf_trancl"; 
0  198 

435  199 

200 

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

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

203 
bind_thm ("underI", (vimage_singleton_iff RS iffD2)); 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

204 
bind_thm ("underD", (vimage_singleton_iff RS iffD1)); 
0  205 

206 
(** is_recfun **) 

207 

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

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

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

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

212 
by (assume_tac 1); 

760  213 
qed "is_recfun_type"; 
0  214 

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

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

443
10884e64c241
added parentheses made necessary by new constrain precedence
clasohm
parents:
437
diff
changeset

217 
by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1); 
0  218 
by (rtac (rel RS underI RS beta) 1); 
760  219 
qed "apply_recfun"; 
0  220 

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

222 
spec RS mp instantiates induction hypotheses*) 

223 
fun indhyp_tac hyps = 

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

224 
resolve_tac (TrueI::refl::hyps) ORELSE' 
0  225 
(cut_facts_tac hyps THEN' 
226 
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE' 

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

228 

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

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

230 
val wf_super_ss = ZF_ss setsolver indhyp_tac; 
0  231 

232 
val prems = goalw WF.thy [is_recfun_def] 

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

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

235 
by (cut_facts_tac prems 1); 

236 
by (wf_ind_tac "x" prems 1); 

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

238 
by (rewtac restrict_def); 

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

239 
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1); 
760  240 
qed "is_recfun_equal_lemma"; 
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset

241 
bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp)); 
0  242 

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

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

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

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

247 
by (cut_facts_tac prems 1); 

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

249 
by (etac is_recfun_type 1); 

250 
by (ALLGOALS 

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

251 
(asm_simp_tac (wf_super_ss addsimps 
0  252 
[ [wfr,transr,recf,recg] MRS is_recfun_equal ]))); 
760  253 
qed "is_recfun_cut"; 
0  254 

255 
(*** Main Existence Lemma ***) 

256 

257 
val prems = goal WF.thy 

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

259 
by (cut_facts_tac prems 1); 

260 
by (rtac fun_extension 1); 

261 
by (REPEAT (ares_tac [is_recfun_equal] 1 

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

760  263 
qed "is_recfun_functional"; 
0  264 

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

266 
val prems = goalw WF.thy [the_recfun_def] 

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

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

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

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

760  271 
qed "is_the_recfun"; 
0  272 

273 
val prems = goal WF.thy 

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

275 
by (cut_facts_tac prems 1); 

276 
by (wf_ind_tac "a" prems 1); 

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

278 
by (REPEAT (assume_tac 2)); 

279 
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); 

280 
(*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

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

283 
by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1); 
0  284 
by (rtac is_recfun_type 1); 
285 
by (ALLGOALS 

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

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

287 
(wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut]))); 
760  288 
qed "unfold_the_recfun"; 
0  289 

290 

291 
(*** Unfolding wftrec ***) 

292 

293 
val prems = goal WF.thy 

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

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

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

760  297 
qed "the_recfun_cut"; 
0  298 

299 
(*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

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

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

302 
\ wftrec(r,a,H) = H(a, lam x: r``{a}. wftrec(r,x,H))"; 
0  303 
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

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

305 
(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut]))); 
760  306 
qed "wftrec"; 
0  307 

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

309 

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

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

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

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

314 
by (rtac trans_trancl 1); 

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

315 
by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1); 
0  316 
by (etac r_into_trancl 1); 
317 
by (rtac subset_refl 1); 

760  318 
qed "wfrec"; 
0  319 

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

321 
val rew::prems = goal WF.thy 

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

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

324 
by (rewtac rew); 

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

760  326 
qed "def_wfrec"; 
0  327 

328 
val prems = goal WF.thy 

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

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

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

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

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

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

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

760  336 
qed "wfrec_type"; 
435  337 

338 

339 
goalw WF.thy [wf_on_def, wfrec_on_def] 

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

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

437  342 
by (etac (wfrec RS trans) 1); 
435  343 
by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1); 
760  344 
qed "wfrec_on"; 
435  345 