1(* ========================================================================= *)
2(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS                         *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure Thm :> Thm =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* An abstract type of first order logic theorems.                           *)
13(* ------------------------------------------------------------------------- *)
14
15type clause = LiteralSet.set;
16
17datatype inferenceType =
18    Axiom
19  | Assume
20  | Subst
21  | Factor
22  | Resolve
23  | Refl
24  | Equality;
25
26datatype thm = Thm of clause * (inferenceType * thm list);
27
28type inference = inferenceType * thm list;
29
30(* ------------------------------------------------------------------------- *)
31(* Theorem destructors.                                                      *)
32(* ------------------------------------------------------------------------- *)
33
34fun clause (Thm (cl,_)) = cl;
35
36fun inference (Thm (_,inf)) = inf;
37
38(* Tautologies *)
39
40local
41  fun chk (_,NONE) = NONE
42    | chk ((pol,atm), SOME set) =
43      if (pol andalso Atom.isRefl atm) orelse AtomSet.member atm set then NONE
44      else SOME (AtomSet.add set atm);
45in
46  fun isTautology th =
47      case LiteralSet.foldl chk (SOME AtomSet.empty) (clause th) of
48        SOME _ => false
49      | NONE => true;
50end;
51
52(* Contradictions *)
53
54fun isContradiction th = LiteralSet.null (clause th);
55
56(* Unit theorems *)
57
58fun destUnit (Thm (cl,_)) =
59    if LiteralSet.size cl = 1 then LiteralSet.pick cl
60    else raise Error "Thm.destUnit";
61
62val isUnit = can destUnit;
63
64(* Unit equality theorems *)
65
66fun destUnitEq th = Literal.destEq (destUnit th);
67
68val isUnitEq = can destUnitEq;
69
70(* Literals *)
71
72fun member lit (Thm (cl,_)) = LiteralSet.member lit cl;
73
74fun negateMember lit (Thm (cl,_)) = LiteralSet.negateMember lit cl;
75
76(* ------------------------------------------------------------------------- *)
77(* A total order.                                                            *)
78(* ------------------------------------------------------------------------- *)
79
80fun compare (th1,th2) = LiteralSet.compare (clause th1, clause th2);
81
82fun equal th1 th2 = LiteralSet.equal (clause th1) (clause th2);
83
84(* ------------------------------------------------------------------------- *)
85(* Free variables.                                                           *)
86(* ------------------------------------------------------------------------- *)
87
88fun freeIn v (Thm (cl,_)) = LiteralSet.freeIn v cl;
89
90fun freeVars (Thm (cl,_)) = LiteralSet.freeVars cl;
91
92(* ------------------------------------------------------------------------- *)
93(* Pretty-printing.                                                          *)
94(* ------------------------------------------------------------------------- *)
95
96fun inferenceTypeToString Axiom = "Axiom"
97  | inferenceTypeToString Assume = "Assume"
98  | inferenceTypeToString Subst = "Subst"
99  | inferenceTypeToString Factor = "Factor"
100  | inferenceTypeToString Resolve = "Resolve"
101  | inferenceTypeToString Refl = "Refl"
102  | inferenceTypeToString Equality = "Equality";
103
104fun ppInferenceType inf =
105    Print.ppString (inferenceTypeToString inf);
106
107local
108  fun toFormula th =
109      Formula.listMkDisj
110        (List.map Literal.toFormula (LiteralSet.toList (clause th)));
111in
112  fun pp th =
113      Print.inconsistentBlock 3
114        [Print.ppString "|- ",
115         Formula.pp (toFormula th)];
116end;
117
118val toString = Print.toString pp;
119
120(* ------------------------------------------------------------------------- *)
121(* Primitive rules of inference.                                             *)
122(* ------------------------------------------------------------------------- *)
123
124(* ------------------------------------------------------------------------- *)
125(*                                                                           *)
126(* ----- axiom C                                                             *)
127(*   C                                                                       *)
128(* ------------------------------------------------------------------------- *)
129
130fun axiom cl = Thm (cl,(Axiom,[]));
131
132(* ------------------------------------------------------------------------- *)
133(*                                                                           *)
134(* ----------- assume L                                                      *)
135(*   L \/ ~L                                                                 *)
136(* ------------------------------------------------------------------------- *)
137
138fun assume lit =
139    Thm (LiteralSet.fromList [lit, Literal.negate lit], (Assume,[]));
140
141(* ------------------------------------------------------------------------- *)
142(*    C                                                                      *)
143(* -------- subst s                                                          *)
144(*   C[s]                                                                    *)
145(* ------------------------------------------------------------------------- *)
146
147fun subst sub (th as Thm (cl,inf)) =
148    let
149      val cl' = LiteralSet.subst sub cl
150    in
151      if Portable.pointerEqual (cl,cl') then th
152      else
153        case inf of
154          (Subst,_) => Thm (cl',inf)
155        | _ => Thm (cl',(Subst,[th]))
156    end;
157
158(* ------------------------------------------------------------------------- *)
159(*   L \/ C    ~L \/ D                                                       *)
160(* --------------------- resolve L                                           *)
161(*        C \/ D                                                             *)
162(*                                                                           *)
163(* The literal L must occur in the first theorem, and the literal ~L must    *)
164(* occur in the second theorem.                                              *)
165(* ------------------------------------------------------------------------- *)
166
167fun resolve lit (th1 as Thm (cl1,_)) (th2 as Thm (cl2,_)) =
168    let
169      val cl1' = LiteralSet.delete cl1 lit
170      and cl2' = LiteralSet.delete cl2 (Literal.negate lit)
171    in
172      Thm (LiteralSet.union cl1' cl2', (Resolve,[th1,th2]))
173    end;
174
175(*MetisDebug
176val resolve = fn lit => fn pos => fn neg =>
177    resolve lit pos neg
178    handle Error err =>
179      raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
180                   "\npos = " ^ toString pos ^
181                   "\nneg = " ^ toString neg ^ "\n" ^ err);
182*)
183
184(* ------------------------------------------------------------------------- *)
185(*                                                                           *)
186(* --------- refl t                                                          *)
187(*   t = t                                                                   *)
188(* ------------------------------------------------------------------------- *)
189
190fun refl tm = Thm (LiteralSet.singleton (true, Atom.mkRefl tm), (Refl,[]));
191
192(* ------------------------------------------------------------------------- *)
193(*                                                                           *)
194(* ------------------------ equality L p t                                   *)
195(*   ~(s = t) \/ ~L \/ L'                                                    *)
196(*                                                                           *)
197(* where s is the subterm of L at path p, and L' is L with the subterm at    *)
198(* path p being replaced by t.                                               *)
199(* ------------------------------------------------------------------------- *)
200
201fun equality lit path t =
202    let
203      val s = Literal.subterm lit path
204
205      val lit' = Literal.replace lit (path,t)
206
207      val eqLit = Literal.mkNeq (s,t)
208
209      val cl = LiteralSet.fromList [eqLit, Literal.negate lit, lit']
210    in
211      Thm (cl,(Equality,[]))
212    end;
213
214end
215