author  wenzelm 
Sat, 25 May 2013 17:40:44 +0200  
changeset 52147  9943f8067f11 
parent 51798  ad3a241def73 
child 56245  84fc7dfa3cd4 
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 *}) 
47966  212 
apply (fastforce iff: NatPRXH) 
20140  213 
apply (erule Nat_ind) 
47966  214 
apply (fastforce iff: NatPRXH)+ 
20140  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 *}) 
47966  221 
apply (fastforce iff: ListPRXH) 
20140  222 
apply (erule List_ind) 
47966  223 
apply (fastforce iff: ListPRXH)+ 
20140  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]) 

41526  256 
apply (assumption  rule letrecT pairT splitT assms)+ 
20140  257 
apply (subst SPLITB) 
41526  258 
apply (assumption  rule ballI SubtypeI assms)+ 
20140  259 
apply (rule SPLITB [THEN subst]) 
41526  260 
apply (assumption  rule letrecT SubtypeI pairT splitT assms  
20140  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]) 

41526  278 
apply (assumption  rule letrecT pairT splitT assms)+ 
20140  279 
apply (simp add: SPLITB) 
41526  280 
apply (assumption  rule ballI SubtypeI assms)+ 
20140  281 
apply (rule lem [THEN subst]) 
41526  282 
apply (assumption  rule letrecT SubtypeI pairT splitT assms  
20140  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 

38500  426 
fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l) 
20140  427 
 bvars _ l = l 
428 

38500  429 
fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t 
430 
 get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t 

431 
 get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t 

432 
 get_bno l n (Const(@{const_name 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 [] 

33317  443 
val ihs = filter could_IH (Logic.strip_assums_hyp Bi) 
20140  444 
val rnames = map (fn x=> 
445 
let val (a,b) = get_bno [] 0 x 

42364  446 
in (nth bvs a, b) end) ihs 
20140  447 
fun try_IHs [] = no_tac 
42364  448 
 try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (nth rls (y  1)) 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 

38500  453 
(Const(@{const_name Trueprop},_) $ (Const(@{const_name 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 
fun clean_ccs_tac ctxt = 
27239  477 
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

478 
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' 
51798  479 
eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' 
480 
hyp_subst_tac ctxt)) 

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

481 
end 
20140  482 

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

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

484 
SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i 
17456  485 

0  486 
end 
20140  487 
*} 
488 

489 

490 
subsection {* Evaluation *} 

491 

492 
ML {* 

47432  493 
structure Eval_Rules = 
494 
Named_Thms(val name = @{binding eval} val description = "evaluation rules"); 

20140  495 

32282
853ef99c04cc
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
wenzelm
parents:
32211
diff
changeset

496 
fun eval_tac ths = 
32283  497 
Subgoal.FOCUS_PREMS (fn {context, prems, ...} => 
47432  498 
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1)); 
499 
*} 

500 
setup Eval_Rules.setup 

20140  501 

47432  502 
method_setup eval = {* 
503 
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)) 

20140  504 
*} 
505 

506 

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

508 

509 
lemma applyV [eval]: 

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

511 
and "b(a) > c" 

512 
shows "f ` a > c" 

41526  513 
unfolding apply_def by (eval assms) 
20140  514 

515 
lemma letV: 

516 
assumes 1: "t > a" 

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

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

519 
apply (unfold let_def) 

520 
apply (rule 1 [THEN canonical]) 

521 
apply (tactic {* 

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

20140  524 
done 
525 

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

527 
apply (unfold fix_def) 

528 
apply (rule applyV) 

529 
apply (rule lamV) 

530 
apply assumption 

531 
done 

532 

533 
lemma letrecV: 

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

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

536 
apply (unfold letrec_def) 

537 
apply (assumption  rule fixV applyV lamV)+ 

538 
done 

539 

540 
lemmas [eval] = letV letrecV fixV 

541 

542 
lemma V_rls [eval]: 

543 
"true > true" 

544 
"false > false" 

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

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

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

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

549 
"zero > zero" 

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

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

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

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

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

555 
"[] > []" 

556 
"!!h t. h$t > h$t" 

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

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

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

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

561 
unfolding data_defs by eval+ 

562 

563 

564 
subsection {* Factorial *} 

565 

36319  566 
schematic_lemma 
20140  567 
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) 
568 
in f(succ(succ(zero))) > ?a" 

569 
by eval 

570 

36319  571 
schematic_lemma 
20140  572 
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) 
573 
in f(succ(succ(succ(zero)))) > ?a" 

574 
by eval 

575 

576 
subsection {* Less Than Or Equal *} 

577 

36319  578 
schematic_lemma 
20140  579 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) 
580 
in f(<succ(zero), succ(zero)>) > ?a" 

581 
by eval 

582 

36319  583 
schematic_lemma 
20140  584 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) 
585 
in f(<succ(zero), succ(succ(succ(succ(zero))))>) > ?a" 

586 
by eval 

587 

36319  588 
schematic_lemma 
20140  589 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) 
590 
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) > ?a" 

591 
by eval 

592 

593 

594 
subsection {* Reverse *} 

595 

36319  596 
schematic_lemma 
20140  597 
"letrec id l be lcase(l,[],%x xs. x$id(xs)) 
598 
in id(zero$succ(zero)$[]) > ?a" 

599 
by eval 

600 

36319  601 
schematic_lemma 
20140  602 
"letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) 
603 
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) > ?a" 

604 
by eval 

605 

606 
end 