(* 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 (* set of 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 (* conjunctive 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);
(* ------------------------------------------------------------------------- *)
(* exception SAME: raised to indicate that the return value of a function is *)
(* identical to its argument (optimization to allow sharing, *)
(* rather than copying) *)
(* ------------------------------------------------------------------------- *)
exception SAME;
(* ------------------------------------------------------------------------- *)
(* 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 conjunctive 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 fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *)
(* pushing 'or' inside of 'and' using distributive laws *)
| cnf_from_nnf (Or (fm1, fm2)) =
let
fun cnf_or (And (fm11, fm12), fm2) =
And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
| cnf_or (fm1, And (fm21, fm22)) =
And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
(* neither subformula contains 'and' *)
| cnf_or (fm1, fm2) =
Or (fm1, fm2)
in
cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
end
(* 'and' as outermost connective is left untouched *)
| cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
in
(cnf_from_nnf o nnf) fm
end;
(* ------------------------------------------------------------------------- *)
(* defcnf: computes the definitional conjunctive 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 fm1, new) = (Not fm1, new) (* 'fm1' must be a variable since the formula is in NNF *)
(* pushing 'or' inside of 'and' using auxiliary variables *)
| defcnf_from_nnf (Or (fm1, fm2), new) =
let
val (fm1', new') = defcnf_from_nnf (fm1, new)
val (fm2', new'') = defcnf_from_nnf (fm2, new')
(* prop_formula * prop_formula -> int -> prop_formula * int *)
fun defcnf_or (And (fm11, fm12), fm2) new =
let
val aux = BoolVar new
val (fm_a, new') = defcnf_or (fm11, aux) (new+1)
val (fm_b, new'') = defcnf_or (fm12, aux) new'
val (fm_c, new''') = defcnf_or (fm2, Not aux) new''
in
(And (And (fm_a, fm_b), fm_c), new''')
end
| defcnf_or (fm1, And (fm21, fm22)) new =
let
val aux = BoolVar new
val (fm_a, new') = defcnf_or (fm1, Not aux) (new+1)
val (fm_b, new'') = defcnf_or (fm21, aux) new'
val (fm_c, new''') = defcnf_or (fm22, aux) new''
in
(And (fm_a, And (fm_b, fm_c)), new''')
end
(* neither subformula contains 'and' *)
| defcnf_or (fm1, fm2) new =
(Or (fm1, fm2), new)
in
defcnf_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
(And (fm1', fm2'), new'')
end
val fm' = nnf fm
in
(fst o defcnf_from_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;