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