author  wenzelm 
Wed, 28 Dec 2011 13:00:51 +0100  
changeset 46003  c0fe5e8e4864 
parent 45294  3c5d3d286055 
child 47432  e1576d13e933 
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]) 

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 
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 

45294  498 
structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules"); 
20140  499 
in 
500 

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

501 
fun eval_tac ths = 
32283  502 
Subgoal.FOCUS_PREMS (fn {context, prems, ...} => 
32282
853ef99c04cc
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
wenzelm
parents:
32211
diff
changeset

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

505 
val eval_setup = 

24034  506 
Data.setup #> 
30515  507 
Method.setup @{binding eval} 
32282
853ef99c04cc
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
wenzelm
parents:
32211
diff
changeset

508 
(Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))) 
30515  509 
"evaluation"; 
20140  510 

511 
end; 

512 

513 
*} 

514 

515 
setup eval_setup 

516 

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

518 

519 
lemma applyV [eval]: 

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

521 
and "b(a) > c" 

522 
shows "f ` a > c" 

41526  523 
unfolding apply_def by (eval assms) 
20140  524 

525 
lemma letV: 

526 
assumes 1: "t > a" 

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

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

529 
apply (unfold let_def) 

530 
apply (rule 1 [THEN canonical]) 

531 
apply (tactic {* 

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

20140  534 
done 
535 

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

537 
apply (unfold fix_def) 

538 
apply (rule applyV) 

539 
apply (rule lamV) 

540 
apply assumption 

541 
done 

542 

543 
lemma letrecV: 

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

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

546 
apply (unfold letrec_def) 

547 
apply (assumption  rule fixV applyV lamV)+ 

548 
done 

549 

550 
lemmas [eval] = letV letrecV fixV 

551 

552 
lemma V_rls [eval]: 

553 
"true > true" 

554 
"false > false" 

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

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

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

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

559 
"zero > zero" 

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

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

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

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

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

565 
"[] > []" 

566 
"!!h t. h$t > h$t" 

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

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

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

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

571 
unfolding data_defs by eval+ 

572 

573 

574 
subsection {* Factorial *} 

575 

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

579 
by eval 

580 

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

584 
by eval 

585 

586 
subsection {* Less Than Or Equal *} 

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(zero), succ(zero)>) > ?a" 

591 
by eval 

592 

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

596 
by eval 

597 

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

601 
by eval 

602 

603 

604 
subsection {* Reverse *} 

605 

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

609 
by eval 

610 

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

614 
by eval 

615 

616 
end 