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