author  nipkow 
Sat, 08 Aug 1998 14:00:56 +0200  
changeset 5281  f4d16517b360 
parent 5278  a903b66822e2 
child 5316  7a8975451a89 
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 

9 
open WF; 

10 

950  11 
val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); 
923  12 
val H_cong1 = refl RS H_cong; 
13 

14 
(*Restriction to domain A. If r is wellfounded over A then wf(r)*) 

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

1642  16 
"[ r <= A Times A; \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

17 
\ !!x P. [ ! x. (! y. (y,x) : r > P(y)) > P(x); x:A ] ==> P(x) ] \ 
923  18 
\ ==> wf(r)"; 
3708  19 
by (Clarify_tac 1); 
923  20 
by (rtac allE 1); 
21 
by (assume_tac 1); 

4089  22 
by (best_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); 
923  23 
qed "wfI"; 
24 

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

26 
"[ wf(r); \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

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

4089  30 
by (blast_tac (claset() addIs prems) 1); 
923  31 
qed "wf_induct"; 
32 

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

34 
fun wf_ind_tac a prems i = 

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

1465  36 
rename_last_tac a ["1"] (i+1), 
37 
ares_tac prems i]; 

923  38 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

39 
val prems = goal WF.thy "[ wf(r); (a,x):r; (x,a):r ] ==> P"; 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

40 
by (subgoal_tac "! x. (a,x):r > (x,a):r > P" 1); 
4089  41 
by (blast_tac (claset() addIs prems) 1); 
923  42 
by (wf_ind_tac "a" prems 1); 
2935  43 
by (Blast_tac 1); 
923  44 
qed "wf_asym"; 
45 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

46 
val prems = goal WF.thy "[ wf(r); (a,a): r ] ==> P"; 
923  47 
by (rtac wf_asym 1); 
48 
by (REPEAT (resolve_tac prems 1)); 

1618  49 
qed "wf_irrefl"; 
923  50 

1475  51 
(*transitive closure of a wf relation is wf! *) 
923  52 
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; 
53 
by (rewtac wf_def); 

3708  54 
by (Clarify_tac 1); 
923  55 
(*must retain the universal formula for later use!*) 
56 
by (rtac allE 1 THEN assume_tac 1); 

57 
by (etac mp 1); 

58 
by (res_inst_tac [("a","x")] (prem RS wf_induct) 1); 

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

60 
by (etac tranclE 1); 

2935  61 
by (Blast_tac 1); 
62 
by (Blast_tac 1); 

923  63 
qed "wf_trancl"; 
64 

65 

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

68 
stac (trancl_converse RS sym) 1, 

69 
etac wf_trancl 1]); 

70 

3198  71 
(* 
72 
* Minimalelement characterization of wellfoundedness 

73 
**) 

74 

75 
val wfr::_ = goalw WF.thy [wf_def] 

76 
"wf r ==> x:Q > (? z:Q. ! y. (y,z):r > y~:Q)"; 

77 
by (rtac (wfr RS spec RS mp RS spec) 1); 

78 
by (Blast_tac 1); 

79 
val lemma1 = result(); 

80 

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

82 
"(! 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; 
3457  120 
by (EVERY1[rtac allE, atac, etac impE, Blast_tac]); 
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 

141 
Goal 

142 
"[ !i:I. wf(r i); \ 

143 
\ !i:I.!j:I. r i ~= r j > Domain(r i) Int Range(r j) = {} & \ 

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

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

146 
by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); 

147 
by(Clarify_tac 1); 

148 
by(rename_tac "A a" 1); 

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

150 
by(Clarify_tac 1); 

151 
by(EVERY1[dtac bspec, atac, 

152 
eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]); 

153 
by(EVERY1[etac allE,etac impE]); 

154 
by(Blast_tac 1); 

155 
by(Clarify_tac 1); 

156 
by(rename_tac "z'" 1); 

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

158 
ba 2; 

159 
by(Clarify_tac 1); 

160 
by(rename_tac "j" 1); 

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

162 
by(EVERY1[etac allE,etac impE,atac]); 

163 
by(Asm_full_simp_tac 1); 

164 
by(Blast_tac 1); 

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

166 
by(Asm_full_simp_tac 1); 

167 
by(case_tac "? i. i:I" 1); 

168 
by(Clarify_tac 1); 

169 
by(EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]); 

170 
by(Blast_tac 1); 

171 
by(Blast_tac 1); 

172 
qed "wf_UN"; 

173 

174 
Goalw [Union_def] 

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

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

177 
\ Domain s Int Range r = {} \ 

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

179 
br wf_UN 1; 

180 
by(Blast_tac 1); 

181 
by(Blast_tac 1); 

182 
qed "wf_Union"; 

183 

184 
Goal 

185 
"[ wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \ 

186 
\ ] ==> wf(r Un s)"; 

187 
br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1; 

188 
by(Blast_tac 1); 

189 
by(Blast_tac 1); 

190 
qed "wf_Un"; 

191 

192 
(* 

193 
* Wellfoundedness of `image' 

194 
**) 

195 

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

197 
by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); 

198 
by(Clarify_tac 1); 

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

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

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

202 
by(Blast_tac 1); 

203 
qed "wf_prod_fun_image"; 

204 

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

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

206 

4750  207 
val acyclicI = prove_goalw WF.thy [acyclic_def] 
208 
"!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]); 

209 

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

211 
"wf r ==> acyclic r"; 
4089  212 
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

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

214 

5069  215 
Goalw [acyclic_def] 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3320
diff
changeset

216 
"acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"; 
4089  217 
by (simp_tac (simpset() addsimps [trancl_insert]) 1); 
218 
by (blast_tac (claset() addEs [make_elim rtrancl_trans]) 1); 

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

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

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

221 

5069  222 
Goalw [acyclic_def] "acyclic(r^1) = acyclic r"; 
4746  223 
by (simp_tac (simpset() addsimps [trancl_converse]) 1); 
224 
qed "acyclic_converse"; 

3198  225 

923  226 
(** cut **) 
227 

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

229 
H_cong to expose the equality*) 

5069  230 
Goalw [cut_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset

231 
"(cut f r x = cut g r x) = (!y. (y,x):r > f(y)=g(y))"; 
4686  232 
by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1); 
1475  233 
qed "cuts_eq"; 
923  234 

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

235 
Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)"; 
1552  236 
by (asm_simp_tac HOL_ss 1); 
923  237 
qed "cut_apply"; 
238 

239 
(*** is_recfun ***) 

240 

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

242 
"[ is_recfun r H a f; ~(b,a):r ] ==> f(b) = arbitrary"; 
923  243 
by (etac ssubst 1); 
1552  244 
by (asm_simp_tac HOL_ss 1); 
923  245 
qed "is_recfun_undef"; 
246 

247 
(*** NOTE! some simplifications need a different finish_tac!! ***) 

248 
fun indhyp_tac hyps = 

249 
(cut_facts_tac hyps THEN' 

250 
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' 

1465  251 
eresolve_tac [transD, mp, allE])); 
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2031
diff
changeset

252 
val wf_super_ss = HOL_ss addSolver indhyp_tac; 
923  253 

254 
val prems = goalw WF.thy [is_recfun_def,cut_def] 

1475  255 
"[ 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

256 
\ (x,a):r > (x,b):r > f(x)=g(x)"; 
923  257 
by (cut_facts_tac prems 1); 
258 
by (etac wf_induct 1); 

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

260 
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

261 
qed_spec_mp "is_recfun_equal"; 
923  262 

263 

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

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

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

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

270 
by (cut_facts_tac prems 1); 

271 
by (rtac ext 1); 

4686  272 
by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1); 
923  273 
qed "is_recfun_cut"; 
274 

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

276 

277 
val prems = goalw WF.thy [the_recfun_def] 

1475  278 
"is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)"; 
279 
by (res_inst_tac [("P", "is_recfun r H a")] selectI 1); 

923  280 
by (resolve_tac prems 1); 
281 
qed "is_the_recfun"; 

282 

283 
val prems = goal WF.thy 

4821  284 
"!!r. [ wf(r); trans(r) ] ==> is_recfun r H a (the_recfun r H a)"; 
285 
by (wf_ind_tac "a" prems 1); 

286 
by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] 

287 
is_the_recfun 1); 

288 
by (rewtac is_recfun_def); 

289 
by (stac cuts_eq 1); 

290 
by (Clarify_tac 1); 

291 
by (rtac (refl RSN (2,H_cong)) 1); 

292 
by (subgoal_tac 

1475  293 
"the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1); 
4821  294 
by (etac allE 2); 
295 
by (dtac impE 2); 

296 
by (atac 2); 

1475  297 
by (atac 3); 
4821  298 
by (atac 2); 
299 
by (etac ssubst 1); 

300 
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); 

301 
by (Clarify_tac 1); 

302 
by (stac cut_apply 1); 

5132  303 
by (fast_tac (claset() addDs [transD]) 1); 
4821  304 
by (rtac (refl RSN (2,H_cong)) 1); 
305 
by (fold_tac [is_recfun_def]); 

306 
by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1); 

923  307 
qed "unfold_the_recfun"; 
308 

1475  309 
val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun; 
923  310 

1475  311 
(*Old proof 
923  312 
val prems = goal WF.thy 
1475  313 
"[ wf(r); trans(r) ] ==> is_recfun r H a (the_recfun r H a)"; 
314 
by (cut_facts_tac prems 1); 

315 
by (wf_ind_tac "a" prems 1); 

316 
by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); 

317 
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); 

2031  318 
by (stac cuts_eq 1); 
1475  319 
(*Applying the substitution: must keep the quantified assumption!!*) 
3708  320 
by (EVERY1 [Clarify_tac, rtac H_cong1, rtac allE, atac, 
1475  321 
etac (mp RS ssubst), atac]); 
322 
by (fold_tac [is_recfun_def]); 

323 
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); 

324 
qed "unfold_the_recfun"; 

325 
*) 

923  326 

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

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

923  330 

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

332 
"wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; 
1475  333 
by (rtac H_cong 1); 
334 
by (rtac refl 2); 

335 
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); 

336 
by (rtac allI 1); 

337 
by (rtac impI 1); 

338 
by (simp_tac(HOL_ss addsimps [wfrec_def]) 1); 

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

340 
by (atac 1); 

341 
by (forward_tac[wf_trancl] 1); 

342 
by (forward_tac[r_into_trancl] 1); 

343 
by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); 

344 
by (rtac H_cong 1); (*expose the equality of cuts*) 

345 
by (rtac refl 2); 

346 
by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); 

3708  347 
by (Clarify_tac 1); 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

348 
by (res_inst_tac [("r","r^+")] is_recfun_equal 1); 
1475  349 
by (atac 1); 
350 
by (rtac trans_trancl 1); 

351 
by (rtac unfold_the_recfun 1); 

352 
by (atac 1); 

353 
by (rtac trans_trancl 1); 

354 
by (rtac unfold_the_recfun 1); 

355 
by (atac 1); 

356 
by (rtac trans_trancl 1); 

357 
by (rtac transD 1); 

358 
by (rtac trans_trancl 1); 

4762  359 
by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1); 
1475  360 
by (atac 1); 
361 
by (atac 1); 

4762  362 
by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1); 
1475  363 
by (atac 1); 
364 
qed "wfrec"; 

365 

366 
(*Old proof 

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

368 
"wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; 
923  369 
by (etac (wf_trancl RS wftrec RS ssubst) 1); 
370 
by (rtac trans_trancl 1); 

371 
by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) 

1475  372 
by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); 
923  373 
qed "wfrec"; 
1475  374 
*) 
923  375 

1475  376 
(* 
377 
* This form avoids giant explosions in proofs. NOTE USE OF == 

378 
**) 

923  379 
val rew::prems = goal WF.thy 
1475  380 
"[ f==wfrec r H; wf(r) ] ==> f(a) = H (cut f r a) a"; 
923  381 
by (rewtac rew); 
382 
by (REPEAT (resolve_tac (prems@[wfrec]) 1)); 

383 
qed "def_wfrec"; 

1475  384 

3198  385 

386 
(**** TFL variants ****) 

387 

5278  388 
Goal "!R. wf R > (!P. (!x. (!y. (y,x):R > P y) > P x) > (!x. P x))"; 
3708  389 
by (Clarify_tac 1); 
3198  390 
by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); 
391 
by (assume_tac 1); 

392 
by (Blast_tac 1); 

393 
qed"tfl_wf_induct"; 

394 

5069  395 
Goal "!f R. (x,a):R > (cut f R a)(x) = f(x)"; 
3708  396 
by (Clarify_tac 1); 
3198  397 
by (rtac cut_apply 1); 
398 
by (assume_tac 1); 

399 
qed"tfl_cut_apply"; 

400 

5069  401 
Goal "!M R f. (f=wfrec R M) > wf R > (!x. f x = M (cut f R x) x)"; 
3708  402 
by (Clarify_tac 1); 
4153  403 
by (etac wfrec 1); 
3198  404 
qed "tfl_wfrec"; 