1(* ========================================================================= *) 2(* FIRST ORDER LOGIC FORMULAS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Formula :> Formula = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* A type of first order logic formulas. *) 13(* ------------------------------------------------------------------------- *) 14 15datatype formula = 16 True 17 | False 18 | Atom of Atom.atom 19 | Not of formula 20 | And of formula * formula 21 | Or of formula * formula 22 | Imp of formula * formula 23 | Iff of formula * formula 24 | Forall of Term.var * formula 25 | Exists of Term.var * formula; 26 27(* ------------------------------------------------------------------------- *) 28(* Constructors and destructors. *) 29(* ------------------------------------------------------------------------- *) 30 31(* Booleans *) 32 33fun mkBoolean true = True 34 | mkBoolean false = False; 35 36fun destBoolean True = true 37 | destBoolean False = false 38 | destBoolean _ = raise Error "destBoolean"; 39 40val isBoolean = can destBoolean; 41 42fun isTrue fm = 43 case fm of 44 True => true 45 | _ => false; 46 47fun isFalse fm = 48 case fm of 49 False => true 50 | _ => false; 51 52(* Functions *) 53 54local 55 fun funcs fs [] = fs 56 | funcs fs (True :: fms) = funcs fs fms 57 | funcs fs (False :: fms) = funcs fs fms 58 | funcs fs (Atom atm :: fms) = 59 funcs (NameAritySet.union (Atom.functions atm) fs) fms 60 | funcs fs (Not p :: fms) = funcs fs (p :: fms) 61 | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms) 62 | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms) 63 | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms) 64 | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms) 65 | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms) 66 | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms); 67in 68 fun functions fm = funcs NameAritySet.empty [fm]; 69end; 70 71local 72 fun funcs fs [] = fs 73 | funcs fs (True :: fms) = funcs fs fms 74 | funcs fs (False :: fms) = funcs fs fms 75 | funcs fs (Atom atm :: fms) = 76 funcs (NameSet.union (Atom.functionNames atm) fs) fms 77 | funcs fs (Not p :: fms) = funcs fs (p :: fms) 78 | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms) 79 | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms) 80 | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms) 81 | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms) 82 | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms) 83 | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms); 84in 85 fun functionNames fm = funcs NameSet.empty [fm]; 86end; 87 88(* Relations *) 89 90local 91 fun rels fs [] = fs 92 | rels fs (True :: fms) = rels fs fms 93 | rels fs (False :: fms) = rels fs fms 94 | rels fs (Atom atm :: fms) = 95 rels (NameAritySet.add fs (Atom.relation atm)) fms 96 | rels fs (Not p :: fms) = rels fs (p :: fms) 97 | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms) 98 | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms) 99 | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms) 100 | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms) 101 | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms) 102 | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms); 103in 104 fun relations fm = rels NameAritySet.empty [fm]; 105end; 106 107local 108 fun rels fs [] = fs 109 | rels fs (True :: fms) = rels fs fms 110 | rels fs (False :: fms) = rels fs fms 111 | rels fs (Atom atm :: fms) = rels (NameSet.add fs (Atom.name atm)) fms 112 | rels fs (Not p :: fms) = rels fs (p :: fms) 113 | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms) 114 | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms) 115 | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms) 116 | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms) 117 | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms) 118 | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms); 119in 120 fun relationNames fm = rels NameSet.empty [fm]; 121end; 122 123(* Atoms *) 124 125fun destAtom (Atom atm) = atm 126 | destAtom _ = raise Error "Formula.destAtom"; 127 128val isAtom = can destAtom; 129 130(* Negations *) 131 132fun destNeg (Not p) = p 133 | destNeg _ = raise Error "Formula.destNeg"; 134 135val isNeg = can destNeg; 136 137val stripNeg = 138 let 139 fun strip n (Not fm) = strip (n + 1) fm 140 | strip n fm = (n,fm) 141 in 142 strip 0 143 end; 144 145(* Conjunctions *) 146 147fun listMkConj fms = 148 case List.rev fms of [] => True | fm :: fms => List.foldl And fm fms; 149 150local 151 fun strip cs (And (p,q)) = strip (p :: cs) q 152 | strip cs fm = List.rev (fm :: cs); 153in 154 fun stripConj True = [] 155 | stripConj fm = strip [] fm; 156end; 157 158val flattenConj = 159 let 160 fun flat acc [] = acc 161 | flat acc (And (p,q) :: fms) = flat acc (q :: p :: fms) 162 | flat acc (True :: fms) = flat acc fms 163 | flat acc (fm :: fms) = flat (fm :: acc) fms 164 in 165 fn fm => flat [] [fm] 166 end; 167 168(* Disjunctions *) 169 170fun listMkDisj fms = 171 case List.rev fms of [] => False | fm :: fms => List.foldl Or fm fms; 172 173local 174 fun strip cs (Or (p,q)) = strip (p :: cs) q 175 | strip cs fm = List.rev (fm :: cs); 176in 177 fun stripDisj False = [] 178 | stripDisj fm = strip [] fm; 179end; 180 181val flattenDisj = 182 let 183 fun flat acc [] = acc 184 | flat acc (Or (p,q) :: fms) = flat acc (q :: p :: fms) 185 | flat acc (False :: fms) = flat acc fms 186 | flat acc (fm :: fms) = flat (fm :: acc) fms 187 in 188 fn fm => flat [] [fm] 189 end; 190 191(* Equivalences *) 192 193fun listMkEquiv fms = 194 case List.rev fms of [] => True | fm :: fms => List.foldl Iff fm fms; 195 196local 197 fun strip cs (Iff (p,q)) = strip (p :: cs) q 198 | strip cs fm = List.rev (fm :: cs); 199in 200 fun stripEquiv True = [] 201 | stripEquiv fm = strip [] fm; 202end; 203 204val flattenEquiv = 205 let 206 fun flat acc [] = acc 207 | flat acc (Iff (p,q) :: fms) = flat acc (q :: p :: fms) 208 | flat acc (True :: fms) = flat acc fms 209 | flat acc (fm :: fms) = flat (fm :: acc) fms 210 in 211 fn fm => flat [] [fm] 212 end; 213 214(* Universal quantifiers *) 215 216fun destForall (Forall v_f) = v_f 217 | destForall _ = raise Error "destForall"; 218 219val isForall = can destForall; 220 221fun listMkForall ([],body) = body 222 | listMkForall (v :: vs, body) = Forall (v, listMkForall (vs,body)); 223 224fun setMkForall (vs,body) = NameSet.foldr Forall body vs; 225 226local 227 fun strip vs (Forall (v,b)) = strip (v :: vs) b 228 | strip vs tm = (List.rev vs, tm); 229in 230 val stripForall = strip []; 231end; 232 233(* Existential quantifiers *) 234 235fun destExists (Exists v_f) = v_f 236 | destExists _ = raise Error "destExists"; 237 238val isExists = can destExists; 239 240fun listMkExists ([],body) = body 241 | listMkExists (v :: vs, body) = Exists (v, listMkExists (vs,body)); 242 243fun setMkExists (vs,body) = NameSet.foldr Exists body vs; 244 245local 246 fun strip vs (Exists (v,b)) = strip (v :: vs) b 247 | strip vs tm = (List.rev vs, tm); 248in 249 val stripExists = strip []; 250end; 251 252(* ------------------------------------------------------------------------- *) 253(* The size of a formula in symbols. *) 254(* ------------------------------------------------------------------------- *) 255 256local 257 fun sz n [] = n 258 | sz n (True :: fms) = sz (n + 1) fms 259 | sz n (False :: fms) = sz (n + 1) fms 260 | sz n (Atom atm :: fms) = sz (n + Atom.symbols atm) fms 261 | sz n (Not p :: fms) = sz (n + 1) (p :: fms) 262 | sz n (And (p,q) :: fms) = sz (n + 1) (p :: q :: fms) 263 | sz n (Or (p,q) :: fms) = sz (n + 1) (p :: q :: fms) 264 | sz n (Imp (p,q) :: fms) = sz (n + 1) (p :: q :: fms) 265 | sz n (Iff (p,q) :: fms) = sz (n + 1) (p :: q :: fms) 266 | sz n (Forall (_,p) :: fms) = sz (n + 1) (p :: fms) 267 | sz n (Exists (_,p) :: fms) = sz (n + 1) (p :: fms); 268in 269 fun symbols fm = sz 0 [fm]; 270end; 271 272(* ------------------------------------------------------------------------- *) 273(* A total comparison function for formulas. *) 274(* ------------------------------------------------------------------------- *) 275 276local 277 fun cmp [] = EQUAL 278 | cmp (f1_f2 :: fs) = 279 if Portable.pointerEqual f1_f2 then cmp fs 280 else 281 case f1_f2 of 282 (True,True) => cmp fs 283 | (True,_) => LESS 284 | (_,True) => GREATER 285 | (False,False) => cmp fs 286 | (False,_) => LESS 287 | (_,False) => GREATER 288 | (Atom atm1, Atom atm2) => 289 (case Atom.compare (atm1,atm2) of 290 LESS => LESS 291 | EQUAL => cmp fs 292 | GREATER => GREATER) 293 | (Atom _, _) => LESS 294 | (_, Atom _) => GREATER 295 | (Not p1, Not p2) => cmp ((p1,p2) :: fs) 296 | (Not _, _) => LESS 297 | (_, Not _) => GREATER 298 | (And (p1,q1), And (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs) 299 | (And _, _) => LESS 300 | (_, And _) => GREATER 301 | (Or (p1,q1), Or (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs) 302 | (Or _, _) => LESS 303 | (_, Or _) => GREATER 304 | (Imp (p1,q1), Imp (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs) 305 | (Imp _, _) => LESS 306 | (_, Imp _) => GREATER 307 | (Iff (p1,q1), Iff (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs) 308 | (Iff _, _) => LESS 309 | (_, Iff _) => GREATER 310 | (Forall (v1,p1), Forall (v2,p2)) => 311 (case Name.compare (v1,v2) of 312 LESS => LESS 313 | EQUAL => cmp ((p1,p2) :: fs) 314 | GREATER => GREATER) 315 | (Forall _, Exists _) => LESS 316 | (Exists _, Forall _) => GREATER 317 | (Exists (v1,p1), Exists (v2,p2)) => 318 (case Name.compare (v1,v2) of 319 LESS => LESS 320 | EQUAL => cmp ((p1,p2) :: fs) 321 | GREATER => GREATER); 322in 323 fun compare fm1_fm2 = cmp [fm1_fm2]; 324end; 325 326fun equal fm1 fm2 = compare (fm1,fm2) = EQUAL; 327 328(* ------------------------------------------------------------------------- *) 329(* Free variables. *) 330(* ------------------------------------------------------------------------- *) 331 332fun freeIn v = 333 let 334 fun f [] = false 335 | f (True :: fms) = f fms 336 | f (False :: fms) = f fms 337 | f (Atom atm :: fms) = Atom.freeIn v atm orelse f fms 338 | f (Not p :: fms) = f (p :: fms) 339 | f (And (p,q) :: fms) = f (p :: q :: fms) 340 | f (Or (p,q) :: fms) = f (p :: q :: fms) 341 | f (Imp (p,q) :: fms) = f (p :: q :: fms) 342 | f (Iff (p,q) :: fms) = f (p :: q :: fms) 343 | f (Forall (w,p) :: fms) = 344 if Name.equal v w then f fms else f (p :: fms) 345 | f (Exists (w,p) :: fms) = 346 if Name.equal v w then f fms else f (p :: fms) 347 in 348 fn fm => f [fm] 349 end; 350 351local 352 fun fv vs [] = vs 353 | fv vs ((_,True) :: fms) = fv vs fms 354 | fv vs ((_,False) :: fms) = fv vs fms 355 | fv vs ((bv, Atom atm) :: fms) = 356 fv (NameSet.union vs (NameSet.difference (Atom.freeVars atm) bv)) fms 357 | fv vs ((bv, Not p) :: fms) = fv vs ((bv,p) :: fms) 358 | fv vs ((bv, And (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms) 359 | fv vs ((bv, Or (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms) 360 | fv vs ((bv, Imp (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms) 361 | fv vs ((bv, Iff (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms) 362 | fv vs ((bv, Forall (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms) 363 | fv vs ((bv, Exists (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms); 364 365 fun add (fm,vs) = fv vs [(NameSet.empty,fm)]; 366in 367 fun freeVars fm = add (fm,NameSet.empty); 368 369 fun freeVarsList fms = List.foldl add NameSet.empty fms; 370end; 371 372fun specialize fm = snd (stripForall fm); 373 374fun generalize fm = listMkForall (NameSet.toList (freeVars fm), fm); 375 376(* ------------------------------------------------------------------------- *) 377(* Substitutions. *) 378(* ------------------------------------------------------------------------- *) 379 380local 381 fun substCheck sub fm = if Subst.null sub then fm else substFm sub fm 382 383 and substFm sub fm = 384 case fm of 385 True => fm 386 | False => fm 387 | Atom (p,tms) => 388 let 389 val tms' = Sharing.map (Subst.subst sub) tms 390 in 391 if Portable.pointerEqual (tms,tms') then fm else Atom (p,tms') 392 end 393 | Not p => 394 let 395 val p' = substFm sub p 396 in 397 if Portable.pointerEqual (p,p') then fm else Not p' 398 end 399 | And (p,q) => substConn sub fm And p q 400 | Or (p,q) => substConn sub fm Or p q 401 | Imp (p,q) => substConn sub fm Imp p q 402 | Iff (p,q) => substConn sub fm Iff p q 403 | Forall (v,p) => substQuant sub fm Forall v p 404 | Exists (v,p) => substQuant sub fm Exists v p 405 406 and substConn sub fm conn p q = 407 let 408 val p' = substFm sub p 409 and q' = substFm sub q 410 in 411 if Portable.pointerEqual (p,p') andalso 412 Portable.pointerEqual (q,q') 413 then fm 414 else conn (p',q') 415 end 416 417 and substQuant sub fm quant v p = 418 let 419 val v' = 420 let 421 fun f (w,s) = 422 if Name.equal w v then s 423 else 424 case Subst.peek sub w of 425 NONE => NameSet.add s w 426 | SOME tm => NameSet.union s (Term.freeVars tm) 427 428 val vars = freeVars p 429 val vars = NameSet.foldl f NameSet.empty vars 430 in 431 Term.variantPrime vars v 432 end 433 434 val sub = 435 if Name.equal v v' then Subst.remove sub (NameSet.singleton v) 436 else Subst.insert sub (v, Term.Var v') 437 438 val p' = substCheck sub p 439 in 440 if Name.equal v v' andalso Portable.pointerEqual (p,p') then fm 441 else quant (v',p') 442 end; 443in 444 val subst = substCheck; 445end; 446 447(* ------------------------------------------------------------------------- *) 448(* The equality relation. *) 449(* ------------------------------------------------------------------------- *) 450 451fun mkEq a_b = Atom (Atom.mkEq a_b); 452 453fun destEq fm = Atom.destEq (destAtom fm); 454 455val isEq = can destEq; 456 457fun mkNeq a_b = Not (mkEq a_b); 458 459fun destNeq (Not fm) = destEq fm 460 | destNeq _ = raise Error "Formula.destNeq"; 461 462val isNeq = can destNeq; 463 464fun mkRefl tm = Atom (Atom.mkRefl tm); 465 466fun destRefl fm = Atom.destRefl (destAtom fm); 467 468val isRefl = can destRefl; 469 470fun sym fm = Atom (Atom.sym (destAtom fm)); 471 472fun lhs fm = fst (destEq fm); 473 474fun rhs fm = snd (destEq fm); 475 476(* ------------------------------------------------------------------------- *) 477(* Parsing and pretty-printing. *) 478(* ------------------------------------------------------------------------- *) 479 480type quotation = formula Parse.quotation; 481 482val truthName = Name.fromString "T" 483and falsityName = Name.fromString "F" 484and conjunctionName = Name.fromString "/\\" 485and disjunctionName = Name.fromString "\\/" 486and implicationName = Name.fromString "==>" 487and equivalenceName = Name.fromString "<=>" 488and universalName = Name.fromString "!" 489and existentialName = Name.fromString "?"; 490 491local 492 fun demote True = Term.Fn (truthName,[]) 493 | demote False = Term.Fn (falsityName,[]) 494 | demote (Atom (p,tms)) = Term.Fn (p,tms) 495 | demote (Not p) = 496 let 497 val ref s = Term.negation 498 in 499 Term.Fn (Name.fromString s, [demote p]) 500 end 501 | demote (And (p,q)) = Term.Fn (conjunctionName, [demote p, demote q]) 502 | demote (Or (p,q)) = Term.Fn (disjunctionName, [demote p, demote q]) 503 | demote (Imp (p,q)) = Term.Fn (implicationName, [demote p, demote q]) 504 | demote (Iff (p,q)) = Term.Fn (equivalenceName, [demote p, demote q]) 505 | demote (Forall (v,b)) = Term.Fn (universalName, [Term.Var v, demote b]) 506 | demote (Exists (v,b)) = 507 Term.Fn (existentialName, [Term.Var v, demote b]); 508in 509 fun pp fm = Term.pp (demote fm); 510end; 511 512val toString = Print.toString pp; 513 514local 515 fun isQuant [Term.Var _, _] = true 516 | isQuant _ = false; 517 518 fun promote (Term.Var v) = Atom (v,[]) 519 | promote (Term.Fn (f,tms)) = 520 if Name.equal f truthName andalso List.null tms then 521 True 522 else if Name.equal f falsityName andalso List.null tms then 523 False 524 else if Name.toString f = !Term.negation andalso length tms = 1 then 525 Not (promote (hd tms)) 526 else if Name.equal f conjunctionName andalso length tms = 2 then 527 And (promote (hd tms), promote (List.nth (tms,1))) 528 else if Name.equal f disjunctionName andalso length tms = 2 then 529 Or (promote (hd tms), promote (List.nth (tms,1))) 530 else if Name.equal f implicationName andalso length tms = 2 then 531 Imp (promote (hd tms), promote (List.nth (tms,1))) 532 else if Name.equal f equivalenceName andalso length tms = 2 then 533 Iff (promote (hd tms), promote (List.nth (tms,1))) 534 else if Name.equal f universalName andalso isQuant tms then 535 Forall (Term.destVar (hd tms), promote (List.nth (tms,1))) 536 else if Name.equal f existentialName andalso isQuant tms then 537 Exists (Term.destVar (hd tms), promote (List.nth (tms,1))) 538 else 539 Atom (f,tms); 540in 541 fun fromString s = promote (Term.fromString s); 542end; 543 544val parse = Parse.parseQuotation toString fromString; 545 546(* ------------------------------------------------------------------------- *) 547(* Splitting goals. *) 548(* ------------------------------------------------------------------------- *) 549 550local 551 fun add_asms asms goal = 552 if List.null asms then goal else Imp (listMkConj (List.rev asms), goal); 553 554 fun add_var_asms asms v goal = add_asms asms (Forall (v,goal)); 555 556 fun split asms pol fm = 557 case (pol,fm) of 558 (* Positive splittables *) 559 (true,True) => [] 560 | (true, Not f) => split asms false f 561 | (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2 562 | (true, Or (f1,f2)) => split (Not f1 :: asms) true f2 563 | (true, Imp (f1,f2)) => split (f1 :: asms) true f2 564 | (true, Iff (f1,f2)) => 565 split (f1 :: asms) true f2 @ split (f2 :: asms) true f1 566 | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f) 567 (* Negative splittables *) 568 | (false,False) => [] 569 | (false, Not f) => split asms true f 570 | (false, And (f1,f2)) => split (f1 :: asms) false f2 571 | (false, Or (f1,f2)) => 572 split asms false f1 @ split (Not f1 :: asms) false f2 573 | (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2 574 | (false, Iff (f1,f2)) => 575 split (f1 :: asms) false f2 @ split (f2 :: asms) false f1 576 | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f) 577 (* Unsplittables *) 578 | _ => [add_asms asms (if pol then fm else Not fm)]; 579in 580 fun splitGoal fm = split [] true fm; 581end; 582 583(*MetisTrace3 584val splitGoal = fn fm => 585 let 586 val result = splitGoal fm 587 val () = Print.trace pp "Formula.splitGoal: fm" fm 588 val () = Print.trace (Print.ppList pp) "Formula.splitGoal: result" result 589 in 590 result 591 end; 592*) 593 594end 595 596structure FormulaOrdered = 597struct type t = Formula.formula val compare = Formula.compare end 598 599structure FormulaMap = KeyMap (FormulaOrdered); 600 601structure FormulaSet = ElementSet (FormulaMap); 602