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