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