author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 57945  cacb00a569e0 
child 58889  5b7a9633cfa8 
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 

57521  12 
definition Wfd :: "[i set] => o" 
13 
where "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R > y:P) > x:P) > (ALL a. a:P)" 

0  14 

57521  15 
definition wf :: "[i set] => i set" 
16 
where "wf(R) == {x. x:R & Wfd(R)}" 

17 

18 
definition wmap :: "[i=>i,i set] => i set" 

19 
where "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}" 

0  20 

57521  21 
definition lex :: "[i set,i set] => i set" (infixl "**" 70) 
22 
where "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra  (a=a' & <b,b'> : rb))}" 

0  23 

57521  24 
definition NatPR :: "i set" 
25 
where "NatPR == {p. EX x:Nat. p=<x,succ(x)>}" 

0  26 

57521  27 
definition ListPR :: "i set => i set" 
28 
where "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}" 

17456  29 

20140  30 

31 
lemma wfd_induct: 

32 
assumes 1: "Wfd(R)" 

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

34 
shows "P(a)" 

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

36 
using 2 apply blast 

37 
done 

38 

39 
lemma wfd_strengthen_lemma: 

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

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

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

43 
shows "a:P" 

44 
apply (rule 2 [rule_format]) 

45 
using 1 3 

46 
apply blast 

47 
done 

48 

49 
ML {* 

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

50 
fun wfd_strengthen_tac ctxt s i = 
27239  51 
res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) 
20140  52 
*} 
53 

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

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

56 
apply blast 

57 
apply (erule wfd_induct) 

58 
apply blast 

59 
done 

60 

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

62 
apply (rule wf_anti_sym) 

63 
apply assumption+ 

64 
done 

65 

66 

67 
subsection {* Irreflexive transitive closure *} 

68 

69 
lemma trancl_wf: 

70 
assumes 1: "Wfd(R)" 

71 
shows "Wfd(R^+)" 

72 
apply (unfold Wfd_def) 

73 
apply (rule allI ballI impI)+ 

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

75 
apply (rule allE, assumption) 

76 
apply (erule mp) 

77 
apply (rule 1 [THEN wfd_induct]) 

78 
apply (rule impI [THEN allI]) 

79 
apply (erule tranclE) 

80 
apply blast 

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

82 
apply assumption+ 

83 
done 

84 

85 

86 
subsection {* Lexicographic Ordering *} 

87 

88 
lemma lexXH: 

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

90 
unfolding lex_def by blast 

91 

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

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

94 

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

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

97 

98 
lemma lexE: 

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

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

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

102 
shows R 

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

104 
using 2 3 

105 
apply blast 

106 
done 

107 

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

109 
apply (erule lexE) 

110 
apply blast+ 

111 
done 

112 

113 
lemma lex_wf: 

114 
assumes 1: "Wfd(R)" 

115 
and 2: "Wfd(S)" 

116 
shows "Wfd(R**S)" 

117 
apply (unfold Wfd_def) 

118 
apply safe 

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

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

122 
apply blast 

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

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

125 
apply (fast elim!: lexE) 

126 
done 

127 

128 

129 
subsection {* Mapping *} 

130 

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

132 
unfolding wmap_def by blast 

133 

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

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

136 

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

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

139 

140 
lemma wmap_wf: 

141 
assumes 1: "Wfd(r)" 

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

143 
apply (unfold Wfd_def) 

144 
apply clarify 

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

146 
apply blast 

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

148 
apply clarify 

149 
apply (erule spec [THEN mp]) 

150 
apply (safe elim!: wmapE) 

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

152 
apply assumption 

153 
apply (rule refl) 

154 
done 

155 

156 

157 
subsection {* Projections *} 

158 

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

160 
apply (rule wmapI) 

161 
apply simp 

162 
done 

163 

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

165 
apply (rule wmapI) 

166 
apply simp 

167 
done 

168 

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

170 
apply (rule wmapI) 

171 
apply simp 

172 
done 

173 

174 

175 
subsection {* Ground wellfounded relations *} 

176 

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

178 
unfolding wf_def by blast 

179 

180 
lemma Empty_wf: "Wfd({})" 

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

182 

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

184 
unfolding wf_def 

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

186 
apply simp_all 

187 
apply (rule Empty_wf) 

188 
done 

189 

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

191 
unfolding NatPR_def by blast 

192 

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

194 
unfolding ListPR_def by blast 

195 

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

197 
by (auto simp: NatPRXH) 

198 

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

200 
by (auto simp: ListPRXH) 

201 

202 
lemma NatPR_wf: "Wfd(NatPR)" 

203 
apply (unfold Wfd_def) 

204 
apply clarify 

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

205 
apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *}) 
47966  206 
apply (fastforce iff: NatPRXH) 
20140  207 
apply (erule Nat_ind) 
47966  208 
apply (fastforce iff: NatPRXH)+ 
20140  209 
done 
210 

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

212 
apply (unfold Wfd_def) 

213 
apply clarify 

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

214 
apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *}) 
47966  215 
apply (fastforce iff: ListPRXH) 
20140  216 
apply (erule List_ind) 
47966  217 
apply (fastforce iff: ListPRXH)+ 
20140  218 
done 
219 

220 

221 
subsection {* General Recursive Functions *} 

222 

223 
lemma letrecT: 

224 
assumes 1: "a : A" 

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

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

227 
apply (rule 1 [THEN rev_mp]) 

228 
apply (rule wf_wf [THEN wfd_induct]) 

229 
apply (subst letrecB) 

230 
apply (rule impI) 

231 
apply (erule 2) 

232 
apply blast 

233 
done 

234 

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

236 
unfolding SPLIT_def 

237 
apply (rule set_ext) 

238 
apply blast 

239 
done 

17456  240 

20140  241 
lemma letrec2T: 
242 
assumes "a : A" 

243 
and "b : B" 

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

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

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

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

248 
apply (unfold letrec2_def) 

249 
apply (rule SPLITB [THEN subst]) 

41526  250 
apply (assumption  rule letrecT pairT splitT assms)+ 
20140  251 
apply (subst SPLITB) 
41526  252 
apply (assumption  rule ballI SubtypeI assms)+ 
20140  253 
apply (rule SPLITB [THEN subst]) 
41526  254 
apply (assumption  rule letrecT SubtypeI pairT splitT assms  
20140  255 
erule bspec SubtypeE sym [THEN subst])+ 
256 
done 

257 

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

259 
by (simp add: SPLITB) 

260 

261 
lemma letrec3T: 

262 
assumes "a : A" 

263 
and "b : B" 

264 
and "c : C" 

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

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

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

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

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

270 
apply (unfold letrec3_def) 

271 
apply (rule lem [THEN subst]) 

41526  272 
apply (assumption  rule letrecT pairT splitT assms)+ 
20140  273 
apply (simp add: SPLITB) 
41526  274 
apply (assumption  rule ballI SubtypeI assms)+ 
20140  275 
apply (rule lem [THEN subst]) 
41526  276 
apply (assumption  rule letrecT SubtypeI pairT splitT assms  
20140  277 
erule bspec SubtypeE sym [THEN subst])+ 
278 
done 

279 

280 
lemmas letrecTs = letrecT letrec2T letrec3T 

281 

282 

283 
subsection {* Type Checking for Recursive Calls *} 

284 

285 
lemma rcallT: 

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

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

288 
g(a) : E" 

289 
by blast 

290 

291 
lemma rcall2T: 

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

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

294 
g(a,b) : E" 

295 
by blast 

296 

297 
lemma rcall3T: 

298 
"[ 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); 

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

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

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

302 
by blast 

303 

304 
lemmas rcallTs = rcallT rcall2T rcall3T 

305 

306 

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

308 

309 
lemma hyprcallT: 

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

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

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

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

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

315 
shows P 

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

317 
apply (rule rcallT [OF 2]) 

318 
apply assumption 

319 
apply (rule 4 [OF 2]) 

320 
apply (rule 5 [OF 2]) 

321 
done 

322 

323 
lemma hyprcall2T: 

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

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

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

327 
and 4: "a:A" 

328 
and 5: "b:B" 

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

330 
shows P 

331 
apply (rule 3) 

332 
apply (rule 1 [symmetric]) 

333 
apply (rule rcall2T) 

23467  334 
apply (rule 2) 
335 
apply assumption 

336 
apply (rule 4) 

337 
apply (rule 5) 

338 
apply (rule 6) 

20140  339 
done 
340 

341 
lemma hyprcall3T: 

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

343 
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)" 

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

345 
and 4: "a:A" 

346 
and 5: "b:B" 

347 
and 6: "c:C" 

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

349 
shows P 

350 
apply (rule 3) 

351 
apply (rule 1 [symmetric]) 

352 
apply (rule rcall3T) 

23467  353 
apply (rule 2) 
354 
apply assumption 

355 
apply (rule 4) 

356 
apply (rule 5) 

357 
apply (rule 6) 

358 
apply (rule 7) 

20140  359 
done 
360 

361 
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T 

362 

363 

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

365 

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

367 

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

369 

370 
lemma rmIH3: 

371 
"[ 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); 

372 
P ] ==> 

373 
P" . 

374 

375 
lemmas rmIHs = rmIH1 rmIH2 rmIH3 

376 

377 

378 
subsection {* Lemmas for constructors and subtypes *} 

379 

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

381 
(* correctly by applying SubtypeI *) 

382 

383 
lemma Subtype_canTs: 

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

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

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

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

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

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

390 

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

392 
apply (erule letB [THEN ssubst]) 

393 
apply assumption 

394 
done 

395 

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

397 
apply (erule applyT) 

398 
apply assumption 

399 
done 

400 

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

402 
by blast 

403 

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

405 
by blast 

406 

407 
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2 

408 

409 

410 
subsection {* Typechecking *} 

411 

412 
ML {* 

413 

414 
local 

415 

416 
val type_rls = 

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

417 
@{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

418 
@{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs}; 
20140  419 

56245  420 
fun bvars (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) l = bvars t (s::l) 
20140  421 
 bvars _ l = l 
422 

56245  423 
fun get_bno l n (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) = get_bno (s::l) n t 
38500  424 
 get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t 
425 
 get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t 

426 
 get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t 

20140  427 
 get_bno l n (t $ s) = get_bno l n t 
428 
 get_bno l n (Bound m) = (mlength(l),n) 

429 

430 
(* 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

431 
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

432 
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

433 
Term.could_unify(x,hd (prems_of @{thm rcall3T})) 
20140  434 

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

436 
let val bvs = bvars Bi [] 

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

42364  440 
in (nth bvs a, b) end) ihs 
20140  441 
fun try_IHs [] = no_tac 
42364  442 
 try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (nth rls (y  1)) i ORELSE (try_IHs xs) 
20140  443 
in try_IHs rnames end) 
444 

445 
fun is_rigid_prog t = 

446 
case (Logic.strip_assums_concl t) of 

38500  447 
(Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a []) 
20140  448 
 _ => false 
449 
in 

450 

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

451 
fun rcall_tac ctxt i = 
27239  452 
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

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

454 
THEN eresolve_tac @{thms rcall_lemmas} i 
20140  455 

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

456 
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

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

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

459 
match_tac [@{thm SubtypeI}] i 
20140  460 

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

461 
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

462 
if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac) 
20140  463 

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

464 
fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i 
20140  465 

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

466 
fun tac ctxt = typechk_tac ctxt [] 1 
20140  467 

468 
(*** Clean up Correctness Condictions ***) 

469 

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

470 
fun clean_ccs_tac ctxt = 
27239  471 
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

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

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

475 
end 
20140  476 

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

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

478 
SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i 
17456  479 

0  480 
end 
20140  481 
*} 
482 

483 

484 
subsection {* Evaluation *} 

485 

57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
57521
diff
changeset

486 
named_theorems eval "evaluation rules" 
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
57521
diff
changeset

487 

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

489 
fun eval_tac ths = 
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
57521
diff
changeset

490 
Subgoal.FOCUS_PREMS (fn {context = ctxt, prems, ...} => 
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
57521
diff
changeset

491 
let val eval_rules = Named_Theorems.get ctxt @{named_theorems eval} 
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
57521
diff
changeset

492 
in DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ rev eval_rules) 1) end) 
47432  493 
*} 
20140  494 

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

20140  497 
*} 
498 

499 

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

501 

502 
lemma applyV [eval]: 

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

504 
and "b(a) > c" 

505 
shows "f ` a > c" 

41526  506 
unfolding apply_def by (eval assms) 
20140  507 

508 
lemma letV: 

509 
assumes 1: "t > a" 

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

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

512 
apply (unfold let_def) 

513 
apply (rule 1 [THEN canonical]) 

514 
apply (tactic {* 

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

20140  517 
done 
518 

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

520 
apply (unfold fix_def) 

521 
apply (rule applyV) 

522 
apply (rule lamV) 

523 
apply assumption 

524 
done 

525 

526 
lemma letrecV: 

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

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

529 
apply (unfold letrec_def) 

530 
apply (assumption  rule fixV applyV lamV)+ 

531 
done 

532 

533 
lemmas [eval] = letV letrecV fixV 

534 

535 
lemma V_rls [eval]: 

536 
"true > true" 

537 
"false > false" 

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

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

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

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

542 
"zero > zero" 

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

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

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

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

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

548 
"[] > []" 

549 
"!!h t. h$t > h$t" 

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

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

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

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

554 
unfolding data_defs by eval+ 

555 

556 

557 
subsection {* Factorial *} 

558 

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

562 
by eval 

563 

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

567 
by eval 

568 

569 
subsection {* Less Than Or Equal *} 

570 

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

574 
by eval 

575 

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

579 
by eval 

580 

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

584 
by eval 

585 

586 

587 
subsection {* Reverse *} 

588 

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

592 
by eval 

593 

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

597 
by eval 

598 

599 
end 