author  paulson 
Thu, 01 Oct 1998 18:30:05 +0200  
changeset 5601  b6456ccd9e3e 
parent 5081  7274f7d101ee 
child 5962  0f7375e5e977 
permissions  rwrr 
3302  1 
(* Title: TFL/rules 
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 

3391
5e45dd3b64e9
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3379
diff
changeset

9 
structure Rules : Rules_sig = 
2112  10 
struct 
11 

12 
open Utils; 

13 

14 
structure USyntax = USyntax; 

15 
structure S = USyntax; 

16 
structure U = Utils; 

17 
structure D = Dcterm; 

18 

19 

3391
5e45dd3b64e9
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3379
diff
changeset

20 
fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg}; 
2112  21 

22 

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

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

25 

26 
fun dest_thm thm = 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

27 
let val {prop,hyps,...} = rep_thm thm 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

28 
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) 
2112  29 
end; 
30 

31 

32 

33 
(* Inference rules *) 

34 

35 
(* 

36 
* Equality (one step) 

37 
**) 

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

39 
fun SYM thm = thm RS sym; 

40 

41 
fun ALPHA thm ctm1 = 

42 
let val ctm2 = cprop_of thm 

43 
val ctm2_eq = reflexive ctm2 

44 
val ctm1_eq = reflexive ctm1 

45 
in equal_elim (transitive ctm2_eq ctm1_eq) thm 

46 
end; 

47 

48 

49 
(* 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

50 
* typ instantiation 
2112  51 
**) 
52 
fun INST_TYPE blist thm = 

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

3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

54 
val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist 
2112  55 
in Thm.instantiate (blist',[]) thm 
56 
end 

57 
handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""}; 

58 

59 

60 
(* 

61 
* Implication and the assumption list 

62 
* 

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

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

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

66 
**) 

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

68 

69 

70 
(* 

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

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

73 
**) 

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

75 

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

77 

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

79 

80 

81 
fun FILTER_DISCH_ALL P thm = 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

82 
let fun check tm = U.holds P (#t(rep_cterm tm)) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

83 
in foldr (fn (tm,th) => if (check tm) then DISCH tm th else th) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

84 
(chyps thm, thm) 
2112  85 
end; 
86 

87 
(* freezeT expensive! *) 

88 
fun UNDISCH thm = 

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

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

91 
end 

92 
handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""}; 

93 

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

95 

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

97 
val dummy = by (rtac impI 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

98 
val dummy = by (rtac (p2 RS mp) 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

99 
val dummy = by (rtac (p1 RS mp) 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

100 
val dummy = by (assume_tac 1) 
2112  101 
val imp_trans = result() 
102 
in 

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

104 
end; 

105 

106 
(* 

107 
* Conjunction 

108 
**) 

109 
fun CONJUNCT1 thm = (thm RS conjunct1) 

110 
fun CONJUNCT2 thm = (thm RS conjunct2); 

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

112 
handle _ => [th]; 

113 

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

115 
 LIST_CONJ [th] = th 

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

117 

118 

119 
(* 

120 
* Disjunction 

121 
**) 

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

123 
val [P,Q] = term_vars prop 

124 
val disj1 = forall_intr (cterm_of sign Q) disjI1 

125 
in 

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

127 
end; 

128 

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

130 
val [P,Q] = term_vars prop 

131 
val disj2 = forall_intr (cterm_of sign P) disjI2 

132 
in 

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

134 
end; 

135 

136 

137 
(* 

138 
* 

139 
* A1  M1, ..., An  Mn 

140 
*  

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

142 
* 

143 
**) 

144 

145 

146 
fun EVEN_ORS thms = 

147 
let fun blue ldisjs [] _ = [] 

148 
 blue ldisjs (th::rst) rdisjs = 

149 
let val tail = tl rdisjs 

150 
val rdisj_tl = D.list_mk_disj tail 

151 
in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl) 

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

153 
end handle _ => [itlist DISJ2 ldisjs th] 

154 
in 

155 
blue [] thms (map cconcl thms) 

156 
end; 

157 

158 

159 
(* 

160 
* 

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

162 
*  

163 
* A U B U C  R 

164 
* 

165 
**) 

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

167 
val dummy = by (rtac (p1 RS disjE) 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

168 
val dummy = by (rtac (p2 RS mp) 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

169 
val dummy = by (assume_tac 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

170 
val dummy = by (rtac (p3 RS mp) 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

171 
val dummy = by (assume_tac 1) 
2112  172 
val tfl_exE = result() 
173 
in 

174 
fun DISJ_CASES th1 th2 th3 = 

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

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

177 
val th2' = DISCH disj1 th2 

178 
val th3' = DISCH disj2 th3 

179 
in 

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

181 
end 

182 
end; 

183 

184 

185 
(* 

186 
* 

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

188 
*  

189 
*  M 

190 
* 

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

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

193 
* theorem). 

194 
**) 

195 

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

197 
let fun extract a alist = 

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

199 
mesg = "not a permutation.1"} 

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

201 
in ex ([],alist) 

202 
end 

203 
fun place [] [] = [] 

204 
 place (a::rst) alist = 

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

206 
in item::place rst next 

207 
end 

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

209 
mesg = "not a permutation.2"} 

210 
in place 

211 
end; 

212 
(* freezeT expensive! *) 

213 
fun DISJ_CASESL disjth thl = 

214 
let val c = cconcl disjth 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

215 
fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

216 
aconv term_of atm) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

217 
(#hyps(rep_thm th)) 
2112  218 
val tml = D.strip_disj c 
219 
fun DL th [] = raise RULES_ERR{func="DISJ_CASESL",mesg="no cases"} 

220 
 DL th [th1] = PROVE_HYP th th1 

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

222 
 DL th (th1::rst) = 

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

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

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

226 
end; 

227 

228 

229 
(* 

230 
* Universals 

231 
**) 

232 
local (* this is fragile *) 

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

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

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

236 
val gspec = forall_intr (cterm_of sign x) spec 

237 
in 

238 
fun SPEC tm thm = 

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

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

241 
in thm RS (forall_elim tm gspec') 

242 
end 

243 
end; 

244 

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

246 

247 
val ISPEC = SPEC 

248 
val ISPECL = rev_itlist ISPEC; 

249 

250 
(* Not optimized! Too complicated. *) 

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

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

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

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

255 
let val ctm2 = cterm_of s tm2 

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

257 
end) 

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

259 
ctm_theta s tm_theta) 

260 
in 

261 
fun GEN v th = 

262 
let val gth = forall_intr v th 

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

264 
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) 
2112  265 
val tsig = #tsig(Sign.rep_sg sign) 
266 
val theta = Pattern.match tsig (P,P') 

267 
val allI2 = instantiate (certify sign theta) allI 

268 
val thm = implies_elim allI2 gth 

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

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

271 
in ALPHA thm (cterm_of sign prop') 

272 
end 

273 
end; 

274 

275 
val GENL = itlist GEN; 

276 

277 
fun GEN_ALL thm = 

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

279 
val tycheck = cterm_of sign 

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

281 
in GENL vlist thm 

282 
end; 

283 

284 

285 
fun MATCH_MP th1 th2 = 

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

287 
then MATCH_MP (th1 RS spec) th2 

288 
else MP th1 th2; 

289 

290 

291 
(* 

292 
* Existentials 

293 
**) 

294 

295 

296 

297 
(* 

298 
* Existential elimination 

299 
* 

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

301 
*  (variable v occurs nowhere) 

302 
* A1 u A2  t' 

303 
* 

304 
**) 

305 

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

307 
val dummy = by (rtac (p1 RS exE) 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

308 
val dummy = by (rtac ((p2 RS allE) RS mp) 1) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

309 
val dummy = by (assume_tac 2) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

310 
val dummy = by (assume_tac 1) 
2112  311 
val choose_thm = result() 
312 
in 

313 
fun CHOOSE(fvar,exth) fact = 

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

315 
val redex = capply lam fvar 

3405  316 
val {sign, t = t$u,...} = rep_cterm redex 
317 
val residue = cterm_of sign (betapply(t,u)) 

2112  318 
in GEN fvar (DISCH residue fact) RS (exth RS choose_thm) 
319 
end 

320 
end; 

321 

322 

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

324 
val [P,x] = term_vars prop 

325 
in 

326 
fun EXISTS (template,witness) thm = 

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

328 
val P' = cterm_of sign P 

329 
val x' = cterm_of sign x 

330 
val abstr = #2(dest_comb template) 

331 
in 

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

333 
end 

334 
end; 

335 

336 
(* 

337 
* 

338 
* A  M 

339 
*  [v_1,...,v_n] 

340 
* A  ?v1...v_n. M 

341 
* 

342 
**) 

343 

344 
fun EXISTL vlist th = 

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

346 
vlist th; 

347 

348 

349 
(* 

350 
* 

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

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

353 
* A  ?y_1...y_n. M 

354 
* 

355 
**) 

3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

356 
(* Could be improved, but needs "subst_free" for certified terms *) 
2112  357 

358 
fun IT_EXISTS blist th = 

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

360 
val tych = cterm_of sign 

361 
val detype = #t o rep_cterm 

3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

362 
val blist' = map (fn (x,y) => (detype x, detype y)) blist 
2112  363 
fun ?v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M}) 
364 

365 
in 

3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

366 
U.itlist (fn (b as (r1,r2)) => fn thm => 
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

367 
EXISTS(?r2(subst_free[b] 
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

368 
(HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1) 
2112  369 
thm) 
370 
blist' th 

371 
end; 

372 

373 
(* 

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

375 
* fun IT_EXISTS blist th = 

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

377 
* val tych = cterm_of sign 

3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

378 
* fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y) 
2112  379 
* in 
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

380 
* fold (fn (b as (r1,r2), thm) => 
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

381 
* EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))), 
2112  382 
* r1) thm) blist th 
383 
* end; 

384 
**) 

385 

386 
(* 

387 
* Rewriting 

388 
**) 

389 

390 
fun SUBS thl = 

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

392 

5081  393 
local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None)) 
2112  394 
in 
3405  395 
fun simpl_conv ss thl ctm = 
3556  396 
rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm 
2112  397 
RS meta_eq_to_obj_eq 
398 
end; 

399 

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

401 
in 

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

403 
val ASM = refl RS iffD1 

404 
end; 

405 

406 

407 

408 

409 
(* 

410 
* TERMINATION CONDITION EXTRACTION 

411 
**) 

412 

413 

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

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

416 

417 

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

419 
fun is_cong thm = 

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

421 
in case prop 

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

423 
(Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false 

424 
 _ => true 

425 
end; 

426 

427 

428 

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

3379
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

430 
(Const ("Trueprop",_) $ lhs) 
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

431 
$ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs} 
2112  432 
 dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} 
433 
 dest_equal tm = S.dest_eq tm; 

434 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

435 
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); 
2112  436 

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

438 
 dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"}; 

439 

440 
val is_all = Utils.can dest_all; 

441 

442 
fun strip_all fm = 

443 
if (is_all fm) 

444 
then let val {Bvar,Body} = dest_all fm 

445 
val (bvs,core) = strip_all Body 

446 
in ((Bvar::bvs), core) 

447 
end 

448 
else ([],fm); 

449 

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

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

452 

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

454 
let val (L,core) = list_break_all body 

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

456 
end 

457 
 list_break_all tm = ([],tm); 

458 

459 
(* 

460 
* Rename a term of the form 

461 
* 

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

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

464 
* to one of 

465 
* 

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

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

468 
* 

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

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

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

472 
**) 

473 

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

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

476 
case (list_break_all ant) 

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

478 
 (vlist,body) => 

479 
let val eq = Logic.strip_imp_concl body 

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

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

3405  482 
val names = variantlist (map (#1 o dest_Free) vstrl, 
483 
add_term_names(body, [])) 

2112  484 
in get (rst, n+1, (names,n)::L) 
485 
end handle _ => get (rst, n+1, L); 

486 

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

488 
fun rename thm = 

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

490 
val tych = cterm_of sign 

491 
val ants = Logic.strip_imp_prems prop 

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

493 
in 

494 
U.rev_itlist rename_params_rule news thm 

495 
end; 

496 

497 

498 
(* 

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

500 
**) 

501 

502 
fun list_beta_conv tm = 

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

504 
fun iter [] = reflexive tm 

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

506 
in iter end; 

507 

508 

509 
(* 

510 
* Trace information for the rewriter 

511 
**) 

512 
val term_ref = ref[] : term list ref 

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

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

515 
val tracing = ref false; 

516 

3629  517 
fun say s = if !tracing then prs s else (); 
2112  518 

519 
fun print_thms s L = 

520 
(say s; 

521 
map (fn th => say (string_of_thm th ^"\n")) L; 

522 
say"\n"); 

523 

524 
fun print_cterms s L = 

525 
(say s; 

526 
map (fn th => say (string_of_cterm th ^"\n")) L; 

527 
say"\n"); 

528 

529 
(* 

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

531 
**) 

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

533 
handle _ => S.mk_pabs{varstruct = vstr, body = body}; 

534 

535 
fun list_mk_aabs (vstrl,tm) = 

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

537 

538 
fun dest_aabs tm = 

539 
let val {Bvar,Body} = S.dest_abs tm 

540 
in (Bvar,Body) 

541 
end handle _ => let val {varstruct,body} = S.dest_pabs tm 

542 
in (varstruct,body) 

543 
end; 

544 

545 
fun strip_aabs tm = 

546 
let val (vstr,body) = dest_aabs tm 

547 
val (bvs, core) = strip_aabs body 

548 
in (vstr::bvs, core) 

549 
end 

550 
handle _ => ([],tm); 

551 

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

553 
 dest_combn tm n = 

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

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

556 
in (f,Rand::rands) 

557 
end; 

558 

559 

560 

561 

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

563 
fun mk_fst tm = 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

564 
let val ty as Type("*", [fty,sty]) = type_of tm 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

565 
in Const ("fst", ty > fty) $ tm end 
2112  566 
fun mk_snd tm = 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

567 
let val ty as Type("*", [fty,sty]) = type_of tm 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

568 
in Const ("snd", ty > sty) $ tm end 
2112  569 
in 
570 
fun XFILL tych x vstruct = 

571 
let fun traverse p xocc L = 

3332  572 
if (is_Free p) 
2112  573 
then tych xocc::L 
574 
else let val (p1,p2) = dest_pair p 

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

576 
end 

577 
in 

578 
traverse vstruct x [] 

579 
end end; 

580 

581 
(* 

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

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

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

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

586 
* the wrong word to use). 

587 
**) 

588 

589 
fun VSTRUCT_ELIM tych a vstr th = 

590 
let val L = S.free_vars_lr vstr 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

591 
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr))) 
2112  592 
val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th) 
593 
val thm2 = forall_intr_list (map tych L) thm1 

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

595 
in refl RS 

596 
rewrite_rule[symmetric (surjective_pairing RS eq_reflection)] thm3 

597 
end; 

598 

599 
fun PGEN tych a vstr th = 

600 
let val a1 = tych a 

601 
val vstr1 = tych vstr 

602 
in 

603 
forall_intr a1 

3332  604 
(if (is_Free vstr) 
2112  605 
then cterm_instantiate [(vstr1,a1)] th 
606 
else VSTRUCT_ELIM tych a vstr th) 

607 
end; 

608 

609 

610 
(* 

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

612 
* 

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

614 
**) 

615 
fun dest_pbeta_redex M n = 

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

617 
val dummy = dest_aabs f 
2112  618 
in (strip_aabs f,args) 
619 
end; 

620 

621 
fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M; 

622 

623 
fun dest_impl tm = 

624 
let val ants = Logic.strip_imp_prems tm 

625 
val eq = Logic.strip_imp_concl tm 

626 
in (ants,get_lhs eq) 

627 
end; 

628 

3405  629 
fun restricted t = is_some (S.find_term 
630 
(fn (Const("cut",_)) =>true  _ => false) 

631 
t) 

2112  632 

3405  633 
fun CONTEXT_REWRITE_RULE (ss, func, R, cut_lemma, congs) th = 
634 
let val pbeta_reduce = simpl_conv ss [split RS eq_reflection]; 

635 
val tc_list = ref[]: term list ref 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

636 
val dummy = term_ref := [] 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

637 
val dummy = thm_ref := [] 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

638 
val dummy = mss_ref := [] 
2112  639 
val cut_lemma' = (cut_lemma RS mp) RS eq_reflection 
640 
fun prover mss thm = 

641 
let fun cong_prover mss thm = 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

642 
let val dummy = say "cong_prover:\n" 
2112  643 
val cntxt = prems_of_mss mss 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

644 
val dummy = print_thms "cntxt:\n" cntxt 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

645 
val dummy = say "cong rule:\n" 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

646 
val dummy = say (string_of_thm thm^"\n") 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

647 
val dummy = thm_ref := (thm :: !thm_ref) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

648 
val dummy = mss_ref := (mss :: !mss_ref) 
2112  649 
(* Unquantified eliminate *) 
650 
fun uq_eliminate (thm,imp,sign) = 

651 
let val tych = cterm_of sign 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

652 
val dummy = print_cterms "To eliminate:\n" [tych imp] 
2112  653 
val ants = map tych (Logic.strip_imp_prems imp) 
654 
val eq = Logic.strip_imp_concl imp 

655 
val lhs = tych(get_lhs eq) 

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

5081  657 
val lhs_eq_lhs1 = Thm.rewrite_cterm(false,true,false)mss' prover lhs 
2112  658 
handle _ => reflexive lhs 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

659 
val dummy = print_thms "proven:\n" [lhs_eq_lhs1] 
2112  660 
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 
661 
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq 

662 
in 

663 
lhs_eeq_lhs2 COMP thm 

664 
end 

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

666 
let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist) 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

667 
val dummy = assert (forall (op aconv) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

668 
(ListPair.zip (vlist, args))) 
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

669 
"assertion failed in CONTEXT_REWRITE_RULE" 
3353
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

670 
val imp_body1 = subst_free (ListPair.zip (args, vstrl)) 
9112a2efb9a3
Removal of module Mask and datatype binding with its constructor >
paulson
parents:
3332
diff
changeset

671 
imp_body 
2112  672 
val tych = cterm_of sign 
673 
val ants1 = map tych (Logic.strip_imp_prems imp_body1) 

674 
val eq1 = Logic.strip_imp_concl imp_body1 

675 
val Q = get_lhs eq1 

676 
val QeqQ1 = pbeta_reduce (tych Q) 

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

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

5081  679 
val Q1eeqQ2 = Thm.rewrite_cterm (false,true,false) mss' prover Q1 
2112  680 
handle _ => reflexive Q1 
3379
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

681 
val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2))) 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

682 
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) 
2112  683 
val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection) 
684 
val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 

685 
val QeeqQ3 = transitive thA Q2eeqQ3 handle _ => 

686 
((Q2eeqQ3 RS meta_eq_to_obj_eq) 

687 
RS ((thA RS meta_eq_to_obj_eq) RS trans)) 

688 
RS eq_reflection 

689 
val impth = implies_intr_list ants1 QeeqQ3 

690 
val impth1 = impth RS meta_eq_to_obj_eq 

691 
(* Need to abstract *) 

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

693 
in ant_th COMP thm 

694 
end 

695 
fun q_eliminate (thm,imp,sign) = 

696 
let val (vlist,imp_body) = strip_all imp 

697 
val (ants,Q) = dest_impl imp_body 

698 
in if (pbeta_redex Q) (length vlist) 

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

700 
else 

701 
let val tych = cterm_of sign 

702 
val ants1 = map tych ants 

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

5081  704 
val Q_eeq_Q1 = Thm.rewrite_cterm(false,true,false) mss' 
2112  705 
prover (tych Q) 
706 
handle _ => reflexive (tych Q) 

707 
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 

708 
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq 

709 
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2 

710 
in 

711 
ant_th COMP thm 

712 
end end 

713 

714 
fun eliminate thm = 

715 
case (rep_thm thm) 

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

717 
eliminate 

718 
(if not(is_all imp) 

719 
then uq_eliminate (thm,imp,sign) 

720 
else q_eliminate (thm,imp,sign)) 

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

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

723 
in Some(eliminate (rename thm)) 

724 
end handle _ => None 

725 

726 
fun restrict_prover mss thm = 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

727 
let val dummy = say "restrict_prover:\n" 
2112  728 
val cntxt = rev(prems_of_mss mss) 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

729 
val dummy = print_thms "cntxt:\n" cntxt 
2112  730 
val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, 
731 
sign,...} = rep_thm thm 

3391
5e45dd3b64e9
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3379
diff
changeset

732 
fun genl tm = let val vlist = gen_rems (op aconv) 
5e45dd3b64e9
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3379
diff
changeset

733 
(add_term_frees(tm,[]), [func,R]) 
2112  734 
in U.itlist Forall vlist tm 
735 
end 

736 
(* 

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

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

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

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

741 
* of "f" will match. 

742 
**) 

3405  743 
val func_name = #1(dest_Const func) 
744 
fun is_func (Const (name,_)) = (name = func_name) 

745 
 is_func _ = false 

2112  746 
val rcontext = rev cntxt 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

747 
val cncl = HOLogic.dest_Trueprop o #prop o rep_thm 
2112  748 
val antl = case rcontext of [] => [] 
749 
 _ => [S.list_mk_conj(map cncl rcontext)] 

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

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

751 
val dummy = print_cterms "func:\n" [cterm_of sign func] 
3379
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

752 
val dummy = print_cterms "TC:\n" 
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

753 
[cterm_of sign (HOLogic.mk_Trueprop TC)] 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

754 
val dummy = tc_list := (TC :: !tc_list) 
3405  755 
val nestedp = is_some (S.find_term is_func TC) 
3379
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

756 
val dummy = if nestedp then say"nested\n" else say"not_nested\n" 
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

757 
val dummy = term_ref := ([func,TC]@(!term_ref)) 
2112  758 
val th' = if nestedp then raise RULES_ERR{func = "solver", 
759 
mesg = "nested function"} 

3379
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

760 
else let val cTC = cterm_of sign 
7091ffa99c93
Simplified the calling sequence of CONTEXT_REWRITE_RULE
paulson
parents:
3353
diff
changeset

761 
(HOLogic.mk_Trueprop TC) 
2112  762 
in case rcontext of 
763 
[] => SPEC_ALL(ASSUME cTC) 

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

765 
(LIST_CONJ rcontext) 

766 
end 

767 
val th'' = th' RS thm 

768 
in Some (th'') 

769 
end handle _ => None 

770 
in 

771 
(if (is_cong thm) then cong_prover else restrict_prover) mss thm 

772 
end 

773 
val ctm = cprop_of th 

5081  774 
val th1 = Thm.rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs)) 
2112  775 
prover ctm 
776 
val th2 = equal_elim th1 th 

777 
in 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset

778 
(th2, filter (not o restricted) (!tc_list)) 
2112  779 
end; 
780 

781 

782 

3405  783 
fun prove (ptm,tac) = 
784 
#1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac]))); 

2112  785 

786 

787 
end; (* Rules *) 