Formulas of propositional logic
authorwebertj
Wed Mar 10 20:27:56 2004 +0100 (2004-03-10)
changeset 14452c24d90dbf0c9
parent 14451 2253d273d944
child 14453 3397a69dfa4e
Formulas of propositional logic
src/HOL/Tools/prop_logic.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Wed Mar 10 20:27:56 2004 +0100
     1.3 @@ -0,0 +1,276 @@
     1.4 +(*  Title:      HOL/Tools/prop_logic.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tjark Weber
     1.7 +    Copyright   2004
     1.8 +
     1.9 +Formulas of propositional logic.
    1.10 +*)
    1.11 +
    1.12 +signature PROP_LOGIC =
    1.13 +sig
    1.14 +	datatype prop_formula =
    1.15 +		  True
    1.16 +		| False
    1.17 +		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    1.18 +		| Not of prop_formula
    1.19 +		| Or of prop_formula * prop_formula
    1.20 +		| And of prop_formula * prop_formula
    1.21 +
    1.22 +	val SNot : prop_formula -> prop_formula
    1.23 +	val SOr  : prop_formula * prop_formula -> prop_formula
    1.24 +	val SAnd : prop_formula * prop_formula -> prop_formula
    1.25 +
    1.26 +	val indices : prop_formula -> int list  (* all variable indices *)
    1.27 +	val maxidx  : prop_formula -> int  (* maximal variable index *)
    1.28 +
    1.29 +	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    1.30 +	val cnf    : prop_formula -> prop_formula  (* clause normal form *)
    1.31 +	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
    1.32 +
    1.33 +	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
    1.34 +	val all         : prop_formula list -> prop_formula  (* finite conjunction *)
    1.35 +	val dot_product : prop_formula list * prop_formula list -> prop_formula
    1.36 +
    1.37 +	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
    1.38 +end;
    1.39 +
    1.40 +structure PropLogic : PROP_LOGIC =
    1.41 +struct
    1.42 +
    1.43 +(* ------------------------------------------------------------------------- *)
    1.44 +(* prop_formula: formulas of propositional logic, built from boolean         *)
    1.45 +(*               variables (referred to by index) and True/False using       *)
    1.46 +(*               not/or/and                                                  *)
    1.47 +(* ------------------------------------------------------------------------- *)
    1.48 +
    1.49 +	datatype prop_formula =
    1.50 +		  True
    1.51 +		| False
    1.52 +		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    1.53 +		| Not of prop_formula
    1.54 +		| Or of prop_formula * prop_formula
    1.55 +		| And of prop_formula * prop_formula;
    1.56 +
    1.57 +(* ------------------------------------------------------------------------- *)
    1.58 +(* The following constructor functions make sure that True and False do not  *)
    1.59 +(* occur within any of the other connectives (i.e. Not, Or, And), and        *)
    1.60 +(* perform double-negation elimination.                                      *)
    1.61 +(* ------------------------------------------------------------------------- *)
    1.62 +
    1.63 +	(* prop_formula -> prop_formula *)
    1.64 +
    1.65 +	fun SNot True     = False
    1.66 +	  | SNot False    = True
    1.67 +	  | SNot (Not fm) = fm
    1.68 +	  | SNot fm       = Not fm;
    1.69 +
    1.70 +	(* prop_formula * prop_formula -> prop_formula *)
    1.71 +
    1.72 +	fun SOr (True, _)   = True
    1.73 +	  | SOr (_, True)   = True
    1.74 +	  | SOr (False, fm) = fm
    1.75 +	  | SOr (fm, False) = fm
    1.76 +	  | SOr (fm1, fm2)  = Or (fm1, fm2);
    1.77 +
    1.78 +	(* prop_formula * prop_formula -> prop_formula *)
    1.79 +
    1.80 +	fun SAnd (True, fm) = fm
    1.81 +	  | SAnd (fm, True) = fm
    1.82 +	  | SAnd (False, _) = False
    1.83 +	  | SAnd (_, False) = False
    1.84 +	  | SAnd (fm1, fm2) = And (fm1, fm2);
    1.85 +
    1.86 +(* ------------------------------------------------------------------------- *)
    1.87 +(* indices: collects all indices of boolean variables that occur in a        *)
    1.88 +(*      propositional formula 'fm'; no duplicates                            *)
    1.89 +(* ------------------------------------------------------------------------- *)
    1.90 +
    1.91 +	(* prop_formula -> int list *)
    1.92 +
    1.93 +	fun indices True            = []
    1.94 +	  | indices False           = []
    1.95 +	  | indices (BoolVar i)     = [i]
    1.96 +	  | indices (Not fm)        = indices fm
    1.97 +	  | indices (Or (fm1,fm2))  = (indices fm1) union_int (indices fm2)
    1.98 +	  | indices (And (fm1,fm2)) = (indices fm1) union_int (indices fm2);
    1.99 +
   1.100 +(* ------------------------------------------------------------------------- *)
   1.101 +(* maxidx: computes the maximal variable index occuring in a formula of      *)
   1.102 +(*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
   1.103 +(* ------------------------------------------------------------------------- *)
   1.104 +
   1.105 +	(* prop_formula -> int *)
   1.106 +
   1.107 +	fun maxidx True            = 0
   1.108 +	  | maxidx False           = 0
   1.109 +	  | maxidx (BoolVar i)     = i
   1.110 +	  | maxidx (Not fm)        = maxidx fm
   1.111 +	  | maxidx (Or (fm1,fm2))  = Int.max (maxidx fm1, maxidx fm2)
   1.112 +	  | maxidx (And (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2);
   1.113 +
   1.114 +(* ------------------------------------------------------------------------- *)
   1.115 +(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
   1.116 +(*      logic (i.e. only variables may be negated, but not subformulas)      *)
   1.117 +(* ------------------------------------------------------------------------- *)
   1.118 +
   1.119 +	(* prop_formula -> prop_formula *)
   1.120 +
   1.121 +	fun
   1.122 +	(* constants *)
   1.123 +	    nnf True                  = True
   1.124 +	  | nnf False                 = False
   1.125 +	(* variables *)
   1.126 +	  | nnf (BoolVar i)           = BoolVar i
   1.127 +	(* 'or' and 'and' as outermost connectives are left untouched *)
   1.128 +	  | nnf (Or  (fm1,fm2))       = SOr  (nnf fm1, nnf fm2)
   1.129 +	  | nnf (And (fm1,fm2))       = SAnd (nnf fm1, nnf fm2)
   1.130 +	(* 'not' + constant *)
   1.131 +	  | nnf (Not True)            = False
   1.132 +	  | nnf (Not False)           = True
   1.133 +	(* 'not' + variable *)
   1.134 +	  | nnf (Not (BoolVar i))     = Not (BoolVar i)
   1.135 +	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   1.136 +	  | nnf (Not (Or  (fm1,fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
   1.137 +	  | nnf (Not (And (fm1,fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
   1.138 +	(* double-negation elimination *)
   1.139 +	  | nnf (Not (Not fm))        = nnf fm;
   1.140 +
   1.141 +(* ------------------------------------------------------------------------- *)
   1.142 +(* cnf: computes the clause normal form (i.e. a conjunction of disjunctions) *)
   1.143 +(*      of a formula 'fm' of propositional logic.  The result formula may be *)
   1.144 +(*      exponentially longer than 'fm'.                                      *)
   1.145 +(* ------------------------------------------------------------------------- *)
   1.146 +
   1.147 +	(* prop_formula -> prop_formula *)
   1.148 +
   1.149 +	fun cnf fm =
   1.150 +	let
   1.151 +		fun
   1.152 +		(* constants *)
   1.153 +		    cnf_from_nnf True              = True
   1.154 +		  | cnf_from_nnf False             = False
   1.155 +		(* literals *)
   1.156 +		  | cnf_from_nnf (BoolVar i)       = BoolVar i
   1.157 +		  | cnf_from_nnf (Not (BoolVar i)) = Not (BoolVar i)
   1.158 +		(* pushing 'or' inside of 'and' using distributive laws *)
   1.159 +		  | cnf_from_nnf (Or (fm1,fm2)) =
   1.160 +			let
   1.161 +				val fm1' = cnf_from_nnf fm1
   1.162 +				val fm2' = cnf_from_nnf fm2
   1.163 +			in
   1.164 +				case fm1' of
   1.165 +				  And (fm11,fm12) => cnf_from_nnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
   1.166 +				| _               =>
   1.167 +					(case fm2' of
   1.168 +					  And (fm21,fm22) => cnf_from_nnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
   1.169 +					(* neither subformula contains 'and' *)
   1.170 +					| _               => Or (fm1,fm2))
   1.171 +			end
   1.172 +		(* 'and' as outermost connective is left untouched *)
   1.173 +		  | cnf_from_nnf (And (fm1,fm2))   = SAnd (cnf_from_nnf fm1, cnf_from_nnf fm2)
   1.174 +		(* 'not' + something other than a variable: formula is not in negation normal form *)
   1.175 +		  | cnf_from_nnf _                 = raise ERROR
   1.176 +	in
   1.177 +		(cnf_from_nnf o nnf) fm
   1.178 +	end;
   1.179 +
   1.180 +(* ------------------------------------------------------------------------- *)
   1.181 +(* defcnf: computes the definitional clause normal form of a formula 'fm' of *)
   1.182 +(*      propositional logic, introducing auxiliary variables if necessary to *)
   1.183 +(*      avoid an exponential blowup of the formula.  The result formula is   *)
   1.184 +(*      satisfiable if and only if 'fm' is satisfiable.                      *)
   1.185 +(* ------------------------------------------------------------------------- *)
   1.186 +
   1.187 +	(* prop_formula -> prop_formula *)
   1.188 +
   1.189 +	fun defcnf fm =
   1.190 +	let
   1.191 +		(* prop_formula * int -> prop_formula * int *)
   1.192 +		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   1.193 +		fun
   1.194 +		(* constants *)
   1.195 +		    defcnf_from_nnf (True,new)            = (True, new)
   1.196 +		  | defcnf_from_nnf (False,new)           = (False, new)
   1.197 +		(* literals *)
   1.198 +		  | defcnf_from_nnf (BoolVar i,new)       = (BoolVar i, new)
   1.199 +		  | defcnf_from_nnf (Not (BoolVar i),new) = (Not (BoolVar i), new)
   1.200 +		(* pushing 'or' inside of 'and' using distributive laws *)
   1.201 +		  | defcnf_from_nnf (Or (fm1,fm2),new)    =
   1.202 +			let
   1.203 +				val (fm1',new')  = defcnf_from_nnf (fm1, new)
   1.204 +				val (fm2',new'') = defcnf_from_nnf (fm2, new')
   1.205 +			in
   1.206 +				case fm1' of
   1.207 +				  And (fm11,fm12) =>
   1.208 +					let
   1.209 +						val aux = BoolVar new''
   1.210 +					in
   1.211 +						(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
   1.212 +						defcnf_from_nnf (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fm2', Not aux)), new''+1)
   1.213 +					end
   1.214 +				| _               =>
   1.215 +					(case fm2' of
   1.216 +					  And (fm21,fm22) =>
   1.217 +						let
   1.218 +							val aux = BoolVar new''
   1.219 +						in
   1.220 +							(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
   1.221 +							defcnf_from_nnf (SAnd (SOr (fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), new''+1)
   1.222 +						end
   1.223 +					(* neither subformula contains 'and' *)
   1.224 +					| _               => (Or (fm1,fm2),new))
   1.225 +			end
   1.226 +		(* 'and' as outermost connective is left untouched *)
   1.227 +		  | defcnf_from_nnf (And (fm1,fm2),new)   =
   1.228 +			let
   1.229 +				val (fm1',new')  = defcnf_from_nnf (fm1, new)
   1.230 +				val (fm2',new'') = defcnf_from_nnf (fm2, new')
   1.231 +			in
   1.232 +				(SAnd (fm1', fm2'), new'')
   1.233 +			end
   1.234 +		(* 'not' + something other than a variable: formula is not in negation normal form *)
   1.235 +		  | defcnf_from_nnf (_,_)                 = raise ERROR
   1.236 +	in
   1.237 +		(fst o defcnf_from_nnf) (nnf fm, (maxidx fm)+1)
   1.238 +	end;
   1.239 +
   1.240 +(* ------------------------------------------------------------------------- *)
   1.241 +(* exists: computes the disjunction over a list 'xs' of propositional        *)
   1.242 +(*      formulas                                                             *)
   1.243 +(* ------------------------------------------------------------------------- *)
   1.244 +
   1.245 +	(* prop_formula list -> prop_formula *)
   1.246 +
   1.247 +	fun exists xs = foldl SOr (False, xs);
   1.248 +
   1.249 +(* ------------------------------------------------------------------------- *)
   1.250 +(* all: computes the conjunction over a list 'xs' of propositional formulas  *)
   1.251 +(* ------------------------------------------------------------------------- *)
   1.252 +
   1.253 +	(* prop_formula list -> prop_formula *)
   1.254 +
   1.255 +	fun all xs = foldl SAnd (True, xs);
   1.256 +
   1.257 +(* ------------------------------------------------------------------------- *)
   1.258 +(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
   1.259 +(* ------------------------------------------------------------------------- *)
   1.260 +
   1.261 +	(* prop_formula list * prop_formula list -> prop_formula *)
   1.262 +
   1.263 +	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
   1.264 +
   1.265 +(* ------------------------------------------------------------------------- *)
   1.266 +(* eval: given an assignment 'a' of boolean values to variable indices, the  *)
   1.267 +(*      truth value of a propositional formula 'fm' is computed              *)
   1.268 +(* ------------------------------------------------------------------------- *)
   1.269 +
   1.270 +	(* (int -> bool) -> prop_formula -> bool *)
   1.271 +
   1.272 +	fun eval a True            = true
   1.273 +	  | eval a False           = false
   1.274 +	  | eval a (BoolVar i)     = (a i)
   1.275 +	  | eval a (Not fm)        = not (eval a fm)
   1.276 +	  | eval a (Or (fm1,fm2))  = (eval a fm1) orelse (eval a fm2)
   1.277 +	  | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
   1.278 +
   1.279 +end;