author  wenzelm 
Thu, 13 Apr 2006 12:00:50 +0200  
changeset 19414  a21431e996bf 
parent 18678  dd0c569fa43d 
child 19876  11d447d5d68c 
permissions  rwrr 
10781  1 
(* Title: TFL/rules.ML 
10769  2 
ID: $Id$ 
3 
Author: Konrad Slind, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

6 
Emulation of HOL inference rules for TFL 

7 
*) 

8 

9 
signature RULES = 

10 
sig 

18184  11 
val dest_thm: thm > term list * term 
10769  12 

13 
(* Inference rules *) 

18184  14 
val REFL: cterm > thm 
15 
val ASSUME: cterm > thm 

16 
val MP: thm > thm > thm 

17 
val MATCH_MP: thm > thm > thm 

18 
val CONJUNCT1: thm > thm 

19 
val CONJUNCT2: thm > thm 

20 
val CONJUNCTS: thm > thm list 

21 
val DISCH: cterm > thm > thm 

22 
val UNDISCH: thm > thm 

23 
val SPEC: cterm > thm > thm 

24 
val ISPEC: cterm > thm > thm 

25 
val ISPECL: cterm list > thm > thm 

26 
val GEN: cterm > thm > thm 

27 
val GENL: cterm list > thm > thm 

28 
val LIST_CONJ: thm list > thm 

10769  29 

18184  30 
val SYM: thm > thm 
31 
val DISCH_ALL: thm > thm 

32 
val FILTER_DISCH_ALL: (term > bool) > thm > thm 

33 
val SPEC_ALL: thm > thm 

34 
val GEN_ALL: thm > thm 

35 
val IMP_TRANS: thm > thm > thm 

36 
val PROVE_HYP: thm > thm > thm 

10769  37 

18184  38 
val CHOOSE: cterm * thm > thm > thm 
39 
val EXISTS: cterm * cterm > thm > thm 

40 
val EXISTL: cterm list > thm > thm 

41 
val IT_EXISTS: (cterm*cterm) list > thm > thm 

10769  42 

18184  43 
val EVEN_ORS: thm list > thm list 
44 
val DISJ_CASESL: thm > thm list > thm 

10769  45 

18184  46 
val list_beta_conv: cterm > cterm list > thm 
47 
val SUBS: thm list > thm > thm 

48 
val simpl_conv: simpset > thm list > cterm > thm 

10769  49 

18184  50 
val rbeta: thm > thm 
10769  51 
(* For debugging my isabelle solver in the conditional rewriter *) 
18184  52 
val term_ref: term list ref 
53 
val thm_ref: thm list ref 

54 
val ss_ref: simpset list ref 

55 
val tracing: bool ref 

56 
val CONTEXT_REWRITE_RULE: term * term list * thm * thm list 

10769  57 
> thm > thm * term list 
18184  58 
val RIGHT_ASSOC: thm > thm 
10769  59 

18184  60 
val prove: bool > cterm * tactic > thm 
10769  61 
end; 
62 

63 
structure Rules: RULES = 

64 
struct 

65 

66 
structure S = USyntax; 

67 
structure U = Utils; 

68 
structure D = Dcterm; 

69 

70 

71 
fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg}; 

72 

73 

74 
fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm)); 

75 
fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm)); 

76 

77 
fun dest_thm thm = 

78 
let val {prop,hyps,...} = Thm.rep_thm thm 

79 
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end 

80 
handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop"; 

81 

82 

83 
(* Inference rules *) 

84 

85 
(* 

86 
* Equality (one step) 

87 
**) 

88 

89 
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq 

90 
handle THM (msg, _, _) => raise RULES_ERR "REFL" msg; 

91 

92 
fun SYM thm = thm RS sym 

93 
handle THM (msg, _, _) => raise RULES_ERR "SYM" msg; 

94 

95 
fun ALPHA thm ctm1 = 

96 
let 

97 
val ctm2 = Thm.cprop_of thm; 

98 
val ctm2_eq = Thm.reflexive ctm2; 

99 
val ctm1_eq = Thm.reflexive ctm1; 

100 
in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end 

101 
handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg; 

102 

103 
fun rbeta th = 

104 
(case D.strip_comb (cconcl th) of 

105 
(_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r) 

106 
 _ => raise RULES_ERR "rbeta" ""); 

107 

108 

109 
(* 

110 
* Implication and the assumption list 

111 
* 

112 
* Assumptions get stuck on the metalanguage assumption list. Implications 

113 
* are in the object language, so discharging an assumption "A" from theorem 

114 
* "B" results in something that looks like "A > B". 

115 
**) 

116 

117 
fun ASSUME ctm = Thm.assume (D.mk_prop ctm); 

118 

119 

120 
(* 

121 
* Implication in TFL is >. Metalanguage implication (==>) is only used 

122 
* in the implementation of some of the inference rules below. 

123 
**) 

124 
fun MP th1 th2 = th2 RS (th1 RS mp) 

125 
handle THM (msg, _, _) => raise RULES_ERR "MP" msg; 

126 

127 
(*forces the first argument to be a proposition if necessary*) 

128 
fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI 

129 
handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg; 

130 

16853  131 
fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm; 
10769  132 

133 

134 
fun FILTER_DISCH_ALL P thm = 

135 
let fun check tm = P (#t (Thm.rep_cterm tm)) 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

136 
in foldr (fn (tm,th) => if check tm then DISCH tm th else th) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

137 
thm (chyps thm) 
10769  138 
end; 
139 

140 
(* freezeT expensive! *) 

141 
fun UNDISCH thm = 

142 
let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm)))) 

143 
in Thm.implies_elim (thm RS mp) (ASSUME tm) end 

144 
handle U.ERR _ => raise RULES_ERR "UNDISCH" "" 

145 
 THM _ => raise RULES_ERR "UNDISCH" ""; 

146 

147 
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; 

148 

149 
fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans) 

150 
handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg; 

151 

152 

153 
(* 

154 
* Conjunction 

155 
**) 

156 

157 
fun CONJUNCT1 thm = thm RS conjunct1 

158 
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg; 

159 

160 
fun CONJUNCT2 thm = thm RS conjunct2 

161 
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg; 

162 

163 
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th]; 

164 

165 
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list" 

166 
 LIST_CONJ [th] = th 

167 
 LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst) 

168 
handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg; 

169 

170 

171 
(* 

172 
* Disjunction 

173 
**) 

174 
local val {prop,sign,...} = rep_thm disjI1 

175 
val [P,Q] = term_vars prop 

176 
val disj1 = Thm.forall_intr (Thm.cterm_of sign Q) disjI1 

177 
in 

178 
fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1) 

179 
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; 

180 
end; 

181 

182 
local val {prop,sign,...} = rep_thm disjI2 

183 
val [P,Q] = term_vars prop 

184 
val disj2 = Thm.forall_intr (Thm.cterm_of sign P) disjI2 

185 
in 

186 
fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2) 

187 
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg; 

188 
end; 

189 

190 

191 
(* 

192 
* 

193 
* A1  M1, ..., An  Mn 

194 
*  

195 
* [A1  M1 \/ ... \/ Mn, ..., An  M1 \/ ... \/ Mn] 

196 
* 

197 
**) 

198 

199 

200 
fun EVEN_ORS thms = 

201 
let fun blue ldisjs [] _ = [] 

202 
 blue ldisjs (th::rst) rdisjs = 

203 
let val tail = tl rdisjs 

204 
val rdisj_tl = D.list_mk_disj tail 

16853  205 
in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl) 
10769  206 
:: blue (ldisjs @ [cconcl th]) rst tail 
16853  207 
end handle U.ERR _ => [fold_rev DISJ2 ldisjs th] 
10769  208 
in blue [] thms (map cconcl thms) end; 
209 

210 

211 
(* 

212 
* 

213 
* A  P \/ Q B,P  R C,Q  R 

214 
*  

215 
* A U B U C  R 

216 
* 

217 
**) 

218 

219 
fun DISJ_CASES th1 th2 th3 = 

220 
let 

221 
val c = D.drop_prop (cconcl th1); 

222 
val (disj1, disj2) = D.dest_disj c; 

223 
val th2' = DISCH disj1 th2; 

224 
val th3' = DISCH disj2 th3; 

225 
in 

226 
th3' RS (th2' RS (th1 RS Thms.tfl_disjE)) 

227 
handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg 

228 
end; 

229 

230 

231 
(* 

232 
* 

233 
*  A1 \/ ... \/ An [A1  M, ..., An  M] 

234 
*  

235 
*  M 

236 
* 

237 
* Note. The list of theorems may be all jumbled up, so we have to 

238 
* first organize it to align with the first argument (the disjunctive 

239 
* theorem). 

240 
**) 

241 

242 
fun organize eq = (* a bit slow  analogous to insertion sort *) 

243 
let fun extract a alist = 

244 
let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1" 

245 
 ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t) 

246 
in ex ([],alist) 

247 
end 

248 
fun place [] [] = [] 

249 
 place (a::rst) alist = 

250 
let val (item,next) = extract a alist 

251 
in item::place rst next 

252 
end 

253 
 place _ _ = raise RULES_ERR "organize" "not a permutation.2" 

254 
in place 

255 
end; 

256 
(* freezeT expensive! *) 

257 
fun DISJ_CASESL disjth thl = 

258 
let val c = cconcl disjth 

259 
fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t 

260 
aconv term_of atm) 

261 
(#hyps(rep_thm th)) 

262 
val tml = D.strip_disj c 

263 
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases" 

264 
 DL th [th1] = PROVE_HYP th th1 

265 
 DL th [th1,th2] = DISJ_CASES th th1 th2 

266 
 DL th (th1::rst) = 

267 
let val tm = #2(D.dest_disj(D.drop_prop(cconcl th))) 

268 
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end 

269 
in DL (freezeT disjth) (organize eq tml thl) 

270 
end; 

271 

272 

273 
(* 

274 
* Universals 

275 
**) 

276 
local (* this is fragile *) 

277 
val {prop,sign,...} = rep_thm spec 

278 
val x = hd (tl (term_vars prop)) 

15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset

279 
val cTV = ctyp_of sign (type_of x) 
10769  280 
val gspec = forall_intr (cterm_of sign x) spec 
281 
in 

282 
fun SPEC tm thm = 

283 
let val {sign,T,...} = rep_cterm tm 

15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset

284 
val gspec' = instantiate ([(cTV, ctyp_of sign T)], []) gspec 
10769  285 
in 
286 
thm RS (forall_elim tm gspec') 

287 
end 

288 
end; 

289 

16853  290 
fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm; 
10769  291 

292 
val ISPEC = SPEC 

16853  293 
val ISPECL = fold ISPEC; 
10769  294 

295 
(* Not optimized! Too complicated. *) 

296 
local val {prop,sign,...} = rep_thm allI 

297 
val [P] = add_term_vars (prop, []) 

15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset

298 
fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty)) 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset

299 
fun ctm_theta s = map (fn (i, (_, tm2)) => 
10769  300 
let val ctm2 = cterm_of s tm2 
301 
in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2) 

302 
end) 

15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset

303 
fun certify s (ty_theta,tm_theta) = 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset

304 
(cty_theta s (Vartab.dest ty_theta), 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset

305 
ctm_theta s (Vartab.dest tm_theta)) 
10769  306 
in 
307 
fun GEN v th = 

308 
let val gth = forall_intr v th 

309 
val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth 

310 
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) 

18184  311 
val theta = Pattern.match sign (P,P') (Vartab.empty, Vartab.empty); 
10769  312 
val allI2 = instantiate (certify sign theta) allI 
313 
val thm = Thm.implies_elim allI2 gth 

314 
val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm 

315 
val prop' = tp $ (A $ Abs(x,ty,M)) 

316 
in ALPHA thm (cterm_of sign prop') 

317 
end 

318 
end; 

319 

16853  320 
val GENL = fold_rev GEN; 
10769  321 

322 
fun GEN_ALL thm = 

323 
let val {prop,sign,...} = rep_thm thm 

324 
val tycheck = cterm_of sign 

325 
val vlist = map tycheck (add_term_vars (prop, [])) 

326 
in GENL vlist thm 

327 
end; 

328 

329 

330 
fun MATCH_MP th1 th2 = 

331 
if (D.is_forall (D.drop_prop(cconcl th1))) 

332 
then MATCH_MP (th1 RS spec) th2 

333 
else MP th1 th2; 

334 

335 

336 
(* 

337 
* Existentials 

338 
**) 

339 

340 

341 

342 
(* 

343 
* Existential elimination 

344 
* 

345 
* A1  ?x.t[x] , A2, "t[v]"  t' 

346 
*  (variable v occurs nowhere) 

347 
* A1 u A2  t' 

348 
* 

349 
**) 

350 

351 
fun CHOOSE (fvar, exth) fact = 

352 
let 

353 
val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth))) 

354 
val redex = D.capply lam fvar 

355 
val {sign, t = t$u,...} = Thm.rep_cterm redex 

18184  356 
val residue = Thm.cterm_of sign (Term.betapply (t, u)) 
10769  357 
in 
358 
GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) 

359 
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg 

360 
end; 

361 

362 
local val {prop,sign,...} = rep_thm exI 

363 
val [P,x] = term_vars prop 

364 
in 

365 
fun EXISTS (template,witness) thm = 

366 
let val {prop,sign,...} = rep_thm thm 

367 
val P' = cterm_of sign P 

368 
val x' = cterm_of sign x 

369 
val abstr = #2 (D.dest_comb template) 

370 
in 

371 
thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI) 

372 
handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg 

373 
end 

374 
end; 

375 

376 
(* 

377 
* 

378 
* A  M 

379 
*  [v_1,...,v_n] 

380 
* A  ?v1...v_n. M 

381 
* 

382 
**) 

383 

384 
fun EXISTL vlist th = 

16853  385 
fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm) 
10769  386 
vlist th; 
387 

388 

389 
(* 

390 
* 

391 
* A  M[x_1,...,x_n] 

392 
*  [(x > y)_1,...,(x > y)_n] 

393 
* A  ?y_1...y_n. M 

394 
* 

395 
**) 

396 
(* Could be improved, but needs "subst_free" for certified terms *) 

397 

398 
fun IT_EXISTS blist th = 

399 
let val {sign,...} = rep_thm th 

400 
val tych = cterm_of sign 

401 
val detype = #t o rep_cterm 

402 
val blist' = map (fn (x,y) => (detype x, detype y)) blist 

17171  403 
fun ex v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M}) 
10769  404 

405 
in 

16853  406 
fold_rev (fn (b as (r1,r2)) => fn thm => 
17171  407 
EXISTS(ex r2 (subst_free [b] 
10769  408 
(HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1) 
409 
thm) 

410 
blist' th 

411 
end; 

412 

413 
(* 

414 
* Faster version, that fails for some as yet unknown reason 

415 
* fun IT_EXISTS blist th = 

416 
* let val {sign,...} = rep_thm th 

417 
* val tych = cterm_of sign 

418 
* fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y) 

419 
* in 

420 
* fold (fn (b as (r1,r2), thm) => 

421 
* EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))), 

422 
* r1) thm) blist th 

423 
* end; 

424 
**) 

425 

426 
(* 

427 
* Rewriting 

428 
**) 

429 

430 
fun SUBS thl = 

431 
rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl); 

432 

15531  433 
val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)); 
15021  434 

10769  435 
fun simpl_conv ss thl ctm = 
15021  436 
rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq; 
437 

10769  438 

439 
val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc]; 

440 

441 

442 

443 
(* 

444 
* TERMINATION CONDITION EXTRACTION 

445 
**) 

446 

447 

448 
(* Object language quantifier, i.e., "!" *) 

449 
fun Forall v M = S.mk_forall{Bvar=v, Body=M}; 

450 

451 

452 
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) 

453 
fun is_cong thm = 

454 
let val {prop, ...} = rep_thm thm 

455 
in case prop 

456 
of (Const("==>",_)$(Const("Trueprop",_)$ _) $ 

457 
(Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false 

458 
 _ => true 

459 
end; 

460 

461 

462 

463 
fun dest_equal(Const ("==",_) $ 

464 
(Const ("Trueprop",_) $ lhs) 

465 
$ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs} 

466 
 dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} 

467 
 dest_equal tm = S.dest_eq tm; 

468 

469 
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); 

470 

471 
fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a 

472 
 dest_all _ _ = raise RULES_ERR "dest_all" "not a !!"; 

473 

474 
val is_all = can (dest_all []); 

475 

476 
fun strip_all used fm = 

477 
if (is_all fm) 

478 
then let val ({Bvar, Body}, used') = dest_all used fm 

479 
val (bvs, core, used'') = strip_all used' Body 

480 
in ((Bvar::bvs), core, used'') 

481 
end 

482 
else ([], fm, used); 

483 

484 
fun break_all(Const("all",_) $ Abs (_,_,body)) = body 

485 
 break_all _ = raise RULES_ERR "break_all" "not a !!"; 

486 

487 
fun list_break_all(Const("all",_) $ Abs (s,ty,body)) = 

488 
let val (L,core) = list_break_all body 

489 
in ((s,ty)::L, core) 

490 
end 

491 
 list_break_all tm = ([],tm); 

492 

493 
(* 

494 
* Rename a term of the form 

495 
* 

496 
* !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn 

497 
* ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn. 

498 
* to one of 

499 
* 

500 
* !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn 

501 
* ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn. 

502 
* 

503 
* This prevents name problems in extraction, and helps the result to read 

504 
* better. There is a problem with varstructs, since they can introduce more 

505 
* than n variables, and some extra reasoning needs to be done. 

506 
**) 

507 

508 
fun get ([],_,L) = rev L 

509 
 get (ant::rst,n,L) = 

510 
case (list_break_all ant) 

511 
of ([],_) => get (rst, n+1,L) 

512 
 (vlist,body) => 

513 
let val eq = Logic.strip_imp_concl body 

514 
val (f,args) = S.strip_comb (get_lhs eq) 

515 
val (vstrl,_) = S.strip_abs f 

516 
val names = variantlist (map (#1 o dest_Free) vstrl, 

517 
add_term_names(body, [])) 

518 
in get (rst, n+1, (names,n)::L) end 

519 
handle TERM _ => get (rst, n+1, L) 

520 
 U.ERR _ => get (rst, n+1, L); 

521 

522 
(* Note: rename_params_rule counts from 1, not 0 *) 

523 
fun rename thm = 

524 
let val {prop,sign,...} = rep_thm thm 

525 
val tych = cterm_of sign 

526 
val ants = Logic.strip_imp_prems prop 

527 
val news = get (ants,1,[]) 

528 
in 

16853  529 
fold rename_params_rule news thm 
10769  530 
end; 
531 

532 

533 
(* 

534 
* Betaconversion to the rhs of an equation (taken from hol90/drule.sml) 

535 
**) 

536 

537 
fun list_beta_conv tm = 

538 
let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th)))) 

539 
fun iter [] = Thm.reflexive tm 

540 
 iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v)) 

541 
in iter end; 

542 

543 

544 
(* 

545 
* Trace information for the rewriter 

546 
**) 

547 
val term_ref = ref[] : term list ref 

15021  548 
val ss_ref = ref [] : simpset list ref; 
10769  549 
val thm_ref = ref [] : thm list ref; 
550 
val tracing = ref false; 

551 

552 
fun say s = if !tracing then writeln s else (); 

553 

554 
fun print_thms s L = 

555 
say (cat_lines (s :: map string_of_thm L)); 

556 

557 
fun print_cterms s L = 

558 
say (cat_lines (s :: map string_of_cterm L)); 

559 

560 

561 
(* 

562 
* General abstraction handlers, should probably go in USyntax. 

563 
**) 

564 
fun mk_aabs (vstr, body) = 

565 
S.mk_abs {Bvar = vstr, Body = body} 

566 
handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body}; 

567 

568 
fun list_mk_aabs (vstrl,tm) = 

16853  569 
fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm; 
10769  570 

571 
fun dest_aabs used tm = 

572 
let val ({Bvar,Body}, used') = S.dest_abs used tm 

573 
in (Bvar, Body, used') end 

574 
handle U.ERR _ => 

575 
let val {varstruct, body, used} = S.dest_pabs used tm 

576 
in (varstruct, body, used) end; 

577 

578 
fun strip_aabs used tm = 

579 
let val (vstr, body, used') = dest_aabs used tm 

580 
val (bvs, core, used'') = strip_aabs used' body 

581 
in (vstr::bvs, core, used'') end 

582 
handle U.ERR _ => ([], tm, used); 

583 

584 
fun dest_combn tm 0 = (tm,[]) 

585 
 dest_combn tm n = 

586 
let val {Rator,Rand} = S.dest_comb tm 

587 
val (f,rands) = dest_combn Rator (n1) 

588 
in (f,Rand::rands) 

589 
end; 

590 

591 

592 

593 

594 
local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end 

595 
fun mk_fst tm = 

596 
let val ty as Type("*", [fty,sty]) = type_of tm 

597 
in Const ("fst", ty > fty) $ tm end 

598 
fun mk_snd tm = 

599 
let val ty as Type("*", [fty,sty]) = type_of tm 

600 
in Const ("snd", ty > sty) $ tm end 

601 
in 

602 
fun XFILL tych x vstruct = 

603 
let fun traverse p xocc L = 

604 
if (is_Free p) 

605 
then tych xocc::L 

606 
else let val (p1,p2) = dest_pair p 

607 
in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L) 

608 
end 

609 
in 

610 
traverse vstruct x [] 

611 
end end; 

612 

613 
(* 

614 
* Replace a free tuple (vstr) by a universally quantified variable (a). 

615 
* Note that the notion of "freeness" for a tuple is different than for a 

616 
* variable: if variables in the tuple also occur in any other place than 

617 
* an occurrences of the tuple, they aren't "free" (which is thus probably 

618 
* the wrong word to use). 

619 
**) 

620 

621 
fun VSTRUCT_ELIM tych a vstr th = 

622 
let val L = S.free_vars_lr vstr 

623 
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr))) 

624 
val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th) 

625 
val thm2 = forall_intr_list (map tych L) thm1 

626 
val thm3 = forall_elim_list (XFILL tych a vstr) thm2 

627 
in refl RS 

628 
rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3 

629 
end; 

630 

631 
fun PGEN tych a vstr th = 

632 
let val a1 = tych a 

633 
val vstr1 = tych vstr 

634 
in 

635 
forall_intr a1 

636 
(if (is_Free vstr) 

637 
then cterm_instantiate [(vstr1,a1)] th 

638 
else VSTRUCT_ELIM tych a vstr th) 

639 
end; 

640 

641 

642 
(* 

643 
* Takes apart a paired betaredex, looking like "(\(x,y).N) vstr", into 

644 
* 

645 
* (([x,y],N),vstr) 

646 
**) 

647 
fun dest_pbeta_redex used M n = 

648 
let val (f,args) = dest_combn M n 

649 
val dummy = dest_aabs used f 

650 
in (strip_aabs used f,args) 

651 
end; 

652 

653 
fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M; 

654 

655 
fun dest_impl tm = 

656 
let val ants = Logic.strip_imp_prems tm 

657 
val eq = Logic.strip_imp_concl tm 

658 
in (ants,get_lhs eq) 

659 
end; 

660 

15570  661 
fun restricted t = isSome (S.find_term 
10769  662 
(fn (Const("Wellfounded_Recursion.cut",_)) =>true  _ => false) 
663 
t) 

664 

665 
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th = 

666 
let val globals = func::G 

17892  667 
val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss 
668 
val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection]; 

10769  669 
val tc_list = ref[]: term list ref 
670 
val dummy = term_ref := [] 

671 
val dummy = thm_ref := [] 

15021  672 
val dummy = ss_ref := [] 
10769  673 
val cut_lemma' = cut_lemma RS eq_reflection 
15021  674 
fun prover used ss thm = 
675 
let fun cong_prover ss thm = 

10769  676 
let val dummy = say "cong_prover:" 
15021  677 
val cntxt = MetaSimplifier.prems_of_ss ss 
10769  678 
val dummy = print_thms "cntxt:" cntxt 
679 
val dummy = say "cong rule:" 

680 
val dummy = say (string_of_thm thm) 

681 
val dummy = thm_ref := (thm :: !thm_ref) 

15021  682 
val dummy = ss_ref := (ss :: !ss_ref) 
10769  683 
(* Unquantified eliminate *) 
684 
fun uq_eliminate (thm,imp,sign) = 

685 
let val tych = cterm_of sign 

686 
val dummy = print_cterms "To eliminate:" [tych imp] 

687 
val ants = map tych (Logic.strip_imp_prems imp) 

688 
val eq = Logic.strip_imp_concl imp 

689 
val lhs = tych(get_lhs eq) 

15021  690 
val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss 
691 
val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs 

10769  692 
handle U.ERR _ => Thm.reflexive lhs 
693 
val dummy = print_thms "proven:" [lhs_eq_lhs1] 

694 
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 

695 
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq 

696 
in 

697 
lhs_eeq_lhs2 COMP thm 

698 
end 

699 
fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) = 

700 
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist) 

701 
val dummy = assert (forall (op aconv) 

702 
(ListPair.zip (vlist, args))) 

703 
"assertion failed in CONTEXT_REWRITE_RULE" 

704 
val imp_body1 = subst_free (ListPair.zip (args, vstrl)) 

705 
imp_body 

706 
val tych = cterm_of sign 

707 
val ants1 = map tych (Logic.strip_imp_prems imp_body1) 

708 
val eq1 = Logic.strip_imp_concl imp_body1 

709 
val Q = get_lhs eq1 

710 
val QeqQ1 = pbeta_reduce (tych Q) 

711 
val Q1 = #2(D.dest_eq(cconcl QeqQ1)) 

15021  712 
val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss 
713 
val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1 

10769  714 
handle U.ERR _ => Thm.reflexive Q1 
14643  715 
val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2)) 
10769  716 
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) 
717 
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection) 

718 
val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 

719 
val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ => 

720 
((Q2eeqQ3 RS meta_eq_to_obj_eq) 

721 
RS ((thA RS meta_eq_to_obj_eq) RS trans)) 

722 
RS eq_reflection 

723 
val impth = implies_intr_list ants1 QeeqQ3 

724 
val impth1 = impth RS meta_eq_to_obj_eq 

725 
(* Need to abstract *) 

726 
val ant_th = U.itlist2 (PGEN tych) args vstrl impth1 

727 
in ant_th COMP thm 

728 
end 

729 
fun q_eliminate (thm,imp,sign) = 

730 
let val (vlist, imp_body, used') = strip_all used imp 

731 
val (ants,Q) = dest_impl imp_body 

732 
in if (pbeta_redex Q) (length vlist) 

733 
then pq_eliminate (thm,sign,vlist,imp_body,Q) 

734 
else 

735 
let val tych = cterm_of sign 

736 
val ants1 = map tych ants 

15021  737 
val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss 
10769  738 
val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm 
15021  739 
(false,true,false) (prover used') ss' (tych Q) 
10769  740 
handle U.ERR _ => Thm.reflexive (tych Q) 
741 
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 

742 
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq 

743 
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2 

744 
in 

745 
ant_th COMP thm 

746 
end end 

747 

748 
fun eliminate thm = 

749 
case (rep_thm thm) 

750 
of {prop = (Const("==>",_) $ imp $ _), sign, ...} => 

751 
eliminate 

752 
(if not(is_all imp) 

753 
then uq_eliminate (thm,imp,sign) 

754 
else q_eliminate (thm,imp,sign)) 

755 
(* Assume that the leading constant is ==, *) 

756 
 _ => thm (* if it is not a ==> *) 

15531  757 
in SOME(eliminate (rename thm)) end 
758 
handle U.ERR _ => NONE (* FIXME handle THM as well?? *) 

10769  759 

15021  760 
fun restrict_prover ss thm = 
10769  761 
let val dummy = say "restrict_prover:" 
15021  762 
val cntxt = rev(MetaSimplifier.prems_of_ss ss) 
10769  763 
val dummy = print_thms "cntxt:" cntxt 
764 
val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, 

765 
sign,...} = rep_thm thm 

766 
fun genl tm = let val vlist = gen_rems (op aconv) 

767 
(add_term_frees(tm,[]), globals) 

16853  768 
in fold_rev Forall vlist tm 
10769  769 
end 
770 
(* 

771 
* This actually isn't quite right, since it will think that 

772 
* notfully applied occs. of "f" in the context mean that the 

773 
* current call is nested. The real solution is to pass in a 

774 
* term "f v1..vn" which is a pattern that any full application 

775 
* of "f" will match. 

776 
**) 

777 
val func_name = #1(dest_Const func) 

778 
fun is_func (Const (name,_)) = (name = func_name) 

779 
 is_func _ = false 

780 
val rcontext = rev cntxt 

14643  781 
val cncl = HOLogic.dest_Trueprop o Thm.prop_of 
10769  782 
val antl = case rcontext of [] => [] 
783 
 _ => [S.list_mk_conj(map cncl rcontext)] 

784 
val TC = genl(S.list_mk_imp(antl, A)) 

785 
val dummy = print_cterms "func:" [cterm_of sign func] 

786 
val dummy = print_cterms "TC:" 

787 
[cterm_of sign (HOLogic.mk_Trueprop TC)] 

788 
val dummy = tc_list := (TC :: !tc_list) 

15570  789 
val nestedp = isSome (S.find_term is_func TC) 
10769  790 
val dummy = if nestedp then say "nested" else say "not_nested" 
791 
val dummy = term_ref := ([func,TC]@(!term_ref)) 

792 
val th' = if nestedp then raise RULES_ERR "solver" "nested function" 

793 
else let val cTC = cterm_of sign 

794 
(HOLogic.mk_Trueprop TC) 

795 
in case rcontext of 

796 
[] => SPEC_ALL(ASSUME cTC) 

797 
 _ => MP (SPEC_ALL (ASSUME cTC)) 

798 
(LIST_CONJ rcontext) 

799 
end 

800 
val th'' = th' RS thm 

15531  801 
in SOME (th'') 
802 
end handle U.ERR _ => NONE (* FIXME handle THM as well?? *) 

10769  803 
in 
15021  804 
(if (is_cong thm) then cong_prover else restrict_prover) ss thm 
10769  805 
end 
806 
val ctm = cprop_of th 

807 
val names = add_term_names (term_of ctm, []) 

808 
val th1 = MetaSimplifier.rewrite_cterm(false,true,false) 

17892  809 
(prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm 
10769  810 
val th2 = equal_elim th1 th 
811 
in 

15570  812 
(th2, List.filter (not o restricted) (!tc_list)) 
10769  813 
end; 
814 

815 

11632  816 
fun prove strict (ptm, tac) = 
17985  817 
let 
818 
val {thy, t, ...} = Thm.rep_cterm ptm; 

819 
val result = 

820 
if strict then Goal.prove thy [] [] t (K tac) 

821 
else Goal.prove thy [] [] t (K tac) 

18678  822 
handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg); 
17985  823 
in #1 (freeze_thaw (standard result)) end; 
10769  824 

825 
end; 