author  nipkow 
Fri, 10 Dec 1993 13:46:38 +0100  
changeset 193  b2be328e00c3 
parent 134  595fda4879b6 
child 200  39a931cc6558 
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 

41 
* (string list * (sort list * class))list 

42 
* (string list * string)list * Sign.Syntax.sext option 

43 
> (string*string)list > theory 

44 
val extensional: thm > thm 

45 
val flexflex_rule: thm > thm Sequence.seq 

46 
val flexpair_def: thm 

47 
val forall_elim: Sign.cterm > thm > thm 

48 
val forall_intr: Sign.cterm > thm > thm 

49 
val freezeT: thm > thm 

50 
val get_axiom: theory > string > thm 

51 
val implies_elim: thm > thm > thm 

52 
val implies_intr: Sign.cterm > thm > thm 

53 
val implies_intr_hyps: thm > thm 

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

55 
> thm > thm 

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

57 
val merge_theories: theory * theory > theory 

58 
val mk_rews_of_mss: meta_simpset > thm > thm list 

59 
val mss_of: thm list > meta_simpset 

60 
val nprems_of: thm > int 

61 
val parents_of: theory > theory list 

62 
val prems_of: thm > term list 

63 
val prems_of_mss: meta_simpset > thm list 

64 
val pure_thy: theory 

65 
val reflexive: Sign.cterm > thm 

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

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

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

69 
> Sign.cterm > thm 

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

71 
val sign_of: theory > Sign.sg 

72 
val syn_of: theory > Sign.Syntax.syntax 

73 
val stamps_of_thm: thm > string ref list 

74 
val stamps_of_thy: theory > string ref list 

75 
val symmetric: thm > thm 

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

77 
val trace_simp: bool ref 

78 
val transitive: thm > thm > thm 

79 
val trivial: Sign.cterm > thm 

80 
val varifyT: thm > thm 

81 
end; 

82 

83 

84 

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

86 
and Net:NET 

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

88 
: THM = 

89 
struct 

90 
structure Sequence = Unify.Sequence; 

91 
structure Envir = Unify.Envir; 

92 
structure Sign = Unify.Sign; 

93 
structure Type = Sign.Type; 

94 
structure Syntax = Sign.Syntax; 

95 
structure Symtab = Sign.Symtab; 

96 

97 

98 
(*Metatheorems*) 

99 
datatype thm = Thm of 

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

101 

102 
fun rep_thm (Thm x) = x; 

103 

104 
(*Errors involving theorems*) 

105 
exception THM of string * int * thm list; 

106 

107 
(*maps objectrule to tpairs *) 

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

109 

110 
(*maps objectrule to premises *) 

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

112 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 

113 

114 
(*counts premises in a rule*) 

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

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

117 

118 
(*maps objectrule to conclusion *) 

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

120 

121 
(*Stamps associated with a signature*) 

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

123 

124 
(*Theories. There is one pure theory. 

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

126 
datatype theory = 

127 
Pure of {sign: Sign.sg} 

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

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

130 

131 
(*Errors involving theories*) 

132 
exception THEORY of string * theory list; 

133 

134 
fun sign_of (Pure {sign}) = sign 

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

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

137 

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

139 

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

141 
fun axioms_of (Pure _) = [] 

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

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

144 

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

146 
fun parents_of (Pure _) = [] 

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

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

149 

150 

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

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

153 
fun merge_theories(th1,th2) = 

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

155 
in Sign.merge (sign1,sign2) end 

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

157 

158 
(*Stamps associated with a theory*) 

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

160 

161 

162 
(**** Primitive rules ****) 

163 

164 
(* discharge all assumptions t from ts *) 

165 
val disch = gen_rem (op aconv); 

166 

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

168 
fun assume ct : thm = 

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

170 
in if T<>propT then 

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

172 
else if maxidx <> ~1 then 

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

174 
maxidx, []) 

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

176 
end; 

177 

178 
(* Implication introduction 

179 
A  B 

180 
 

181 
A ==> B *) 

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

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

184 
in if T<>propT then 

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

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

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

188 
handle TERM _ => 

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

190 
end; 

191 

192 
(* Implication elimination 

193 
A ==> B A 

194 
 

195 
B *) 

196 
fun implies_elim thAB thA : thm = 

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

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

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

200 
in case prop of 

201 
imp$A$B => 

202 
if imp=implies andalso A aconv propA 

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

204 
maxidx= max[maxA,maxidx], 

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

206 
prop= B} 

207 
else err("major premise") 

208 
 _ => err("major premise") 

209 
end; 

210 

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

212 
A 

213 
 

214 
!!x.A *) 

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

216 
let val x = Sign.term_of cx; 

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

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

219 
in case x of 

220 
Free(a,T) => 

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

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

223 
else result(a,T) 

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

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

226 
end; 

227 

228 
(* Forall elimination 

229 
!!x.A 

230 
 

231 
A[t/x] *) 

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

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

234 
in case prop of 

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

236 
if T<>qary then 

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

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

239 
maxidx= max[maxidx, maxt], 

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

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

242 
end 

243 
handle TERM _ => 

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

245 

246 

247 
(*** Equality ***) 

248 

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

250 
val flexpair_def = 

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

252 
prop= Sign.term_of 

253 
(Sign.read_cterm Sign.pure 

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

255 

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

257 
fun reflexive ct = 

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

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

260 
end; 

261 

262 
(*The symmetry rule 

263 
t==u 

264 
 

265 
u==t *) 

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

267 
case prop of 

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

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

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

271 

272 
(*The transitive rule 

273 
t1==u u==t2 

274 
 

275 
t1==t2 *) 

276 
fun transitive th1 th2 = 

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

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

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

280 
in case (prop1,prop2) of 

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

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

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

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

285 
 _ => err"premises" 

286 
end; 

287 

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

289 
fun beta_conversion ct = 

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

291 
in case t of 

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

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

294 
maxidx= maxidx_of_term t, 

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

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

297 
end; 

298 

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

300 
f(x) == g(x) 

301 
 

302 
f == g *) 

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

304 
case prop of 

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

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

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

308 
case y of 

309 
Free _ => 

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

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

312 
 Var _ => 

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

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

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

316 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

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

318 
end 

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

320 

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

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

323 
t == u 

324 
 

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

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

327 
let val x = Sign.term_of cx; 

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

329 
handle TERM _ => 

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

331 
fun result T = 

332 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

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

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

335 
in case x of 

336 
Free(_,T) => 

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

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

339 
else result T 

340 
 Var(_,T) => result T 

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

342 
end; 

343 

344 
(*The combination rule 

345 
f==g t==u 

346 
 

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

348 
fun combination th1 th2 = 

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

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

351 
in case (prop1,prop2) of 

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

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

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

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

356 
end; 

357 

358 

359 
(*The equal propositions rule 

360 
A==B A 

361 
 

362 
B *) 

363 
fun equal_elim th1 th2 = 

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

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

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

367 
in case prop1 of 

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

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

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

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

372 
 _ => err"major premise" 

373 
end; 

374 

375 

376 
(* Equality introduction 

377 
A==>B B==>A 

378 
 

379 
A==B *) 

380 
fun equal_intr th1 th2 = 

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

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

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

384 
in case (prop1,prop2) of 

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

386 
if A aconv A' andalso B aconv B' 

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

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

389 
else err"not equal" 

390 
 _ => err"premises" 

391 
end; 

392 

393 
(**** Derived rules ****) 

394 

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

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

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

398 
implies_intr_hyps 

399 
(Thm{sign=sign, maxidx=maxidx, 

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

401 
 implies_intr_hyps th = th; 

402 

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

404 
Instantiates the theorem and deletes trivial tpairs. 

405 
Resulting sequence may contain multiple elements if the tpairs are 

406 
not all flexflex. *) 

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

408 
let fun newthm env = 

409 
let val (tpairs,horn) = 

410 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

414 
in Thm{sign= sign, hyps= hyps, 

415 
maxidx= maxidx_of_term newprop, prop= newprop} 

416 
end; 

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

418 
in Sequence.maps newthm 

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

420 
end; 

421 

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 

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 

808 
(*simple test for looping rewrite*) 

809 
fun loops sign prems (lhs,rhs) = 

810 
null(prems) andalso 

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

812 

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

814 
let val prems = Logic.strip_imp_prems prop 

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

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

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

818 
in if loops sign prems (lhs,rhs) 

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

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

821 
end; 

822 

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

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

826 
in 

827 

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

87  830 
case mk_rrule thm of 
831 
None => mss 

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

833 
Mss{net= (Net.insert_term((lhs,rrule),net,eq) 

834 
handle Net.INSERT => 

835 
(prtm "Warning: ignoring duplicate rewrite rule" sign prop; 

836 
net)), 

837 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}; 

838 

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

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

841 
case mk_rrule thm of 

842 
None => mss 

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

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

845 
handle Net.INSERT => 

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

847 
net)), 

0  848 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews} 
87  849 

850 
end; 

0  851 

852 
val add_simps = foldl add_simp; 

87  853 
val del_simps = foldl del_simp; 
0  854 

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

856 

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

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

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

860 
val lhs = Pattern.eta_contract lhs 

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

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

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

864 
prems=prems, mk_rews=mk_rews} 

865 
end; 

866 

867 
val (op add_congs) = foldl add_cong; 

868 

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

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

871 

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

873 

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

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

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

877 

878 

879 
(*** Metalevel rewriting 

880 
uses conversions, omitting proofs for efficiency. See 

881 
L C Paulson, A higherorder implementation of rewriting, 

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

883 

884 
type prover = meta_simpset > thm > thm option; 

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

886 
type conv = meta_simpset > termrec > termrec; 

887 

888 
val trace_simp = ref false; 

889 

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

891 

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

893 

894 
fun check_conv(thm as Thm{sign,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)) 

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

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

904 
end; 

905 

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

907 
fun rewritec prover (mss as Mss{net,...}) (sghyt as (sgt,hypst),t) = 

908 
let val t = Pattern.eta_contract t 

909 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs} = 

910 
let val sign' = Sign.merge(sgt,sign) 

911 
val tsig = #tsig(Sign.rep_sg sign') 

912 
val insts = Pattern.match tsig (lhs,t) 

913 
val prop' = subst_vars insts prop; 

914 
val hyps' = hyps union hypst; 

915 
val thm' = Thm{sign=sign', hyps=hyps', prop=prop', maxidx=maxidx} 

916 
in if nprems_of thm' = 0 

917 
then let val (_,rhs) = Logic.dest_equals prop' 

918 
in trace_thm "Rewriting:" thm'; Some((sign',hyps'),rhs) end 

919 
else (trace_thm "Trying to rewrite:" thm'; 

920 
case prover mss thm' of 

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

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

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

925 
fun rewl [] = None 

926 
 rewl (rrule::rrules) = 

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

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

929 

930 
in case t of 

931 
Abs(_,_,body) $ u => Some(sghyt,subst_bounds([u], body)) 

932 
 _ => rewl (Net.match_term net t) 

933 
end; 

934 

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

936 
fun congc prover {thm=cong,lhs=lhs} (sghyt as (sgt,hypst),t) = 

937 
let val Thm{sign,hyps,maxidx,prop,...} = cong 

938 
val sign' = Sign.merge(sgt,sign) 

939 
val tsig = #tsig(Sign.rep_sg sign') 

940 
val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH => 

941 
error("Congruence rule did not match") 

942 
val prop' = subst_vars insts prop; 

943 
val thm' = Thm{sign=sign', hyps=hyps union hypst, 

944 
prop=prop', maxidx=maxidx} 

945 
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

946 
fun err() = error("Failed congruence proof!") 
0  947 

948 
in case prover thm' of 

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

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

950 
 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

951 
None => err()  Some(x) => x) 
0  952 
end; 
953 

954 

955 
fun bottomc prover = 

956 
let fun botc mss trec = let val trec1 = subc mss trec 

957 
in case rewritec prover mss trec1 of 

958 
None => trec1 

959 
 Some(trec2) => botc mss trec2 

960 
end 

961 

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

963 
(trec as (sghy,t)) = 

964 
(case t of 

965 
Abs(a,T,t) => 

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

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

968 
prems=prems,mk_rews=mk_rews} 

969 
val (sghy',t') = botc mss' (sghy,subst_bounds([v],t)) 

970 
in (sghy', Abs(a, T, abstract_over(v,t'))) end 

971 
 t$u => (case t of 

972 
Const("==>",_)$s => impc(sghy,s,u,mss) 

973 
 Abs(_,_,body) => subc mss (sghy,subst_bounds([u], body)) 

974 
 _ => 

975 
let fun appc() = let val (sghy1,t1) = botc mss (sghy,t) 

976 
val (sghy2,u1) = botc mss (sghy1,u) 

977 
in (sghy2,t1$u1) end 

978 
val (h,ts) = strip_comb t 

979 
in case h of 

980 
Const(a,_) => 

981 
(case assoc(congs,a) of 

982 
None => appc() 

983 
 Some(cong) => congc (prover mss) cong trec) 

984 
 _ => appc() 

985 
end) 

986 
 _ => trec) 

987 

988 
and impc(sghy,s,u,mss as Mss{mk_rews,...}) = 

989 
let val (sghy1 as (sg1,hyps1),s') = botc mss (sghy,s) 

990 
val (rthms,mss) = 

991 
if maxidx_of_term s' <> ~1 then ([],mss) 

992 
else let val thm = Thm{sign=sg1,hyps=[s'],prop=s',maxidx= ~1} 

993 
in (mk_rews thm, add_prems(mss,[thm])) end 

994 
val unit = seq (trace_thm "Adding rewrite rule:") rthms 

995 
val mss' = add_simps(mss,rthms) 

996 
val ((sg2,hyps2),u') = botc mss' (sghy1,u) 

134
595fda4879b6
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
nipkow
parents:
112
diff
changeset

997 
val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s' 
595fda4879b6
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
nipkow
parents:
112
diff
changeset

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

1000 
in botc end; 

1001 

1002 

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

1004 
(* Parameters: 

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

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

1007 
*) 

1008 

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

1010 
fun rewrite_cterm mss prover ct = 

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

1012 
val ((sign',hyps),u) = bottomc prover mss ((sign,[]),t); 

1013 
val prop = Logic.mk_equals(t,u) 

1014 
in Thm{sign= sign', hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 

1015 
end 

1016 

1017 
end; 