author  wenzelm 
Thu, 03 Feb 1994 13:53:08 +0100  
changeset 250  9b5a069285ce 
parent 242  8fe3e66abf0c 
child 274  dc87495814d5 
permissions  rwrr 
250  1 
(* Title: Pure/thm.ML 
0  2 
ID: $Id$ 
250  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

4 
Copyright 1994 University of Cambridge 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

5 

250  6 
The abstract types "theory" and "thm". 
7 
Also "cterm" / "ctyp" (certified terms / typs under a signature). 

0  8 

250  9 
TODO: 
10 
NO REP_CTERM!! 

0  11 
*) 
12 

250  13 
signature THM = 
14 
sig 

0  15 
structure Envir : ENVIR 
16 
structure Sequence : SEQUENCE 

17 
structure Sign : SIGN 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

18 
type cterm 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

19 
type ctyp 
0  20 
type meta_simpset 
21 
type theory 

22 
type thm 

23 
exception THM of string * int * thm list 

24 
exception THEORY of string * theory list 

25 
exception SIMPLIFIER of string * thm 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

26 
(*Certified terms/types; previously in sign.ML*) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

27 
val cterm_of: Sign.sg > term > cterm 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

28 
val ctyp_of: Sign.sg > typ > ctyp 
250  29 
val read_ctyp: Sign.sg > string > ctyp 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

30 
val read_cterm: Sign.sg > string * typ > cterm 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

31 
val rep_cterm: cterm > {T: typ, t: term, sign: Sign.sg, maxidx: int} 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

32 
val rep_ctyp: ctyp > {T: typ, sign: Sign.sg} 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

33 
val term_of: cterm > term 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

34 
val typ_of: ctyp > typ 
250  35 
val cterm_fun: (term > term) > (cterm > cterm) 
36 
(*End of cterm/ctyp functions*) 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

37 
val abstract_rule: string > cterm > thm > thm 
0  38 
val add_congs: meta_simpset * thm list > meta_simpset 
39 
val add_prems: meta_simpset * thm list > meta_simpset 

40 
val add_simps: meta_simpset * thm list > meta_simpset 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

41 
val assume: cterm > thm 
250  42 
val assumption: int > thm > thm Sequence.seq 
0  43 
val axioms_of: theory > (string * thm) list 
250  44 
val beta_conversion: cterm > thm 
45 
val bicompose: bool > bool * thm * int > int > thm > thm Sequence.seq 

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

47 
val combination: thm > thm > thm 

48 
val concl_of: thm > term 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

49 
val cprop_of: thm > cterm 
87  50 
val del_simps: meta_simpset * thm list > meta_simpset 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

51 
val dest_cimplies: cterm > cterm*cterm 
0  52 
val dest_state: thm * int > (term*term)list * term list * term * term 
53 
val empty_mss: meta_simpset 

250  54 
val eq_assumption: int > thm > thm 
0  55 
val equal_intr: thm > thm > thm 
56 
val equal_elim: thm > thm > thm 

57 
val extend_theory: theory > string 

250  58 
> (class * class list) list * sort 
59 
* (string list * int)list 

60 
* (string * string list * string) list 

61 
* (string list * (sort list * class))list 

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

63 
> (string*string)list > theory 

64 
val extensional: thm > thm 

65 
val flexflex_rule: thm > thm Sequence.seq 

66 
val flexpair_def: thm 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

67 
val forall_elim: cterm > thm > thm 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

68 
val forall_intr: cterm > thm > thm 
0  69 
val freezeT: thm > thm 
70 
val get_axiom: theory > string > thm 

71 
val implies_elim: thm > thm > thm 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

72 
val implies_intr: cterm > thm > thm 
0  73 
val implies_intr_hyps: thm > thm 
250  74 
val instantiate: (indexname*ctyp)list * (cterm*cterm)list 
0  75 
> thm > thm 
76 
val lift_rule: (thm * int) > thm > thm 

77 
val merge_theories: theory * theory > theory 

78 
val mk_rews_of_mss: meta_simpset > thm > thm list 

79 
val mss_of: thm list > meta_simpset 

80 
val nprems_of: thm > int 

81 
val parents_of: theory > theory list 

82 
val prems_of: thm > term list 

83 
val prems_of_mss: meta_simpset > thm list 

84 
val pure_thy: theory 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

85 
val read_def_cterm : 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

86 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

87 
string * typ > cterm * (indexname * typ) list 
250  88 
val reflexive: cterm > thm 
0  89 
val rename_params_rule: string list * int > thm > thm 
90 
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

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

92 
bool*bool > meta_simpset > (meta_simpset > thm > thm option) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

93 
> cterm > thm 
0  94 
val set_mk_rews: meta_simpset * (thm > thm list) > meta_simpset 
250  95 
val sign_of: theory > Sign.sg 
0  96 
val syn_of: theory > Sign.Syntax.syntax 
97 
val stamps_of_thm: thm > string ref list 

98 
val stamps_of_thy: theory > string ref list 

250  99 
val symmetric: thm > thm 
0  100 
val tpairs_of: thm > (term*term)list 
101 
val trace_simp: bool ref 

102 
val transitive: thm > thm > thm 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

103 
val trivial: cterm > thm 
0  104 
val varifyT: thm > thm 
250  105 
end; 
0  106 

250  107 
functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN 
108 
and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)(*: THM *) (* FIXME debug *) = 

0  109 
struct 
250  110 

0  111 
structure Sequence = Unify.Sequence; 
112 
structure Envir = Unify.Envir; 

113 
structure Sign = Unify.Sign; 

114 
structure Type = Sign.Type; 

115 
structure Syntax = Sign.Syntax; 

116 
structure Symtab = Sign.Symtab; 

117 

118 

250  119 
(** certified types **) 
120 

121 
(*certified typs under a signature*) 

122 

123 
datatype ctyp = Ctyp of {sign: Sign.sg, T: typ}; 

124 

125 
fun rep_ctyp (Ctyp args) = args; 

126 
fun typ_of (Ctyp {T, ...}) = T; 

127 

128 
fun ctyp_of sign T = 

129 
Ctyp {sign = sign, T = Sign.certify_typ sign T}; 

130 

131 
fun read_ctyp sign s = 

132 
Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s}; 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

133 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

134 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

135 

250  136 
(** certified terms **) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

137 

250  138 
(*certified terms under a signature, with checked typ and maxidx of Vars*) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

139 

250  140 
datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

141 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

142 
fun rep_cterm (Cterm args) = args; 
250  143 
fun term_of (Cterm {t, ...}) = t; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

144 

250  145 
(*create a cterm by checking a "raw" term with respect to a signature*) 
146 
fun cterm_of sign tm = 

147 
let val (t, T, maxidx) = Sign.certify_term sign tm 

148 
in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} 

149 
end handle TYPE (msg, _, _) 

150 
=> raise TERM ("Term not in signature\n" ^ msg, [tm]); 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

151 

250  152 
fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t); 
153 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

154 

250  155 
(*dest_implies for cterms. Note T=prop below*) 
156 
fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>", _) $ A $ B}) = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

157 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  158 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
159 
 dest_cimplies ct = raise TERM ("dest_cimplies", [term_of ct]); 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

160 

250  161 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

162 

250  163 
(** read cterms **) 
164 

165 
(*read term, infer types, certify term*) 

166 

167 
fun read_def_cterm (sign, types, sorts) (a, T) = 

168 
let 

169 
val {tsig, const_tab, syn, ...} = Sign.rep_sg sign; 

170 
val showtyp = Sign.string_of_typ sign; 

171 
val showterm = Sign.string_of_term sign; 

172 

173 
fun termerr [] = "" 

174 
 termerr [t] = "\nInvolving this term:\n" ^ showterm t 

175 
 termerr ts = "\nInvolving these terms:\n" ^ cat_lines (map showterm ts); 

176 

177 
val T' = Sign.certify_typ sign T 

178 
handle TYPE (msg, _, _) => error msg; 

179 
val t = Syntax.read syn T' a; 

180 
val (t', tye) = Type.infer_types (tsig, const_tab, types, sorts, T', t) 

181 
handle TYPE (msg, Ts, ts) => error ("Type checking error: " ^ msg ^ "\n" 

182 
^ cat_lines (map showtyp Ts) ^ termerr ts); 

183 
val ct = cterm_of sign t' handle TERM (msg, _) => error msg; 

184 
in (ct, tye) end; 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

185 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

186 
fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None)); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

187 

250  188 

189 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

190 
(**** METATHEOREMS ****) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

191 

0  192 
datatype thm = Thm of 
250  193 
{sign: Sign.sg, maxidx: int, hyps: term list, prop: term}; 
0  194 

250  195 
fun rep_thm (Thm args) = args; 
0  196 

197 
(*Errors involving theorems*) 

198 
exception THM of string * int * thm list; 

199 

200 
(*maps objectrule to tpairs *) 

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

202 

203 
(*maps objectrule to premises *) 

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

205 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 

206 

207 
(*counts premises in a rule*) 

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

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

210 

211 
(*maps objectrule to conclusion *) 

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

213 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

214 
(*The statement of any Thm is a Cterm*) 
250  215 
fun cprop_of (Thm{sign,maxidx,hyps,prop}) = 
216 
Cterm{sign=sign, maxidx=maxidx, T=propT, t=prop}; 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

217 

0  218 
(*Stamps associated with a signature*) 
219 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; 

220 

221 
(*Theories. There is one pure theory. 

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

223 
datatype theory = 

224 
Pure of {sign: Sign.sg} 

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

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

227 

228 
(*Errors involving theories*) 

229 
exception THEORY of string * theory list; 

230 

231 
fun sign_of (Pure {sign}) = sign 

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

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

234 

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

236 

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

238 
fun axioms_of (Pure _) = [] 

250  239 
 axioms_of (Extend {axioms, thy, ...}) = 
240 
axioms_of thy @ Symtab.alist_of axioms 

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

0  242 

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

244 
fun parents_of (Pure _) = [] 

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

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

247 

248 

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

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

251 
fun merge_theories(th1,th2) = 

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

253 
in Sign.merge (sign1,sign2) end 

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

255 

256 
(*Stamps associated with a theory*) 

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

258 

259 

260 
(**** Primitive rules ****) 

261 

262 
(* discharge all assumptions t from ts *) 

263 
val disch = gen_rem (op aconv); 

264 

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

250  266 
fun assume ct : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

267 
let val {sign, t=prop, T, maxidx} = rep_cterm ct 
250  268 
in if T<>propT then 
269 
raise THM("assume: assumptions must have type prop", 0, []) 

0  270 
else if maxidx <> ~1 then 
250  271 
raise THM("assume: assumptions may not contain scheme variables", 
272 
maxidx, []) 

0  273 
else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop} 
274 
end; 

275 

250  276 
(* Implication introduction 
277 
A  B 

278 
 

279 
A ==> B *) 

0  280 
fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

281 
let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA 
0  282 
in if T<>propT then 
250  283 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
284 
else Thm{sign= Sign.merge (sign,signA), maxidx= max[maxidxA, maxidx], 

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

0  286 
handle TERM _ => 
287 
raise THM("implies_intr: incompatible signatures", 0, [thB]) 

288 
end; 

289 

290 
(* Implication elimination 

250  291 
A ==> B A 
292 
 

293 
B *) 

0  294 
fun implies_elim thAB thA : thm = 
295 
let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA 

250  296 
and Thm{sign, maxidx, hyps, prop,...} = thAB; 
297 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 

0  298 
in case prop of 
250  299 
imp$A$B => 
300 
if imp=implies andalso A aconv propA 

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

302 
maxidx= max[maxA,maxidx], 

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

304 
prop= B} 

305 
else err("major premise") 

306 
 _ => err("major premise") 

0  307 
end; 
250  308 

0  309 
(* Forall introduction. The Free or Var x must not be free in the hypotheses. 
310 
A 

311 
 

312 
!!x.A *) 

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

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

314 
let val x = term_of cx; 
0  315 
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps, 
250  316 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))} 
0  317 
in case x of 
250  318 
Free(a,T) => 
319 
if exists (apl(x, Logic.occs)) hyps 

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

321 
else result(a,T) 

0  322 
 Var((a,_),T) => result(a,T) 
323 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 

324 
end; 

325 

326 
(* Forall elimination 

250  327 
!!x.A 
328 
 

329 
A[t/x] *) 

0  330 
fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

331 
let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct 
0  332 
in case prop of 
250  333 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 
334 
if T<>qary then 

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

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

337 
maxidx= max[maxidx, maxt], 

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

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

0  340 
end 
341 
handle TERM _ => 

250  342 
raise THM("forall_elim: incompatible signatures", 0, [th]); 
0  343 

344 

345 
(*** Equality ***) 

346 

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

348 
val flexpair_def = 

250  349 
Thm{sign= Sign.pure, hyps= [], maxidx= 0, 
350 
prop= term_of 

351 
(read_cterm Sign.pure 

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

0  353 

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

250  355 
fun reflexive ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

356 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  357 
in Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)} 
358 
end; 

359 

360 
(*The symmetry rule 

361 
t==u 

362 
 

363 
u==t *) 

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

365 
case prop of 

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

250  367 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 
0  368 
 _ => raise THM("symmetric", 0, [th]); 
369 

370 
(*The transitive rule 

371 
t1==u u==t2 

372 
 

373 
t1==t2 *) 

374 
fun transitive th1 th2 = 

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

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

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

378 
in case (prop1,prop2) of 

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

250  380 
if not (u aconv u') then err"middle term" else 
381 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 

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

0  383 
 _ => err"premises" 
384 
end; 

385 

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

250  387 
fun beta_conversion ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

388 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  389 
in case t of 
250  390 
Abs(_,_,bodt) $ u => 
391 
Thm{sign= sign, hyps= [], 

392 
maxidx= maxidx_of_term t, 

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

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

0  395 
end; 
396 

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

398 
f(x) == g(x) 

399 
 

400 
f == g *) 

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

402 
case prop of 

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

250  404 
let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) 
0  405 
in (if x<>y then err"different variables" else 
406 
case y of 

250  407 
Free _ => 
408 
if exists (apl(y, Logic.occs)) (f::g::hyps) 

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

410 
 Var _ => 

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

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

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

414 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

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

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

418 

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

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

421 
t == u 

422 
 

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

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

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

425 
let val x = term_of cx; 
250  426 
val (t,u) = Logic.dest_equals prop 
427 
handle TERM _ => 

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

0  429 
fun result T = 
430 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

250  431 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
432 
Abs(a, T, abstract_over (x,u)))} 

0  433 
in case x of 
250  434 
Free(_,T) => 
435 
if exists (apl(x, Logic.occs)) hyps 

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

437 
else result T 

0  438 
 Var(_,T) => result T 
439 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 

440 
end; 

441 

442 
(*The combination rule 

443 
f==g t==u 

444 
 

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

446 
fun combination th1 th2 = 

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

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

449 
in case (prop1,prop2) of 

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

250  451 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
452 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} 

0  453 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
454 
end; 

455 

456 

457 
(*The equal propositions rule 

458 
A==B A 

459 
 

460 
B *) 

461 
fun equal_elim th1 th2 = 

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

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

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

465 
in case prop1 of 

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

250  467 
if not (prop2 aconv A) then err"not equal" else 
468 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 

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

0  470 
 _ => err"major premise" 
471 
end; 

472 

473 

474 
(* Equality introduction 

475 
A==>B B==>A 

476 
 

477 
A==B *) 

478 
fun equal_intr th1 th2 = 

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

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

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

482 
in case (prop1,prop2) of 

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

250  484 
if A aconv A' andalso B aconv B' 
485 
then Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 

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

487 
else err"not equal" 

0  488 
 _ => err"premises" 
489 
end; 

490 

491 
(**** Derived rules ****) 

492 

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

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

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

496 
implies_intr_hyps 

250  497 
(Thm{sign=sign, maxidx=maxidx, 
498 
hyps= disch(As,A), prop= implies$A$prop}) 

0  499 
 implies_intr_hyps th = th; 
500 

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

250  502 
Instantiates the theorem and deletes trivial tpairs. 
0  503 
Resulting sequence may contain multiple elements if the tpairs are 
504 
not all flexflex. *) 

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

250  506 
let fun newthm env = 
507 
let val (tpairs,horn) = 

508 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

512 
in Thm{sign= sign, hyps= hyps, 

513 
maxidx= maxidx_of_term newprop, prop= newprop} 

514 
end; 

0  515 
val (tpairs,_) = Logic.strip_flexpairs prop 
516 
in Sequence.maps newthm 

250  517 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  518 
end; 
519 

520 
(*Instantiation of Vars 

250  521 
A 
522 
 

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

0  524 

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

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

527 

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

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

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

530 
let val {sign=signt, t=t, T= T, ...} = rep_cterm ct 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

531 
and {sign=signu, t=u, T= U, ...} = rep_cterm cu 
0  532 
in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs) 
533 
else raise TYPE("add_ctpair", [T,U], [t,u]) 

534 
end; 

535 

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

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

537 
let val {T,sign} = rep_ctyp ctyp 
0  538 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
539 

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

541 
Instantiates distinct Vars by terms of same type. 

542 
Normalizes the new theorem! *) 

250  543 
fun instantiate (vcTs,ctpairs) (th as Thm{sign,maxidx,hyps,prop}) = 
0  544 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); 
545 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); 

250  546 
val newprop = 
547 
Envir.norm_term (Envir.empty 0) 

548 
(subst_atomic tpairs 

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

0  550 
val newth = Thm{sign= newsign, hyps= hyps, 
250  551 
maxidx= maxidx_of_term newprop, prop= newprop} 
552 
in if not(instl_ok(map #1 tpairs)) 

193  553 
then raise THM("instantiate: variables not distinct", 0, [th]) 
554 
else if not(null(findrep(map #1 vTs))) 

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

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

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

250  558 
ix::_ => raise THM("instantiate: conflicting types for variable " ^ 
559 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

560 
 [] => 

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

562 
ix::_ => raise THM 

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

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

193  565 
 [] => newth 
0  566 
end 
250  567 
handle TERM _ => 
0  568 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  569 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  570 

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

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

250  573 
fun trivial ct : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

574 
let val {sign, t=A, T, maxidx} = rep_cterm ct 
250  575 
in if T<>propT then 
576 
raise THM("trivial: the term must have type prop", 0, []) 

0  577 
else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A} 
578 
end; 

579 

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

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

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

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

250  584 
prop= Type.varify(prop,tfrees)} 
0  585 
end; 
586 

587 
(* Replace all TVars by new TFrees *) 

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

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

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

591 

592 

593 
(*** Inference rules for tactics ***) 

594 

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

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

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

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

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

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

601 
end 

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

603 

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

605 
resolution with goal i of state. *) 

606 
fun lift_rule (state, i) orule = 

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

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

250  609 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 
0  610 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 
611 
val (Thm{sign,maxidx,hyps,prop}) = orule 

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

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

250  614 
maxidx= maxidx+smax+1, 
615 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 

616 
map lift_all As, lift_all B)} 

0  617 
end; 
618 

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

620 
fun assumption i state = 

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

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

250  623 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
624 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= 

625 
if Envir.is_empty env then (*avoid wasted normalizations*) 

626 
Logic.rule_of (tpairs, Bs, C) 

627 
else (*normalize the new rule fully*) 

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

0  629 
fun addprfs [] = Sequence.null 
630 
 addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull 

631 
(Sequence.mapp newth 

250  632 
(Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) 
633 
(addprfs apairs))) 

0  634 
in addprfs (Logic.assum_pairs Bi) end; 
635 

250  636 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
0  637 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*) 
638 
fun eq_assumption i state = 

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

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

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

250  642 
then Thm{sign=sign, hyps=hyps, maxidx=maxidx, 
643 
prop=Logic.rule_of(tpairs, Bs, C)} 

0  644 
else raise THM("eq_assumption", 0, [state]) 
645 
end; 

646 

647 

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

649 

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

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

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

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

654 
fun rename_params_rule (cs, i) state = 

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

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

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

658 
val short = length iparams  length cs 

250  659 
val newnames = 
660 
if short<0 then error"More names than abstractions!" 

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

0  662 
val freenames = map (#1 o dest_Free) (term_frees prop) 
663 
val newBi = Logic.list_rename_params (newnames, Bi) 

250  664 
in 
0  665 
case findrep cs of 
666 
c::_ => error ("Bound variables not distinct: " ^ c) 

667 
 [] => (case cs inter freenames of 

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

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

250  670 
Logic.rule_of(tpairs, Bs@[newBi], C)}) 
0  671 
end; 
672 

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

674 

250  675 
(*Scan a pair of terms; while they are similar, 
0  676 
accumulate corresponding bound vars in "al"*) 
677 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al) 

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

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

680 

681 
(* strip abstractions created by parameters *) 

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

683 

684 

250  685 
(* strip_apply f A(,B) strips off all assumptions/parameters from A 
0  686 
introduced by lifting over B, and applies f to remaining part of A*) 
687 
fun strip_apply f = 

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

250  689 
Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2) 
690 
 strip((c as Const("all",_)) $ Abs(a,T,t1), 

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

692 
 strip(A,_) = f A 

0  693 
in strip end; 
694 

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

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

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

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

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

250  700 
let val vars = foldr add_term_vars 
701 
(map fst dpairs @ map fst tpairs @ map snd tpairs, []) 

702 
(*unknowns appearing elsewhere be preserved!*) 

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

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

705 
(case assoc(al,x) of 

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

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

708 
 None=> t) 

0  709 
 rename(Abs(x,T,t)) = 
250  710 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
711 
T, rename t) 

0  712 
 rename(f$t) = rename f $ rename t 
713 
 rename(t) = t; 

250  714 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  715 
in strip_ren end; 
716 

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

718 
fun rename_bvars(dpairs, tpairs, B) = 

250  719 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  720 

721 

722 
(*** RESOLUTION ***) 

723 

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

725 
identical because of lifting*) 

250  726 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
727 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  728 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  729 
Const("all",_)$Abs(_,_,t2)) = 
0  730 
let val (B1,B2) = strip_assums2 (t1,t2) 
731 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

732 
 strip_assums2 BB = BB; 

733 

734 

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

250  736 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0  737 
If match then forbid instantiations in proof state 
738 
If lifted then shorten the dpair using strip_assums2. 

739 
If eres_flg then simultaneously proves A1 by assumption. 

250  740 
nsubgoal is the number of new subgoals (written m above). 
0  741 
Curried so that resolution calls dest_state only once. 
742 
*) 

743 
local open Sequence; exception Bicompose 

744 
in 

250  745 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  746 
(eres_flg, orule, nsubgoal) = 
747 
let val Thm{maxidx=smax, hyps=shyps, ...} = state 

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

749 
val sign = merge_theories(state,orule); 

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

250  751 
fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = 
752 
let val normt = Envir.norm_term env; 

753 
(*perform minimal copying here by examining env*) 

754 
val normp = 

755 
if Envir.is_empty env then (tpairs, Bs @ As, C) 

756 
else 

757 
let val ntps = map (pairself normt) tpairs 

758 
in if the (Envir.minidx env) > smax then (*no assignments in state*) 

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

760 
else if match then raise Bicompose 

761 
else (*normalize the new rule fully*) 

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

763 
end 

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

765 
prop= Logic.rule_of normp} 

0  766 
in cons(th, thq) end handle Bicompose => thq 
767 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 

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

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

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

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

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

250  773 
else map (rename_bvars(dpairs,tpairs,B)) As0 
0  774 
in (map (Logic.flatten_params n) As1) 
250  775 
handle TERM _ => 
776 
raise THM("bicompose: 1st premise", 0, [orule]) 

0  777 
end; 
778 
val env = Envir.empty(max[rmax,smax]); 

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

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

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

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

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

250  784 
(case pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of 
785 
None => tryasms (As, n+1, apairs) 

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

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

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

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

0  790 
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) 
791 
 eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1); 

792 
(*ordinary resolution*) 

793 
fun res(None) = null 

250  794 
 res(cell as Some((_,tpairs),_)) = 
795 
its_right (addth(newAs(rev rAs, 0, [BBi], tpairs))) 

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

0  797 
in if eres_flg then eres(rev rAs) 
798 
else res(pull(Unify.unifiers(sign, env, dpairs))) 

799 
end; 

800 
end; (*open Sequence*) 

801 

802 

803 
fun bicompose match arg i state = 

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

805 

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

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

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

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

250  810 
 could_reshyp [] = false; (*no premise  illegal*) 
811 
in could_unify(concl_of rule, B) andalso 

812 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  813 
end; 
814 

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

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

250  817 
fun biresolution match brules i state = 
0  818 
let val lift = lift_rule(state, i); 
250  819 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
820 
val B = Logic.strip_assums_concl Bi; 

821 
val Hs = Logic.strip_assums_hyp Bi; 

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

823 
fun res [] = Sequence.null 

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

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

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

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

828 
res brules)) 

829 
else res brules 

0  830 
in Sequence.flats (res brules) end; 
831 

832 

833 
(**** THEORIES ****) 

834 

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

836 

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

838 
fun get_axiom thy axname = 

839 
let fun get (Pure _) = raise Match 

250  840 
 get (Extend{axioms,thy,...}) = 
841 
(case Symtab.lookup(axioms,axname) of 

842 
Some th => th 

843 
 None => get thy) 

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

845 
get thy1 handle Match => get thy2 

0  846 
in get thy 
250  847 
handle Match => raise THEORY("get_axiom: No axiom "^axname, [thy]) 
0  848 
end; 
849 

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

851 
fun prepare_axiom sign sP = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

852 
Logic.varify (term_of (read_cterm sign (sP,propT))); 
0  853 

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

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

856 
let val prop = prepare_axiom sign sP 

250  857 
in (a, Thm{sign=sign, hyps=[], maxidx= maxidx_of_term prop, prop= prop}) 
0  858 
end 
859 
handle ERROR => 

250  860 
error("extend_theory: The error above occurred in axiom " ^ a); 
0  861 

862 
fun mk_axioms sign axpairs = 

250  863 
Symtab.st_of_alist(map (read_ax sign) axpairs, Symtab.null) 
864 
handle Symtab.DUPLICATE(a) => error("Two axioms named " ^ a); 

0  865 

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

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

868 
fun extend_theory thy thyname ext axpairs = 

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

870 
val axioms= mk_axioms sign axpairs 

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

872 

873 
(*The union of two theories*) 

250  874 
fun merge_theories (thy1, thy2) = 
875 
Merge {sign = Sign.merge (sign_of thy1, sign_of thy2), 

876 
thy1 = thy1, thy2 = thy2} handle TERM (msg, _) => error msg; 

0  877 

878 

879 
(*** Meta simp sets ***) 

880 

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

882 
datatype meta_simpset = 

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

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

885 

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

887 
net: discrimination net of rewrite rules 

888 
congs: association list of congruence rules 

889 
primes: offset for generating unique new names 

890 
for rewriting under lambda abstractions 

891 
mk_rews: used when local assumptions are added 

892 
*) 

893 

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

895 
mk_rews = K[]}; 

896 

897 
exception SIMPLIFIER of string * thm; 

898 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

899 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  900 

209  901 
val trace_simp = ref false; 
902 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

903 
fun trace_term a sign t = if !trace_simp then prtm a sign t else (); 
209  904 

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

906 

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

909 
null(prems) andalso 

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

911 

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

913 
let val prems = Logic.strip_imp_prems prop 

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

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

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

917 
in if loops sign prems (lhs,rhs) 

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

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

920 
end; 

921 

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

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

925 
in 

926 

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

87  929 
case mk_rrule thm of 
930 
None => mss 

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

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

934 
handle Net.INSERT => 

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

209  937 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}); 
87  938 

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

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

941 
case mk_rrule thm of 

942 
None => mss 

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

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

945 
handle Net.INSERT => 

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

947 
net)), 

0  948 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews} 
87  949 

950 
end; 

0  951 

952 
val add_simps = foldl add_simp; 

87  953 
val del_simps = foldl del_simp; 
0  954 

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

956 

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

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

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

960 
val lhs = Pattern.eta_contract lhs 

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

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

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

964 
prems=prems, mk_rews=mk_rews} 

965 
end; 

966 

967 
val (op add_congs) = foldl add_cong; 

968 

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

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

971 

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

973 

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

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

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

977 

978 

250  979 
(*** Metalevel rewriting 
0  980 
uses conversions, omitting proofs for efficiency. See 
250  981 
L C Paulson, A higherorder implementation of rewriting, 
982 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  983 

984 
type prover = meta_simpset > thm > thm option; 

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

986 
type conv = meta_simpset > termrec > termrec; 

987 

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

988 
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

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

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

993 
if (lhs = lhs0) orelse 

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

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

995 
then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) 
0  996 
else err() 
997 
 _ => err() 

998 
end; 

999 

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

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

1001 
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

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

1003 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs} = 
250  1004 
let val unit = if Sign.subsig(sign,signt) then () 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

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

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

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

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

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

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

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

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

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

1017 
 Some(thm2) => check_conv(thm2,prop')) 
0  1018 
end 
1019 

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

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

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

1022 
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

1023 
in case opt of None => rews rrules  some => some end; 
0  1024 

1025 
in case t of 

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

1026 
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

1027 
 _ => rews(Net.match_term net t) 
0  1028 
end; 
1029 

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

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

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

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

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

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

1038 
val prop' = subst_vars insts prop; 

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

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

1042 
fun err() = error("Failed congruence proof!") 
0  1043 

1044 
in case prover thm' of 

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

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

1046 
 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

1047 
None => err()  Some(x) => x) 
0  1048 
end; 
1049 

1050 

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

1051 
fun bottomc ((simprem,useprem),prover,sign) = 
0  1052 
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

1053 
in case rewritec (prover,sign) mss trec1 of 
0  1054 
None => trec1 
1055 
 Some(trec2) => botc mss trec2 

1056 
end 

1057 

1058 
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

1059 
(trec as (hyps,t)) = 
0  1060 
(case t of 
1061 
Abs(a,T,t) => 

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

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

1064 
prems=prems,mk_rews=mk_rews} 

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

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

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

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

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

1071 
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

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

1073 
in (hyps2,t1$u1) end 
0  1074 
val (h,ts) = strip_comb t 
1075 
in case h of 

1076 
Const(a,_) => 

1077 
(case assoc(congs,a) of 

1078 
None => appc() 

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

1079 
 Some(cong) => congc (prover mss,sign) cong trec) 
0  1080 
 _ => appc() 
1081 
end) 

1082 
 _ => trec) 

1083 

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

1084 
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

1085 
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

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

1087 
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

1088 
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

1089 
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

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

1091 
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

1092 
in (hyps2', Logic.mk_implies(s',u')) end 
0  1093 

1094 
in botc end; 

1095 

1096 

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

1098 
(* Parameters: 

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

1102 
*) 

1103 

1104 
(*** 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

1105 
fun rewrite_cterm mode mss prover ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

1106 
let val {sign, t, T, maxidx} = rep_cterm ct; 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

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

1109 
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 
0  1110 
end 
1111 

1112 
end; 

250  1113 