author | blanchet |
Thu, 16 Sep 2010 07:30:15 +0200 | |
changeset 39444 | beabb8443ee4 |
parent 39443 | e330437cd22a |
child 39501 | aaa7078fff55 |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) |
|
39444 | 3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Rule :> Rule = |
|
7 |
struct |
|
8 |
||
9 |
open Useful; |
|
10 |
||
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
(* Variable names. *) |
|
13 |
(* ------------------------------------------------------------------------- *) |
|
14 |
||
15 |
val xVarName = Name.fromString "x"; |
|
16 |
val xVar = Term.Var xVarName; |
|
17 |
||
18 |
val yVarName = Name.fromString "y"; |
|
19 |
val yVar = Term.Var yVarName; |
|
20 |
||
21 |
val zVarName = Name.fromString "z"; |
|
22 |
val zVar = Term.Var zVarName; |
|
23 |
||
24 |
fun xIVarName i = Name.fromString ("x" ^ Int.toString i); |
|
25 |
fun xIVar i = Term.Var (xIVarName i); |
|
26 |
||
27 |
fun yIVarName i = Name.fromString ("y" ^ Int.toString i); |
|
28 |
fun yIVar i = Term.Var (yIVarName i); |
|
29 |
||
30 |
(* ------------------------------------------------------------------------- *) |
|
31 |
(* *) |
|
32 |
(* --------- reflexivity *) |
|
33 |
(* x = x *) |
|
34 |
(* ------------------------------------------------------------------------- *) |
|
35 |
||
36 |
fun reflexivityRule x = Thm.refl x; |
|
37 |
||
38 |
val reflexivity = reflexivityRule xVar; |
|
39 |
||
40 |
(* ------------------------------------------------------------------------- *) |
|
41 |
(* *) |
|
42 |
(* --------------------- symmetry *) |
|
43 |
(* ~(x = y) \/ y = x *) |
|
44 |
(* ------------------------------------------------------------------------- *) |
|
45 |
||
46 |
fun symmetryRule x y = |
|
47 |
let |
|
48 |
val reflTh = reflexivityRule x |
|
49 |
val reflLit = Thm.destUnit reflTh |
|
50 |
val eqTh = Thm.equality reflLit [0] y |
|
51 |
in |
|
52 |
Thm.resolve reflLit reflTh eqTh |
|
53 |
end; |
|
54 |
||
55 |
val symmetry = symmetryRule xVar yVar; |
|
56 |
||
57 |
(* ------------------------------------------------------------------------- *) |
|
58 |
(* *) |
|
59 |
(* --------------------------------- transitivity *) |
|
60 |
(* ~(x = y) \/ ~(y = z) \/ x = z *) |
|
61 |
(* ------------------------------------------------------------------------- *) |
|
62 |
||
63 |
val transitivity = |
|
64 |
let |
|
65 |
val eqTh = Thm.equality (Literal.mkEq (yVar,zVar)) [0] xVar |
|
66 |
in |
|
67 |
Thm.resolve (Literal.mkEq (yVar,xVar)) symmetry eqTh |
|
68 |
end; |
|
69 |
||
70 |
(* ------------------------------------------------------------------------- *) |
|
71 |
(* x = y \/ C *) |
|
72 |
(* -------------- symEq (x = y) *) |
|
73 |
(* y = x \/ C *) |
|
74 |
(* ------------------------------------------------------------------------- *) |
|
75 |
||
76 |
fun symEq lit th = |
|
77 |
let |
|
78 |
val (x,y) = Literal.destEq lit |
|
79 |
in |
|
80 |
if Term.equal x y then th |
|
81 |
else |
|
82 |
let |
|
83 |
val sub = Subst.fromList [(xVarName,x),(yVarName,y)] |
|
84 |
val symTh = Thm.subst sub symmetry |
|
85 |
in |
|
86 |
Thm.resolve lit th symTh |
|
87 |
end |
|
88 |
end; |
|
89 |
||
90 |
(* ------------------------------------------------------------------------- *) |
|
91 |
(* An equation consists of two terms (t,u) plus a theorem (stronger than) *) |
|
92 |
(* t = u \/ C. *) |
|
93 |
(* ------------------------------------------------------------------------- *) |
|
94 |
||
95 |
type equation = (Term.term * Term.term) * Thm.thm; |
|
96 |
||
97 |
fun ppEquation (_,th) = Thm.pp th; |
|
98 |
||
99 |
val equationToString = Print.toString ppEquation; |
|
100 |
||
101 |
fun equationLiteral (t_u,th) = |
|
102 |
let |
|
103 |
val lit = Literal.mkEq t_u |
|
104 |
in |
|
105 |
if LiteralSet.member lit (Thm.clause th) then SOME lit else NONE |
|
106 |
end; |
|
107 |
||
108 |
fun reflEqn t = ((t,t), Thm.refl t); |
|
109 |
||
110 |
fun symEqn (eqn as ((t,u), th)) = |
|
111 |
if Term.equal t u then eqn |
|
112 |
else |
|
113 |
((u,t), |
|
114 |
case equationLiteral eqn of |
|
115 |
SOME t_u => symEq t_u th |
|
116 |
| NONE => th); |
|
117 |
||
118 |
fun transEqn (eqn1 as ((x,y), th1)) (eqn2 as ((_,z), th2)) = |
|
119 |
if Term.equal x y then eqn2 |
|
120 |
else if Term.equal y z then eqn1 |
|
121 |
else if Term.equal x z then reflEqn x |
|
122 |
else |
|
123 |
((x,z), |
|
124 |
case equationLiteral eqn1 of |
|
125 |
NONE => th1 |
|
126 |
| SOME x_y => |
|
127 |
case equationLiteral eqn2 of |
|
128 |
NONE => th2 |
|
129 |
| SOME y_z => |
|
130 |
let |
|
131 |
val sub = Subst.fromList [(xVarName,x),(yVarName,y),(zVarName,z)] |
|
132 |
val th = Thm.subst sub transitivity |
|
133 |
val th = Thm.resolve x_y th1 th |
|
134 |
val th = Thm.resolve y_z th2 th |
|
135 |
in |
|
136 |
th |
|
137 |
end); |
|
138 |
||
139 |
(*MetisDebug |
|
140 |
val transEqn = fn eqn1 => fn eqn2 => |
|
141 |
transEqn eqn1 eqn2 |
|
142 |
handle Error err => |
|
143 |
raise Error ("Rule.transEqn:\neqn1 = " ^ equationToString eqn1 ^ |
|
144 |
"\neqn2 = " ^ equationToString eqn2 ^ "\n" ^ err); |
|
145 |
*) |
|
146 |
||
147 |
(* ------------------------------------------------------------------------- *) |
|
148 |
(* A conversion takes a term t and either: *) |
|
149 |
(* 1. Returns a term u together with a theorem (stronger than) t = u \/ C. *) |
|
150 |
(* 2. Raises an Error exception. *) |
|
151 |
(* ------------------------------------------------------------------------- *) |
|
152 |
||
153 |
type conv = Term.term -> Term.term * Thm.thm; |
|
154 |
||
155 |
fun allConv tm = (tm, Thm.refl tm); |
|
156 |
||
157 |
val noConv : conv = fn _ => raise Error "noConv"; |
|
158 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
159 |
(*MetisDebug |
39348 | 160 |
fun traceConv s conv tm = |
161 |
let |
|
162 |
val res as (tm',th) = conv tm |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
163 |
val () = trace (s ^ ": " ^ Term.toString tm ^ " --> " ^ |
39348 | 164 |
Term.toString tm' ^ " " ^ Thm.toString th ^ "\n") |
165 |
in |
|
166 |
res |
|
167 |
end |
|
168 |
handle Error err => |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
169 |
(trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n"); |
39348 | 170 |
raise Error (s ^ ": " ^ err)); |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
171 |
*) |
39348 | 172 |
|
173 |
fun thenConvTrans tm (tm',th1) (tm'',th2) = |
|
174 |
let |
|
175 |
val eqn1 = ((tm,tm'),th1) |
|
176 |
and eqn2 = ((tm',tm''),th2) |
|
177 |
val (_,th) = transEqn eqn1 eqn2 |
|
178 |
in |
|
179 |
(tm'',th) |
|
180 |
end; |
|
181 |
||
182 |
fun thenConv conv1 conv2 tm = |
|
183 |
let |
|
184 |
val res1 as (tm',_) = conv1 tm |
|
185 |
val res2 = conv2 tm' |
|
186 |
in |
|
187 |
thenConvTrans tm res1 res2 |
|
188 |
end; |
|
189 |
||
190 |
fun orelseConv (conv1 : conv) conv2 tm = conv1 tm handle Error _ => conv2 tm; |
|
191 |
||
192 |
fun tryConv conv = orelseConv conv allConv; |
|
193 |
||
194 |
fun changedConv conv tm = |
|
195 |
let |
|
196 |
val res as (tm',_) = conv tm |
|
197 |
in |
|
198 |
if tm = tm' then raise Error "changedConv" else res |
|
199 |
end; |
|
200 |
||
201 |
fun repeatConv conv tm = tryConv (thenConv conv (repeatConv conv)) tm; |
|
202 |
||
203 |
fun firstConv [] _ = raise Error "firstConv" |
|
204 |
| firstConv [conv] tm = conv tm |
|
205 |
| firstConv (conv :: convs) tm = orelseConv conv (firstConv convs) tm; |
|
206 |
||
207 |
fun everyConv [] tm = allConv tm |
|
208 |
| everyConv [conv] tm = conv tm |
|
209 |
| everyConv (conv :: convs) tm = thenConv conv (everyConv convs) tm; |
|
210 |
||
211 |
fun rewrConv (eqn as ((x,y), eqTh)) path tm = |
|
212 |
if Term.equal x y then allConv tm |
|
213 |
else if null path then (y,eqTh) |
|
214 |
else |
|
215 |
let |
|
216 |
val reflTh = Thm.refl tm |
|
217 |
val reflLit = Thm.destUnit reflTh |
|
218 |
val th = Thm.equality reflLit (1 :: path) y |
|
219 |
val th = Thm.resolve reflLit reflTh th |
|
220 |
val th = |
|
221 |
case equationLiteral eqn of |
|
222 |
NONE => th |
|
223 |
| SOME x_y => Thm.resolve x_y eqTh th |
|
224 |
val tm' = Term.replace tm (path,y) |
|
225 |
in |
|
226 |
(tm',th) |
|
227 |
end; |
|
228 |
||
229 |
(*MetisDebug |
|
230 |
val rewrConv = fn eqn as ((x,y),eqTh) => fn path => fn tm => |
|
231 |
rewrConv eqn path tm |
|
232 |
handle Error err => |
|
233 |
raise Error ("Rule.rewrConv:\nx = " ^ Term.toString x ^ |
|
234 |
"\ny = " ^ Term.toString y ^ |
|
235 |
"\neqTh = " ^ Thm.toString eqTh ^ |
|
236 |
"\npath = " ^ Term.pathToString path ^ |
|
237 |
"\ntm = " ^ Term.toString tm ^ "\n" ^ err); |
|
238 |
*) |
|
239 |
||
240 |
fun pathConv conv path tm = |
|
241 |
let |
|
242 |
val x = Term.subterm tm path |
|
243 |
val (y,th) = conv x |
|
244 |
in |
|
245 |
rewrConv ((x,y),th) path tm |
|
246 |
end; |
|
247 |
||
248 |
fun subtermConv conv i = pathConv conv [i]; |
|
249 |
||
250 |
fun subtermsConv _ (tm as Term.Var _) = allConv tm |
|
251 |
| subtermsConv conv (tm as Term.Fn (_,a)) = |
|
252 |
everyConv (map (subtermConv conv) (interval 0 (length a))) tm; |
|
253 |
||
254 |
(* ------------------------------------------------------------------------- *) |
|
255 |
(* Applying a conversion to every subterm, with some traversal strategy. *) |
|
256 |
(* ------------------------------------------------------------------------- *) |
|
257 |
||
258 |
fun bottomUpConv conv tm = |
|
259 |
thenConv (subtermsConv (bottomUpConv conv)) (repeatConv conv) tm; |
|
260 |
||
261 |
fun topDownConv conv tm = |
|
262 |
thenConv (repeatConv conv) (subtermsConv (topDownConv conv)) tm; |
|
263 |
||
264 |
fun repeatTopDownConv conv = |
|
265 |
let |
|
266 |
fun f tm = thenConv (repeatConv conv) g tm |
|
267 |
and g tm = thenConv (subtermsConv f) h tm |
|
268 |
and h tm = tryConv (thenConv conv f) tm |
|
269 |
in |
|
270 |
f |
|
271 |
end; |
|
272 |
||
273 |
(*MetisDebug |
|
274 |
val repeatTopDownConv = fn conv => fn tm => |
|
275 |
repeatTopDownConv conv tm |
|
276 |
handle Error err => raise Error ("repeatTopDownConv: " ^ err); |
|
277 |
*) |
|
278 |
||
279 |
(* ------------------------------------------------------------------------- *) |
|
280 |
(* A literule (bad pun) takes a literal L and either: *) |
|
281 |
(* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C. *) |
|
282 |
(* 2. Raises an Error exception. *) |
|
283 |
(* ------------------------------------------------------------------------- *) |
|
284 |
||
285 |
type literule = Literal.literal -> Literal.literal * Thm.thm; |
|
286 |
||
287 |
fun allLiterule lit = (lit, Thm.assume lit); |
|
288 |
||
289 |
val noLiterule : literule = fn _ => raise Error "noLiterule"; |
|
290 |
||
291 |
fun thenLiterule literule1 literule2 lit = |
|
292 |
let |
|
293 |
val res1 as (lit',th1) = literule1 lit |
|
294 |
val res2 as (lit'',th2) = literule2 lit' |
|
295 |
in |
|
296 |
if Literal.equal lit lit' then res2 |
|
297 |
else if Literal.equal lit' lit'' then res1 |
|
298 |
else if Literal.equal lit lit'' then allLiterule lit |
|
299 |
else |
|
300 |
(lit'', |
|
301 |
if not (Thm.member lit' th1) then th1 |
|
302 |
else if not (Thm.negateMember lit' th2) then th2 |
|
303 |
else Thm.resolve lit' th1 th2) |
|
304 |
end; |
|
305 |
||
306 |
fun orelseLiterule (literule1 : literule) literule2 lit = |
|
307 |
literule1 lit handle Error _ => literule2 lit; |
|
308 |
||
309 |
fun tryLiterule literule = orelseLiterule literule allLiterule; |
|
310 |
||
311 |
fun changedLiterule literule lit = |
|
312 |
let |
|
313 |
val res as (lit',_) = literule lit |
|
314 |
in |
|
315 |
if lit = lit' then raise Error "changedLiterule" else res |
|
316 |
end; |
|
317 |
||
318 |
fun repeatLiterule literule lit = |
|
319 |
tryLiterule (thenLiterule literule (repeatLiterule literule)) lit; |
|
320 |
||
321 |
fun firstLiterule [] _ = raise Error "firstLiterule" |
|
322 |
| firstLiterule [literule] lit = literule lit |
|
323 |
| firstLiterule (literule :: literules) lit = |
|
324 |
orelseLiterule literule (firstLiterule literules) lit; |
|
325 |
||
326 |
fun everyLiterule [] lit = allLiterule lit |
|
327 |
| everyLiterule [literule] lit = literule lit |
|
328 |
| everyLiterule (literule :: literules) lit = |
|
329 |
thenLiterule literule (everyLiterule literules) lit; |
|
330 |
||
331 |
fun rewrLiterule (eqn as ((x,y),eqTh)) path lit = |
|
332 |
if Term.equal x y then allLiterule lit |
|
333 |
else |
|
334 |
let |
|
335 |
val th = Thm.equality lit path y |
|
336 |
val th = |
|
337 |
case equationLiteral eqn of |
|
338 |
NONE => th |
|
339 |
| SOME x_y => Thm.resolve x_y eqTh th |
|
340 |
val lit' = Literal.replace lit (path,y) |
|
341 |
in |
|
342 |
(lit',th) |
|
343 |
end; |
|
344 |
||
345 |
(*MetisDebug |
|
346 |
val rewrLiterule = fn eqn => fn path => fn lit => |
|
347 |
rewrLiterule eqn path lit |
|
348 |
handle Error err => |
|
349 |
raise Error ("Rule.rewrLiterule:\neqn = " ^ equationToString eqn ^ |
|
350 |
"\npath = " ^ Term.pathToString path ^ |
|
351 |
"\nlit = " ^ Literal.toString lit ^ "\n" ^ err); |
|
352 |
*) |
|
353 |
||
354 |
fun pathLiterule conv path lit = |
|
355 |
let |
|
356 |
val tm = Literal.subterm lit path |
|
357 |
val (tm',th) = conv tm |
|
358 |
in |
|
359 |
rewrLiterule ((tm,tm'),th) path lit |
|
360 |
end; |
|
361 |
||
362 |
fun argumentLiterule conv i = pathLiterule conv [i]; |
|
363 |
||
364 |
fun allArgumentsLiterule conv lit = |
|
365 |
everyLiterule |
|
366 |
(map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit; |
|
367 |
||
368 |
(* ------------------------------------------------------------------------- *) |
|
369 |
(* A rule takes one theorem and either deduces another or raises an Error *) |
|
370 |
(* exception. *) |
|
371 |
(* ------------------------------------------------------------------------- *) |
|
372 |
||
373 |
type rule = Thm.thm -> Thm.thm; |
|
374 |
||
375 |
val allRule : rule = fn th => th; |
|
376 |
||
377 |
val noRule : rule = fn _ => raise Error "noRule"; |
|
378 |
||
379 |
fun thenRule (rule1 : rule) (rule2 : rule) th = rule1 (rule2 th); |
|
380 |
||
381 |
fun orelseRule (rule1 : rule) rule2 th = rule1 th handle Error _ => rule2 th; |
|
382 |
||
383 |
fun tryRule rule = orelseRule rule allRule; |
|
384 |
||
385 |
fun changedRule rule th = |
|
386 |
let |
|
387 |
val th' = rule th |
|
388 |
in |
|
389 |
if not (LiteralSet.equal (Thm.clause th) (Thm.clause th')) then th' |
|
390 |
else raise Error "changedRule" |
|
391 |
end; |
|
392 |
||
393 |
fun repeatRule rule lit = tryRule (thenRule rule (repeatRule rule)) lit; |
|
394 |
||
395 |
fun firstRule [] _ = raise Error "firstRule" |
|
396 |
| firstRule [rule] th = rule th |
|
397 |
| firstRule (rule :: rules) th = orelseRule rule (firstRule rules) th; |
|
398 |
||
399 |
fun everyRule [] th = allRule th |
|
400 |
| everyRule [rule] th = rule th |
|
401 |
| everyRule (rule :: rules) th = thenRule rule (everyRule rules) th; |
|
402 |
||
403 |
fun literalRule literule lit th = |
|
404 |
let |
|
405 |
val (lit',litTh) = literule lit |
|
406 |
in |
|
407 |
if Literal.equal lit lit' then th |
|
408 |
else if not (Thm.negateMember lit litTh) then litTh |
|
409 |
else Thm.resolve lit th litTh |
|
410 |
end; |
|
411 |
||
412 |
(*MetisDebug |
|
413 |
val literalRule = fn literule => fn lit => fn th => |
|
414 |
literalRule literule lit th |
|
415 |
handle Error err => |
|
416 |
raise Error ("Rule.literalRule:\nlit = " ^ Literal.toString lit ^ |
|
417 |
"\nth = " ^ Thm.toString th ^ "\n" ^ err); |
|
418 |
*) |
|
419 |
||
420 |
fun rewrRule eqTh lit path = literalRule (rewrLiterule eqTh path) lit; |
|
421 |
||
422 |
fun pathRule conv lit path = literalRule (pathLiterule conv path) lit; |
|
423 |
||
424 |
fun literalsRule literule = |
|
425 |
let |
|
426 |
fun f (lit,th) = |
|
427 |
if Thm.member lit th then literalRule literule lit th else th |
|
428 |
in |
|
429 |
fn lits => fn th => LiteralSet.foldl f th lits |
|
430 |
end; |
|
431 |
||
432 |
fun allLiteralsRule literule th = literalsRule literule (Thm.clause th) th; |
|
433 |
||
434 |
fun convRule conv = allLiteralsRule (allArgumentsLiterule conv); |
|
435 |
||
436 |
(* ------------------------------------------------------------------------- *) |
|
437 |
(* *) |
|
438 |
(* ---------------------------------------------- functionCongruence (f,n) *) |
|
439 |
(* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) |
|
440 |
(* f x0 ... x{n-1} = f y0 ... y{n-1} *) |
|
441 |
(* ------------------------------------------------------------------------- *) |
|
442 |
||
443 |
fun functionCongruence (f,n) = |
|
444 |
let |
|
445 |
val xs = List.tabulate (n,xIVar) |
|
446 |
and ys = List.tabulate (n,yIVar) |
|
447 |
||
448 |
fun cong ((i,yi),(th,lit)) = |
|
449 |
let |
|
450 |
val path = [1,i] |
|
451 |
val th = Thm.resolve lit th (Thm.equality lit path yi) |
|
452 |
val lit = Literal.replace lit (path,yi) |
|
453 |
in |
|
454 |
(th,lit) |
|
455 |
end |
|
456 |
||
457 |
val reflTh = Thm.refl (Term.Fn (f,xs)) |
|
458 |
val reflLit = Thm.destUnit reflTh |
|
459 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
460 |
fst (List.foldl cong (reflTh,reflLit) (enumerate ys)) |
39348 | 461 |
end; |
462 |
||
463 |
(* ------------------------------------------------------------------------- *) |
|
464 |
(* *) |
|
465 |
(* ---------------------------------------------- relationCongruence (R,n) *) |
|
466 |
(* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) |
|
467 |
(* ~R x0 ... x{n-1} \/ R y0 ... y{n-1} *) |
|
468 |
(* ------------------------------------------------------------------------- *) |
|
469 |
||
470 |
fun relationCongruence (R,n) = |
|
471 |
let |
|
472 |
val xs = List.tabulate (n,xIVar) |
|
473 |
and ys = List.tabulate (n,yIVar) |
|
474 |
||
475 |
fun cong ((i,yi),(th,lit)) = |
|
476 |
let |
|
477 |
val path = [i] |
|
478 |
val th = Thm.resolve lit th (Thm.equality lit path yi) |
|
479 |
val lit = Literal.replace lit (path,yi) |
|
480 |
in |
|
481 |
(th,lit) |
|
482 |
end |
|
483 |
||
484 |
val assumeLit = (false,(R,xs)) |
|
485 |
val assumeTh = Thm.assume assumeLit |
|
486 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
487 |
fst (List.foldl cong (assumeTh,assumeLit) (enumerate ys)) |
39348 | 488 |
end; |
489 |
||
490 |
(* ------------------------------------------------------------------------- *) |
|
491 |
(* ~(x = y) \/ C *) |
|
492 |
(* ----------------- symNeq ~(x = y) *) |
|
493 |
(* ~(y = x) \/ C *) |
|
494 |
(* ------------------------------------------------------------------------- *) |
|
495 |
||
496 |
fun symNeq lit th = |
|
497 |
let |
|
498 |
val (x,y) = Literal.destNeq lit |
|
499 |
in |
|
500 |
if Term.equal x y then th |
|
501 |
else |
|
502 |
let |
|
503 |
val sub = Subst.fromList [(xVarName,y),(yVarName,x)] |
|
504 |
val symTh = Thm.subst sub symmetry |
|
505 |
in |
|
506 |
Thm.resolve lit th symTh |
|
507 |
end |
|
508 |
end; |
|
509 |
||
510 |
(* ------------------------------------------------------------------------- *) |
|
511 |
(* sym (x = y) = symEq (x = y) /\ sym ~(x = y) = symNeq ~(x = y) *) |
|
512 |
(* ------------------------------------------------------------------------- *) |
|
513 |
||
514 |
fun sym (lit as (pol,_)) th = if pol then symEq lit th else symNeq lit th; |
|
515 |
||
516 |
(* ------------------------------------------------------------------------- *) |
|
517 |
(* ~(x = x) \/ C *) |
|
518 |
(* ----------------- removeIrrefl *) |
|
519 |
(* C *) |
|
520 |
(* *) |
|
521 |
(* where all irreflexive equalities. *) |
|
522 |
(* ------------------------------------------------------------------------- *) |
|
523 |
||
524 |
local |
|
525 |
fun irrefl ((true,_),th) = th |
|
526 |
| irrefl (lit as (false,atm), th) = |
|
527 |
case total Atom.destRefl atm of |
|
528 |
SOME x => Thm.resolve lit th (Thm.refl x) |
|
529 |
| NONE => th; |
|
530 |
in |
|
531 |
fun removeIrrefl th = LiteralSet.foldl irrefl th (Thm.clause th); |
|
532 |
end; |
|
533 |
||
534 |
(* ------------------------------------------------------------------------- *) |
|
535 |
(* x = y \/ y = x \/ C *) |
|
536 |
(* ----------------------- removeSym *) |
|
537 |
(* x = y \/ C *) |
|
538 |
(* *) |
|
539 |
(* where all duplicate copies of equalities and disequalities are removed. *) |
|
540 |
(* ------------------------------------------------------------------------- *) |
|
541 |
||
542 |
local |
|
543 |
fun rem (lit as (pol,atm), eqs_th as (eqs,th)) = |
|
544 |
case total Atom.sym atm of |
|
545 |
NONE => eqs_th |
|
546 |
| SOME atm' => |
|
547 |
if LiteralSet.member lit eqs then |
|
548 |
(eqs, if pol then symEq lit th else symNeq lit th) |
|
549 |
else |
|
550 |
(LiteralSet.add eqs (pol,atm'), th); |
|
551 |
in |
|
552 |
fun removeSym th = |
|
553 |
snd (LiteralSet.foldl rem (LiteralSet.empty,th) (Thm.clause th)); |
|
554 |
end; |
|
555 |
||
556 |
(* ------------------------------------------------------------------------- *) |
|
557 |
(* ~(v = t) \/ C *) |
|
558 |
(* ----------------- expandAbbrevs *) |
|
559 |
(* C[t/v] *) |
|
560 |
(* *) |
|
561 |
(* where t must not contain any occurrence of the variable v. *) |
|
562 |
(* ------------------------------------------------------------------------- *) |
|
563 |
||
564 |
local |
|
565 |
fun expand lit = |
|
566 |
let |
|
567 |
val (x,y) = Literal.destNeq lit |
|
568 |
val _ = Term.isTypedVar x orelse Term.isTypedVar y orelse |
|
569 |
raise Error "Rule.expandAbbrevs: no vars" |
|
570 |
val _ = not (Term.equal x y) orelse |
|
571 |
raise Error "Rule.expandAbbrevs: equal vars" |
|
572 |
in |
|
573 |
Subst.unify Subst.empty x y |
|
574 |
end; |
|
575 |
in |
|
576 |
fun expandAbbrevs th = |
|
577 |
case LiteralSet.firstl (total expand) (Thm.clause th) of |
|
578 |
NONE => removeIrrefl th |
|
579 |
| SOME sub => expandAbbrevs (Thm.subst sub th); |
|
580 |
end; |
|
581 |
||
582 |
(* ------------------------------------------------------------------------- *) |
|
583 |
(* simplify = isTautology + expandAbbrevs + removeSym *) |
|
584 |
(* ------------------------------------------------------------------------- *) |
|
585 |
||
586 |
fun simplify th = |
|
587 |
if Thm.isTautology th then NONE |
|
588 |
else |
|
589 |
let |
|
590 |
val th' = th |
|
591 |
val th' = expandAbbrevs th' |
|
592 |
val th' = removeSym th' |
|
593 |
in |
|
594 |
if Thm.equal th th' then SOME th else simplify th' |
|
595 |
end; |
|
596 |
||
597 |
(* ------------------------------------------------------------------------- *) |
|
598 |
(* C *) |
|
599 |
(* -------- freshVars *) |
|
600 |
(* C[s] *) |
|
601 |
(* *) |
|
602 |
(* where s is a renaming substitution chosen so that all of the variables in *) |
|
603 |
(* C are replaced by fresh variables. *) |
|
604 |
(* ------------------------------------------------------------------------- *) |
|
605 |
||
606 |
fun freshVars th = Thm.subst (Subst.freshVars (Thm.freeVars th)) th; |
|
607 |
||
608 |
(* ------------------------------------------------------------------------- *) |
|
609 |
(* C *) |
|
610 |
(* ---------------------------- factor *) |
|
611 |
(* C_s_1, C_s_2, ..., C_s_n *) |
|
612 |
(* *) |
|
613 |
(* where each s_i is a substitution that factors C, meaning that the theorem *) |
|
614 |
(* *) |
|
615 |
(* C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C *) |
|
616 |
(* *) |
|
617 |
(* has fewer literals than C. *) |
|
618 |
(* *) |
|
619 |
(* Also, if s is any substitution that factors C, then one of the s_i will *) |
|
620 |
(* result in a theorem C_s_i that strictly subsumes the theorem C_s. *) |
|
621 |
(* ------------------------------------------------------------------------- *) |
|
622 |
||
623 |
local |
|
624 |
datatype edge = |
|
625 |
FactorEdge of Atom.atom * Atom.atom |
|
626 |
| ReflEdge of Term.term * Term.term; |
|
627 |
||
628 |
fun ppEdge (FactorEdge atm_atm') = Print.ppPair Atom.pp Atom.pp atm_atm' |
|
629 |
| ppEdge (ReflEdge tm_tm') = Print.ppPair Term.pp Term.pp tm_tm'; |
|
630 |
||
631 |
datatype joinStatus = |
|
632 |
Joined |
|
633 |
| Joinable of Subst.subst |
|
634 |
| Apart; |
|
635 |
||
636 |
fun joinEdge sub edge = |
|
637 |
let |
|
638 |
val result = |
|
639 |
case edge of |
|
640 |
FactorEdge (atm,atm') => total (Atom.unify sub atm) atm' |
|
641 |
| ReflEdge (tm,tm') => total (Subst.unify sub tm) tm' |
|
642 |
in |
|
643 |
case result of |
|
644 |
NONE => Apart |
|
645 |
| SOME sub' => |
|
646 |
if Portable.pointerEqual (sub,sub') then Joined else Joinable sub' |
|
647 |
end; |
|
648 |
||
649 |
fun updateApart sub = |
|
650 |
let |
|
651 |
fun update acc [] = SOME acc |
|
652 |
| update acc (edge :: edges) = |
|
653 |
case joinEdge sub edge of |
|
654 |
Joined => NONE |
|
655 |
| Joinable _ => update (edge :: acc) edges |
|
656 |
| Apart => update acc edges |
|
657 |
in |
|
658 |
update [] |
|
659 |
end; |
|
660 |
||
661 |
fun addFactorEdge (pol,atm) ((pol',atm'),acc) = |
|
662 |
if pol <> pol' then acc |
|
663 |
else |
|
664 |
let |
|
665 |
val edge = FactorEdge (atm,atm') |
|
666 |
in |
|
667 |
case joinEdge Subst.empty edge of |
|
668 |
Joined => raise Bug "addFactorEdge: joined" |
|
669 |
| Joinable sub => (sub,edge) :: acc |
|
670 |
| Apart => acc |
|
671 |
end; |
|
672 |
||
673 |
fun addReflEdge (false,_) acc = acc |
|
674 |
| addReflEdge (true,atm) acc = |
|
675 |
let |
|
676 |
val edge = ReflEdge (Atom.destEq atm) |
|
677 |
in |
|
678 |
case joinEdge Subst.empty edge of |
|
679 |
Joined => raise Bug "addRefl: joined" |
|
680 |
| Joinable _ => edge :: acc |
|
681 |
| Apart => acc |
|
682 |
end; |
|
683 |
||
684 |
fun addIrreflEdge (true,_) acc = acc |
|
685 |
| addIrreflEdge (false,atm) acc = |
|
686 |
let |
|
687 |
val edge = ReflEdge (Atom.destEq atm) |
|
688 |
in |
|
689 |
case joinEdge Subst.empty edge of |
|
690 |
Joined => raise Bug "addRefl: joined" |
|
691 |
| Joinable sub => (sub,edge) :: acc |
|
692 |
| Apart => acc |
|
693 |
end; |
|
694 |
||
695 |
fun init_edges acc _ [] = |
|
696 |
let |
|
697 |
fun init ((apart,sub,edge),(edges,acc)) = |
|
698 |
(edge :: edges, (apart,sub,edges) :: acc) |
|
699 |
in |
|
700 |
snd (List.foldl init ([],[]) acc) |
|
701 |
end |
|
702 |
| init_edges acc apart ((sub,edge) :: sub_edges) = |
|
703 |
let |
|
704 |
(*MetisDebug |
|
705 |
val () = if not (Subst.null sub) then () |
|
706 |
else raise Bug "Rule.factor.init_edges: empty subst" |
|
707 |
*) |
|
708 |
val (acc,apart) = |
|
709 |
case updateApart sub apart of |
|
710 |
SOME apart' => ((apart',sub,edge) :: acc, edge :: apart) |
|
711 |
| NONE => (acc,apart) |
|
712 |
in |
|
713 |
init_edges acc apart sub_edges |
|
714 |
end; |
|
715 |
||
716 |
fun mk_edges apart sub_edges [] = init_edges [] apart sub_edges |
|
717 |
| mk_edges apart sub_edges (lit :: lits) = |
|
718 |
let |
|
719 |
val sub_edges = List.foldl (addFactorEdge lit) sub_edges lits |
|
720 |
||
721 |
val (apart,sub_edges) = |
|
722 |
case total Literal.sym lit of |
|
723 |
NONE => (apart,sub_edges) |
|
724 |
| SOME lit' => |
|
725 |
let |
|
726 |
val apart = addReflEdge lit apart |
|
727 |
val sub_edges = addIrreflEdge lit sub_edges |
|
728 |
val sub_edges = List.foldl (addFactorEdge lit') sub_edges lits |
|
729 |
in |
|
730 |
(apart,sub_edges) |
|
731 |
end |
|
732 |
in |
|
733 |
mk_edges apart sub_edges lits |
|
734 |
end; |
|
735 |
||
736 |
fun fact acc [] = acc |
|
737 |
| fact acc ((_,sub,[]) :: others) = fact (sub :: acc) others |
|
738 |
| fact acc ((apart, sub, edge :: edges) :: others) = |
|
739 |
let |
|
740 |
val others = |
|
741 |
case joinEdge sub edge of |
|
742 |
Joinable sub' => |
|
743 |
let |
|
744 |
val others = (edge :: apart, sub, edges) :: others |
|
745 |
in |
|
746 |
case updateApart sub' apart of |
|
747 |
NONE => others |
|
748 |
| SOME apart' => (apart',sub',edges) :: others |
|
749 |
end |
|
750 |
| _ => (apart,sub,edges) :: others |
|
751 |
in |
|
752 |
fact acc others |
|
753 |
end; |
|
754 |
in |
|
755 |
fun factor' cl = |
|
756 |
let |
|
757 |
(*MetisTrace6 |
|
758 |
val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl |
|
759 |
*) |
|
760 |
val edges = mk_edges [] [] (LiteralSet.toList cl) |
|
761 |
(*MetisTrace6 |
|
762 |
val ppEdgesSize = Print.ppMap length Print.ppInt |
|
763 |
val ppEdgel = Print.ppList ppEdge |
|
764 |
val ppEdges = Print.ppList (Print.ppTriple ppEdgel Subst.pp ppEdgel) |
|
765 |
val () = Print.trace ppEdgesSize "Rule.factor': |edges|" edges |
|
766 |
val () = Print.trace ppEdges "Rule.factor': edges" edges |
|
767 |
*) |
|
768 |
val result = fact [] edges |
|
769 |
(*MetisTrace6 |
|
770 |
val ppResult = Print.ppList Subst.pp |
|
771 |
val () = Print.trace ppResult "Rule.factor': result" result |
|
772 |
*) |
|
773 |
in |
|
774 |
result |
|
775 |
end; |
|
776 |
end; |
|
777 |
||
778 |
fun factor th = |
|
779 |
let |
|
780 |
fun fact sub = removeSym (Thm.subst sub th) |
|
781 |
in |
|
782 |
map fact (factor' (Thm.clause th)) |
|
783 |
end; |
|
784 |
||
785 |
end |