author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8703  816d8f6513be 
child 9108  9fff97d29837 
permissions  rwrr 
1475  1 
(* Title: HOL/wf.ML 
923  2 
ID: $Id$ 
1475  3 
Author: Tobias Nipkow, with minor changes by Konrad Slind 
4 
Copyright 1992 University of Cambridge/1995 TU Munich 

923  5 

3198  6 
Wellfoundedness, induction, and recursion 
923  7 
*) 
8 

7249  9 
Goal "x = y ==> H x z = H y z"; 
10 
by (Asm_simp_tac 1); 

11 
val H_cong2 = (*freeze H!*) 

12 
read_instantiate [("H","H")] (result()); 

923  13 

5579  14 
val [prem] = Goalw [wf_def] 
15 
"[ !!P x. [ !x. (!y. (y,x) : r > P(y)) > P(x) ] ==> P(x) ] ==> wf(r)"; 

16 
by (Clarify_tac 1); 

17 
by (rtac prem 1); 

18 
by (assume_tac 1); 

19 
qed "wfUNIVI"; 

20 

923  21 
(*Restriction to domain A. If r is wellfounded over A then wf(r)*) 
5316  22 
val [prem1,prem2] = Goalw [wf_def] 
8703  23 
"[ r <= A <*> A; \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

24 
\ !!x P. [ ! x. (! y. (y,x) : r > P(y)) > P(x); x:A ] ==> P(x) ] \ 
923  25 
\ ==> wf(r)"; 
7249  26 
by (blast_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); 
923  27 
qed "wfI"; 
28 

5316  29 
val major::prems = Goalw [wf_def] 
923  30 
"[ wf(r); \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

31 
\ !!x.[ ! y. (y,x): r > P(y) ] ==> P(x) \ 
923  32 
\ ] ==> P(a)"; 
33 
by (rtac (major RS spec RS mp RS spec) 1); 

4089  34 
by (blast_tac (claset() addIs prems) 1); 
923  35 
qed "wf_induct"; 
36 

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

38 
fun wf_ind_tac a prems i = 

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

1465  40 
rename_last_tac a ["1"] (i+1), 
41 
ares_tac prems i]; 

923  42 

5452  43 
Goal "wf(r) ==> ! x. (a,x):r > (x,a)~:r"; 
5316  44 
by (wf_ind_tac "a" [] 1); 
2935  45 
by (Blast_tac 1); 
5452  46 
qed_spec_mp "wf_not_sym"; 
47 

48 
(* [ wf(r); (a,x):r; ~P ==> (x,a):r ] ==> P *) 

49 
bind_thm ("wf_asym", wf_not_sym RS swap); 

923  50 

5316  51 
Goal "[ wf(r); (a,a): r ] ==> P"; 
52 
by (blast_tac (claset() addEs [wf_asym]) 1); 

1618  53 
qed "wf_irrefl"; 
923  54 

1475  55 
(*transitive closure of a wf relation is wf! *) 
5316  56 
Goal "wf(r) ==> wf(r^+)"; 
57 
by (stac wf_def 1); 

3708  58 
by (Clarify_tac 1); 
923  59 
(*must retain the universal formula for later use!*) 
60 
by (rtac allE 1 THEN assume_tac 1); 

61 
by (etac mp 1); 

5316  62 
by (eres_inst_tac [("a","x")] wf_induct 1); 
7249  63 
by (blast_tac (claset() addEs [tranclE]) 1); 
923  64 
qed "wf_trancl"; 
65 

66 

4762  67 
val wf_converse_trancl = prove_goal thy 
68 
"!!X. wf (r^1) ==> wf ((r^+)^1)" (K [ 

69 
stac (trancl_converse RS sym) 1, 

70 
etac wf_trancl 1]); 

71 

3198  72 
(* 
73 
* Minimalelement characterization of wellfoundedness 

74 
**) 

75 

5316  76 
Goalw [wf_def] "wf r ==> x:Q > (? z:Q. ! y. (y,z):r > y~:Q)"; 
5318  77 
by (dtac spec 1); 
5316  78 
by (etac (mp RS spec) 1); 
3198  79 
by (Blast_tac 1); 
80 
val lemma1 = result(); 

81 

5316  82 
Goalw [wf_def] "(! Q x. x:Q > (? z:Q. ! y. (y,z):r > y~:Q)) ==> wf r"; 
3708  83 
by (Clarify_tac 1); 
3198  84 
by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1); 
85 
by (Blast_tac 1); 

86 
val lemma2 = result(); 

87 

5069  88 
Goal "wf r = (! Q x. x:Q > (? z:Q. ! y. (y,z):r > y~:Q))"; 
4089  89 
by (blast_tac (claset() addSIs [lemma1, lemma2]) 1); 
3198  90 
qed "wf_eq_minimal"; 
91 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

92 
(* 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

93 
* Wellfoundedness of subsets 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

94 
**) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

95 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

96 
Goal "[ wf(r); p<=r ] ==> wf(p)"; 
4089  97 
by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

98 
by (Fast_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

99 
qed "wf_subset"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

100 

c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

101 
(* 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

102 
* Wellfoundedness of the empty relation. 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

103 
**) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

104 

5069  105 
Goal "wf({})"; 
4089  106 
by (simp_tac (simpset() addsimps [wf_def]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

107 
qed "wf_empty"; 
5281  108 
AddIffs [wf_empty]; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

109 

c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

110 
(* 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

111 
* Wellfoundedness of `insert' 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

112 
**) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

113 

5069  114 
Goal "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"; 
3457  115 
by (rtac iffI 1); 
4350
1983e4054fd8
updated for latest Blast_tac, which treats equality differently
paulson
parents:
4153
diff
changeset

116 
by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] 
1983e4054fd8
updated for latest Blast_tac, which treats equality differently
paulson
parents:
4153
diff
changeset

117 
addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1); 
4089  118 
by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); 
4153  119 
by Safe_tac; 
7249  120 
by (EVERY1[rtac allE, assume_tac, etac impE, Blast_tac]); 
3457  121 
by (etac bexE 1); 
122 
by (rename_tac "a" 1); 

123 
by (case_tac "a = x" 1); 

124 
by (res_inst_tac [("x","a")]bexI 2); 

125 
by (assume_tac 3); 

126 
by (Blast_tac 2); 

127 
by (case_tac "y:Q" 1); 

128 
by (Blast_tac 2); 

4059  129 
by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1); 
3457  130 
by (assume_tac 1); 
4059  131 
by (thin_tac "! Q. (? x. x : Q) > ?P Q" 1); (*essential for speed*) 
4350
1983e4054fd8
updated for latest Blast_tac, which treats equality differently
paulson
parents:
4153
diff
changeset

132 
(*Blast_tac with new substOccur fails*) 
1983e4054fd8
updated for latest Blast_tac, which treats equality differently
paulson
parents:
4153
diff
changeset

133 
by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

134 
qed "wf_insert"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

135 
AddIffs [wf_insert]; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

136 

5281  137 
(* 
138 
* Wellfoundedness of `disjoint union' 

139 
**) 

140 

5330  141 
(*Intuition behind this proof for the case of binary union: 
142 

143 
Goal: find an (R u S)min element of a nonempty subset A. 

144 
by case distinction: 

145 
1. There is a step a R> b with a,b : A. 

146 
Pick an Rmin element z of the (nonempty) set {a:A  EX b:A. a R> b}. 

147 
By definition, there is z':A s.t. z R> z'. Because z is Rmin in the 

148 
subset, z' must be Rmin in A. Because z' has an Rpredecessor, it cannot 

149 
have an Ssuccessor and is thus Smin in A as well. 

150 
2. There is no such step. 

151 
Pick an Smin element of A. In this case it must be an Rmin 

152 
element of A as well. 

153 

154 
*) 

155 

5316  156 
Goal "[ !i:I. wf(r i); \ 
157 
\ !i:I.!j:I. r i ~= r j > Domain(r i) Int Range(r j) = {} & \ 

158 
\ Domain(r j) Int Range(r i) = {} \ 

159 
\ ] ==> wf(UN i:I. r i)"; 

5318  160 
by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); 
161 
by (Clarify_tac 1); 

162 
by (rename_tac "A a" 1); 

163 
by (case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1); 

164 
by (Clarify_tac 1); 

7249  165 
by (EVERY1[dtac bspec, assume_tac, 
5281  166 
eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]); 
5318  167 
by (EVERY1[etac allE,etac impE]); 
168 
by (Blast_tac 1); 

169 
by (Clarify_tac 1); 

170 
by (rename_tac "z'" 1); 

171 
by (res_inst_tac [("x","z'")] bexI 1); 

172 
by (assume_tac 2); 

173 
by (Clarify_tac 1); 

174 
by (rename_tac "j" 1); 

175 
by (case_tac "r j = r i" 1); 

7249  176 
by (EVERY1[etac allE,etac impE,assume_tac]); 
5318  177 
by (Asm_full_simp_tac 1); 
178 
by (Blast_tac 1); 

179 
by (blast_tac (claset() addEs [equalityE]) 1); 

180 
by (Asm_full_simp_tac 1); 

5521  181 
by (fast_tac (claset() delWrapper "bspec") 1); (*faster than Blast_tac*) 
5281  182 
qed "wf_UN"; 
183 

184 
Goalw [Union_def] 

185 
"[ !r:R. wf r; \ 

186 
\ !r:R.!s:R. r ~= s > Domain r Int Range s = {} & \ 

187 
\ Domain s Int Range r = {} \ 

188 
\ ] ==> wf(Union R)"; 

5318  189 
by (rtac wf_UN 1); 
190 
by (Blast_tac 1); 

191 
by (Blast_tac 1); 

5281  192 
qed "wf_Union"; 
193 

5316  194 
Goal "[ wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \ 
195 
\ ] ==> wf(r Un s)"; 

5318  196 
by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1); 
197 
by (Blast_tac 1); 

198 
by (Blast_tac 1); 

5281  199 
qed "wf_Un"; 
200 

201 
(* 

202 
* Wellfoundedness of `image' 

203 
**) 

204 

205 
Goal "[ wf r; inj f ] ==> wf(prod_fun f f `` r)"; 

5318  206 
by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); 
207 
by (Clarify_tac 1); 

208 
by (case_tac "? p. f p : Q" 1); 

209 
by (eres_inst_tac [("x","{p. f p : Q}")]allE 1); 

210 
by (fast_tac (claset() addDs [injD]) 1); 

211 
by (Blast_tac 1); 

5281  212 
qed "wf_prod_fun_image"; 
213 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

214 
(*** acyclic ***) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

215 

7249  216 
Goalw [acyclic_def] "!x. (x, x) ~: r^+ ==> acyclic r"; 
217 
by (assume_tac 1); 

218 
qed "acyclicI"; 

4750  219 

7249  220 
Goalw [acyclic_def] "wf r ==> acyclic r"; 
4089  221 
by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

222 
qed "wf_acyclic"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

223 

5452  224 
Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"; 
4089  225 
by (simp_tac (simpset() addsimps [trancl_insert]) 1); 
5452  226 
by (blast_tac (claset() addIs [rtrancl_trans]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

227 
qed "acyclic_insert"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

228 
AddIffs [acyclic_insert]; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

229 

5069  230 
Goalw [acyclic_def] "acyclic(r^1) = acyclic r"; 
4746  231 
by (simp_tac (simpset() addsimps [trancl_converse]) 1); 
232 
qed "acyclic_converse"; 

8265  233 
AddIffs [acyclic_converse]; 
234 

235 
Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)"; 

236 
by(blast_tac (claset() addEs [rtranclE] 

237 
addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1); 

238 
qed "acyclic_impl_antisym_rtrancl"; 

239 

240 
(* Other direction: 

241 
acyclic = no loops 

242 
antisym = only self loops 

243 
Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r  Id)"; 

244 
==> "antisym(r^* ) = acyclic(r  Id)"; 

245 
*) 

3198  246 

6433  247 
Goalw [acyclic_def] "[ acyclic s; r <= s ] ==> acyclic r"; 
6814  248 
by (blast_tac (claset() addIs [trancl_mono]) 1); 
6433  249 
qed "acyclic_subset"; 
250 

923  251 
(** cut **) 
252 

253 
(*This rewrite rule works upon formulae; thus it requires explicit use of 

254 
H_cong to expose the equality*) 

7249  255 
Goalw [cut_def] "(cut f r x = cut g r x) = (!y. (y,x):r > f(y)=g(y))"; 
4686  256 
by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1); 
1475  257 
qed "cuts_eq"; 
923  258 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

259 
Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)"; 
1552  260 
by (asm_simp_tac HOL_ss 1); 
923  261 
qed "cut_apply"; 
262 

263 
(*** is_recfun ***) 

264 

5069  265 
Goalw [is_recfun_def,cut_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

266 
"[ is_recfun r H a f; ~(b,a):r ] ==> f(b) = arbitrary"; 
923  267 
by (etac ssubst 1); 
1552  268 
by (asm_simp_tac HOL_ss 1); 
923  269 
qed "is_recfun_undef"; 
270 

7249  271 
(*** NOTE! some simplifications need a different Solver!! ***) 
923  272 
fun indhyp_tac hyps = 
273 
(cut_facts_tac hyps THEN' 

274 
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' 

1465  275 
eresolve_tac [transD, mp, allE])); 
7570  276 
val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac); 
923  277 

5316  278 
Goalw [is_recfun_def,cut_def] 
1475  279 
"[ wf(r); trans(r); is_recfun r H a f; is_recfun r H b g ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

280 
\ (x,a):r > (x,b):r > f(x)=g(x)"; 
923  281 
by (etac wf_induct 1); 
282 
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); 

283 
by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); 

1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

284 
qed_spec_mp "is_recfun_equal"; 
923  285 

286 

287 
val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] 

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

1475  289 
\ is_recfun r H a f; is_recfun r H b g; (b,a):r ] ==> \ 
923  290 
\ cut f r b = g"; 
291 
val gundef = recgb RS is_recfun_undef 

292 
and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); 

293 
by (cut_facts_tac prems 1); 

294 
by (rtac ext 1); 

4686  295 
by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1); 
923  296 
qed "is_recfun_cut"; 
297 

298 
(*** Main Existence Lemma  Basic Properties of the_recfun ***) 

299 

5316  300 
Goalw [the_recfun_def] 
1475  301 
"is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)"; 
5316  302 
by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1); 
923  303 
qed "is_the_recfun"; 
304 

5316  305 
Goal "[ wf(r); trans(r) ] ==> is_recfun r H a (the_recfun r H a)"; 
306 
by (wf_ind_tac "a" [] 1); 

4821  307 
by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] 
308 
is_the_recfun 1); 

309 
by (rewtac is_recfun_def); 

310 
by (stac cuts_eq 1); 

311 
by (Clarify_tac 1); 

7249  312 
by (rtac H_cong2 1); 
4821  313 
by (subgoal_tac 
1475  314 
"the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1); 
7249  315 
by (Blast_tac 2); 
4821  316 
by (etac ssubst 1); 
317 
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); 

318 
by (Clarify_tac 1); 

319 
by (stac cut_apply 1); 

5132  320 
by (fast_tac (claset() addDs [transD]) 1); 
4821  321 
by (fold_tac [is_recfun_def]); 
322 
by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1); 

923  323 
qed "unfold_the_recfun"; 
324 

7249  325 
Goal "[ wf r; trans r; (x,a) : r; (x,b) : r ] \ 
326 
\ ==> the_recfun r H a x = the_recfun r H b x"; 

327 
by (best_tac (claset() addIs [is_recfun_equal, unfold_the_recfun]) 1); 

328 
qed "the_recfun_equal"; 

923  329 

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

1475  331 
val th = rewrite_rule[is_recfun_def] 
332 
(trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun))); 

923  333 

5069  334 
Goalw [wfrec_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

335 
"wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; 
7249  336 
by (rtac H_cong2 1); 
1475  337 
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); 
338 
by (rtac allI 1); 

339 
by (rtac impI 1); 

340 
by (res_inst_tac [("a1","a")] (th RS ssubst) 1); 

7249  341 
by (assume_tac 1); 
7499  342 
by (ftac wf_trancl 1); 
343 
by (ftac r_into_trancl 1); 

1475  344 
by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); 
7249  345 
by (rtac H_cong2 1); (*expose the equality of cuts*) 
1475  346 
by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); 
7249  347 
by (blast_tac (claset() addIs [the_recfun_equal, transD, trans_trancl, 
348 
r_into_trancl]) 1); 

1475  349 
qed "wfrec"; 
350 

351 
(* 

352 
* This form avoids giant explosions in proofs. NOTE USE OF == 

353 
**) 

5316  354 
val rew::prems = goal thy 
1475  355 
"[ f==wfrec r H; wf(r) ] ==> f(a) = H (cut f r a) a"; 
923  356 
by (rewtac rew); 
357 
by (REPEAT (resolve_tac (prems@[wfrec]) 1)); 

358 
qed "def_wfrec"; 

1475  359 

3198  360 

361 
(**** TFL variants ****) 

362 

5278  363 
Goal "!R. wf R > (!P. (!x. (!y. (y,x):R > P y) > P x) > (!x. P x))"; 
3708  364 
by (Clarify_tac 1); 
3198  365 
by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); 
366 
by (assume_tac 1); 

367 
by (Blast_tac 1); 

368 
qed"tfl_wf_induct"; 

369 

5069  370 
Goal "!f R. (x,a):R > (cut f R a)(x) = f(x)"; 
3708  371 
by (Clarify_tac 1); 
3198  372 
by (rtac cut_apply 1); 
373 
by (assume_tac 1); 

374 
qed"tfl_cut_apply"; 

375 

5069  376 
Goal "!M R f. (f=wfrec R M) > wf R > (!x. f x = M (cut f R x) x)"; 
3708  377 
by (Clarify_tac 1); 
4153  378 
by (etac wfrec 1); 
3198  379 
qed "tfl_wfrec"; 