1(* ========================================================================= *)
2(* PROOFS IN FIRST ORDER LOGIC                                               *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure Proof :> Proof =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* A type of first order logic proofs.                                       *)
13(* ------------------------------------------------------------------------- *)
14
15datatype 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
23type proof = (Thm.thm * inference) list;
24
25(* ------------------------------------------------------------------------- *)
26(* Printing.                                                                 *)
27(* ------------------------------------------------------------------------- *)
28
29fun 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
36local
37  fun ppAssume atm = Print.sequence Print.break (Atom.pp atm);
38
39  fun ppSubst ppThm (sub,thm) =
40      Print.sequence Print.break
41        (Print.inconsistentBlock 1
42           [Print.ppString "{",
43            Print.ppOp2 " =" Print.ppString Subst.pp ("sub",sub),
44            Print.ppString ",",
45            Print.break,
46            Print.ppOp2 " =" Print.ppString ppThm ("thm",thm),
47            Print.ppString "}"]);
48
49  fun ppResolve ppThm (res,pos,neg) =
50      Print.sequence Print.break
51        (Print.inconsistentBlock 1
52           [Print.ppString "{",
53            Print.ppOp2 " =" Print.ppString Atom.pp ("res",res),
54            Print.ppString ",",
55            Print.break,
56            Print.ppOp2 " =" Print.ppString ppThm ("pos",pos),
57            Print.ppString ",",
58            Print.break,
59            Print.ppOp2 " =" Print.ppString ppThm ("neg",neg),
60            Print.ppString "}"]);
61
62  fun ppRefl tm = Print.sequence Print.break (Term.pp tm);
63
64  fun ppEquality (lit,path,res) =
65      Print.sequence Print.break
66        (Print.inconsistentBlock 1
67           [Print.ppString "{",
68            Print.ppOp2 " =" Print.ppString Literal.pp ("lit",lit),
69            Print.ppString ",",
70            Print.break,
71            Print.ppOp2 " =" Print.ppString Term.ppPath ("path",path),
72            Print.ppString ",",
73            Print.break,
74            Print.ppOp2 " =" Print.ppString Term.pp ("res",res),
75            Print.ppString "}"]);
76
77  fun ppInf ppAxiom ppThm inf =
78      let
79        val infString = Thm.inferenceTypeToString (inferenceType inf)
80      in
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)]
90      end;
91
92  fun ppAxiom cl =
93      Print.sequence
94        Print.break
95        (Print.ppMap
96           LiteralSet.toList
97           (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl);
98in
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 =
108            Print.ppString
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
124                (Print.consistentBlock (1 + size s)
125                   [Print.ppString (s ^ " "),
126                    Thm.pp th,
127                    Print.breaks 2,
128                    Print.ppBracket "[" "]" (ppInf (K Print.skip) ppThm) inf])
129                Print.newline
130            end
131      in
132        Print.consistentBlock 0
133          [Print.ppString "START OF PROOF",
134           Print.newline,
135           Print.program (List.map ppStep prf),
136           Print.ppString "END OF PROOF"]
137      end
138(*MetisDebug
139      handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err);
140*)
141
142end;
143
144val inferenceToString = Print.toString ppInference;
145
146val toString = Print.toString pp;
147
148(* ------------------------------------------------------------------------- *)
149(* Reconstructing single inferences.                                         *)
150(* ------------------------------------------------------------------------- *)
151
152fun parents (Axiom _) = []
153  | parents (Assume _) = []
154  | parents (Subst (_,th)) = [th]
155  | parents (Resolve (_,th,th')) = [th,th']
156  | parents (Refl _) = []
157  | parents (Equality _) = [];
158
159fun 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
166local
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
236                      SOME (List.rev path)
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";
305in
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*)
348end;
349
350(* ------------------------------------------------------------------------- *)
351(* Reconstructing whole proofs.                                              *)
352(* ------------------------------------------------------------------------- *)
353
354local
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
398        List.rev acc
399      end;
400in
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;
414end;
415
416(* ------------------------------------------------------------------------- *)
417(* Free variables.                                                           *)
418(* ------------------------------------------------------------------------- *)
419
420fun 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
435val 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
451end
452