author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 29269  5c25a2012975 
child 30510  4120fc59dd85 
permissions  rwrr 
17456  1 
(* Title: CCL/Wfd.thy 
1474  2 
Author: Martin Coen, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

17456  6 
header {* Wellfounded relations in CCL *} 
7 

8 
theory Wfd 

9 
imports Trancl Type Hered 

10 
begin 

0  11 

12 
consts 

13 
(*** Predicates ***) 

14 
Wfd :: "[i set] => o" 

15 
(*** Relations ***) 

16 
wf :: "[i set] => i set" 

17 
wmap :: "[i=>i,i set] => i set" 

24825  18 
lex :: "[i set,i set] => i set" (infixl "**" 70) 
0  19 
NatPR :: "i set" 
20 
ListPR :: "i set => i set" 

21 

24825  22 
defs 
0  23 

17456  24 
Wfd_def: 
3837  25 
"Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R > y:P) > x:P) > (ALL a. a:P)" 
0  26 

17456  27 
wf_def: "wf(R) == {x. x:R & Wfd(R)}" 
0  28 

17456  29 
wmap_def: "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}" 
30 
lex_def: 

3837  31 
"ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra  (a=a' & <b,b'> : rb))}" 
0  32 

17456  33 
NatPR_def: "NatPR == {p. EX x:Nat. p=<x,succ(x)>}" 
34 
ListPR_def: "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}" 

35 

20140  36 

37 
lemma wfd_induct: 

38 
assumes 1: "Wfd(R)" 

39 
and 2: "!!x.[ ALL y. <y,x>: R > P(y) ] ==> P(x)" 

40 
shows "P(a)" 

41 
apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD]) 

42 
using 2 apply blast 

43 
done 

44 

45 
lemma wfd_strengthen_lemma: 

46 
assumes 1: "!!x y.<x,y> : R ==> Q(x)" 

47 
and 2: "ALL x. (ALL y. <y,x> : R > y : P) > x : P" 

48 
and 3: "!!x. Q(x) ==> x:P" 

49 
shows "a:P" 

50 
apply (rule 2 [rule_format]) 

51 
using 1 3 

52 
apply blast 

53 
done 

54 

55 
ML {* 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset

56 
fun wfd_strengthen_tac ctxt s i = 
27239  57 
res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) 
20140  58 
*} 
59 

60 
lemma wf_anti_sym: "[ Wfd(r); <a,x>:r; <x,a>:r ] ==> P" 

61 
apply (subgoal_tac "ALL x. <a,x>:r > <x,a>:r > P") 

62 
apply blast 

63 
apply (erule wfd_induct) 

64 
apply blast 

65 
done 

66 

67 
lemma wf_anti_refl: "[ Wfd(r); <a,a>: r ] ==> P" 

68 
apply (rule wf_anti_sym) 

69 
apply assumption+ 

70 
done 

71 

72 

73 
subsection {* Irreflexive transitive closure *} 

74 

75 
lemma trancl_wf: 

76 
assumes 1: "Wfd(R)" 

77 
shows "Wfd(R^+)" 

78 
apply (unfold Wfd_def) 

79 
apply (rule allI ballI impI)+ 

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

81 
apply (rule allE, assumption) 

82 
apply (erule mp) 

83 
apply (rule 1 [THEN wfd_induct]) 

84 
apply (rule impI [THEN allI]) 

85 
apply (erule tranclE) 

86 
apply blast 

87 
apply (erule spec [THEN mp, THEN spec, THEN mp]) 

88 
apply assumption+ 

89 
done 

90 

91 

92 
subsection {* Lexicographic Ordering *} 

93 

94 
lemma lexXH: 

95 
"p : ra**rb <> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra  a=a' & <b,b'> : rb))" 

96 
unfolding lex_def by blast 

97 

98 
lemma lexI1: "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb" 

99 
by (blast intro!: lexXH [THEN iffD2]) 

100 

101 
lemma lexI2: "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb" 

102 
by (blast intro!: lexXH [THEN iffD2]) 

103 

104 
lemma lexE: 

105 
assumes 1: "p : ra**rb" 

106 
and 2: "!!a a' b b'.[ <a,a'> : ra; p=<<a,b>,<a',b'>> ] ==> R" 

107 
and 3: "!!a b b'.[ <b,b'> : rb; p = <<a,b>,<a,b'>> ] ==> R" 

108 
shows R 

109 
apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE]) 

110 
using 2 3 

111 
apply blast 

112 
done 

113 

114 
lemma lex_pair: "[ p : r**s; !!a a' b b'. p = <<a,b>,<a',b'>> ==> P ] ==>P" 

115 
apply (erule lexE) 

116 
apply blast+ 

117 
done 

118 

119 
lemma lex_wf: 

120 
assumes 1: "Wfd(R)" 

121 
and 2: "Wfd(S)" 

122 
shows "Wfd(R**S)" 

123 
apply (unfold Wfd_def) 

124 
apply safe 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset

125 
apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *}) 
20140  126 
apply (blast elim!: lex_pair) 
127 
apply (subgoal_tac "ALL a b.<a,b>:P") 

128 
apply blast 

129 
apply (rule 1 [THEN wfd_induct, THEN allI]) 

130 
apply (rule 2 [THEN wfd_induct, THEN allI]) back 

131 
apply (fast elim!: lexE) 

132 
done 

133 

134 

135 
subsection {* Mapping *} 

136 

137 
lemma wmapXH: "p : wmap(f,r) <> (EX x y. p=<x,y> & <f(x),f(y)> : r)" 

138 
unfolding wmap_def by blast 

139 

140 
lemma wmapI: "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)" 

141 
by (blast intro!: wmapXH [THEN iffD2]) 

142 

143 
lemma wmapE: "[ p : wmap(f,r); !!a b.[ <f(a),f(b)> : r; p=<a,b> ] ==> R ] ==> R" 

144 
by (blast dest!: wmapXH [THEN iffD1]) 

145 

146 
lemma wmap_wf: 

147 
assumes 1: "Wfd(r)" 

148 
shows "Wfd(wmap(f,r))" 

149 
apply (unfold Wfd_def) 

150 
apply clarify 

151 
apply (subgoal_tac "ALL b. ALL a. f (a) =b>a:P") 

152 
apply blast 

153 
apply (rule 1 [THEN wfd_induct, THEN allI]) 

154 
apply clarify 

155 
apply (erule spec [THEN mp]) 

156 
apply (safe elim!: wmapE) 

157 
apply (erule spec [THEN mp, THEN spec, THEN mp]) 

158 
apply assumption 

159 
apply (rule refl) 

160 
done 

161 

162 

163 
subsection {* Projections *} 

164 

165 
lemma wfstI: "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)" 

166 
apply (rule wmapI) 

167 
apply simp 

168 
done 

169 

170 
lemma wsndI: "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)" 

171 
apply (rule wmapI) 

172 
apply simp 

173 
done 

174 

175 
lemma wthdI: "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)" 

176 
apply (rule wmapI) 

177 
apply simp 

178 
done 

179 

180 

181 
subsection {* Ground wellfounded relations *} 

182 

183 
lemma wfI: "[ Wfd(r); a : r ] ==> a : wf(r)" 

184 
unfolding wf_def by blast 

185 

186 
lemma Empty_wf: "Wfd({})" 

187 
unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE]) 

188 

189 
lemma wf_wf: "Wfd(wf(R))" 

190 
unfolding wf_def 

191 
apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE]) 

192 
apply simp_all 

193 
apply (rule Empty_wf) 

194 
done 

195 

196 
lemma NatPRXH: "p : NatPR <> (EX x:Nat. p=<x,succ(x)>)" 

197 
unfolding NatPR_def by blast 

198 

199 
lemma ListPRXH: "p : ListPR(A) <> (EX h:A. EX t:List(A).p=<t,h$t>)" 

200 
unfolding ListPR_def by blast 

201 

202 
lemma NatPRI: "x : Nat ==> <x,succ(x)> : NatPR" 

203 
by (auto simp: NatPRXH) 

204 

205 
lemma ListPRI: "[ t : List(A); h : A ] ==> <t,h $ t> : ListPR(A)" 

206 
by (auto simp: ListPRXH) 

207 

208 
lemma NatPR_wf: "Wfd(NatPR)" 

209 
apply (unfold Wfd_def) 

210 
apply clarify 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset

211 
apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *}) 
20140  212 
apply (fastsimp iff: NatPRXH) 
213 
apply (erule Nat_ind) 

214 
apply (fastsimp iff: NatPRXH)+ 

215 
done 

216 

217 
lemma ListPR_wf: "Wfd(ListPR(A))" 

218 
apply (unfold Wfd_def) 

219 
apply clarify 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset

220 
apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *}) 
20140  221 
apply (fastsimp iff: ListPRXH) 
222 
apply (erule List_ind) 

223 
apply (fastsimp iff: ListPRXH)+ 

224 
done 

225 

226 

227 
subsection {* General Recursive Functions *} 

228 

229 
lemma letrecT: 

230 
assumes 1: "a : A" 

231 
and 2: "!!p g.[ p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) ] ==> h(p,g) : D(p)" 

232 
shows "letrec g x be h(x,g) in g(a) : D(a)" 

233 
apply (rule 1 [THEN rev_mp]) 

234 
apply (rule wf_wf [THEN wfd_induct]) 

235 
apply (subst letrecB) 

236 
apply (rule impI) 

237 
apply (erule 2) 

238 
apply blast 

239 
done 

240 

241 
lemma SPLITB: "SPLIT(<a,b>,B) = B(a,b)" 

242 
unfolding SPLIT_def 

243 
apply (rule set_ext) 

244 
apply blast 

245 
done 

17456  246 

20140  247 
lemma letrec2T: 
248 
assumes "a : A" 

249 
and "b : B" 

250 
and "!!p q g.[ p:A; q:B; 

251 
ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) ] ==> 

252 
h(p,q,g) : D(p,q)" 

253 
shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)" 

254 
apply (unfold letrec2_def) 

255 
apply (rule SPLITB [THEN subst]) 

256 
apply (assumption  rule letrecT pairT splitT prems)+ 

257 
apply (subst SPLITB) 

258 
apply (assumption  rule ballI SubtypeI prems)+ 

259 
apply (rule SPLITB [THEN subst]) 

260 
apply (assumption  rule letrecT SubtypeI pairT splitT prems  

261 
erule bspec SubtypeE sym [THEN subst])+ 

262 
done 

263 

264 
lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)" 

265 
by (simp add: SPLITB) 

266 

267 
lemma letrec3T: 

268 
assumes "a : A" 

269 
and "b : B" 

270 
and "c : C" 

271 
and "!!p q r g.[ p:A; q:B; r:C; 

272 
ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. 

273 
g(x,y,z) : D(x,y,z) ] ==> 

274 
h(p,q,r,g) : D(p,q,r)" 

275 
shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)" 

276 
apply (unfold letrec3_def) 

277 
apply (rule lem [THEN subst]) 

278 
apply (assumption  rule letrecT pairT splitT prems)+ 

279 
apply (simp add: SPLITB) 

280 
apply (assumption  rule ballI SubtypeI prems)+ 

281 
apply (rule lem [THEN subst]) 

282 
apply (assumption  rule letrecT SubtypeI pairT splitT prems  

283 
erule bspec SubtypeE sym [THEN subst])+ 

284 
done 

285 

286 
lemmas letrecTs = letrecT letrec2T letrec3T 

287 

288 

289 
subsection {* Type Checking for Recursive Calls *} 

290 

291 
lemma rcallT: 

292 
"[ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); 

293 
g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) ] ==> 

294 
g(a) : E" 

295 
by blast 

296 

297 
lemma rcall2T: 

298 
"[ ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); 

299 
g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) ] ==> 

300 
g(a,b) : E" 

301 
by blast 

302 

303 
lemma rcall3T: 

304 
"[ ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); 

305 
g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; 

306 
a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) ] ==> 

307 
g(a,b,c) : E" 

308 
by blast 

309 

310 
lemmas rcallTs = rcallT rcall2T rcall3T 

311 

312 

313 
subsection {* Instantiating an induction hypothesis with an equality assumption *} 

314 

315 
lemma hyprcallT: 

316 
assumes 1: "g(a) = b" 

317 
and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)" 

318 
and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P" 

319 
and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A" 

320 
and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R)" 

321 
shows P 

322 
apply (rule 3 [OF 2, OF 1 [symmetric]]) 

323 
apply (rule rcallT [OF 2]) 

324 
apply assumption 

325 
apply (rule 4 [OF 2]) 

326 
apply (rule 5 [OF 2]) 

327 
done 

328 

329 
lemma hyprcall2T: 

330 
assumes 1: "g(a,b) = c" 

331 
and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)" 

332 
and 3: "[ c=g(a,b); g(a,b) : D(a,b) ] ==> P" 

333 
and 4: "a:A" 

334 
and 5: "b:B" 

335 
and 6: "<<a,b>,<p,q>>:wf(R)" 

336 
shows P 

337 
apply (rule 3) 

338 
apply (rule 1 [symmetric]) 

339 
apply (rule rcall2T) 

23467  340 
apply (rule 2) 
341 
apply assumption 

342 
apply (rule 4) 

343 
apply (rule 5) 

344 
apply (rule 6) 

20140  345 
done 
346 

347 
lemma hyprcall3T: 

348 
assumes 1: "g(a,b,c) = d" 

349 
and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z)" 

350 
and 3: "[ d=g(a,b,c); g(a,b,c) : D(a,b,c) ] ==> P" 

351 
and 4: "a:A" 

352 
and 5: "b:B" 

353 
and 6: "c:C" 

354 
and 7: "<<a,<b,c>>,<p,<q,r>>> : wf(R)" 

355 
shows P 

356 
apply (rule 3) 

357 
apply (rule 1 [symmetric]) 

358 
apply (rule rcall3T) 

23467  359 
apply (rule 2) 
360 
apply assumption 

361 
apply (rule 4) 

362 
apply (rule 5) 

363 
apply (rule 6) 

364 
apply (rule 7) 

20140  365 
done 
366 

367 
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T 

368 

369 

370 
subsection {* Rules to Remove Induction Hypotheses after Type Checking *} 

371 

372 
lemma rmIH1: "[ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P ] ==> P" . 

373 

374 
lemma rmIH2: "[ ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P ] ==> P" . 

375 

376 
lemma rmIH3: 

377 
"[ ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); 

378 
P ] ==> 

379 
P" . 

380 

381 
lemmas rmIHs = rmIH1 rmIH2 rmIH3 

382 

383 

384 
subsection {* Lemmas for constructors and subtypes *} 

385 

386 
(* 0ary constructors do not need additional rules as they are handled *) 

387 
(* correctly by applying SubtypeI *) 

388 

389 
lemma Subtype_canTs: 

390 
"!!a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}" 

391 
"!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}" 

392 
"!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}" 

393 
"!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}" 

394 
"!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" 

395 
by (assumption  rule SubtypeI canTs icanTs  erule SubtypeE)+ 

396 

397 
lemma letT: "[ f(t):B; ~t=bot ] ==> let x be t in f(x) : B" 

398 
apply (erule letB [THEN ssubst]) 

399 
apply assumption 

400 
done 

401 

402 
lemma applyT2: "[ a:A; f : Pi(A,B) ] ==> f ` a : B(a)" 

403 
apply (erule applyT) 

404 
apply assumption 

405 
done 

406 

407 
lemma rcall_lemma1: "[ a:A; a:A ==> P(a) ] ==> a : {x:A. P(x)}" 

408 
by blast 

409 

410 
lemma rcall_lemma2: "[ a:{x:A. Q(x)}; [ a:A; Q(a) ] ==> P(a) ] ==> a : {x:A. P(x)}" 

411 
by blast 

412 

413 
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2 

414 

415 

416 
subsection {* Typechecking *} 

417 

418 
ML {* 

419 

420 
local 

421 

422 
val type_rls = 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

423 
@{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @ 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

424 
@{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs}; 
20140  425 

426 
fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) 

427 
 bvars _ l = l 

428 

429 
fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t 

430 
 get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t 

431 
 get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t 

24825  432 
 get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t 
20140  433 
 get_bno l n (t $ s) = get_bno l n t 
434 
 get_bno l n (Bound m) = (mlength(l),n) 

435 

436 
(* Not a great way of identifying induction hypothesis! *) 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29264
diff
changeset

437 
fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29264
diff
changeset

438 
Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29264
diff
changeset

439 
Term.could_unify(x,hd (prems_of @{thm rcall3T})) 
20140  440 

441 
fun IHinst tac rls = SUBGOAL (fn (Bi,i) => 

442 
let val bvs = bvars Bi [] 

443 
val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi) 

444 
val rnames = map (fn x=> 

445 
let val (a,b) = get_bno [] 0 x 

446 
in (List.nth(bvs,a),b) end) ihs 

447 
fun try_IHs [] = no_tac 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

448 
 try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y1)) i ORELSE (try_IHs xs) 
20140  449 
in try_IHs rnames end) 
450 

451 
fun is_rigid_prog t = 

452 
case (Logic.strip_assums_concl t) of 

29264  453 
(Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a []) 
20140  454 
 _ => false 
455 
in 

456 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

457 
fun rcall_tac ctxt i = 
27239  458 
let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i 
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

459 
in IHinst tac @{thms rcallTs} i end 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

460 
THEN eresolve_tac @{thms rcall_lemmas} i 
20140  461 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

462 
fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

463 
rcall_tac ctxt i ORELSE 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

464 
ematch_tac [@{thm SubtypeE}] i ORELSE 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

465 
match_tac [@{thm SubtypeI}] i 
20140  466 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

467 
fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) => 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

468 
if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac) 
20140  469 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

470 
fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i 
20140  471 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

472 
fun tac ctxt = typechk_tac ctxt [] 1 
20140  473 

474 
(*** Clean up Correctness Condictions ***) 

475 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

476 
val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' 
20140  477 
hyp_subst_tac) 
478 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

479 
fun clean_ccs_tac ctxt = 
27239  480 
let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in 
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

481 
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

482 
eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

483 
hyp_subst_tac)) 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

484 
end 
20140  485 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

486 
fun gen_ccs_tac ctxt rls i = 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset

487 
SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i 
17456  488 

0  489 
end 
20140  490 
*} 
491 

492 

493 
subsection {* Evaluation *} 

494 

495 
ML {* 

496 

497 
local 

24034  498 
structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules"); 
20140  499 
in 
500 

501 
fun eval_tac ctxt ths = 

502 
METAHYPS (fn prems => 

24034  503 
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get ctxt) 1)) 1; 
20140  504 

505 
val eval_setup = 

24034  506 
Data.setup #> 
20140  507 
Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt => 
508 
Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")]; 

509 

510 
end; 

511 

512 
*} 

513 

514 
setup eval_setup 

515 

516 
lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam 

517 

518 
lemma applyV [eval]: 

519 
assumes "f > lam x. b(x)" 

520 
and "b(a) > c" 

521 
shows "f ` a > c" 

522 
unfolding apply_def by (eval prems) 

523 

524 
lemma letV: 

525 
assumes 1: "t > a" 

526 
and 2: "f(a) > c" 

527 
shows "let x be t in f(x) > c" 

528 
apply (unfold let_def) 

529 
apply (rule 1 [THEN canonical]) 

530 
apply (tactic {* 

26391  531 
REPEAT (DEPTH_SOLVE_1 (resolve_tac (@{thms assms} @ @{thms eval_rls}) 1 ORELSE 
532 
etac @{thm substitute} 1)) *}) 

20140  533 
done 
534 

535 
lemma fixV: "f(fix(f)) > c ==> fix(f) > c" 

536 
apply (unfold fix_def) 

537 
apply (rule applyV) 

538 
apply (rule lamV) 

539 
apply assumption 

540 
done 

541 

542 
lemma letrecV: 

543 
"h(t,%y. letrec g x be h(x,g) in g(y)) > c ==> 

544 
letrec g x be h(x,g) in g(t) > c" 

545 
apply (unfold letrec_def) 

546 
apply (assumption  rule fixV applyV lamV)+ 

547 
done 

548 

549 
lemmas [eval] = letV letrecV fixV 

550 

551 
lemma V_rls [eval]: 

552 
"true > true" 

553 
"false > false" 

554 
"!!b c t u. [ b>true; t>c ] ==> if b then t else u > c" 

555 
"!!b c t u. [ b>false; u>c ] ==> if b then t else u > c" 

556 
"!!a b. <a,b> > <a,b>" 

557 
"!!a b c t h. [ t > <a,b>; h(a,b) > c ] ==> split(t,h) > c" 

558 
"zero > zero" 

559 
"!!n. succ(n) > succ(n)" 

560 
"!!c n t u. [ n > zero; t > c ] ==> ncase(n,t,u) > c" 

561 
"!!c n t u x. [ n > succ(x); u(x) > c ] ==> ncase(n,t,u) > c" 

562 
"!!c n t u. [ n > zero; t > c ] ==> nrec(n,t,u) > c" 

563 
"!!c n t u x. [ n>succ(x); u(x,nrec(x,t,u))>c ] ==> nrec(n,t,u)>c" 

564 
"[] > []" 

565 
"!!h t. h$t > h$t" 

566 
"!!c l t u. [ l > []; t > c ] ==> lcase(l,t,u) > c" 

567 
"!!c l t u x xs. [ l > x$xs; u(x,xs) > c ] ==> lcase(l,t,u) > c" 

568 
"!!c l t u. [ l > []; t > c ] ==> lrec(l,t,u) > c" 

569 
"!!c l t u x xs. [ l>x$xs; u(x,xs,lrec(xs,t,u))>c ] ==> lrec(l,t,u)>c" 

570 
unfolding data_defs by eval+ 

571 

572 

573 
subsection {* Factorial *} 

574 

575 
lemma 

576 
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) 

577 
in f(succ(succ(zero))) > ?a" 

578 
by eval 

579 

580 
lemma 

581 
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) 

582 
in f(succ(succ(succ(zero)))) > ?a" 

583 
by eval 

584 

585 
subsection {* Less Than Or Equal *} 

586 

587 
lemma 

588 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) 

589 
in f(<succ(zero), succ(zero)>) > ?a" 

590 
by eval 

591 

592 
lemma 

593 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) 

594 
in f(<succ(zero), succ(succ(succ(succ(zero))))>) > ?a" 

595 
by eval 

596 

597 
lemma 

598 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) 

599 
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) > ?a" 

600 
by eval 

601 

602 

603 
subsection {* Reverse *} 

604 

605 
lemma 

606 
"letrec id l be lcase(l,[],%x xs. x$id(xs)) 

607 
in id(zero$succ(zero)$[]) > ?a" 

608 
by eval 

609 

610 
lemma 

611 
"letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) 

612 
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) > ?a" 

613 
by eval 

614 

615 
end 