author  nipkow 
Fri, 14 Jan 1994 08:09:07 +0100  
changeset 225  76f60e6400e8 
parent 222  5eb3020f7a03 
child 229  4002c4cd450c 
permissions  rwrr 
0  1 
(* Title: thm 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
The abstract types "theory" and "thm" 

7 
*) 

8 

9 
signature THM = 

10 
sig 

11 
structure Envir : ENVIR 

12 
structure Sequence : SEQUENCE 

13 
structure Sign : SIGN 

14 
type meta_simpset 

15 
type theory 

16 
type thm 

17 
exception THM of string * int * thm list 

18 
exception THEORY of string * theory list 

19 
exception SIMPLIFIER of string * thm 

20 
val abstract_rule: string > Sign.cterm > thm > thm 

21 
val add_congs: meta_simpset * thm list > meta_simpset 

22 
val add_prems: meta_simpset * thm list > meta_simpset 

23 
val add_simps: meta_simpset * thm list > meta_simpset 

24 
val assume: Sign.cterm > thm 

25 
val assumption: int > thm > thm Sequence.seq 

26 
val axioms_of: theory > (string * thm) list 

27 
val beta_conversion: Sign.cterm > thm 

28 
val bicompose: bool > bool * thm * int > int > thm > thm Sequence.seq 

29 
val biresolution: bool > (bool*thm)list > int > thm > thm Sequence.seq 

30 
val combination: thm > thm > thm 

31 
val concl_of: thm > term 

87  32 
val del_simps: meta_simpset * thm list > meta_simpset 
0  33 
val dest_state: thm * int > (term*term)list * term list * term * term 
34 
val empty_mss: meta_simpset 

35 
val eq_assumption: int > thm > thm 

36 
val equal_intr: thm > thm > thm 

37 
val equal_elim: thm > thm > thm 

38 
val extend_theory: theory > string 

39 
> (class * class list) list * sort 

40 
* (string list * int)list 

200  41 
* (string * indexname list * string) list 
0  42 
* (string list * (sort list * class))list 
43 
* (string list * string)list * Sign.Syntax.sext option 

44 
> (string*string)list > theory 

45 
val extensional: thm > thm 

46 
val flexflex_rule: thm > thm Sequence.seq 

47 
val flexpair_def: thm 

48 
val forall_elim: Sign.cterm > thm > thm 

49 
val forall_intr: Sign.cterm > thm > thm 

50 
val freezeT: thm > thm 

51 
val get_axiom: theory > string > thm 

52 
val implies_elim: thm > thm > thm 

53 
val implies_intr: Sign.cterm > thm > thm 

54 
val implies_intr_hyps: thm > thm 

55 
val instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list 

56 
> thm > thm 

57 
val lift_rule: (thm * int) > thm > thm 

58 
val merge_theories: theory * theory > theory 

59 
val mk_rews_of_mss: meta_simpset > thm > thm list 

60 
val mss_of: thm list > meta_simpset 

61 
val nprems_of: thm > int 

62 
val parents_of: theory > theory list 

63 
val prems_of: thm > term list 

64 
val prems_of_mss: meta_simpset > thm list 

65 
val pure_thy: theory 

66 
val reflexive: Sign.cterm > thm 

67 
val rename_params_rule: string list * int > thm > thm 

68 
val rep_thm: thm > {prop: term, hyps: term list, maxidx: int, sign: Sign.sg} 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

69 
val rewrite_cterm: 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

70 
bool*bool > meta_simpset > (meta_simpset > thm > thm option) 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

71 
> Sign.cterm > thm 
0  72 
val set_mk_rews: meta_simpset * (thm > thm list) > meta_simpset 
73 
val sign_of: theory > Sign.sg 

74 
val syn_of: theory > Sign.Syntax.syntax 

75 
val stamps_of_thm: thm > string ref list 

76 
val stamps_of_thy: theory > string ref list 

77 
val symmetric: thm > thm 

78 
val tpairs_of: thm > (term*term)list 

79 
val trace_simp: bool ref 

80 
val transitive: thm > thm > thm 

81 
val trivial: Sign.cterm > thm 

82 
val varifyT: thm > thm 

83 
end; 

84 

85 

86 

87 
functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN 

88 
and Net:NET 

89 
sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) 

219
a2447b00517b
commented out sig constraint of functor (for debugging purposes);
wenzelm
parents:
214
diff
changeset

90 
(*: THM*) = (* FIXME *) 
0  91 
struct 
92 
structure Sequence = Unify.Sequence; 

93 
structure Envir = Unify.Envir; 

94 
structure Sign = Unify.Sign; 

95 
structure Type = Sign.Type; 

96 
structure Syntax = Sign.Syntax; 

97 
structure Symtab = Sign.Symtab; 

98 

99 

100 
(*Metatheorems*) 

101 
datatype thm = Thm of 

102 
{sign: Sign.sg, maxidx: int, hyps: term list, prop: term}; 

103 

104 
fun rep_thm (Thm x) = x; 

105 

106 
(*Errors involving theorems*) 

107 
exception THM of string * int * thm list; 

108 

109 
(*maps objectrule to tpairs *) 

110 
fun tpairs_of (Thm{prop,...}) = #1 (Logic.strip_flexpairs prop); 

111 

112 
(*maps objectrule to premises *) 

113 
fun prems_of (Thm{prop,...}) = 

114 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 

115 

116 
(*counts premises in a rule*) 

117 
fun nprems_of (Thm{prop,...}) = 

118 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 

119 

120 
(*maps objectrule to conclusion *) 

121 
fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop; 

122 

123 
(*Stamps associated with a signature*) 

124 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; 

125 

126 
(*Theories. There is one pure theory. 

127 
A theory can be extended. Two theories can be merged.*) 

128 
datatype theory = 

129 
Pure of {sign: Sign.sg} 

130 
 Extend of {sign: Sign.sg, axioms: thm Symtab.table, thy: theory} 

131 
 Merge of {sign: Sign.sg, thy1: theory, thy2: theory}; 

132 

133 
(*Errors involving theories*) 

134 
exception THEORY of string * theory list; 

135 

136 
fun sign_of (Pure {sign}) = sign 

137 
 sign_of (Extend {sign,...}) = sign 

138 
 sign_of (Merge {sign,...}) = sign; 

139 

140 
val syn_of = #syn o Sign.rep_sg o sign_of; 

141 

142 
(*return the axioms of a theory and its ancestors*) 

143 
fun axioms_of (Pure _) = [] 

144 
 axioms_of (Extend{axioms,thy,...}) = Symtab.alist_of axioms 

145 
 axioms_of (Merge{thy1,thy2,...}) = axioms_of thy1 @ axioms_of thy2; 

146 

147 
(*return the immediate ancestors  also distinguishes the kinds of theories*) 

148 
fun parents_of (Pure _) = [] 

149 
 parents_of (Extend{thy,...}) = [thy] 

150 
 parents_of (Merge{thy1,thy2,...}) = [thy1,thy2]; 

151 

152 

153 
(*Merge theories of two theorems. Raise exception if incompatible. 

154 
Prefers (via Sign.merge) the signature of th1. *) 

155 
fun merge_theories(th1,th2) = 

156 
let val Thm{sign=sign1,...} = th1 and Thm{sign=sign2,...} = th2 

157 
in Sign.merge (sign1,sign2) end 

158 
handle TERM _ => raise THM("incompatible signatures", 0, [th1,th2]); 

159 

160 
(*Stamps associated with a theory*) 

161 
val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; 

162 

163 

164 
(**** Primitive rules ****) 

165 

166 
(* discharge all assumptions t from ts *) 

167 
val disch = gen_rem (op aconv); 

168 

169 
(*The assumption rule AA in a theory *) 

170 
fun assume ct : thm = 

171 
let val {sign, t=prop, T, maxidx} = Sign.rep_cterm ct 

172 
in if T<>propT then 

173 
raise THM("assume: assumptions must have type prop", 0, []) 

174 
else if maxidx <> ~1 then 

175 
raise THM("assume: assumptions may not contain scheme variables", 

176 
maxidx, []) 

177 
else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop} 

178 
end; 

179 

180 
(* Implication introduction 

181 
A  B 

182 
 

183 
A ==> B *) 

184 
fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm = 

185 
let val {sign=signA, t=A, T, maxidx=maxidxA} = Sign.rep_cterm cA 

186 
in if T<>propT then 

187 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 

188 
else Thm{sign= Sign.merge (sign,signA), maxidx= max[maxidxA, maxidx], 

189 
hyps= disch(hyps,A), prop= implies$A$prop} 

190 
handle TERM _ => 

191 
raise THM("implies_intr: incompatible signatures", 0, [thB]) 

192 
end; 

193 

194 
(* Implication elimination 

195 
A ==> B A 

196 
 

197 
B *) 

198 
fun implies_elim thAB thA : thm = 

199 
let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA 

200 
and Thm{sign, maxidx, hyps, prop,...} = thAB; 

201 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 

202 
in case prop of 

203 
imp$A$B => 

204 
if imp=implies andalso A aconv propA 

205 
then Thm{sign= merge_theories(thAB,thA), 

206 
maxidx= max[maxA,maxidx], 

207 
hyps= hypsA union hyps, (*dups suppressed*) 

208 
prop= B} 

209 
else err("major premise") 

210 
 _ => err("major premise") 

211 
end; 

212 

213 
(* Forall introduction. The Free or Var x must not be free in the hypotheses. 

214 
A 

215 
 

216 
!!x.A *) 

217 
fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) = 

218 
let val x = Sign.term_of cx; 

219 
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

220 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))} 

221 
in case x of 

222 
Free(a,T) => 

223 
if exists (apl(x, Logic.occs)) hyps 

224 
then raise THM("forall_intr: variable free in assumptions", 0, [th]) 

225 
else result(a,T) 

226 
 Var((a,_),T) => result(a,T) 

227 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 

228 
end; 

229 

230 
(* Forall elimination 

231 
!!x.A 

232 
 

233 
A[t/x] *) 

234 
fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm = 

235 
let val {sign=signt, t, T, maxidx=maxt} = Sign.rep_cterm ct 

236 
in case prop of 

237 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 

238 
if T<>qary then 

239 
raise THM("forall_elim: type mismatch", 0, [th]) 

240 
else Thm{sign= Sign.merge(sign,signt), 

241 
maxidx= max[maxidx, maxt], 

242 
hyps= hyps, prop= betapply(A,t)} 

243 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 

244 
end 

245 
handle TERM _ => 

246 
raise THM("forall_elim: incompatible signatures", 0, [th]); 

247 

248 

249 
(*** Equality ***) 

250 

251 
(*Definition of the relation =?= *) 

252 
val flexpair_def = 

253 
Thm{sign= Sign.pure, hyps= [], maxidx= 0, 

254 
prop= Sign.term_of 

255 
(Sign.read_cterm Sign.pure 

256 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}; 

257 

258 
(*The reflexivity rule: maps t to the theorem t==t *) 

259 
fun reflexive ct = 

260 
let val {sign, t, T, maxidx} = Sign.rep_cterm ct 

261 
in Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)} 

262 
end; 

263 

264 
(*The symmetry rule 

265 
t==u 

266 
 

267 
u==t *) 

268 
fun symmetric (th as Thm{sign,hyps,prop,maxidx}) = 

269 
case prop of 

270 
(eq as Const("==",_)) $ t $ u => 

271 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 

272 
 _ => raise THM("symmetric", 0, [th]); 

273 

274 
(*The transitive rule 

275 
t1==u u==t2 

276 
 

277 
t1==t2 *) 

278 
fun transitive th1 th2 = 

279 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

280 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

281 
fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) 

282 
in case (prop1,prop2) of 

283 
((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => 

284 
if not (u aconv u') then err"middle term" else 

285 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 

286 
maxidx= max[max1,max2], prop= eq$t1$t2} 

287 
 _ => err"premises" 

288 
end; 

289 

290 
(*Betaconversion: maps (%(x)t)(u) to the theorem (%(x)t)(u) == t[u/x] *) 

291 
fun beta_conversion ct = 

292 
let val {sign, t, T, maxidx} = Sign.rep_cterm ct 

293 
in case t of 

294 
Abs(_,_,bodt) $ u => 

295 
Thm{sign= sign, hyps= [], 

296 
maxidx= maxidx_of_term t, 

297 
prop= Logic.mk_equals(t, subst_bounds([u],bodt))} 

298 
 _ => raise THM("beta_conversion: not a redex", 0, []) 

299 
end; 

300 

301 
(*The extensionality rule (proviso: x not free in f, g, or hypotheses) 

302 
f(x) == g(x) 

303 
 

304 
f == g *) 

305 
fun extensional (th as Thm{sign,maxidx,hyps,prop}) = 

306 
case prop of 

307 
(Const("==",_)) $ (f$x) $ (g$y) => 

308 
let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) 

309 
in (if x<>y then err"different variables" else 

310 
case y of 

311 
Free _ => 

312 
if exists (apl(y, Logic.occs)) (f::g::hyps) 

313 
then err"variable free in hyps or functions" else () 

314 
 Var _ => 

315 
if Logic.occs(y,f) orelse Logic.occs(y,g) 

316 
then err"variable free in functions" else () 

317 
 _ => err"not a variable"); 

318 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

319 
prop= Logic.mk_equals(f,g)} 

320 
end 

321 
 _ => raise THM("extensional: premise", 0, [th]); 

322 

323 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 

324 
The bound variable will be named "a" (since x will be something like x320) 

325 
t == u 

326 
 

327 
%(x)t == %(x)u *) 

328 
fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) = 

329 
let val x = Sign.term_of cx; 

330 
val (t,u) = Logic.dest_equals prop 

331 
handle TERM _ => 

332 
raise THM("abstract_rule: premise not an equality", 0, [th]) 

333 
fun result T = 

334 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

335 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 

336 
Abs(a, T, abstract_over (x,u)))} 

337 
in case x of 

338 
Free(_,T) => 

339 
if exists (apl(x, Logic.occs)) hyps 

340 
then raise THM("abstract_rule: variable free in assumptions", 0, [th]) 

341 
else result T 

342 
 Var(_,T) => result T 

343 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 

344 
end; 

345 

346 
(*The combination rule 

347 
f==g t==u 

348 
 

349 
f(t)==g(u) *) 

350 
fun combination th1 th2 = 

351 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

352 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2 

353 
in case (prop1,prop2) of 

354 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 

355 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 

356 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} 

357 
 _ => raise THM("combination: premises", 0, [th1,th2]) 

358 
end; 

359 

360 

361 
(*The equal propositions rule 

362 
A==B A 

363 
 

364 
B *) 

365 
fun equal_elim th1 th2 = 

366 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

367 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

368 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) 

369 
in case prop1 of 

370 
Const("==",_) $ A $ B => 

371 
if not (prop2 aconv A) then err"not equal" else 

372 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 

373 
maxidx= max[max1,max2], prop= B} 

374 
 _ => err"major premise" 

375 
end; 

376 

377 

378 
(* Equality introduction 

379 
A==>B B==>A 

380 
 

381 
A==B *) 

382 
fun equal_intr th1 th2 = 

383 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

384 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

385 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 

386 
in case (prop1,prop2) of 

387 
(Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => 

388 
if A aconv A' andalso B aconv B' 

389 
then Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 

390 
maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} 

391 
else err"not equal" 

392 
 _ => err"premises" 

393 
end; 

394 

395 
(**** Derived rules ****) 

396 

397 
(*Discharge all hypotheses (need not verify cterms) 

398 
Repeated hypotheses are discharged only once; fold cannot do this*) 

399 
fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) = 

400 
implies_intr_hyps 

401 
(Thm{sign=sign, maxidx=maxidx, 

402 
hyps= disch(As,A), prop= implies$A$prop}) 

403 
 implies_intr_hyps th = th; 

404 

405 
(*Smash" unifies the list of term pairs leaving no flexflex pairs. 

406 
Instantiates the theorem and deletes trivial tpairs. 

407 
Resulting sequence may contain multiple elements if the tpairs are 

408 
not all flexflex. *) 

409 
fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) = 

410 
let fun newthm env = 

411 
let val (tpairs,horn) = 

412 
Logic.strip_flexpairs (Envir.norm_term env prop) 

413 
(*Remove trivial tpairs, of the form t=t*) 

414 
val distpairs = filter (not o op aconv) tpairs 

415 
val newprop = Logic.list_flexpairs(distpairs, horn) 

416 
in Thm{sign= sign, hyps= hyps, 

417 
maxidx= maxidx_of_term newprop, prop= newprop} 

418 
end; 

419 
val (tpairs,_) = Logic.strip_flexpairs prop 

420 
in Sequence.maps newthm 

421 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 

422 
end; 

423 

424 
(*Instantiation of Vars 

425 
A 

426 
 

427 
A[t1/v1,....,tn/vn] *) 

428 

429 
(*Check that all the terms are Vars and are distinct*) 

430 
fun instl_ok ts = forall is_Var ts andalso null(findrep ts); 

431 

432 
(*For instantiate: process pair of cterms, merge theories*) 

433 
fun add_ctpair ((ct,cu), (sign,tpairs)) = 

434 
let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct 

435 
and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu 

436 
in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs) 

437 
else raise TYPE("add_ctpair", [T,U], [t,u]) 

438 
end; 

439 

440 
fun add_ctyp ((v,ctyp), (sign',vTs)) = 

441 
let val {T,sign} = Sign.rep_ctyp ctyp 

442 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 

443 

444 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 

445 
Instantiates distinct Vars by terms of same type. 

446 
Normalizes the new theorem! *) 

447 
fun instantiate (vcTs,ctpairs) (th as Thm{sign,maxidx,hyps,prop}) = 

448 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); 

449 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); 

193  450 
val newprop = 
451 
Envir.norm_term (Envir.empty 0) 

452 
(subst_atomic tpairs 

453 
(Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop)) 

0  454 
val newth = Thm{sign= newsign, hyps= hyps, 
455 
maxidx= maxidx_of_term newprop, prop= newprop} 

193  456 
in if not(instl_ok(map #1 tpairs)) 
457 
then raise THM("instantiate: variables not distinct", 0, [th]) 

458 
else if not(null(findrep(map #1 vTs))) 

459 
then raise THM("instantiate: type variables not distinct", 0, [th]) 

460 
else (*Check types of Vars for agreement*) 

461 
case findrep (map (#1 o dest_Var) (term_vars newprop)) of 

462 
ix::_ => raise THM("instantiate: conflicting types for variable " ^ 

463 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

464 
 [] => 

465 
case findrep (map #1 (term_tvars newprop)) of 

466 
ix::_ => raise THM 

467 
("instantiate: conflicting sorts for type variable " ^ 

468 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

469 
 [] => newth 

0  470 
end 
471 
handle TERM _ => 

472 
raise THM("instantiate: incompatible signatures",0,[th]) 

193  473 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  474 

475 
(*The trivial implication A==>A, justified by assume and forall rules. 

476 
A can contain Vars, not so for assume! *) 

477 
fun trivial ct : thm = 

478 
let val {sign, t=A, T, maxidx} = Sign.rep_cterm ct 

479 
in if T<>propT then 

480 
raise THM("trivial: the term must have type prop", 0, []) 

481 
else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A} 

482 
end; 

483 

484 
(* Replace all TFrees not in the hyps by new TVars *) 

485 
fun varifyT(Thm{sign,maxidx,hyps,prop}) = 

486 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 

487 
in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps, 

488 
prop= Type.varify(prop,tfrees)} 

489 
end; 

490 

491 
(* Replace all TVars by new TFrees *) 

492 
fun freezeT(Thm{sign,maxidx,hyps,prop}) = 

493 
let val prop' = Type.freeze (K true) prop 

494 
in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end; 

495 

496 

497 
(*** Inference rules for tactics ***) 

498 

499 
(*Destruct proof state into constraints, other goals, goal(i), rest *) 

500 
fun dest_state (state as Thm{prop,...}, i) = 

501 
let val (tpairs,horn) = Logic.strip_flexpairs prop 

502 
in case Logic.strip_prems(i, [], horn) of 

503 
(B::rBs, C) => (tpairs, rev rBs, B, C) 

504 
 _ => raise THM("dest_state", i, [state]) 

505 
end 

506 
handle TERM _ => raise THM("dest_state", i, [state]); 

507 

508 
(*Increment variables and parameters of rule as required for 

509 
resolution with goal i of state. *) 

510 
fun lift_rule (state, i) orule = 

511 
let val Thm{prop=sprop,maxidx=smax,...} = state; 

512 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 

513 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 

514 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 

515 
val (Thm{sign,maxidx,hyps,prop}) = orule 

516 
val (tpairs,As,B) = Logic.strip_horn prop 

517 
in Thm{hyps=hyps, sign= merge_theories(state,orule), 

518 
maxidx= maxidx+smax+1, 

519 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 

520 
map lift_all As, lift_all B)} 

521 
end; 

522 

523 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 

524 
fun assumption i state = 

525 
let val Thm{sign,maxidx,hyps,prop} = state; 

526 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 

527 
fun newth (env as Envir.Envir{maxidx,asol,iTs}, tpairs) = 

528 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= 

529 
case (Envir.alist_of_olist asol, iTs) of 

530 
(*avoid wasted normalizations*) 

531 
([],[]) => Logic.rule_of(tpairs, Bs, C) 

532 
 _ => (*normalize the new rule fully*) 

533 
Envir.norm_term env (Logic.rule_of(tpairs, Bs, C))}; 

534 
fun addprfs [] = Sequence.null 

535 
 addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull 

536 
(Sequence.mapp newth 

537 
(Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) 

538 
(addprfs apairs))) 

539 
in addprfs (Logic.assum_pairs Bi) end; 

540 

541 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 

542 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*) 

543 
fun eq_assumption i state = 

544 
let val Thm{sign,maxidx,hyps,prop} = state; 

545 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 

546 
in if exists (op aconv) (Logic.assum_pairs Bi) 

547 
then Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

548 
prop=Logic.rule_of(tpairs, Bs, C)} 

549 
else raise THM("eq_assumption", 0, [state]) 

550 
end; 

551 

552 

553 
(** User renaming of parameters in a subgoal **) 

554 

555 
(*Calls error rather than raising an exception because it is intended 

556 
for toplevel use  exception handling would not make sense here. 

557 
The names in cs, if distinct, are used for the innermost parameters; 

558 
preceding parameters may be renamed to make all params distinct.*) 

559 
fun rename_params_rule (cs, i) state = 

560 
let val Thm{sign,maxidx,hyps,prop} = state 

561 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 

562 
val iparams = map #1 (Logic.strip_params Bi) 

563 
val short = length iparams  length cs 

564 
val newnames = 

565 
if short<0 then error"More names than abstractions!" 

566 
else variantlist(take (short,iparams), cs) @ cs 

567 
val freenames = map (#1 o dest_Free) (term_frees prop) 

568 
val newBi = Logic.list_rename_params (newnames, Bi) 

569 
in 

570 
case findrep cs of 

571 
c::_ => error ("Bound variables not distinct: " ^ c) 

572 
 [] => (case cs inter freenames of 

573 
a::_ => error ("Bound/Free variable clash: " ^ a) 

574 
 [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= 

575 
Logic.rule_of(tpairs, Bs@[newBi], C)}) 

576 
end; 

577 

578 
(*** Preservation of bound variable names ***) 

579 

580 
(*Scan a pair of terms; while they are similar, 

581 
accumulate corresponding bound vars in "al"*) 

582 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al) 

583 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 

584 
 match_bvs(_,_,al) = al; 

585 

586 
(* strip abstractions created by parameters *) 

587 
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); 

588 

589 

590 
(* strip_apply f A(,B) strips off all assumptions/parameters from A 

591 
introduced by lifting over B, and applies f to remaining part of A*) 

592 
fun strip_apply f = 

593 
let fun strip(Const("==>",_)$ A1 $ B1, 

594 
Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2) 

595 
 strip((c as Const("all",_)) $ Abs(a,T,t1), 

596 
Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2)) 

597 
 strip(A,_) = f A 

598 
in strip end; 

599 

600 
(*Use the alist to rename all bound variables and some unknowns in a term 

601 
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); 

602 
Preserves unknowns in tpairs and on lhs of dpairs. *) 

603 
fun rename_bvs([],_,_,_) = I 

604 
 rename_bvs(al,dpairs,tpairs,B) = 

605 
let val vars = foldr add_term_vars 

606 
(map fst dpairs @ map fst tpairs @ map snd tpairs, []) 

607 
(*unknowns appearing elsewhere be preserved!*) 

608 
val vids = map (#1 o #1 o dest_Var) vars; 

609 
fun rename(t as Var((x,i),T)) = 

610 
(case assoc(al,x) of 

611 
Some(y) => if x mem vids orelse y mem vids then t 

612 
else Var((y,i),T) 

613 
 None=> t) 

614 
 rename(Abs(x,T,t)) = 

615 
Abs(case assoc(al,x) of Some(y) => y  None => x, 

616 
T, rename t) 

617 
 rename(f$t) = rename f $ rename t 

618 
 rename(t) = t; 

619 
fun strip_ren Ai = strip_apply rename (Ai,B) 

620 
in strip_ren end; 

621 

622 
(*Function to rename bounds/unknowns in the argument, lifted over B*) 

623 
fun rename_bvars(dpairs, tpairs, B) = 

624 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 

625 

626 

627 
(*** RESOLUTION ***) 

628 

629 
(*strip off pairs of assumptions/parameters in parallel  they are 

630 
identical because of lifting*) 

631 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 

632 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

633 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 

634 
Const("all",_)$Abs(_,_,t2)) = 

635 
let val (B1,B2) = strip_assums2 (t1,t2) 

636 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

637 
 strip_assums2 BB = BB; 

638 

639 

640 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 

641 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 

642 
If match then forbid instantiations in proof state 

643 
If lifted then shorten the dpair using strip_assums2. 

644 
If eres_flg then simultaneously proves A1 by assumption. 

645 
nsubgoal is the number of new subgoals (written m above). 

646 
Curried so that resolution calls dest_state only once. 

647 
*) 

648 
local open Sequence; exception Bicompose 

649 
in 

650 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 

651 
(eres_flg, orule, nsubgoal) = 

652 
let val Thm{maxidx=smax, hyps=shyps, ...} = state 

653 
and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule; 

654 
val sign = merge_theories(state,orule); 

655 
(** Add new theorem with prop = '[ Bs; As ] ==> C' to thq **) 

656 
fun addth As ((env as Envir.Envir{maxidx,asol,iTs}, tpairs), thq) = 

657 
let val minenv = case Envir.alist_of_olist asol of 

658 
[] => ~1  ((_,i),_) :: _ => i; 

659 
val minx = min (minenv :: map (fn ((_,i),_) => i) iTs); 

660 
val normt = Envir.norm_term env; 

661 
(*Perform minimal copying here by examining env*) 

662 
val normp = if minx = ~1 then (tpairs, Bs@As, C) 

663 
else 

664 
let val ntps = map (pairself normt) tpairs 

665 
in if minx>smax then (*no assignments in state*) 

666 
(ntps, Bs @ map normt As, C) 

667 
else if match then raise Bicompose 

668 
else (*normalize the new rule fully*) 

669 
(ntps, map normt (Bs @ As), normt C) 

670 
end 

671 
val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx, 

672 
prop= Logic.rule_of normp} 

673 
in cons(th, thq) end handle Bicompose => thq 

674 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 

675 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

676 
handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); 

677 
(*Modify assumptions, deleting nth if n>0 for eresolution*) 

678 
fun newAs(As0, n, dpairs, tpairs) = 

679 
let val As1 = if !Logic.auto_rename orelse not lifted then As0 

680 
else map (rename_bvars(dpairs,tpairs,B)) As0 

681 
in (map (Logic.flatten_params n) As1) 

682 
handle TERM _ => 

683 
raise THM("bicompose: 1st premise", 0, [orule]) 

684 
end; 

685 
val env = Envir.empty(max[rmax,smax]); 

686 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 

687 
val dpairs = BBi :: (rtpairs@stpairs); 

688 
(*elimresolution: try each assumption in turn. Initially n=1*) 

689 
fun tryasms (_, _, []) = null 

690 
 tryasms (As, n, (t,u)::apairs) = 

691 
(case pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of 

692 
None => tryasms (As, n+1, apairs) 

693 
 cell as Some((_,tpairs),_) => 

694 
its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs))) 

695 
(seqof (fn()=> cell), 

696 
seqof (fn()=> pull (tryasms (As, n+1, apairs))))); 

697 
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) 

698 
 eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1); 

699 
(*ordinary resolution*) 

700 
fun res(None) = null 

701 
 res(cell as Some((_,tpairs),_)) = 

702 
its_right (addth(newAs(rev rAs, 0, [BBi], tpairs))) 

703 
(seqof (fn()=> cell), null) 

704 
in if eres_flg then eres(rev rAs) 

705 
else res(pull(Unify.unifiers(sign, env, dpairs))) 

706 
end; 

707 
end; (*open Sequence*) 

708 

709 

710 
fun bicompose match arg i state = 

711 
bicompose_aux match (state, dest_state(state,i), false) arg; 

712 

713 
(*Quick test whether rule is resolvable with the subgoal with hyps Hs 

714 
and conclusion B. If eres_flg then checks 1st premise of rule also*) 

715 
fun could_bires (Hs, B, eres_flg, rule) = 

716 
let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs 

717 
 could_reshyp [] = false; (*no premise  illegal*) 

718 
in could_unify(concl_of rule, B) andalso 

719 
(not eres_flg orelse could_reshyp (prems_of rule)) 

720 
end; 

721 

722 
(*Biresolution of a state with a list of (flag,rule) pairs. 

723 
Puts the rule above: rule/state. Renames vars in the rules. *) 

724 
fun biresolution match brules i state = 

725 
let val lift = lift_rule(state, i); 

726 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 

727 
val B = Logic.strip_assums_concl Bi; 

728 
val Hs = Logic.strip_assums_hyp Bi; 

729 
val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true); 

730 
fun res [] = Sequence.null 

731 
 res ((eres_flg, rule)::brules) = 

732 
if could_bires (Hs, B, eres_flg, rule) 

733 
then Sequence.seqof (*delay processing remainder til needed*) 

734 
(fn()=> Some(comp (eres_flg, lift rule, nprems_of rule), 

735 
res brules)) 

736 
else res brules 

737 
in Sequence.flats (res brules) end; 

738 

739 

740 
(**** THEORIES ****) 

741 

742 
val pure_thy = Pure{sign = Sign.pure}; 

743 

744 
(*Look up the named axiom in the theory*) 

745 
fun get_axiom thy axname = 

746 
let fun get (Pure _) = raise Match 

747 
 get (Extend{axioms,thy,...}) = 

748 
(case Symtab.lookup(axioms,axname) of 

749 
Some th => th 

750 
 None => get thy) 

751 
 get (Merge{thy1,thy2,...}) = 

752 
get thy1 handle Match => get thy2 

753 
in get thy 

754 
handle Match => raise THEORY("get_axiom: No axiom "^axname, [thy]) 

755 
end; 

756 

757 
(*Converts Frees to Vars: axioms can be written without question marks*) 

758 
fun prepare_axiom sign sP = 

759 
Logic.varify (Sign.term_of (Sign.read_cterm sign (sP,propT))); 

760 

761 
(*Read an axiom for a new theory*) 

762 
fun read_ax sign (a, sP) : string*thm = 

763 
let val prop = prepare_axiom sign sP 

764 
in (a, Thm{sign=sign, hyps=[], maxidx= maxidx_of_term prop, prop= prop}) 

765 
end 

766 
handle ERROR => 

767 
error("extend_theory: The error above occurred in axiom " ^ a); 

768 

769 
fun mk_axioms sign axpairs = 

770 
Symtab.st_of_alist(map (read_ax sign) axpairs, Symtab.null) 

771 
handle Symtab.DUPLICATE(a) => error("Two axioms named " ^ a); 

772 

773 
(*Extension of a theory with given classes, types, constants and syntax. 

774 
Reads the axioms from strings: axpairs have the form (axname, axiom). *) 

775 
fun extend_theory thy thyname ext axpairs = 

776 
let val sign = Sign.extend (sign_of thy) thyname ext; 

777 
val axioms= mk_axioms sign axpairs 

778 
in Extend{sign=sign, axioms= axioms, thy = thy} end; 

779 

780 
(*The union of two theories*) 

781 
fun merge_theories (thy1,thy2) = 

782 
Merge{sign = Sign.merge(sign_of thy1, sign_of thy2), 

783 
thy1 = thy1, thy2 = thy2}; 

784 

785 

786 
(*** Meta simp sets ***) 

787 

788 
type rrule = {thm:thm, lhs:term}; 

789 
datatype meta_simpset = 

790 
Mss of {net:rrule Net.net, congs:(string * rrule)list, primes:string, 

791 
prems: thm list, mk_rews: thm > thm list}; 

792 

793 
(*A "mss" contains data needed during conversion: 

794 
net: discrimination net of rewrite rules 

795 
congs: association list of congruence rules 

796 
primes: offset for generating unique new names 

797 
for rewriting under lambda abstractions 

798 
mk_rews: used when local assumptions are added 

799 
*) 

800 

801 
val empty_mss = Mss{net= Net.empty, congs= [], primes="", prems= [], 

802 
mk_rews = K[]}; 

803 

804 
exception SIMPLIFIER of string * thm; 

805 

806 
fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t)); 

807 

209  808 
val trace_simp = ref false; 
809 

810 
fun trace_term a sg t = if !trace_simp then prtm a sg t else (); 

811 

812 
fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop; 

813 

0  814 
(*simple test for looping rewrite*) 
815 
fun loops sign prems (lhs,rhs) = 

816 
null(prems) andalso 

817 
Pattern.eta_matches (#tsig(Sign.rep_sg sign)) (lhs,rhs); 

818 

819 
fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) = 

820 
let val prems = Logic.strip_imp_prems prop 

821 
val concl = Pattern.eta_contract (Logic.strip_imp_concl prop) 

822 
val (lhs,rhs) = Logic.dest_equals concl handle TERM _ => 

823 
raise SIMPLIFIER("Rewrite rule not a metaequality",thm) 

824 
in if loops sign prems (lhs,rhs) 

825 
then (prtm "Warning: ignoring looping rewrite rule" sign prop; None) 

826 
else Some{thm=thm,lhs=lhs} 

827 
end; 

828 

87  829 
local 
830 
fun eq({thm=Thm{prop=p1,...},...}:rrule, 

831 
{thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2 

832 
in 

833 

0  834 
fun add_simp(mss as Mss{net,congs,primes,prems,mk_rews}, 
835 
thm as Thm{sign,prop,...}) = 

87  836 
case mk_rrule thm of 
837 
None => mss 

838 
 Some(rrule as {lhs,...}) => 

209  839 
(trace_thm "Adding rewrite rule:" thm; 
840 
Mss{net= (Net.insert_term((lhs,rrule),net,eq) 

841 
handle Net.INSERT => 

87  842 
(prtm "Warning: ignoring duplicate rewrite rule" sign prop; 
843 
net)), 

209  844 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}); 
87  845 

846 
fun del_simp(mss as Mss{net,congs,primes,prems,mk_rews}, 

847 
thm as Thm{sign,prop,...}) = 

848 
case mk_rrule thm of 

849 
None => mss 

850 
 Some(rrule as {lhs,...}) => 

851 
Mss{net= (Net.delete_term((lhs,rrule),net,eq) 

852 
handle Net.INSERT => 

853 
(prtm "Warning: rewrite rule not in simpset" sign prop; 

854 
net)), 

0  855 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews} 
87  856 

857 
end; 

0  858 

859 
val add_simps = foldl add_simp; 

87  860 
val del_simps = foldl del_simp; 
0  861 

862 
fun mss_of thms = add_simps(empty_mss,thms); 

863 

864 
fun add_cong(Mss{net,congs,primes,prems,mk_rews},thm) = 

865 
let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ => 

866 
raise SIMPLIFIER("Congruence not a metaequality",thm) 

867 
val lhs = Pattern.eta_contract lhs 

868 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 

869 
raise SIMPLIFIER("Congruence must start with a constant",thm) 

870 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, primes=primes, 

871 
prems=prems, mk_rews=mk_rews} 

872 
end; 

873 

874 
val (op add_congs) = foldl add_cong; 

875 

876 
fun add_prems(Mss{net,congs,primes,prems,mk_rews},thms) = 

877 
Mss{net=net, congs=congs, primes=primes, prems=thms@prems, mk_rews=mk_rews}; 

878 

879 
fun prems_of_mss(Mss{prems,...}) = prems; 

880 

881 
fun set_mk_rews(Mss{net,congs,primes,prems,...},mk_rews) = 

882 
Mss{net=net, congs=congs, primes=primes, prems=prems, mk_rews=mk_rews}; 

883 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 

884 

885 

886 
(*** Metalevel rewriting 

887 
uses conversions, omitting proofs for efficiency. See 

888 
L C Paulson, A higherorder implementation of rewriting, 

889 
Science of Computer Programming 3 (1983), pages 119149. ***) 

890 

891 
type prover = meta_simpset > thm > thm option; 

892 
type termrec = (Sign.sg * term list) * term; 

893 
type conv = meta_simpset > termrec > termrec; 

894 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

895 
fun check_conv(thm as Thm{hyps,prop,...}, prop0) = 
112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

896 
let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None) 
0  897 
val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0) 
898 
in case prop of 

899 
Const("==",_) $ lhs $ rhs => 

900 
if (lhs = lhs0) orelse 

901 
(lhs aconv (Envir.norm_term (Envir.empty 0) lhs0)) 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

902 
then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) 
0  903 
else err() 
904 
 _ => err() 

905 
end; 

906 

907 
(*Conversion to apply the meta simpset to a term*) 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

908 
fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) = 
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

909 
let val t = Pattern.eta_contract t; 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

910 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs} = 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

911 
let val unit = if Sign.subsig(sign,signt) then () 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

912 
else (writeln"Warning: rewrite rule from different theory"; 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

913 
raise Pattern.MATCH) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

914 
val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t) 
0  915 
val prop' = subst_vars insts prop; 
916 
val hyps' = hyps union hypst; 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

917 
val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx} 
0  918 
in if nprems_of thm' = 0 
919 
then let val (_,rhs) = Logic.dest_equals prop' 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

920 
in trace_thm "Rewriting:" thm'; Some(hyps',rhs) end 
0  921 
else (trace_thm "Trying to rewrite:" thm'; 
922 
case prover mss thm' of 

923 
None => (trace_thm "FAILED" thm'; None) 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

924 
 Some(thm2) => check_conv(thm2,prop')) 
0  925 
end 
926 

225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

927 
fun rews [] = None 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

928 
 rews (rrule::rrules) = 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

929 
let val opt = rew rrule handle Pattern.MATCH => None 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

930 
in case opt of None => rews rrules  some => some end; 
0  931 

932 
in case t of 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

933 
Abs(_,_,body) $ u => Some(hypst,subst_bounds([u], body)) 
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

934 
 _ => rews(Net.match_term net t) 
0  935 
end; 
936 

937 
(*Conversion to apply a congruence rule to a term*) 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

938 
fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,t) = 
0  939 
let val Thm{sign,hyps,maxidx,prop,...} = cong 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

940 
val unit = if Sign.subsig(sign,signt) then () 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

941 
else error("Congruence rule from different theory") 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

942 
val tsig = #tsig(Sign.rep_sg signt) 
0  943 
val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH => 
944 
error("Congruence rule did not match") 

945 
val prop' = subst_vars insts prop; 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

946 
val thm' = Thm{sign=signt, hyps=hyps union hypst, 
0  947 
prop=prop', maxidx=maxidx} 
948 
val unit = trace_thm "Applying congruence rule" thm'; 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

949 
fun err() = error("Failed congruence proof!") 
0  950 

951 
in case prover thm' of 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

952 
None => err() 
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

953 
 Some(thm2) => (case check_conv(thm2,prop') of 
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

954 
None => err()  Some(x) => x) 
0  955 
end; 
956 

957 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

958 
fun bottomc ((simprem,useprem),prover,sign) = 
0  959 
let fun botc mss trec = let val trec1 = subc mss trec 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

960 
in case rewritec (prover,sign) mss trec1 of 
0  961 
None => trec1 
962 
 Some(trec2) => botc mss trec2 

963 
end 

964 

965 
and subc (mss as Mss{net,congs,primes,prems,mk_rews}) 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

966 
(trec as (hyps,t)) = 
0  967 
(case t of 
968 
Abs(a,T,t) => 

969 
let val v = Free(".subc." ^ primes,T) 

970 
val mss' = Mss{net=net, congs=congs, primes=primes^"'", 

971 
prems=prems,mk_rews=mk_rews} 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

972 
val (hyps',t') = botc mss' (hyps,subst_bounds([v],t)) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

973 
in (hyps', Abs(a, T, abstract_over(v,t'))) end 
0  974 
 t$u => (case t of 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

975 
Const("==>",_)$s => impc(hyps,s,u,mss) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

976 
 Abs(_,_,body) => subc mss (hyps,subst_bounds([u], body)) 
0  977 
 _ => 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

978 
let fun appc() = let val (hyps1,t1) = botc mss (hyps,t) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

979 
val (hyps2,u1) = botc mss (hyps1,u) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

980 
in (hyps2,t1$u1) end 
0  981 
val (h,ts) = strip_comb t 
982 
in case h of 

983 
Const(a,_) => 

984 
(case assoc(congs,a) of 

985 
None => appc() 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

986 
 Some(cong) => congc (prover mss,sign) cong trec) 
0  987 
 _ => appc() 
988 
end) 

989 
 _ => trec) 

990 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

991 
and impc(hyps,s,u,mss as Mss{mk_rews,...}) = 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

992 
let val (hyps1,s') = if simprem then botc mss (hyps,s) else (hyps,s) 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

993 
val mss' = 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

994 
if not useprem orelse maxidx_of_term s' <> ~1 then mss 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

995 
else let val thm = Thm{sign=sign,hyps=[s'],prop=s',maxidx= ~1} 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

996 
in add_simps(add_prems(mss,[thm]), mk_rews thm) end 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

997 
val (hyps2,u') = botc mss' (hyps1,u) 
134
595fda4879b6
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
nipkow
parents:
112
diff
changeset

998 
val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s' 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

999 
in (hyps2', Logic.mk_implies(s',u')) end 
0  1000 

1001 
in botc end; 

1002 

1003 

1004 
(*** Metarewriting: rewrites t to u and returns the theorem t==u ***) 

1005 
(* Parameters: 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1006 
mode = (simplify A, use A in simplifying B) when simplifying A ==> B 
0  1007 
mss: contains equality theorems of the form [p1,...] ==> t==u 
1008 
prover: how to solve premises in conditional rewrites and congruences 

1009 
*) 

1010 

1011 
(*** FIXME: check that #primes(mss) does not "occur" in ct alread ***) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1012 
fun rewrite_cterm mode mss prover ct = 
0  1013 
let val {sign, t, T, maxidx} = Sign.rep_cterm ct; 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1014 
val (hyps,u) = bottomc (mode,prover,sign) mss ([],t); 
0  1015 
val prop = Logic.mk_equals(t,u) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1016 
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 
0  1017 
end 
1018 

1019 
end; 