author | desharna |
Thu, 09 Jul 2020 11:39:16 +0200 | |
changeset 72004 | 913162a47d9f |
parent 45778 | df6e210fb44c |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* PROOFS IN FIRST ORDER LOGIC *) |
|
72004 | 3 |
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Proof :> Proof = |
|
7 |
struct |
|
8 |
||
9 |
open Useful; |
|
10 |
||
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
(* A type of first order logic proofs. *) |
|
13 |
(* ------------------------------------------------------------------------- *) |
|
14 |
||
15 |
datatype inference = |
|
16 |
Axiom of LiteralSet.set |
|
17 |
| Assume of Atom.atom |
|
18 |
| Subst of Subst.subst * Thm.thm |
|
19 |
| Resolve of Atom.atom * Thm.thm * Thm.thm |
|
20 |
| Refl of Term.term |
|
21 |
| Equality of Literal.literal * Term.path * Term.term; |
|
22 |
||
23 |
type proof = (Thm.thm * inference) list; |
|
24 |
||
25 |
(* ------------------------------------------------------------------------- *) |
|
26 |
(* Printing. *) |
|
27 |
(* ------------------------------------------------------------------------- *) |
|
28 |
||
29 |
fun inferenceType (Axiom _) = Thm.Axiom |
|
30 |
| inferenceType (Assume _) = Thm.Assume |
|
31 |
| inferenceType (Subst _) = Thm.Subst |
|
32 |
| inferenceType (Resolve _) = Thm.Resolve |
|
33 |
| inferenceType (Refl _) = Thm.Refl |
|
34 |
| inferenceType (Equality _) = Thm.Equality; |
|
35 |
||
36 |
local |
|
45778 | 37 |
fun ppAssume atm = Print.sequence Print.break (Atom.pp atm); |
39348 | 38 |
|
39 |
fun ppSubst ppThm (sub,thm) = |
|
45778 | 40 |
Print.sequence Print.break |
41 |
(Print.inconsistentBlock 1 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
42 |
[Print.ppString "{", |
39348 | 43 |
Print.ppOp2 " =" Print.ppString Subst.pp ("sub",sub), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
44 |
Print.ppString ",", |
45778 | 45 |
Print.break, |
39348 | 46 |
Print.ppOp2 " =" Print.ppString ppThm ("thm",thm), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
47 |
Print.ppString "}"]); |
39348 | 48 |
|
49 |
fun ppResolve ppThm (res,pos,neg) = |
|
45778 | 50 |
Print.sequence Print.break |
51 |
(Print.inconsistentBlock 1 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
52 |
[Print.ppString "{", |
39348 | 53 |
Print.ppOp2 " =" Print.ppString Atom.pp ("res",res), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
54 |
Print.ppString ",", |
45778 | 55 |
Print.break, |
39348 | 56 |
Print.ppOp2 " =" Print.ppString ppThm ("pos",pos), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
57 |
Print.ppString ",", |
45778 | 58 |
Print.break, |
39348 | 59 |
Print.ppOp2 " =" Print.ppString ppThm ("neg",neg), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
60 |
Print.ppString "}"]); |
39348 | 61 |
|
45778 | 62 |
fun ppRefl tm = Print.sequence Print.break (Term.pp tm); |
39348 | 63 |
|
64 |
fun ppEquality (lit,path,res) = |
|
45778 | 65 |
Print.sequence Print.break |
66 |
(Print.inconsistentBlock 1 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
67 |
[Print.ppString "{", |
39348 | 68 |
Print.ppOp2 " =" Print.ppString Literal.pp ("lit",lit), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
69 |
Print.ppString ",", |
45778 | 70 |
Print.break, |
39348 | 71 |
Print.ppOp2 " =" Print.ppString Term.ppPath ("path",path), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
72 |
Print.ppString ",", |
45778 | 73 |
Print.break, |
39348 | 74 |
Print.ppOp2 " =" Print.ppString Term.pp ("res",res), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
75 |
Print.ppString "}"]); |
39348 | 76 |
|
77 |
fun ppInf ppAxiom ppThm inf = |
|
78 |
let |
|
79 |
val infString = Thm.inferenceTypeToString (inferenceType inf) |
|
80 |
in |
|
45778 | 81 |
Print.inconsistentBlock 2 |
82 |
[Print.ppString infString, |
|
83 |
(case inf of |
|
84 |
Axiom cl => ppAxiom cl |
|
85 |
| Assume x => ppAssume x |
|
86 |
| Subst x => ppSubst ppThm x |
|
87 |
| Resolve x => ppResolve ppThm x |
|
88 |
| Refl x => ppRefl x |
|
89 |
| Equality x => ppEquality x)] |
|
39348 | 90 |
end; |
91 |
||
92 |
fun ppAxiom cl = |
|
93 |
Print.sequence |
|
45778 | 94 |
Print.break |
39348 | 95 |
(Print.ppMap |
96 |
LiteralSet.toList |
|
97 |
(Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl); |
|
98 |
in |
|
99 |
val ppInference = ppInf ppAxiom Thm.pp; |
|
100 |
||
101 |
fun pp prf = |
|
102 |
let |
|
103 |
fun thmString n = "(" ^ Int.toString n ^ ")" |
|
104 |
||
105 |
val prf = enumerate prf |
|
106 |
||
107 |
fun ppThm th = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
108 |
Print.ppString |
39348 | 109 |
let |
110 |
val cl = Thm.clause th |
|
111 |
||
112 |
fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl |
|
113 |
in |
|
114 |
case List.find pred prf of |
|
115 |
NONE => "(?)" |
|
116 |
| SOME (n,_) => thmString n |
|
117 |
end |
|
118 |
||
119 |
fun ppStep (n,(th,inf)) = |
|
120 |
let |
|
121 |
val s = thmString n |
|
122 |
in |
|
123 |
Print.sequence |
|
45778 | 124 |
(Print.consistentBlock (1 + size s) |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
125 |
[Print.ppString (s ^ " "), |
39348 | 126 |
Thm.pp th, |
45778 | 127 |
Print.breaks 2, |
39348 | 128 |
Print.ppBracket "[" "]" (ppInf (K Print.skip) ppThm) inf]) |
45778 | 129 |
Print.newline |
39348 | 130 |
end |
131 |
in |
|
45778 | 132 |
Print.consistentBlock 0 |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
133 |
[Print.ppString "START OF PROOF", |
45778 | 134 |
Print.newline, |
42102 | 135 |
Print.program (List.map ppStep prf), |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
136 |
Print.ppString "END OF PROOF"] |
39348 | 137 |
end |
138 |
(*MetisDebug |
|
139 |
handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err); |
|
140 |
*) |
|
141 |
||
142 |
end; |
|
143 |
||
144 |
val inferenceToString = Print.toString ppInference; |
|
145 |
||
146 |
val toString = Print.toString pp; |
|
147 |
||
148 |
(* ------------------------------------------------------------------------- *) |
|
149 |
(* Reconstructing single inferences. *) |
|
150 |
(* ------------------------------------------------------------------------- *) |
|
151 |
||
152 |
fun parents (Axiom _) = [] |
|
153 |
| parents (Assume _) = [] |
|
154 |
| parents (Subst (_,th)) = [th] |
|
155 |
| parents (Resolve (_,th,th')) = [th,th'] |
|
156 |
| parents (Refl _) = [] |
|
157 |
| parents (Equality _) = []; |
|
158 |
||
159 |
fun inferenceToThm (Axiom cl) = Thm.axiom cl |
|
160 |
| inferenceToThm (Assume atm) = Thm.assume (true,atm) |
|
161 |
| inferenceToThm (Subst (sub,th)) = Thm.subst sub th |
|
162 |
| inferenceToThm (Resolve (atm,th,th')) = Thm.resolve (true,atm) th th' |
|
163 |
| inferenceToThm (Refl tm) = Thm.refl tm |
|
164 |
| inferenceToThm (Equality (lit,path,r)) = Thm.equality lit path r; |
|
165 |
||
166 |
local |
|
167 |
fun reconstructSubst cl cl' = |
|
168 |
let |
|
169 |
fun recon [] = |
|
170 |
let |
|
171 |
(*MetisTrace3 |
|
172 |
val () = Print.trace LiteralSet.pp "reconstructSubst: cl" cl |
|
173 |
val () = Print.trace LiteralSet.pp "reconstructSubst: cl'" cl' |
|
174 |
*) |
|
175 |
in |
|
176 |
raise Bug "can't reconstruct Subst rule" |
|
177 |
end |
|
178 |
| recon (([],sub) :: others) = |
|
179 |
if LiteralSet.equal (LiteralSet.subst sub cl) cl' then sub |
|
180 |
else recon others |
|
181 |
| recon ((lit :: lits, sub) :: others) = |
|
182 |
let |
|
183 |
fun checkLit (lit',acc) = |
|
184 |
case total (Literal.match sub lit) lit' of |
|
185 |
NONE => acc |
|
186 |
| SOME sub => (lits,sub) :: acc |
|
187 |
in |
|
188 |
recon (LiteralSet.foldl checkLit others cl') |
|
189 |
end |
|
190 |
in |
|
191 |
Subst.normalize (recon [(LiteralSet.toList cl, Subst.empty)]) |
|
192 |
end |
|
193 |
(*MetisDebug |
|
194 |
handle Error err => |
|
195 |
raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err); |
|
196 |
*) |
|
197 |
||
198 |
fun reconstructResolvant cl1 cl2 cl = |
|
199 |
(if not (LiteralSet.subset cl1 cl) then |
|
200 |
LiteralSet.pick (LiteralSet.difference cl1 cl) |
|
201 |
else if not (LiteralSet.subset cl2 cl) then |
|
202 |
Literal.negate (LiteralSet.pick (LiteralSet.difference cl2 cl)) |
|
203 |
else |
|
204 |
(* A useless resolution, but we must reconstruct it anyway *) |
|
205 |
let |
|
206 |
val cl1' = LiteralSet.negate cl1 |
|
207 |
and cl2' = LiteralSet.negate cl2 |
|
208 |
val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2'] |
|
209 |
in |
|
210 |
if not (LiteralSet.null lits) then LiteralSet.pick lits |
|
211 |
else raise Bug "can't reconstruct Resolve rule" |
|
212 |
end) |
|
213 |
(*MetisDebug |
|
214 |
handle Error err => |
|
215 |
raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err); |
|
216 |
*) |
|
217 |
||
218 |
fun reconstructEquality cl = |
|
219 |
let |
|
220 |
(*MetisTrace3 |
|
221 |
val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl |
|
222 |
*) |
|
223 |
||
224 |
fun sync s t path (f,a) (f',a') = |
|
225 |
if not (Name.equal f f' andalso length a = length a') then NONE |
|
226 |
else |
|
227 |
let |
|
228 |
val itms = enumerate (zip a a') |
|
229 |
in |
|
230 |
case List.filter (not o uncurry Term.equal o snd) itms of |
|
231 |
[(i,(tm,tm'))] => |
|
232 |
let |
|
233 |
val path = i :: path |
|
234 |
in |
|
235 |
if Term.equal tm s andalso Term.equal tm' t then |
|
45778 | 236 |
SOME (List.rev path) |
39348 | 237 |
else |
238 |
case (tm,tm') of |
|
239 |
(Term.Fn f_a, Term.Fn f_a') => sync s t path f_a f_a' |
|
240 |
| _ => NONE |
|
241 |
end |
|
242 |
| _ => NONE |
|
243 |
end |
|
244 |
||
245 |
fun recon (neq,(pol,atm),(pol',atm')) = |
|
246 |
if pol = pol' then NONE |
|
247 |
else |
|
248 |
let |
|
249 |
val (s,t) = Literal.destNeq neq |
|
250 |
||
251 |
val path = |
|
252 |
if not (Term.equal s t) then sync s t [] atm atm' |
|
253 |
else if not (Atom.equal atm atm') then NONE |
|
254 |
else Atom.find (Term.equal s) atm |
|
255 |
in |
|
256 |
case path of |
|
257 |
SOME path => SOME ((pol',atm),path,t) |
|
258 |
| NONE => NONE |
|
259 |
end |
|
260 |
||
261 |
val candidates = |
|
262 |
case List.partition Literal.isNeq (LiteralSet.toList cl) of |
|
263 |
([l1],[l2,l3]) => [(l1,l2,l3),(l1,l3,l2)] |
|
264 |
| ([l1,l2],[l3]) => [(l1,l2,l3),(l1,l3,l2),(l2,l1,l3),(l2,l3,l1)] |
|
265 |
| ([l1],[l2]) => [(l1,l1,l2),(l1,l2,l1)] |
|
266 |
| _ => raise Bug "reconstructEquality: malformed" |
|
267 |
||
268 |
(*MetisTrace3 |
|
269 |
val ppCands = |
|
270 |
Print.ppList (Print.ppTriple Literal.pp Literal.pp Literal.pp) |
|
271 |
val () = Print.trace ppCands |
|
272 |
"Proof.reconstructEquality: candidates" candidates |
|
273 |
*) |
|
274 |
in |
|
275 |
case first recon candidates of |
|
276 |
SOME info => info |
|
277 |
| NONE => raise Bug "can't reconstruct Equality rule" |
|
278 |
end |
|
279 |
(*MetisDebug |
|
280 |
handle Error err => |
|
281 |
raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err); |
|
282 |
*) |
|
283 |
||
284 |
fun reconstruct cl (Thm.Axiom,[]) = Axiom cl |
|
285 |
| reconstruct cl (Thm.Assume,[]) = |
|
286 |
(case LiteralSet.findl Literal.positive cl of |
|
287 |
SOME (_,atm) => Assume atm |
|
288 |
| NONE => raise Bug "malformed Assume inference") |
|
289 |
| reconstruct cl (Thm.Subst,[th]) = |
|
290 |
Subst (reconstructSubst (Thm.clause th) cl, th) |
|
291 |
| reconstruct cl (Thm.Resolve,[th1,th2]) = |
|
292 |
let |
|
293 |
val cl1 = Thm.clause th1 |
|
294 |
and cl2 = Thm.clause th2 |
|
295 |
val (pol,atm) = reconstructResolvant cl1 cl2 cl |
|
296 |
in |
|
297 |
if pol then Resolve (atm,th1,th2) else Resolve (atm,th2,th1) |
|
298 |
end |
|
299 |
| reconstruct cl (Thm.Refl,[]) = |
|
300 |
(case LiteralSet.findl (K true) cl of |
|
301 |
SOME lit => Refl (Literal.destRefl lit) |
|
302 |
| NONE => raise Bug "malformed Refl inference") |
|
303 |
| reconstruct cl (Thm.Equality,[]) = Equality (reconstructEquality cl) |
|
304 |
| reconstruct _ _ = raise Bug "malformed inference"; |
|
305 |
in |
|
306 |
fun thmToInference th = |
|
307 |
let |
|
308 |
(*MetisTrace3 |
|
309 |
val () = Print.trace Thm.pp "Proof.thmToInference: th" th |
|
310 |
*) |
|
311 |
||
312 |
val cl = Thm.clause th |
|
313 |
||
314 |
val thmInf = Thm.inference th |
|
315 |
||
316 |
(*MetisTrace3 |
|
317 |
val ppThmInf = Print.ppPair Thm.ppInferenceType (Print.ppList Thm.pp) |
|
318 |
val () = Print.trace ppThmInf "Proof.thmToInference: thmInf" thmInf |
|
319 |
*) |
|
320 |
||
321 |
val inf = reconstruct cl thmInf |
|
322 |
||
323 |
(*MetisTrace3 |
|
324 |
val () = Print.trace ppInference "Proof.thmToInference: inf" inf |
|
325 |
*) |
|
326 |
(*MetisDebug |
|
327 |
val () = |
|
328 |
let |
|
329 |
val th' = inferenceToThm inf |
|
330 |
in |
|
331 |
if LiteralSet.equal (Thm.clause th') cl then () |
|
332 |
else |
|
333 |
raise |
|
334 |
Bug |
|
335 |
("Proof.thmToInference: bad inference reconstruction:" ^ |
|
336 |
"\n th = " ^ Thm.toString th ^ |
|
337 |
"\n inf = " ^ inferenceToString inf ^ |
|
338 |
"\n inf th = " ^ Thm.toString th') |
|
339 |
end |
|
340 |
*) |
|
341 |
in |
|
342 |
inf |
|
343 |
end |
|
344 |
(*MetisDebug |
|
345 |
handle Error err => |
|
346 |
raise Bug ("Proof.thmToInference: shouldn't fail:\n" ^ err); |
|
347 |
*) |
|
348 |
end; |
|
349 |
||
350 |
(* ------------------------------------------------------------------------- *) |
|
351 |
(* Reconstructing whole proofs. *) |
|
352 |
(* ------------------------------------------------------------------------- *) |
|
353 |
||
354 |
local |
|
355 |
val emptyThms : Thm.thm LiteralSetMap.map = LiteralSetMap.new (); |
|
356 |
||
357 |
fun addThms (th,ths) = |
|
358 |
let |
|
359 |
val cl = Thm.clause th |
|
360 |
in |
|
361 |
if LiteralSetMap.inDomain cl ths then ths |
|
362 |
else |
|
363 |
let |
|
364 |
val (_,pars) = Thm.inference th |
|
365 |
val ths = List.foldl addThms ths pars |
|
366 |
in |
|
367 |
if LiteralSetMap.inDomain cl ths then ths |
|
368 |
else LiteralSetMap.insert ths (cl,th) |
|
369 |
end |
|
370 |
end; |
|
371 |
||
372 |
fun mkThms th = addThms (th,emptyThms); |
|
373 |
||
374 |
fun addProof (th,(ths,acc)) = |
|
375 |
let |
|
376 |
val cl = Thm.clause th |
|
377 |
in |
|
378 |
case LiteralSetMap.peek ths cl of |
|
379 |
NONE => (ths,acc) |
|
380 |
| SOME th => |
|
381 |
let |
|
382 |
val (_,pars) = Thm.inference th |
|
383 |
val (ths,acc) = List.foldl addProof (ths,acc) pars |
|
384 |
val ths = LiteralSetMap.delete ths cl |
|
385 |
val acc = (th, thmToInference th) :: acc |
|
386 |
in |
|
387 |
(ths,acc) |
|
388 |
end |
|
389 |
end; |
|
390 |
||
391 |
fun mkProof ths th = |
|
392 |
let |
|
393 |
val (ths,acc) = addProof (th,(ths,[])) |
|
394 |
(*MetisTrace4 |
|
395 |
val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths) |
|
396 |
*) |
|
397 |
in |
|
45778 | 398 |
List.rev acc |
39348 | 399 |
end; |
400 |
in |
|
401 |
fun proof th = |
|
402 |
let |
|
403 |
(*MetisTrace3 |
|
404 |
val () = Print.trace Thm.pp "Proof.proof: th" th |
|
405 |
*) |
|
406 |
val ths = mkThms th |
|
407 |
val infs = mkProof ths th |
|
408 |
(*MetisTrace3 |
|
409 |
val () = Print.trace Print.ppInt "Proof.proof: size" (length infs) |
|
410 |
*) |
|
411 |
in |
|
412 |
infs |
|
413 |
end; |
|
414 |
end; |
|
415 |
||
416 |
(* ------------------------------------------------------------------------- *) |
|
417 |
(* Free variables. *) |
|
418 |
(* ------------------------------------------------------------------------- *) |
|
419 |
||
420 |
fun freeIn v = |
|
421 |
let |
|
422 |
fun free th_inf = |
|
423 |
case th_inf of |
|
424 |
(_, Axiom lits) => LiteralSet.freeIn v lits |
|
425 |
| (_, Assume atm) => Atom.freeIn v atm |
|
426 |
| (th, Subst _) => Thm.freeIn v th |
|
427 |
| (_, Resolve _) => false |
|
428 |
| (_, Refl tm) => Term.freeIn v tm |
|
429 |
| (_, Equality (lit,_,tm)) => |
|
430 |
Literal.freeIn v lit orelse Term.freeIn v tm |
|
431 |
in |
|
432 |
List.exists free |
|
433 |
end; |
|
434 |
||
435 |
val freeVars = |
|
436 |
let |
|
437 |
fun inc (th_inf,set) = |
|
438 |
NameSet.union set |
|
439 |
(case th_inf of |
|
440 |
(_, Axiom lits) => LiteralSet.freeVars lits |
|
441 |
| (_, Assume atm) => Atom.freeVars atm |
|
442 |
| (th, Subst _) => Thm.freeVars th |
|
443 |
| (_, Resolve _) => NameSet.empty |
|
444 |
| (_, Refl tm) => Term.freeVars tm |
|
445 |
| (_, Equality (lit,_,tm)) => |
|
446 |
NameSet.union (Literal.freeVars lit) (Term.freeVars tm)) |
|
447 |
in |
|
448 |
List.foldl inc NameSet.empty |
|
449 |
end; |
|
450 |
||
451 |
end |