author  paulson 
Fri, 03 Nov 2000 10:23:24 +0100  
changeset 10368  f7e8abd8ea15 
parent 10212  33fe2d701ddd 
child 10417  42e6b8502d52 
permissions  rwrr 
9867  1 
(* Title: TFL/rules.sml 
6498  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 

9867  9 
signature Rules_sig = 
10 
sig 

11 
val dest_thm : thm > term list * term 

12 

13 
(* Inference rules *) 

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 INST_TYPE :(typ*typ)list > thm > thm 

24 
val SPEC :cterm > thm > thm 

25 
val ISPEC :cterm > thm > thm 

26 
val ISPECL :cterm list > thm > thm 

27 
val GEN :cterm > thm > thm 

28 
val GENL :cterm list > thm > thm 

29 
val LIST_CONJ :thm list > thm 

30 

31 
val SYM : thm > thm 

32 
val DISCH_ALL : thm > thm 

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

34 
val SPEC_ALL : thm > thm 

35 
val GEN_ALL : thm > thm 

36 
val IMP_TRANS : thm > thm > thm 

37 
val PROVE_HYP : thm > thm > thm 

38 

39 
val CHOOSE : cterm * thm > thm > thm 

40 
val EXISTS : cterm * cterm > thm > thm 

41 
val EXISTL : cterm list > thm > thm 

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

43 

44 
val EVEN_ORS : thm list > thm list 

45 
val DISJ_CASESL : thm > thm list > thm 

46 

47 
val list_beta_conv : cterm > cterm list > thm 

48 
val SUBS : thm list > thm > thm 

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

50 

51 
val rbeta : thm > thm 

52 
(* For debugging my isabelle solver in the conditional rewriter *) 

53 
val term_ref : term list ref 

54 
val thm_ref : thm list ref 

55 
val mss_ref : meta_simpset list ref 

56 
val tracing : bool ref 

57 
val CONTEXT_REWRITE_RULE : term * term list * thm * thm list 

58 
> thm > thm * term list 

59 
val RIGHT_ASSOC : thm > thm 

60 

61 
val prove : cterm * tactic > thm 

62 
end; 

63 

6498  64 

65 
structure Rules : Rules_sig = 

66 
struct 

67 

68 
open Utils; 

69 

70 
structure USyntax = USyntax; 

71 
structure S = USyntax; 

72 
structure U = Utils; 

73 
structure D = Dcterm; 

74 

75 

76 
fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg}; 

77 

78 

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

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

81 

82 
fun dest_thm thm = 

83 
let val {prop,hyps,...} = rep_thm thm 

84 
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) 

85 
end; 

86 

87 

88 

89 
(* Inference rules *) 

90 

91 
(* 

92 
* Equality (one step) 

93 
**) 

94 
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq; 

95 
fun SYM thm = thm RS sym; 

96 

97 
fun ALPHA thm ctm1 = 

98 
let val ctm2 = cprop_of thm 

99 
val ctm2_eq = reflexive ctm2 

100 
val ctm1_eq = reflexive ctm1 

101 
in equal_elim (transitive ctm2_eq ctm1_eq) thm 

102 
end; 

103 

7262  104 
fun rbeta th = 
105 
case Dcterm.strip_comb (cconcl th) 

106 
of (eeq,[l,r]) => transitive th (beta_conversion r) 

107 
 _ => raise RULES_ERR{func="rbeta", mesg =""}; 

6498  108 

109 
(* 

110 
* typ instantiation 

111 
**) 

112 
fun INST_TYPE blist thm = 

113 
let val {sign,...} = rep_thm thm 

114 
val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist 

115 
in Thm.instantiate (blist',[]) thm 

116 
end 

10015  117 
handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""}; (* FIXME do not handle _ !!! *) 
6498  118 

119 

120 
(* 

121 
* Implication and the assumption list 

122 
* 

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

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

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

126 
**) 

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

128 

129 

130 
(* 

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

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

133 
**) 

134 
fun MP th1 th2 = th2 RS (th1 RS mp); 

135 

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

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

138 

139 
fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm; 

140 

141 

142 
fun FILTER_DISCH_ALL P thm = 

143 
let fun check tm = U.holds P (#t(rep_cterm tm)) 

144 
in foldr (fn (tm,th) => if (check tm) then DISCH tm th else th) 

145 
(chyps thm, thm) 

146 
end; 

147 

148 
(* freezeT expensive! *) 

149 
fun UNDISCH thm = 

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

151 
in implies_elim (thm RS mp) (ASSUME tm) 

152 
end 

10015  153 
handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""}; (* FIXME do not handle _ !!! *) 
6498  154 

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

156 

157 
local val [p1,p2] = goal HOL.thy "(A>B) ==> (B > C) ==> (A>C)" 

158 
val dummy = by (rtac impI 1) 

159 
val dummy = by (rtac (p2 RS mp) 1) 

160 
val dummy = by (rtac (p1 RS mp) 1) 

161 
val dummy = by (assume_tac 1) 

162 
val imp_trans = result() 

163 
in 

164 
fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans) 

165 
end; 

166 

167 
(* 

168 
* Conjunction 

169 
**) 

170 
fun CONJUNCT1 thm = (thm RS conjunct1) 

171 
fun CONJUNCT2 thm = (thm RS conjunct2); 

172 
fun CONJUNCTS th = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th)) 

10015  173 
handle _ => [th]; (* FIXME do not handle _ !!! *) 
6498  174 

175 
fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"} 

176 
 LIST_CONJ [th] = th 

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

178 

179 

180 
(* 

181 
* Disjunction 

182 
**) 

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

184 
val [P,Q] = term_vars prop 

185 
val disj1 = forall_intr (cterm_of sign Q) disjI1 

186 
in 

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

188 
end; 

189 

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

191 
val [P,Q] = term_vars prop 

192 
val disj2 = forall_intr (cterm_of sign P) disjI2 

193 
in 

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

195 
end; 

196 

197 

198 
(* 

199 
* 

200 
* A1  M1, ..., An  Mn 

201 
*  

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

203 
* 

204 
**) 

205 

206 

207 
fun EVEN_ORS thms = 

208 
let fun blue ldisjs [] _ = [] 

209 
 blue ldisjs (th::rst) rdisjs = 

210 
let val tail = tl rdisjs 

211 
val rdisj_tl = D.list_mk_disj tail 

212 
in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl) 

213 
:: blue (ldisjs@[cconcl th]) rst tail 

10015  214 
end handle _ => [itlist DISJ2 ldisjs th] (* FIXME do not handle _ !!! *) 
6498  215 
in 
216 
blue [] thms (map cconcl thms) 

217 
end; 

218 

219 

220 
(* 

221 
* 

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

223 
*  

224 
* A U B U C  R 

225 
* 

226 
**) 

227 
local val [p1,p2,p3] = goal HOL.thy "(P  Q) ==> (P > R) ==> (Q > R) ==> R" 

228 
val dummy = by (rtac (p1 RS disjE) 1) 

229 
val dummy = by (rtac (p2 RS mp) 1) 

230 
val dummy = by (assume_tac 1) 

231 
val dummy = by (rtac (p3 RS mp) 1) 

232 
val dummy = by (assume_tac 1) 

233 
val tfl_exE = result() 

234 
in 

235 
fun DISJ_CASES th1 th2 th3 = 

236 
let val c = D.drop_prop(cconcl th1) 

237 
val (disj1,disj2) = D.dest_disj c 

238 
val th2' = DISCH disj1 th2 

239 
val th3' = DISCH disj2 th3 

240 
in 

241 
th3' RS (th2' RS (th1 RS tfl_exE)) 

242 
end 

243 
end; 

244 

245 

246 
(* 

247 
* 

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

249 
*  

250 
*  M 

251 
* 

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

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

254 
* theorem). 

255 
**) 

256 

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

258 
let fun extract a alist = 

259 
let fun ex (_,[]) = raise RULES_ERR{func = "organize", 

260 
mesg = "not a permutation.1"} 

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

262 
in ex ([],alist) 

263 
end 

264 
fun place [] [] = [] 

265 
 place (a::rst) alist = 

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

267 
in item::place rst next 

268 
end 

269 
 place _ _ = raise RULES_ERR{func = "organize", 

270 
mesg = "not a permutation.2"} 

271 
in place 

272 
end; 

273 
(* freezeT expensive! *) 

274 
fun DISJ_CASESL disjth thl = 

275 
let val c = cconcl disjth 

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

277 
aconv term_of atm) 

278 
(#hyps(rep_thm th)) 

279 
val tml = D.strip_disj c 

280 
fun DL th [] = raise RULES_ERR{func="DISJ_CASESL",mesg="no cases"} 

281 
 DL th [th1] = PROVE_HYP th th1 

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

283 
 DL th (th1::rst) = 

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

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

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

287 
end; 

288 

289 

290 
(* 

291 
* Universals 

292 
**) 

293 
local (* this is fragile *) 

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

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

296 
val (TVar (indx,_)) = type_of x 

297 
val gspec = forall_intr (cterm_of sign x) spec 

298 
in 

299 
fun SPEC tm thm = 

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

301 
val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec 

302 
in 

303 
thm RS (forall_elim tm gspec') 

304 
end 

305 
end; 

306 

307 
fun SPEC_ALL thm = rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm; 

308 

309 
val ISPEC = SPEC 

310 
val ISPECL = rev_itlist ISPEC; 

311 

312 
(* Not optimized! Too complicated. *) 

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

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

315 
fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty)) 

316 
fun ctm_theta s = map (fn (i,tm2) => 

317 
let val ctm2 = cterm_of s tm2 

318 
in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2) 

319 
end) 

320 
fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta, 

321 
ctm_theta s tm_theta) 

322 
in 

323 
fun GEN v th = 

324 
let val gth = forall_intr v th 

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

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

327 
val tsig = #tsig(Sign.rep_sg sign) 

328 
val theta = Pattern.match tsig (P,P') 

329 
val allI2 = instantiate (certify sign theta) allI 

330 
val thm = implies_elim allI2 gth 

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

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

333 
in ALPHA thm (cterm_of sign prop') 

334 
end 

335 
end; 

336 

337 
val GENL = itlist GEN; 

338 

339 
fun GEN_ALL thm = 

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

341 
val tycheck = cterm_of sign 

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

343 
in GENL vlist thm 

344 
end; 

345 

346 

347 
fun MATCH_MP th1 th2 = 

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

349 
then MATCH_MP (th1 RS spec) th2 

350 
else MP th1 th2; 

351 

352 

353 
(* 

354 
* Existentials 

355 
**) 

356 

357 

358 

359 
(* 

360 
* Existential elimination 

361 
* 

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

363 
*  (variable v occurs nowhere) 

364 
* A1 u A2  t' 

365 
* 

366 
**) 

367 

368 
local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x > Q) ==> Q" 

369 
val dummy = by (rtac (p1 RS exE) 1) 

370 
val dummy = by (rtac ((p2 RS allE) RS mp) 1) 

371 
val dummy = by (assume_tac 2) 

372 
val dummy = by (assume_tac 1) 

373 
val choose_thm = result() 

374 
in 

375 
fun CHOOSE(fvar,exth) fact = 

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

377 
val redex = capply lam fvar 

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

379 
val residue = cterm_of sign (betapply(t,u)) 

380 
in GEN fvar (DISCH residue fact) RS (exth RS choose_thm) 

381 
end 

382 
end; 

383 

384 

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

386 
val [P,x] = term_vars prop 

387 
in 

388 
fun EXISTS (template,witness) thm = 

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

390 
val P' = cterm_of sign P 

391 
val x' = cterm_of sign x 

392 
val abstr = #2(dest_comb template) 

393 
in 

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

395 
end 

396 
end; 

397 

398 
(* 

399 
* 

400 
* A  M 

401 
*  [v_1,...,v_n] 

402 
* A  ?v1...v_n. M 

403 
* 

404 
**) 

405 

406 
fun EXISTL vlist th = 

407 
U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm) 

408 
vlist th; 

409 

410 

411 
(* 

412 
* 

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

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

415 
* A  ?y_1...y_n. M 

416 
* 

417 
**) 

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

419 

420 
fun IT_EXISTS blist th = 

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

422 
val tych = cterm_of sign 

423 
val detype = #t o rep_cterm 

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

425 
fun ?v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M}) 

426 

427 
in 

428 
U.itlist (fn (b as (r1,r2)) => fn thm => 

429 
EXISTS(?r2(subst_free[b] 

430 
(HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1) 

431 
thm) 

432 
blist' th 

433 
end; 

434 

435 
(* 

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

437 
* fun IT_EXISTS blist th = 

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

439 
* val tych = cterm_of sign 

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

441 
* in 

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

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

444 
* r1) thm) blist th 

445 
* end; 

446 
**) 

447 

448 
(* 

449 
* Rewriting 

450 
**) 

451 

452 
fun SUBS thl = 

10015  453 
rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl); (* FIXME do not handle _ !!! *) 
6498  454 

455 
local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None)) 

456 
in 

457 
fun simpl_conv ss thl ctm = 

458 
rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm 

459 
RS meta_eq_to_obj_eq 

460 
end; 

461 

462 
local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]) 

463 
in 

464 
val RIGHT_ASSOC = rewrite_rule [prover"((ab)c) = (a(bc))" RS eq_reflection] 

465 
val ASM = refl RS iffD1 

466 
end; 

467 

468 

469 

470 

471 
(* 

472 
* TERMINATION CONDITION EXTRACTION 

473 
**) 

474 

475 

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

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

478 

479 

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

481 
fun is_cong thm = 

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

483 
in case prop 

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

10212  485 
(Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false 
6498  486 
 _ => true 
487 
end; 

488 

489 

490 

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

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

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

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

495 
 dest_equal tm = S.dest_eq tm; 

496 

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

498 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

499 
fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

500 
 dest_all _ _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"}; 
6498  501 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

502 
val is_all = Utils.can (dest_all []); 
6498  503 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

504 
fun strip_all used fm = 
6498  505 
if (is_all fm) 
10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

506 
then let val ({Bvar, Body}, used') = dest_all used fm 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

507 
val (bvs, core, used'') = strip_all used' Body 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

508 
in ((Bvar::bvs), core, used'') 
6498  509 
end 
10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

510 
else ([], fm, used); 
6498  511 

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

513 
 break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"}; 

514 

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

516 
let val (L,core) = list_break_all body 

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

518 
end 

519 
 list_break_all tm = ([],tm); 

520 

521 
(* 

522 
* Rename a term of the form 

523 
* 

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

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

526 
* to one of 

527 
* 

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

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

530 
* 

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

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

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

534 
**) 

535 

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

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

538 
case (list_break_all ant) 

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

540 
 (vlist,body) => 

541 
let val eq = Logic.strip_imp_concl body 

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

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

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

545 
add_term_names(body, [])) 

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

10015  547 
end handle _ => get (rst, n+1, L); (* FIXME do not handle _ !!! *) 
6498  548 

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

550 
fun rename thm = 

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

552 
val tych = cterm_of sign 

553 
val ants = Logic.strip_imp_prems prop 

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

555 
in 

556 
U.rev_itlist rename_params_rule news thm 

557 
end; 

558 

559 

560 
(* 

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

562 
**) 

563 

564 
fun list_beta_conv tm = 

565 
let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th)))) 

566 
fun iter [] = reflexive tm 

567 
 iter (v::rst) = rbeta (combination(iter rst) (reflexive v)) 

568 
in iter end; 

569 

570 

571 
(* 

572 
* Trace information for the rewriter 

573 
**) 

574 
val term_ref = ref[] : term list ref 

575 
val mss_ref = ref [] : meta_simpset list ref; 

576 
val thm_ref = ref [] : thm list ref; 

577 
val tracing = ref false; 

578 

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

580 

581 
fun print_thms s L = 

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

583 

584 
fun print_cterms s L = 

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

586 

587 

588 
(* 

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

590 
**) 

591 
fun mk_aabs(vstr,body) = S.mk_abs{Bvar=vstr,Body=body} 

10015  592 
handle _ => S.mk_pabs{varstruct = vstr, body = body}; (* FIXME do not handle _ !!! *) 
6498  593 

594 
fun list_mk_aabs (vstrl,tm) = 

595 
U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm; 

596 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

597 
fun dest_aabs used tm = 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

598 
let val ({Bvar,Body}, used') = S.dest_abs used tm 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

599 
in (Bvar, Body, used') end handle _ => (* FIXME do not handle _ !!! *) 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

600 
let val {varstruct, body, used} = S.dest_pabs used tm 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

601 
in (varstruct, body, used) end; 
6498  602 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

603 
fun strip_aabs used tm = 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

604 
let val (vstr, body, used') = dest_aabs used tm 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

605 
val (bvs, core, used'') = strip_aabs used' body 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

606 
in (vstr::bvs, core, used'') 
6498  607 
end 
10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

608 
handle _ => ([], tm, used); (* FIXME do not handle _ !!! *) 
6498  609 

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

611 
 dest_combn tm n = 

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

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

614 
in (f,Rand::rands) 

615 
end; 

616 

617 

618 

619 

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

621 
fun mk_fst tm = 

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

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

624 
fun mk_snd tm = 

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

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

627 
in 

628 
fun XFILL tych x vstruct = 

629 
let fun traverse p xocc L = 

630 
if (is_Free p) 

631 
then tych xocc::L 

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

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

634 
end 

635 
in 

636 
traverse vstruct x [] 

637 
end end; 

638 

639 
(* 

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

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

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

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

644 
* the wrong word to use). 

645 
**) 

646 

647 
fun VSTRUCT_ELIM tych a vstr th = 

648 
let val L = S.free_vars_lr vstr 

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

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

651 
val thm2 = forall_intr_list (map tych L) thm1 

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

653 
in refl RS 

654 
rewrite_rule[symmetric (surjective_pairing RS eq_reflection)] thm3 

655 
end; 

656 

657 
fun PGEN tych a vstr th = 

658 
let val a1 = tych a 

659 
val vstr1 = tych vstr 

660 
in 

661 
forall_intr a1 

662 
(if (is_Free vstr) 

663 
then cterm_instantiate [(vstr1,a1)] th 

664 
else VSTRUCT_ELIM tych a vstr th) 

665 
end; 

666 

667 

668 
(* 

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

670 
* 

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

672 
**) 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

673 
fun dest_pbeta_redex used M n = 
6498  674 
let val (f,args) = dest_combn M n 
10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

675 
val dummy = dest_aabs used f 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

676 
in (strip_aabs used f,args) 
6498  677 
end; 
678 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

679 
fun pbeta_redex M n = U.can (U.C (dest_pbeta_redex []) n) M; 
6498  680 

681 
fun dest_impl tm = 

682 
let val ants = Logic.strip_imp_prems tm 

683 
val eq = Logic.strip_imp_concl tm 

684 
in (ants,get_lhs eq) 

685 
end; 

686 

687 
fun restricted t = is_some (S.find_term 

10212  688 
(fn (Const("Wellfounded_Recursion.cut",_)) =>true  _ => false) 
6498  689 
t) 
690 

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

692 
let val globals = func::G 

693 
val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection]; 

694 
val tc_list = ref[]: term list ref 

695 
val dummy = term_ref := [] 

696 
val dummy = thm_ref := [] 

697 
val dummy = mss_ref := [] 

698 
val cut_lemma' = cut_lemma RS eq_reflection 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

699 
fun prover used mss thm = 
6498  700 
let fun cong_prover mss thm = 
701 
let val dummy = say "cong_prover:" 

702 
val cntxt = prems_of_mss mss 

703 
val dummy = print_thms "cntxt:" cntxt 

704 
val dummy = say "cong rule:" 

705 
val dummy = say (string_of_thm thm) 

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

707 
val dummy = mss_ref := (mss :: !mss_ref) 

708 
(* Unquantified eliminate *) 

709 
fun uq_eliminate (thm,imp,sign) = 

710 
let val tych = cterm_of sign 

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

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

713 
val eq = Logic.strip_imp_concl imp 

714 
val lhs = tych(get_lhs eq) 

715 
val mss' = add_prems(mss, map ASSUME ants) 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

716 
val lhs_eq_lhs1 = Thm.rewrite_cterm (false,true,false) mss' (prover used) lhs 
10015  717 
handle _ => reflexive lhs (* FIXME do not handle _ !!! *) 
6498  718 
val dummy = print_thms "proven:" [lhs_eq_lhs1] 
719 
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 

720 
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq 

721 
in 

722 
lhs_eeq_lhs2 COMP thm 

723 
end 

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

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

725 
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist) 
6498  726 
val dummy = assert (forall (op aconv) 
727 
(ListPair.zip (vlist, args))) 

728 
"assertion failed in CONTEXT_REWRITE_RULE" 

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

730 
imp_body 

731 
val tych = cterm_of sign 

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

733 
val eq1 = Logic.strip_imp_concl imp_body1 

734 
val Q = get_lhs eq1 

735 
val QeqQ1 = pbeta_reduce (tych Q) 

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

737 
val mss' = add_prems(mss, map ASSUME ants1) 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

738 
val Q1eeqQ2 = Thm.rewrite_cterm (false,true,false) mss' (prover used') Q1 
10015  739 
handle _ => reflexive Q1 (* FIXME do not handle _ !!! *) 
6498  740 
val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2))) 
741 
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) 

742 
val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection) 

743 
val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 

10015  744 
val QeeqQ3 = transitive thA Q2eeqQ3 handle _ => (* FIXME do not handle _ !!! *) 
6498  745 
((Q2eeqQ3 RS meta_eq_to_obj_eq) 
746 
RS ((thA RS meta_eq_to_obj_eq) RS trans)) 

747 
RS eq_reflection 

748 
val impth = implies_intr_list ants1 QeeqQ3 

749 
val impth1 = impth RS meta_eq_to_obj_eq 

750 
(* Need to abstract *) 

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

752 
in ant_th COMP thm 

753 
end 

754 
fun q_eliminate (thm,imp,sign) = 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

755 
let val (vlist, imp_body, used') = strip_all used imp 
6498  756 
val (ants,Q) = dest_impl imp_body 
757 
in if (pbeta_redex Q) (length vlist) 

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

759 
else 

760 
let val tych = cterm_of sign 

761 
val ants1 = map tych ants 

762 
val mss' = add_prems(mss, map ASSUME ants1) 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

763 
val Q_eeq_Q1 = Thm.rewrite_cterm 
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

764 
(false,true,false) mss' (prover used') (tych Q) 
10015  765 
handle _ => reflexive (tych Q) (* FIXME do not handle _ !!! *) 
6498  766 
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 
767 
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq 

768 
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2 

769 
in 

770 
ant_th COMP thm 

771 
end end 

772 

773 
fun eliminate thm = 

774 
case (rep_thm thm) 

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

776 
eliminate 

777 
(if not(is_all imp) 

778 
then uq_eliminate (thm,imp,sign) 

779 
else q_eliminate (thm,imp,sign)) 

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

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

782 
in Some(eliminate (rename thm)) 

10015  783 
end handle _ => None (* FIXME do not handle _ !!! *) 
6498  784 

785 
fun restrict_prover mss thm = 

786 
let val dummy = say "restrict_prover:" 

787 
val cntxt = rev(prems_of_mss mss) 

788 
val dummy = print_thms "cntxt:" cntxt 

789 
val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, 

790 
sign,...} = rep_thm thm 

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

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

793 
in U.itlist Forall vlist tm 

794 
end 

795 
(* 

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

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

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

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

800 
* of "f" will match. 

801 
**) 

802 
val func_name = #1(dest_Const func) 

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

804 
 is_func _ = false 

805 
val rcontext = rev cntxt 

806 
val cncl = HOLogic.dest_Trueprop o #prop o rep_thm 

807 
val antl = case rcontext of [] => [] 

808 
 _ => [S.list_mk_conj(map cncl rcontext)] 

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

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

811 
val dummy = print_cterms "TC:" 

812 
[cterm_of sign (HOLogic.mk_Trueprop TC)] 

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

814 
val nestedp = is_some (S.find_term is_func TC) 

815 
val dummy = if nestedp then say "nested" else say "not_nested" 

816 
val dummy = term_ref := ([func,TC]@(!term_ref)) 

817 
val th' = if nestedp then raise RULES_ERR{func = "solver", 

818 
mesg = "nested function"} 

819 
else let val cTC = cterm_of sign 

820 
(HOLogic.mk_Trueprop TC) 

821 
in case rcontext of 

822 
[] => SPEC_ALL(ASSUME cTC) 

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

824 
(LIST_CONJ rcontext) 

825 
end 

826 
val th'' = th' RS thm 

827 
in Some (th'') 

10015  828 
end handle _ => None (* FIXME do not handle _ !!! *) 
6498  829 
in 
830 
(if (is_cong thm) then cong_prover else restrict_prover) mss thm 

831 
end 

832 
val ctm = cprop_of th 

10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

833 
val names = add_term_names (term_of ctm, []) 
7262  834 
val th1 = Thm.rewrite_cterm(false,true,false) 
10117
8e58b3045e29
Now some functions try to avoid name clashes when introducing new free
berghofe
parents:
10015
diff
changeset

835 
(add_congs(mss_of [cut_lemma'], congs)) (prover names) ctm 
6498  836 
val th2 = equal_elim th1 th 
837 
in 

838 
(th2, filter (not o restricted) (!tc_list)) 

839 
end; 

840 

841 

842 

843 
fun prove (ptm,tac) = 

844 
#1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac]))); 

845 

846 

847 
end; (* Rules *) 