author  lcp 
Fri, 17 Sep 1993 16:16:38 +0200  
changeset 6  8ce8c4d13d4d 
parent 0  a5a9c433f639 
child 435  ca5356bd315a 
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 

25 
(*Are these two theorems at all useful??*) 

26 

27 
(*If every subset of field(r) possesses an rminimal element then wf(r). 

28 
Seems impossible to prove this for domain(r) or range(r) instead... 

29 
Consider in particular finite wf relations!*) 

30 
val [prem1,prem2] = goalw WF.thy [wf_def] 

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

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

33 
\ ==> wf(r)"; 

34 
by (rtac (equals0I RS disjCI RS allI) 1); 

35 
by (rtac prem2 1); 

36 
by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1); 

37 
by (fast_tac ZF_cs 1); 

38 
by (fast_tac ZF_cs 1); 

39 
val wfI = result(); 

40 

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

42 
val [prem1,prem2] = goal WF.thy 

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

44 
\ !!B. ALL x:A. (ALL y. <y,x>: r > y:B) > x:B ==> A<=B ] \ 

45 
\ ==> wf(r)"; 

46 
by (rtac (prem1 RS wfI) 1); 

47 
by (res_inst_tac [ ("B", "AZ") ] (prem2 RS subsetCE) 1); 

48 
by (fast_tac ZF_cs 3); 

49 
by (fast_tac ZF_cs 2); 

50 
by (fast_tac ZF_cs 1); 

51 
val wfI2 = result(); 

52 

53 

54 
(** Wellfounded Induction **) 

55 

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

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

58 
"[ wf(r); \ 

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

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

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

62 
by (etac disjE 1); 

63 
by (rtac classical 1); 

64 
by (etac equals0D 1); 

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

66 
by (etac bexE 1); 

67 
by (etac CollectE 1); 

68 
by (etac swap 1); 

69 
by (resolve_tac prems 1); 

70 
by (fast_tac ZF_cs 1); 

71 
val wf_induct = result(); 

72 

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

74 
fun wf_ind_tac a prems i = 

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

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

77 
ares_tac prems i]; 

78 

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

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

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

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

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

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

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

86 
by (rtac impI 1); 

87 
by (eresolve_tac prems 1); 

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

89 
val wf_induct2 = result(); 

90 

91 
val prems = goal WF.thy "[ wf(r); <a,x>:r; <x,a>:r ] ==> False"; 

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

93 
by (wf_ind_tac "a" prems 2); 

94 
by (fast_tac ZF_cs 2); 

95 
by (fast_tac (FOL_cs addIs prems) 1); 

96 
val wf_anti_sym = result(); 

97 

98 
(*transitive closure of a WF relation is WF!*) 

99 
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; 

100 
by (rtac (trancl_type RS field_rel_subset RS wfI2) 1); 

101 
by (rtac subsetI 1); 

102 
(*must retain the universal formula for later use!*) 

103 
by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1); 

104 
by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1); 

105 
by (rtac subset_refl 1); 

106 
by (rtac (impI RS allI) 1); 

107 
by (etac tranclE 1); 

108 
by (etac (bspec RS mp) 1); 

109 
by (etac fieldI1 1); 

110 
by (fast_tac ZF_cs 1); 

111 
by (fast_tac ZF_cs 1); 

112 
val wf_trancl = result(); 

113 

114 
(** r``{a} is the set of everything under a in r **) 

115 

116 
val underI = standard (vimage_singleton_iff RS iffD2); 

117 
val underD = standard (vimage_singleton_iff RS iffD1); 

118 

119 
(** is_recfun **) 

120 

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

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

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

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

125 
by (assume_tac 1); 

126 
val is_recfun_type = result(); 

127 

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

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

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

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

132 
val apply_recfun = result(); 

133 

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

135 
spec RS mp instantiates induction hypotheses*) 

136 
fun indhyp_tac hyps = 

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

137 
resolve_tac (TrueI::refl::hyps) ORELSE' 
0  138 
(cut_facts_tac hyps THEN' 
139 
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE' 

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

141 

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

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

143 
val wf_super_ss = ZF_ss setsolver indhyp_tac; 
0  144 

145 
val prems = goalw WF.thy [is_recfun_def] 

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

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

148 
by (cut_facts_tac prems 1); 

149 
by (wf_ind_tac "x" prems 1); 

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

151 
by (rewtac restrict_def); 

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

152 
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1); 
0  153 
val is_recfun_equal_lemma = result(); 
154 
val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp); 

155 

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

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

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

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

160 
by (cut_facts_tac prems 1); 

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

162 
by (etac is_recfun_type 1); 

163 
by (ALLGOALS 

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

164 
(asm_simp_tac (wf_super_ss addsimps 
0  165 
[ [wfr,transr,recf,recg] MRS is_recfun_equal ]))); 
166 
val is_recfun_cut = result(); 

167 

168 
(*** Main Existence Lemma ***) 

169 

170 
val prems = goal WF.thy 

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

172 
by (cut_facts_tac prems 1); 

173 
by (rtac fun_extension 1); 

174 
by (REPEAT (ares_tac [is_recfun_equal] 1 

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

176 
val is_recfun_functional = result(); 

177 

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

179 
val prems = goalw WF.thy [the_recfun_def] 

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

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

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

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

184 
val is_the_recfun = result(); 

185 

186 
val prems = goal WF.thy 

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

188 
by (cut_facts_tac prems 1); 

189 
by (wf_ind_tac "a" prems 1); 

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

191 
by (REPEAT (assume_tac 2)); 

192 
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); 

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

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

196 
by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1); 
0  197 
by (rtac is_recfun_type 1); 
198 
by (ALLGOALS 

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

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

200 
(wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut]))); 
0  201 
val unfold_the_recfun = result(); 
202 

203 

204 
(*** Unfolding wftrec ***) 

205 

206 
val prems = goal WF.thy 

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

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

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

210 
val the_recfun_cut = result(); 

211 

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

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

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

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

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

218 
(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut]))); 
0  219 
val wftrec = result(); 
220 

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

222 

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

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

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

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

227 
by (rtac trans_trancl 1); 

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

228 
by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1); 
0  229 
by (etac r_into_trancl 1); 
230 
by (rtac subset_refl 1); 

231 
val wfrec = result(); 

232 

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

234 
val rew::prems = goal WF.thy 

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

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

237 
by (rewtac rew); 

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

239 
val def_wfrec = result(); 

240 

241 
val prems = goal WF.thy 

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

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

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

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

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

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

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

249 
val wfrec_type = result(); 