# HG changeset patch # User webertj # Date 1078946876 -3600 # Node ID c24d90dbf0c9d8328ae47a6d4fba9a4ac56719e8 # Parent 2253d273d94480e02d335a868a7d5f93efc20a98 Formulas of propositional logic diff -r 2253d273d944 -r c24d90dbf0c9 src/HOL/Tools/prop_logic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/prop_logic.ML Wed Mar 10 20:27:56 2004 +0100 @@ -0,0 +1,276 @@ +(* Title: HOL/Tools/prop_logic.ML + ID: $Id$ + Author: Tjark Weber + Copyright 2004 + +Formulas of propositional logic. +*) + +signature PROP_LOGIC = +sig + datatype prop_formula = + True + | False + | BoolVar of int (* NOTE: only use indices >= 1 *) + | Not of prop_formula + | Or of prop_formula * prop_formula + | And of prop_formula * prop_formula + + val SNot : prop_formula -> prop_formula + val SOr : prop_formula * prop_formula -> prop_formula + val SAnd : prop_formula * prop_formula -> prop_formula + + val indices : prop_formula -> int list (* all variable indices *) + val maxidx : prop_formula -> int (* maximal variable index *) + + val nnf : prop_formula -> prop_formula (* negation normal form *) + val cnf : prop_formula -> prop_formula (* clause normal form *) + val defcnf : prop_formula -> prop_formula (* definitional cnf *) + + val exists : prop_formula list -> prop_formula (* finite disjunction *) + val all : prop_formula list -> prop_formula (* finite conjunction *) + val dot_product : prop_formula list * prop_formula list -> prop_formula + + val eval : (int -> bool) -> prop_formula -> bool (* semantics *) +end; + +structure PropLogic : PROP_LOGIC = +struct + +(* ------------------------------------------------------------------------- *) +(* prop_formula: formulas of propositional logic, built from boolean *) +(* variables (referred to by index) and True/False using *) +(* not/or/and *) +(* ------------------------------------------------------------------------- *) + + datatype prop_formula = + True + | False + | BoolVar of int (* NOTE: only use indices >= 1 *) + | Not of prop_formula + | Or of prop_formula * prop_formula + | And of prop_formula * prop_formula; + +(* ------------------------------------------------------------------------- *) +(* The following constructor functions make sure that True and False do not *) +(* occur within any of the other connectives (i.e. Not, Or, And), and *) +(* perform double-negation elimination. *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula -> prop_formula *) + + fun SNot True = False + | SNot False = True + | SNot (Not fm) = fm + | SNot fm = Not fm; + + (* prop_formula * prop_formula -> prop_formula *) + + fun SOr (True, _) = True + | SOr (_, True) = True + | SOr (False, fm) = fm + | SOr (fm, False) = fm + | SOr (fm1, fm2) = Or (fm1, fm2); + + (* prop_formula * prop_formula -> prop_formula *) + + fun SAnd (True, fm) = fm + | SAnd (fm, True) = fm + | SAnd (False, _) = False + | SAnd (_, False) = False + | SAnd (fm1, fm2) = And (fm1, fm2); + +(* ------------------------------------------------------------------------- *) +(* indices: collects all indices of boolean variables that occur in a *) +(* propositional formula 'fm'; no duplicates *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula -> int list *) + + fun indices True = [] + | indices False = [] + | indices (BoolVar i) = [i] + | indices (Not fm) = indices fm + | indices (Or (fm1,fm2)) = (indices fm1) union_int (indices fm2) + | indices (And (fm1,fm2)) = (indices fm1) union_int (indices fm2); + +(* ------------------------------------------------------------------------- *) +(* maxidx: computes the maximal variable index occuring in a formula of *) +(* propositional logic 'fm'; 0 if 'fm' contains no variable *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula -> int *) + + fun maxidx True = 0 + | maxidx False = 0 + | maxidx (BoolVar i) = i + | maxidx (Not fm) = maxidx fm + | maxidx (Or (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2) + | maxidx (And (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2); + +(* ------------------------------------------------------------------------- *) +(* nnf: computes the negation normal form of a formula 'fm' of propositional *) +(* logic (i.e. only variables may be negated, but not subformulas) *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula -> prop_formula *) + + fun + (* constants *) + nnf True = True + | nnf False = False + (* variables *) + | nnf (BoolVar i) = BoolVar i + (* 'or' and 'and' as outermost connectives are left untouched *) + | nnf (Or (fm1,fm2)) = SOr (nnf fm1, nnf fm2) + | nnf (And (fm1,fm2)) = SAnd (nnf fm1, nnf fm2) + (* 'not' + constant *) + | nnf (Not True) = False + | nnf (Not False) = True + (* 'not' + variable *) + | nnf (Not (BoolVar i)) = Not (BoolVar i) + (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) + | nnf (Not (Or (fm1,fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2)) + | nnf (Not (And (fm1,fm2))) = SOr (nnf (SNot fm1), nnf (SNot fm2)) + (* double-negation elimination *) + | nnf (Not (Not fm)) = nnf fm; + +(* ------------------------------------------------------------------------- *) +(* cnf: computes the clause normal form (i.e. a conjunction of disjunctions) *) +(* of a formula 'fm' of propositional logic. The result formula may be *) +(* exponentially longer than 'fm'. *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula -> prop_formula *) + + fun cnf fm = + let + fun + (* constants *) + cnf_from_nnf True = True + | cnf_from_nnf False = False + (* literals *) + | cnf_from_nnf (BoolVar i) = BoolVar i + | cnf_from_nnf (Not (BoolVar i)) = Not (BoolVar i) + (* pushing 'or' inside of 'and' using distributive laws *) + | cnf_from_nnf (Or (fm1,fm2)) = + let + val fm1' = cnf_from_nnf fm1 + val fm2' = cnf_from_nnf fm2 + in + case fm1' of + And (fm11,fm12) => cnf_from_nnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2'))) + | _ => + (case fm2' of + And (fm21,fm22) => cnf_from_nnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22))) + (* neither subformula contains 'and' *) + | _ => Or (fm1,fm2)) + end + (* 'and' as outermost connective is left untouched *) + | cnf_from_nnf (And (fm1,fm2)) = SAnd (cnf_from_nnf fm1, cnf_from_nnf fm2) + (* 'not' + something other than a variable: formula is not in negation normal form *) + | cnf_from_nnf _ = raise ERROR + in + (cnf_from_nnf o nnf) fm + end; + +(* ------------------------------------------------------------------------- *) +(* defcnf: computes the definitional clause normal form of a formula 'fm' of *) +(* propositional logic, introducing auxiliary variables if necessary to *) +(* avoid an exponential blowup of the formula. The result formula is *) +(* satisfiable if and only if 'fm' is satisfiable. *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula -> prop_formula *) + + fun defcnf fm = + let + (* prop_formula * int -> prop_formula * int *) + (* 'new' specifies the next index that is available to introduce an auxiliary variable *) + fun + (* constants *) + defcnf_from_nnf (True,new) = (True, new) + | defcnf_from_nnf (False,new) = (False, new) + (* literals *) + | defcnf_from_nnf (BoolVar i,new) = (BoolVar i, new) + | defcnf_from_nnf (Not (BoolVar i),new) = (Not (BoolVar i), new) + (* pushing 'or' inside of 'and' using distributive laws *) + | defcnf_from_nnf (Or (fm1,fm2),new) = + let + val (fm1',new') = defcnf_from_nnf (fm1, new) + val (fm2',new'') = defcnf_from_nnf (fm2, new') + in + case fm1' of + And (fm11,fm12) => + let + val aux = BoolVar new'' + in + (* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *) + defcnf_from_nnf (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fm2', Not aux)), new''+1) + end + | _ => + (case fm2' of + And (fm21,fm22) => + let + val aux = BoolVar new'' + in + (* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *) + defcnf_from_nnf (SAnd (SOr (fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), new''+1) + end + (* neither subformula contains 'and' *) + | _ => (Or (fm1,fm2),new)) + end + (* 'and' as outermost connective is left untouched *) + | defcnf_from_nnf (And (fm1,fm2),new) = + let + val (fm1',new') = defcnf_from_nnf (fm1, new) + val (fm2',new'') = defcnf_from_nnf (fm2, new') + in + (SAnd (fm1', fm2'), new'') + end + (* 'not' + something other than a variable: formula is not in negation normal form *) + | defcnf_from_nnf (_,_) = raise ERROR + in + (fst o defcnf_from_nnf) (nnf fm, (maxidx fm)+1) + end; + +(* ------------------------------------------------------------------------- *) +(* exists: computes the disjunction over a list 'xs' of propositional *) +(* formulas *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula list -> prop_formula *) + + fun exists xs = foldl SOr (False, xs); + +(* ------------------------------------------------------------------------- *) +(* all: computes the conjunction over a list 'xs' of propositional formulas *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula list -> prop_formula *) + + fun all xs = foldl SAnd (True, xs); + +(* ------------------------------------------------------------------------- *) +(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *) +(* ------------------------------------------------------------------------- *) + + (* prop_formula list * prop_formula list -> prop_formula *) + + fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); + +(* ------------------------------------------------------------------------- *) +(* eval: given an assignment 'a' of boolean values to variable indices, the *) +(* truth value of a propositional formula 'fm' is computed *) +(* ------------------------------------------------------------------------- *) + + (* (int -> bool) -> prop_formula -> bool *) + + fun eval a True = true + | eval a False = false + | eval a (BoolVar i) = (a i) + | eval a (Not fm) = not (eval a fm) + | eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2) + | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2); + +end;