src/HOL/Tools/prop_logic.ML
author webertj
Fri Nov 19 17:52:07 2004 +0100 (2004-11-19)
changeset 15301 26724034de5e
parent 14964 2c1456d705e9
child 15548 aea2f1706fdf
permissions -rw-r--r--
comment modified
     1 (*  Title:      HOL/Tools/prop_logic.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2004
     5 
     6 Formulas of propositional logic.
     7 *)
     8 
     9 signature PROP_LOGIC =
    10 sig
    11 	datatype prop_formula =
    12 		  True
    13 		| False
    14 		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    15 		| Not of prop_formula
    16 		| Or of prop_formula * prop_formula
    17 		| And of prop_formula * prop_formula
    18 
    19 	val SNot : prop_formula -> prop_formula
    20 	val SOr  : prop_formula * prop_formula -> prop_formula
    21 	val SAnd : prop_formula * prop_formula -> prop_formula
    22 
    23 	val indices : prop_formula -> int list  (* set of all variable indices *)
    24 	val maxidx  : prop_formula -> int       (* maximal variable index *)
    25 
    26 	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    27 	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
    28 	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
    29 
    30 	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
    31 	val all         : prop_formula list -> prop_formula  (* finite conjunction *)
    32 	val dot_product : prop_formula list * prop_formula list -> prop_formula
    33 
    34 	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
    35 end;
    36 
    37 structure PropLogic : PROP_LOGIC =
    38 struct
    39 
    40 (* ------------------------------------------------------------------------- *)
    41 (* prop_formula: formulas of propositional logic, built from Boolean         *)
    42 (*               variables (referred to by index) and True/False using       *)
    43 (*               not/or/and                                                  *)
    44 (* ------------------------------------------------------------------------- *)
    45 
    46 	datatype prop_formula =
    47 		  True
    48 		| False
    49 		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    50 		| Not of prop_formula
    51 		| Or of prop_formula * prop_formula
    52 		| And of prop_formula * prop_formula;
    53 
    54 (* ------------------------------------------------------------------------- *)
    55 (* The following constructor functions make sure that True and False do not  *)
    56 (* occur within any of the other connectives (i.e. Not, Or, And), and        *)
    57 (* perform double-negation elimination.                                      *)
    58 (* ------------------------------------------------------------------------- *)
    59 
    60 	(* prop_formula -> prop_formula *)
    61 
    62 	fun SNot True     = False
    63 	  | SNot False    = True
    64 	  | SNot (Not fm) = fm
    65 	  | SNot fm       = Not fm;
    66 
    67 	(* prop_formula * prop_formula -> prop_formula *)
    68 
    69 	fun SOr (True, _)   = True
    70 	  | SOr (_, True)   = True
    71 	  | SOr (False, fm) = fm
    72 	  | SOr (fm, False) = fm
    73 	  | SOr (fm1, fm2)  = Or (fm1, fm2);
    74 
    75 	(* prop_formula * prop_formula -> prop_formula *)
    76 
    77 	fun SAnd (True, fm) = fm
    78 	  | SAnd (fm, True) = fm
    79 	  | SAnd (False, _) = False
    80 	  | SAnd (_, False) = False
    81 	  | SAnd (fm1, fm2) = And (fm1, fm2);
    82 
    83 (* ------------------------------------------------------------------------- *)
    84 (* indices: collects all indices of Boolean variables that occur in a        *)
    85 (*      propositional formula 'fm'; no duplicates                            *)
    86 (* ------------------------------------------------------------------------- *)
    87 
    88 	(* prop_formula -> int list *)
    89 
    90 	fun indices True            = []
    91 	  | indices False           = []
    92 	  | indices (BoolVar i)     = [i]
    93 	  | indices (Not fm)        = indices fm
    94 	  | indices (Or (fm1,fm2))  = (indices fm1) union_int (indices fm2)
    95 	  | indices (And (fm1,fm2)) = (indices fm1) union_int (indices fm2);
    96 
    97 (* ------------------------------------------------------------------------- *)
    98 (* maxidx: computes the maximal variable index occuring in a formula of      *)
    99 (*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
   100 (* ------------------------------------------------------------------------- *)
   101 
   102 	(* prop_formula -> int *)
   103 
   104 	fun maxidx True            = 0
   105 	  | maxidx False           = 0
   106 	  | maxidx (BoolVar i)     = i
   107 	  | maxidx (Not fm)        = maxidx fm
   108 	  | maxidx (Or (fm1,fm2))  = Int.max (maxidx fm1, maxidx fm2)
   109 	  | maxidx (And (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2);
   110 
   111 (* ------------------------------------------------------------------------- *)
   112 (* exception SAME: raised to indicate that the return value of a function is *)
   113 (*                 identical to its argument (optimization to allow sharing, *)
   114 (*                 rather than copying)                                      *)
   115 (* ------------------------------------------------------------------------- *)
   116 
   117 	exception SAME;
   118 
   119 (* ------------------------------------------------------------------------- *)
   120 (* nnf: computes the negation normal form of a formula 'fm' of propositional *)
   121 (*      logic (i.e. only variables may be negated, but not subformulas)      *)
   122 (* ------------------------------------------------------------------------- *)
   123 
   124 	(* prop_formula -> prop_formula *)
   125 
   126 	fun
   127 	(* constants *)
   128 	    nnf True                  = True
   129 	  | nnf False                 = False
   130 	(* variables *)
   131 	  | nnf (BoolVar i)           = (BoolVar i)
   132 	(* 'or' and 'and' as outermost connectives are left untouched *)
   133 	  | nnf (Or  (fm1,fm2))       = SOr  (nnf fm1, nnf fm2)
   134 	  | nnf (And (fm1,fm2))       = SAnd (nnf fm1, nnf fm2)
   135 	(* 'not' + constant *)
   136 	  | nnf (Not True)            = False
   137 	  | nnf (Not False)           = True
   138 	(* 'not' + variable *)
   139 	  | nnf (Not (BoolVar i))     = Not (BoolVar i)
   140 	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   141 	  | nnf (Not (Or  (fm1,fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
   142 	  | nnf (Not (And (fm1,fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
   143 	(* double-negation elimination *)
   144 	  | nnf (Not (Not fm))        = nnf fm;
   145 
   146 (* ------------------------------------------------------------------------- *)
   147 (* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
   148 (*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
   149 (*      formula may be exponentially longer than 'fm'.                       *)
   150 (* ------------------------------------------------------------------------- *)
   151 
   152 	(* prop_formula -> prop_formula *)
   153 
   154 	fun cnf fm =
   155 	let
   156 		fun
   157 		(* constants *)
   158 		    cnf_from_nnf True             = True
   159 		  | cnf_from_nnf False            = False
   160 		(* literals *)
   161 		  | cnf_from_nnf (BoolVar i)      = BoolVar i
   162 		  | cnf_from_nnf (Not fm1)        = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
   163 		(* pushing 'or' inside of 'and' using distributive laws *)
   164 		  | cnf_from_nnf (Or (fm1, fm2))  =
   165 			let
   166 				fun cnf_or (And (fm11, fm12), fm2) =
   167 					And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
   168 				  | cnf_or (fm1, And (fm21, fm22)) =
   169 					And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
   170 				(* neither subformula contains 'and' *)
   171 				  | cnf_or (fm1, fm2) =
   172 					Or (fm1, fm2)
   173 			in
   174 				cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
   175 			end
   176 		(* 'and' as outermost connective is left untouched *)
   177 		  | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
   178 	in
   179 		(cnf_from_nnf o nnf) fm
   180 	end;
   181 
   182 (* ------------------------------------------------------------------------- *)
   183 (* defcnf: computes the definitional conjunctive normal form of a formula    *)
   184 (*      'fm' of propositional logic, introducing auxiliary variables if      *)
   185 (*      necessary to avoid an exponential blowup of the formula.  The result *)
   186 (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
   187 (* ------------------------------------------------------------------------- *)
   188 
   189 	(* prop_formula -> prop_formula *)
   190 
   191 	fun defcnf fm =
   192 	let
   193 		(* prop_formula * int -> prop_formula * int *)
   194 		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   195 		fun
   196 		(* constants *)
   197 		    defcnf_from_nnf (True, new)            = (True, new)
   198 		  | defcnf_from_nnf (False, new)           = (False, new)
   199 		(* literals *)
   200 		  | defcnf_from_nnf (BoolVar i, new)       = (BoolVar i, new)
   201 		  | defcnf_from_nnf (Not fm1, new)         = (Not fm1, new)  (* 'fm1' must be a variable since the formula is in NNF *)
   202 		(* pushing 'or' inside of 'and' using auxiliary variables *)
   203 		  | defcnf_from_nnf (Or (fm1, fm2), new)   =
   204 			let
   205 				val (fm1', new')  = defcnf_from_nnf (fm1, new)
   206 				val (fm2', new'') = defcnf_from_nnf (fm2, new')
   207 				(* prop_formula * prop_formula -> int -> prop_formula * int *)
   208 				fun defcnf_or (And (fm11, fm12), fm2) new =
   209 					(case fm2 of
   210 					(* do not introduce an auxiliary variable for literals *)
   211 					  BoolVar _ =>
   212 						let
   213 							val (fm_a, new')  = defcnf_or (fm11, fm2) new
   214 							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
   215 						in
   216 							(And (fm_a, fm_b), new'')
   217 						end
   218 					| Not _ =>
   219 						let
   220 							val (fm_a, new')  = defcnf_or (fm11, fm2) new
   221 							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
   222 						in
   223 							(And (fm_a, fm_b), new'')
   224 						end
   225 					| _ =>
   226 						let
   227 							val aux            = BoolVar new
   228 							val (fm_a, new')   = defcnf_or (fm11, aux)     (new+1)
   229 							val (fm_b, new'')  = defcnf_or (fm12, aux)     new'
   230 							val (fm_c, new''') = defcnf_or (fm2,  Not aux) new''
   231 						in
   232 							(And (And (fm_a, fm_b), fm_c), new''')
   233 						end)
   234 				  | defcnf_or (fm1, And (fm21, fm22)) new =
   235 					(case fm1 of
   236 					(* do not introduce an auxiliary variable for literals *)
   237 					  BoolVar _ =>
   238 						let
   239 							val (fm_a, new')  = defcnf_or (fm1, fm21) new
   240 							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
   241 						in
   242 							(And (fm_a, fm_b), new'')
   243 						end
   244 					| Not _ =>
   245 						let
   246 							val (fm_a, new')  = defcnf_or (fm1, fm21) new
   247 							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
   248 						in
   249 							(And (fm_a, fm_b), new'')
   250 						end
   251 					| _ =>
   252 						let
   253 							val aux            = BoolVar new
   254 							val (fm_a, new')   = defcnf_or (fm1,  Not aux) (new+1)
   255 							val (fm_b, new'')  = defcnf_or (fm21, aux)     new'
   256 							val (fm_c, new''') = defcnf_or (fm22, aux)     new''
   257 						in
   258 							(And (fm_a, And (fm_b, fm_c)), new''')
   259 						end)
   260 				(* neither subformula contains 'and' *)
   261 				  | defcnf_or (fm1, fm2) new =
   262 					(Or (fm1, fm2), new)
   263 			in
   264 				defcnf_or (fm1', fm2') new''
   265 			end
   266 		(* 'and' as outermost connective is left untouched *)
   267 		  | defcnf_from_nnf (And (fm1, fm2), new)   =
   268 			let
   269 				val (fm1', new')  = defcnf_from_nnf (fm1, new)
   270 				val (fm2', new'') = defcnf_from_nnf (fm2, new')
   271 			in
   272 				(And (fm1', fm2'), new'')
   273 			end
   274 		val fm' = nnf fm
   275 	in
   276 		(fst o defcnf_from_nnf) (fm', (maxidx fm')+1)
   277 	end;
   278 
   279 (* ------------------------------------------------------------------------- *)
   280 (* exists: computes the disjunction over a list 'xs' of propositional        *)
   281 (*      formulas                                                             *)
   282 (* ------------------------------------------------------------------------- *)
   283 
   284 	(* prop_formula list -> prop_formula *)
   285 
   286 	fun exists xs = foldl SOr (False, xs);
   287 
   288 (* ------------------------------------------------------------------------- *)
   289 (* all: computes the conjunction over a list 'xs' of propositional formulas  *)
   290 (* ------------------------------------------------------------------------- *)
   291 
   292 	(* prop_formula list -> prop_formula *)
   293 
   294 	fun all xs = foldl SAnd (True, xs);
   295 
   296 (* ------------------------------------------------------------------------- *)
   297 (* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
   298 (* ------------------------------------------------------------------------- *)
   299 
   300 	(* prop_formula list * prop_formula list -> prop_formula *)
   301 
   302 	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
   303 
   304 (* ------------------------------------------------------------------------- *)
   305 (* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
   306 (*      truth value of a propositional formula 'fm' is computed              *)
   307 (* ------------------------------------------------------------------------- *)
   308 
   309 	(* (int -> bool) -> prop_formula -> bool *)
   310 
   311 	fun eval a True            = true
   312 	  | eval a False           = false
   313 	  | eval a (BoolVar i)     = (a i)
   314 	  | eval a (Not fm)        = not (eval a fm)
   315 	  | eval a (Or (fm1,fm2))  = (eval a fm1) orelse (eval a fm2)
   316 	  | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
   317 
   318 end;