author  nipkow 
Tue, 04 Jan 1994 10:09:33 +0100  
changeset 209  feb8ff35810a 
parent 208  342f88d2e8ab 
child 214  ed6a3e2b1a33 
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} 

69 
val rewrite_cterm: meta_simpset > (meta_simpset > thm > thm option) 

70 
> Sign.cterm > thm 

71 
val set_mk_rews: meta_simpset * (thm > thm list) > meta_simpset 

72 
val sign_of: theory > Sign.sg 

73 
val syn_of: theory > Sign.Syntax.syntax 

74 
val stamps_of_thm: thm > string ref list 

75 
val stamps_of_thy: theory > string ref list 

76 
val symmetric: thm > thm 

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

78 
val trace_simp: bool ref 

79 
val transitive: thm > thm > thm 

80 
val trivial: Sign.cterm > thm 

81 
val varifyT: thm > thm 

82 
end; 

83 

84 

85 

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

87 
and Net:NET 

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

89 
: THM = 

90 
struct 

91 
structure Sequence = Unify.Sequence; 

92 
structure Envir = Unify.Envir; 

93 
structure Sign = Unify.Sign; 

94 
structure Type = Sign.Type; 

95 
structure Syntax = Sign.Syntax; 

96 
structure Symtab = Sign.Symtab; 

97 

98 

99 
(*Metatheorems*) 

100 
datatype thm = Thm of 

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

102 

103 
fun rep_thm (Thm x) = x; 

104 

105 
(*Errors involving theorems*) 

106 
exception THM of string * int * thm list; 

107 

108 
(*maps objectrule to tpairs *) 

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

110 

111 
(*maps objectrule to premises *) 

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

113 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 

114 

115 
(*counts premises in a rule*) 

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

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

118 

119 
(*maps objectrule to conclusion *) 

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

121 

122 
(*Stamps associated with a signature*) 

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

124 

125 
(*Theories. There is one pure theory. 

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

127 
datatype theory = 

128 
Pure of {sign: Sign.sg} 

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

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

131 

132 
(*Errors involving theories*) 

133 
exception THEORY of string * theory list; 

134 

135 
fun sign_of (Pure {sign}) = sign 

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

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

138 

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

140 

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

142 
fun axioms_of (Pure _) = [] 

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

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

145 

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

147 
fun parents_of (Pure _) = [] 

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

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

150 

151 

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

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

154 
fun merge_theories(th1,th2) = 

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

156 
in Sign.merge (sign1,sign2) end 

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

158 

159 
(*Stamps associated with a theory*) 

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

161 

162 

163 
(**** Primitive rules ****) 

164 

165 
(* discharge all assumptions t from ts *) 

166 
val disch = gen_rem (op aconv); 

167 

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

169 
fun assume ct : thm = 

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

171 
in if T<>propT then 

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

173 
else if maxidx <> ~1 then 

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

175 
maxidx, []) 

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

177 
end; 

178 

179 
(* Implication introduction 

180 
A  B 

181 
 

182 
A ==> B *) 

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

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

185 
in if T<>propT then 

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

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

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

189 
handle TERM _ => 

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

191 
end; 

192 

193 
(* Implication elimination 

194 
A ==> B A 

195 
 

196 
B *) 

197 
fun implies_elim thAB thA : thm = 

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

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

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

201 
in case prop of 

202 
imp$A$B => 

203 
if imp=implies andalso A aconv propA 

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

205 
maxidx= max[maxA,maxidx], 

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

207 
prop= B} 

208 
else err("major premise") 

209 
 _ => err("major premise") 

210 
end; 

211 

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

213 
A 

214 
 

215 
!!x.A *) 

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

217 
let val x = Sign.term_of cx; 

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

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

220 
in case x of 

221 
Free(a,T) => 

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

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

224 
else result(a,T) 

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

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

227 
end; 

228 

229 
(* Forall elimination 

230 
!!x.A 

231 
 

232 
A[t/x] *) 

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

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

235 
in case prop of 

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

237 
if T<>qary then 

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

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

240 
maxidx= max[maxidx, maxt], 

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

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

243 
end 

244 
handle TERM _ => 

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

246 

247 

248 
(*** Equality ***) 

249 

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

251 
val flexpair_def = 

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

253 
prop= Sign.term_of 

254 
(Sign.read_cterm Sign.pure 

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

256 

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

258 
fun reflexive ct = 

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

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

261 
end; 

262 

263 
(*The symmetry rule 

264 
t==u 

265 
 

266 
u==t *) 

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

268 
case prop of 

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

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

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

272 

273 
(*The transitive rule 

274 
t1==u u==t2 

275 
 

276 
t1==t2 *) 

277 
fun transitive th1 th2 = 

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

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

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

281 
in case (prop1,prop2) of 

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

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

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

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

286 
 _ => err"premises" 

287 
end; 

288 

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

290 
fun beta_conversion ct = 

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

292 
in case t of 

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

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

295 
maxidx= maxidx_of_term t, 

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

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

298 
end; 

299 

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

301 
f(x) == g(x) 

302 
 

303 
f == g *) 

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

305 
case prop of 

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

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

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

309 
case y of 

310 
Free _ => 

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

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

313 
 Var _ => 

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

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

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

317 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

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

319 
end 

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

321 

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

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

324 
t == u 

325 
 

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

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

328 
let val x = Sign.term_of cx; 

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

330 
handle TERM _ => 

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

332 
fun result T = 

333 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

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

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

336 
in case x of 

337 
Free(_,T) => 

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

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

340 
else result T 

341 
 Var(_,T) => result T 

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

343 
end; 

344 

345 
(*The combination rule 

346 
f==g t==u 

347 
 

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

349 
fun combination th1 th2 = 

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

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

352 
in case (prop1,prop2) of 

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

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

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

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

357 
end; 

358 

359 

360 
(*The equal propositions rule 

361 
A==B A 

362 
 

363 
B *) 

364 
fun equal_elim th1 th2 = 

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

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

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

368 
in case prop1 of 

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

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

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

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

373 
 _ => err"major premise" 

374 
end; 

375 

376 

377 
(* Equality introduction 

378 
A==>B B==>A 

379 
 

380 
A==B *) 

381 
fun equal_intr th1 th2 = 

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

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

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

385 
in case (prop1,prop2) of 

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

387 
if A aconv A' andalso B aconv B' 

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

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

390 
else err"not equal" 

391 
 _ => err"premises" 

392 
end; 

393 

394 
(**** Derived rules ****) 

395 

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

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

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

399 
implies_intr_hyps 

400 
(Thm{sign=sign, maxidx=maxidx, 

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

402 
 implies_intr_hyps th = th; 

403 

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

405 
Instantiates the theorem and deletes trivial tpairs. 

406 
Resulting sequence may contain multiple elements if the tpairs are 

407 
not all flexflex. *) 

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

409 
let fun newthm env = 

410 
let val (tpairs,horn) = 

411 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

415 
in Thm{sign= sign, hyps= hyps, 

416 
maxidx= maxidx_of_term newprop, prop= newprop} 

417 
end; 

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

419 
in Sequence.maps newthm 

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

421 
end; 

422 

423 
(*Instantiation of Vars 

424 
A 

425 
 

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

427 

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

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

430 

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

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

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

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

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

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

437 
end; 

438 

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

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

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

442 

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

444 
Instantiates distinct Vars by terms of same type. 

445 
Normalizes the new theorem! *) 

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

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

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

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

451 
(subst_atomic tpairs 

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

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

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

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

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

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

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

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

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

463 
 [] => 

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

465 
ix::_ => raise THM 

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

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

468 
 [] => newth 

0  469 
end 
470 
handle TERM _ => 

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

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

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

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

476 
fun trivial ct : thm = 

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

478 
in if T<>propT then 

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

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

481 
end; 

482 

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

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

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

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

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

488 
end; 

489 

490 
(* Replace all TVars by new TFrees *) 

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

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

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

494 

495 

496 
(*** Inference rules for tactics ***) 

497 

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

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

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

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

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

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

504 
end 

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

506 

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

508 
resolution with goal i of state. *) 

509 
fun lift_rule (state, i) orule = 

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

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

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

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

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

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

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

517 
maxidx= maxidx+smax+1, 

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

519 
map lift_all As, lift_all B)} 

520 
end; 

521 

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

523 
fun assumption i state = 

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

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

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

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

528 
case (Envir.alist_of_olist asol, iTs) of 

529 
(*avoid wasted normalizations*) 

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

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

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

533 
fun addprfs [] = Sequence.null 

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

535 
(Sequence.mapp newth 

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

537 
(addprfs apairs))) 

538 
in addprfs (Logic.assum_pairs Bi) end; 

539 

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

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

542 
fun eq_assumption i state = 

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

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

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

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

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

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

549 
end; 

550 

551 

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

553 

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

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

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

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

558 
fun rename_params_rule (cs, i) state = 

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

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

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

562 
val short = length iparams  length cs 

563 
val newnames = 

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

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

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

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

568 
in 

569 
case findrep cs of 

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

571 
 [] => (case cs inter freenames of 

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

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

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

575 
end; 

576 

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

578 

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

580 
accumulate corresponding bound vars in "al"*) 

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

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

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

584 

585 
(* strip abstractions created by parameters *) 

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

587 

588 

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

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

591 
fun strip_apply f = 

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

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

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

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

596 
 strip(A,_) = f A 

597 
in strip end; 

598 

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

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

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

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

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

604 
let val vars = foldr add_term_vars 

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

606 
(*unknowns appearing elsewhere be preserved!*) 

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

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

609 
(case assoc(al,x) of 

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

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

612 
 None=> t) 

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

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

615 
T, rename t) 

616 
 rename(f$t) = rename f $ rename t 

617 
 rename(t) = t; 

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

619 
in strip_ren end; 

620 

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

622 
fun rename_bvars(dpairs, tpairs, B) = 

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

624 

625 

626 
(*** RESOLUTION ***) 

627 

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

629 
identical because of lifting*) 

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

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

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

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

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

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

636 
 strip_assums2 BB = BB; 

637 

638 

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

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

641 
If match then forbid instantiations in proof state 

642 
If lifted then shorten the dpair using strip_assums2. 

643 
If eres_flg then simultaneously proves A1 by assumption. 

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

645 
Curried so that resolution calls dest_state only once. 

646 
*) 

647 
local open Sequence; exception Bicompose 

648 
in 

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

650 
(eres_flg, orule, nsubgoal) = 

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

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

653 
val sign = merge_theories(state,orule); 

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

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

656 
let val minenv = case Envir.alist_of_olist asol of 

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

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

659 
val normt = Envir.norm_term env; 

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

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

662 
else 

663 
let val ntps = map (pairself normt) tpairs 

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

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

666 
else if match then raise Bicompose 

667 
else (*normalize the new rule fully*) 

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

669 
end 

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

671 
prop= Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

681 
handle TERM _ => 

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

683 
end; 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

698 
(*ordinary resolution*) 

699 
fun res(None) = null 

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

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

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

703 
in if eres_flg then eres(rev rAs) 

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

705 
end; 

706 
end; (*open Sequence*) 

707 

708 

709 
fun bicompose match arg i state = 

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

711 

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

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

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

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

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

717 
in could_unify(concl_of rule, B) andalso 

718 
(not eres_flg orelse could_reshyp (prems_of rule)) 

719 
end; 

720 

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

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

723 
fun biresolution match brules i state = 

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

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

726 
val B = Logic.strip_assums_concl Bi; 

727 
val Hs = Logic.strip_assums_hyp Bi; 

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

729 
fun res [] = Sequence.null 

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

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

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

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

734 
res brules)) 

735 
else res brules 

736 
in Sequence.flats (res brules) end; 

737 

738 

739 
(**** THEORIES ****) 

740 

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

742 

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

744 
fun get_axiom thy axname = 

745 
let fun get (Pure _) = raise Match 

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

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

748 
Some th => th 

749 
 None => get thy) 

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

751 
get thy1 handle Match => get thy2 

752 
in get thy 

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

754 
end; 

755 

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

757 
fun prepare_axiom sign sP = 

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

759 

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

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

762 
let val prop = prepare_axiom sign sP 

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

764 
end 

765 
handle ERROR => 

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

767 

768 
fun mk_axioms sign axpairs = 

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

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

771 

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

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

774 
fun extend_theory thy thyname ext axpairs = 

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

776 
val axioms= mk_axioms sign axpairs 

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

778 

779 
(*The union of two theories*) 

780 
fun merge_theories (thy1,thy2) = 

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

782 
thy1 = thy1, thy2 = thy2}; 

783 

784 

785 
(*** Meta simp sets ***) 

786 

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

788 
datatype meta_simpset = 

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

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

791 

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

793 
net: discrimination net of rewrite rules 

794 
congs: association list of congruence rules 

795 
primes: offset for generating unique new names 

796 
for rewriting under lambda abstractions 

797 
mk_rews: used when local assumptions are added 

798 
*) 

799 

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

801 
mk_rews = K[]}; 

802 

803 
exception SIMPLIFIER of string * thm; 

804 

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

806 

209  807 
val trace_simp = ref false; 
808 

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

810 

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

812 

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

815 
null(prems) andalso 

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

817 

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

819 
let val prems = Logic.strip_imp_prems prop 

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

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

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

823 
in if loops sign prems (lhs,rhs) 

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

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

826 
end; 

827 

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

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

831 
in 

832 

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

87  835 
case mk_rrule thm of 
836 
None => mss 

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

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

840 
handle Net.INSERT => 

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

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

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

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

847 
case mk_rrule thm of 

848 
None => mss 

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

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

851 
handle Net.INSERT => 

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

853 
net)), 

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

856 
end; 

0  857 

858 
val add_simps = foldl add_simp; 

87  859 
val del_simps = foldl del_simp; 
0  860 

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

862 

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

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

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

866 
val lhs = Pattern.eta_contract lhs 

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

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

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

870 
prems=prems, mk_rews=mk_rews} 

871 
end; 

872 

873 
val (op add_congs) = foldl add_cong; 

874 

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

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

877 

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

879 

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

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

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

883 

884 

885 
(*** Metalevel rewriting 

886 
uses conversions, omitting proofs for efficiency. See 

887 
L C Paulson, A higherorder implementation of rewriting, 

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

889 

890 
type prover = meta_simpset > thm > thm option; 

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

892 
type conv = meta_simpset > termrec > termrec; 

893 

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

894 
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

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

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

899 
if (lhs = lhs0) orelse 

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

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

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

904 
end; 

905 

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

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

907 
fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) = 
0  908 
let val t = Pattern.eta_contract t 
909 
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

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

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

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

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

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

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

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

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

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

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

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

926 
fun rewl [] = None 

927 
 rewl (rrule::rrules) = 

928 
let val opt = rew rrule handle Pattern.MATCH => None 

929 
in case opt of None => rewl rrules  some => some end; 

930 

931 
in case t of 

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

932 
Abs(_,_,body) $ u => Some(hypst,subst_bounds([u], body)) 
0  933 
 _ => rewl (Net.match_term net t) 
934 
end; 

935 

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

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

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

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

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

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

944 
val prop' = subst_vars insts prop; 

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

945 
val thm' = Thm{sign=signt, hyps=hyps union hypst, 
0  946 
prop=prop', maxidx=maxidx} 
947 
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

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

950 
in case prover thm' of 

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

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

952 
 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

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

956 

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

957 
fun bottomc (prover,sign) = 
0  958 
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

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

962 
end 

963 

964 
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

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

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

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

970 
prems=prems,mk_rews=mk_rews} 

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

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

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

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

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

977 
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

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

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

982 
Const(a,_) => 

983 
(case assoc(congs,a) of 

984 
None => appc() 

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

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

988 
 _ => trec) 

989 

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

990 
and impc(hyps,s,u,mss as Mss{mk_rews,...}) = 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

991 
let val (hyps1,s') = botc mss (hyps,s) 
0  992 
val (rthms,mss) = 
993 
if maxidx_of_term s' <> ~1 then ([],mss) 

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

994 
else let val thm = Thm{sign=sign,hyps=[s'],prop=s',maxidx= ~1} 
0  995 
in (mk_rews thm, add_prems(mss,[thm])) end 
996 
val mss' = add_simps(mss,rthms) 

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: 

1006 
mss: contains equality theorems of the form [p1,...] ==> t==u 

1007 
prover: how to solve premises in conditional rewrites and congruences 

1008 
*) 

1009 

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

1011 
fun rewrite_cterm mss prover ct = 

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

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

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

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

1018 
end; 