1(* Title: HOL/Tools/prop_logic.ML 2 Author: Tjark Weber 3 Copyright 2004-2009 4 5Formulas of propositional logic. 6*) 7 8signature PROP_LOGIC = 9sig 10 datatype prop_formula = 11 True 12 | False 13 | BoolVar of int (* NOTE: only use indices >= 1 *) 14 | Not of prop_formula 15 | Or of prop_formula * prop_formula 16 | And of prop_formula * prop_formula 17 18 val SNot: prop_formula -> prop_formula 19 val SOr: prop_formula * prop_formula -> prop_formula 20 val SAnd: prop_formula * prop_formula -> prop_formula 21 val simplify: prop_formula -> prop_formula (* eliminates True/False and double-negation *) 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 exists: prop_formula list -> prop_formula (* finite disjunction *) 27 val all: prop_formula list -> prop_formula (* finite conjunction *) 28 val dot_product: prop_formula list * prop_formula list -> prop_formula 29 30 val is_nnf: prop_formula -> bool (* returns true iff the formula is in negation normal form *) 31 val is_cnf: prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *) 32 33 val nnf: prop_formula -> prop_formula (* negation normal form *) 34 val cnf: prop_formula -> prop_formula (* conjunctive normal form *) 35 val defcnf: prop_formula -> prop_formula (* definitional cnf *) 36 37 val eval: (int -> bool) -> prop_formula -> bool (* semantics *) 38 39 (* propositional representation of HOL terms *) 40 val prop_formula_of_term: term -> int Termtab.table -> prop_formula * int Termtab.table 41 (* HOL term representation of propositional formulae *) 42 val term_of_prop_formula: prop_formula -> term 43end; 44 45structure Prop_Logic : PROP_LOGIC = 46struct 47 48(* ------------------------------------------------------------------------- *) 49(* prop_formula: formulas of propositional logic, built from Boolean *) 50(* variables (referred to by index) and True/False using *) 51(* not/or/and *) 52(* ------------------------------------------------------------------------- *) 53 54datatype prop_formula = 55 True 56 | False 57 | BoolVar of int (* NOTE: only use indices >= 1 *) 58 | Not of prop_formula 59 | Or of prop_formula * prop_formula 60 | And of prop_formula * prop_formula; 61 62(* ------------------------------------------------------------------------- *) 63(* The following constructor functions make sure that True and False do not *) 64(* occur within any of the other connectives (i.e. Not, Or, And), and *) 65(* perform double-negation elimination. *) 66(* ------------------------------------------------------------------------- *) 67 68fun SNot True = False 69 | SNot False = True 70 | SNot (Not fm) = fm 71 | SNot fm = Not fm; 72 73fun SOr (True, _) = True 74 | SOr (_, True) = True 75 | SOr (False, fm) = fm 76 | SOr (fm, False) = fm 77 | SOr (fm1, fm2) = Or (fm1, fm2); 78 79fun SAnd (True, fm) = fm 80 | SAnd (fm, True) = fm 81 | SAnd (False, _) = False 82 | SAnd (_, False) = False 83 | SAnd (fm1, fm2) = And (fm1, fm2); 84 85(* ------------------------------------------------------------------------- *) 86(* simplify: eliminates True/False below other connectives, and double- *) 87(* negation *) 88(* ------------------------------------------------------------------------- *) 89 90fun simplify (Not fm) = SNot (simplify fm) 91 | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2) 92 | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2) 93 | simplify fm = fm; 94 95(* ------------------------------------------------------------------------- *) 96(* indices: collects all indices of Boolean variables that occur in a *) 97(* propositional formula 'fm'; no duplicates *) 98(* ------------------------------------------------------------------------- *) 99 100fun indices True = [] 101 | indices False = [] 102 | indices (BoolVar i) = [i] 103 | indices (Not fm) = indices fm 104 | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) 105 | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); 106 107(* ------------------------------------------------------------------------- *) 108(* maxidx: computes the maximal variable index occurring in a formula of *) 109(* propositional logic 'fm'; 0 if 'fm' contains no variable *) 110(* ------------------------------------------------------------------------- *) 111 112fun maxidx True = 0 113 | maxidx False = 0 114 | maxidx (BoolVar i) = i 115 | maxidx (Not fm) = maxidx fm 116 | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2) 117 | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2); 118 119(* ------------------------------------------------------------------------- *) 120(* exists: computes the disjunction over a list 'xs' of propositional *) 121(* formulas *) 122(* ------------------------------------------------------------------------- *) 123 124fun exists xs = Library.foldl SOr (False, xs); 125 126(* ------------------------------------------------------------------------- *) 127(* all: computes the conjunction over a list 'xs' of propositional formulas *) 128(* ------------------------------------------------------------------------- *) 129 130fun all xs = Library.foldl SAnd (True, xs); 131 132(* ------------------------------------------------------------------------- *) 133(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *) 134(* ------------------------------------------------------------------------- *) 135 136fun dot_product (xs, ys) = exists (map SAnd (xs ~~ ys)); 137 138(* ------------------------------------------------------------------------- *) 139(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e., *) 140(* only variables may be negated, but not subformulas). *) 141(* ------------------------------------------------------------------------- *) 142 143local 144 fun is_literal (BoolVar _) = true 145 | is_literal (Not (BoolVar _)) = true 146 | is_literal _ = false 147 fun is_conj_disj (Or (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2 148 | is_conj_disj (And (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2 149 | is_conj_disj fm = is_literal fm 150in 151 fun is_nnf True = true 152 | is_nnf False = true 153 | is_nnf fm = is_conj_disj fm 154end; 155 156(* ------------------------------------------------------------------------- *) 157(* is_cnf: returns 'true' iff the formula is in conjunctive normal form *) 158(* (i.e., a conjunction of disjunctions of literals). 'is_cnf' *) 159(* implies 'is_nnf'. *) 160(* ------------------------------------------------------------------------- *) 161 162local 163 fun is_literal (BoolVar _) = true 164 | is_literal (Not (BoolVar _)) = true 165 | is_literal _ = false 166 fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2 167 | is_disj fm = is_literal fm 168 fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2 169 | is_conj fm = is_disj fm 170in 171 fun is_cnf True = true 172 | is_cnf False = true 173 | is_cnf fm = is_conj fm 174end; 175 176(* ------------------------------------------------------------------------- *) 177(* nnf: computes the negation normal form of a formula 'fm' of propositional *) 178(* logic (i.e., only variables may be negated, but not subformulas). *) 179(* Simplification (cf. 'simplify') is performed as well. Not *) 180(* surprisingly, 'is_nnf o nnf' always returns 'true'. 'nnf fm' returns *) 181(* 'fm' if (and only if) 'is_nnf fm' returns 'true'. *) 182(* ------------------------------------------------------------------------- *) 183 184fun nnf fm = 185 let 186 fun 187 (* constants *) 188 nnf_aux True = True 189 | nnf_aux False = False 190 (* variables *) 191 | nnf_aux (BoolVar i) = (BoolVar i) 192 (* 'or' and 'and' as outermost connectives are left untouched *) 193 | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2) 194 | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2) 195 (* 'not' + constant *) 196 | nnf_aux (Not True) = False 197 | nnf_aux (Not False) = True 198 (* 'not' + variable *) 199 | nnf_aux (Not (BoolVar i)) = Not (BoolVar i) 200 (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) 201 | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) 202 | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) 203 (* double-negation elimination *) 204 | nnf_aux (Not (Not fm)) = nnf_aux fm 205 in 206 if is_nnf fm then fm 207 else nnf_aux fm 208 end; 209 210(* ------------------------------------------------------------------------- *) 211(* cnf: computes the conjunctive normal form (i.e., a conjunction of *) 212(* disjunctions of literals) of a formula 'fm' of propositional logic. *) 213(* Simplification (cf. 'simplify') is performed as well. The result *) 214(* is equivalent to 'fm', but may be exponentially longer. Not *) 215(* surprisingly, 'is_cnf o cnf' always returns 'true'. 'cnf fm' returns *) 216(* 'fm' if (and only if) 'is_cnf fm' returns 'true'. *) 217(* ------------------------------------------------------------------------- *) 218 219fun cnf fm = 220 let 221 (* function to push an 'Or' below 'And's, using distributive laws *) 222 fun cnf_or (And (fm11, fm12), fm2) = 223 And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) 224 | cnf_or (fm1, And (fm21, fm22)) = 225 And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) 226 (* neither subformula contains 'And' *) 227 | cnf_or (fm1, fm2) = Or (fm1, fm2) 228 fun cnf_from_nnf True = True 229 | cnf_from_nnf False = False 230 | cnf_from_nnf (BoolVar i) = BoolVar i 231 (* 'fm' must be a variable since the formula is in NNF *) 232 | cnf_from_nnf (Not fm) = Not fm 233 (* 'Or' may need to be pushed below 'And' *) 234 | cnf_from_nnf (Or (fm1, fm2)) = 235 cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) 236 (* 'And' as outermost connective is left untouched *) 237 | cnf_from_nnf (And (fm1, fm2)) = 238 And (cnf_from_nnf fm1, cnf_from_nnf fm2) 239 in 240 if is_cnf fm then fm 241 else (cnf_from_nnf o nnf) fm 242 end; 243 244(* ------------------------------------------------------------------------- *) 245(* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *) 246(* of propositional logic. Simplification (cf. 'simplify') is performed *) 247(* as well. 'defcnf' may introduce auxiliary Boolean variables to avoid *) 248(* an exponential blowup of the formula. The result is equisatisfiable *) 249(* (i.e., satisfiable if and only if 'fm' is satisfiable), but not *) 250(* necessarily equivalent to 'fm'. Not surprisingly, 'is_cnf o defcnf' *) 251(* always returns 'true'. 'defcnf fm' returns 'fm' if (and only if) *) 252(* 'is_cnf fm' returns 'true'. *) 253(* ------------------------------------------------------------------------- *) 254 255fun defcnf fm = 256 if is_cnf fm then fm 257 else 258 let 259 val fm' = nnf fm 260 (* 'new' specifies the next index that is available to introduce an auxiliary variable *) 261 val new = Unsynchronized.ref (maxidx fm' + 1) 262 fun new_idx () = let val idx = !new in new := idx+1; idx end 263 (* replaces 'And' by an auxiliary variable (and its definition) *) 264 fun defcnf_or (And x) = 265 let 266 val i = new_idx () 267 in 268 (* Note that definitions are in NNF, but not CNF. *) 269 (BoolVar i, [Or (Not (BoolVar i), And x)]) 270 end 271 | defcnf_or (Or (fm1, fm2)) = 272 let 273 val (fm1', defs1) = defcnf_or fm1 274 val (fm2', defs2) = defcnf_or fm2 275 in 276 (Or (fm1', fm2'), defs1 @ defs2) 277 end 278 | defcnf_or fm = (fm, []) 279 fun defcnf_from_nnf True = True 280 | defcnf_from_nnf False = False 281 | defcnf_from_nnf (BoolVar i) = BoolVar i 282 (* 'fm' must be a variable since the formula is in NNF *) 283 | defcnf_from_nnf (Not fm) = Not fm 284 (* 'Or' may need to be pushed below 'And' *) 285 (* 'Or' of literal and 'And': use distributivity *) 286 | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) = 287 And (defcnf_from_nnf (Or (BoolVar i, fm1)), 288 defcnf_from_nnf (Or (BoolVar i, fm2))) 289 | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) = 290 And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)), 291 defcnf_from_nnf (Or (Not (BoolVar i), fm2))) 292 | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) = 293 And (defcnf_from_nnf (Or (fm1, BoolVar i)), 294 defcnf_from_nnf (Or (fm2, BoolVar i))) 295 | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) = 296 And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))), 297 defcnf_from_nnf (Or (fm2, Not (BoolVar i)))) 298 (* all other cases: turn the formula into a disjunction of literals, *) 299 (* adding definitions as necessary *) 300 | defcnf_from_nnf (Or x) = 301 let 302 val (fm, defs) = defcnf_or (Or x) 303 val cnf_defs = map defcnf_from_nnf defs 304 in 305 all (fm :: cnf_defs) 306 end 307 (* 'And' as outermost connective is left untouched *) 308 | defcnf_from_nnf (And (fm1, fm2)) = 309 And (defcnf_from_nnf fm1, defcnf_from_nnf fm2) 310 in 311 defcnf_from_nnf fm' 312 end; 313 314(* ------------------------------------------------------------------------- *) 315(* eval: given an assignment 'a' of Boolean values to variable indices, the *) 316(* truth value of a propositional formula 'fm' is computed *) 317(* ------------------------------------------------------------------------- *) 318 319fun eval _ True = true 320 | eval _ False = false 321 | eval a (BoolVar i) = (a i) 322 | eval a (Not fm) = not (eval a fm) 323 | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2) 324 | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2); 325 326(* ------------------------------------------------------------------------- *) 327(* prop_formula_of_term: returns the propositional structure of a HOL term, *) 328(* with subterms replaced by Boolean variables. Also returns a table *) 329(* of terms and corresponding variables that extends the table that was *) 330(* given as an argument. Usually, you'll just want to use *) 331(* 'Termtab.empty' as value for 'table'. *) 332(* ------------------------------------------------------------------------- *) 333 334(* Note: The implementation is somewhat optimized; the next index to be used *) 335(* is computed only when it is actually needed. However, when *) 336(* 'prop_formula_of_term' is invoked many times, it might be more *) 337(* efficient to pass and return this value as an additional parameter, *) 338(* so that it does not have to be recomputed (by folding over the *) 339(* table) for each invocation. *) 340 341fun prop_formula_of_term t table = 342 let 343 val next_idx_is_valid = Unsynchronized.ref false 344 val next_idx = Unsynchronized.ref 0 345 fun get_next_idx () = 346 if !next_idx_is_valid then 347 Unsynchronized.inc next_idx 348 else ( 349 next_idx := Termtab.fold (Integer.max o snd) table 0; 350 next_idx_is_valid := true; 351 Unsynchronized.inc next_idx 352 ) 353 fun aux (Const (\<^const_name>\<open>True\<close>, _)) table = (True, table) 354 | aux (Const (\<^const_name>\<open>False\<close>, _)) table = (False, table) 355 | aux (Const (\<^const_name>\<open>Not\<close>, _) $ x) table = apfst Not (aux x table) 356 | aux (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ x $ y) table = 357 let 358 val (fm1, table1) = aux x table 359 val (fm2, table2) = aux y table1 360 in 361 (Or (fm1, fm2), table2) 362 end 363 | aux (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ x $ y) table = 364 let 365 val (fm1, table1) = aux x table 366 val (fm2, table2) = aux y table1 367 in 368 (And (fm1, fm2), table2) 369 end 370 | aux x table = 371 (case Termtab.lookup table x of 372 SOME i => (BoolVar i, table) 373 | NONE => 374 let 375 val i = get_next_idx () 376 in 377 (BoolVar i, Termtab.update (x, i) table) 378 end) 379 in 380 aux t table 381 end; 382 383(* ------------------------------------------------------------------------- *) 384(* term_of_prop_formula: returns a HOL term that corresponds to a *) 385(* propositional formula, with Boolean variables replaced by Free's *) 386(* ------------------------------------------------------------------------- *) 387 388(* Note: A more generic implementation should take another argument of type *) 389(* Term.term Inttab.table (or so) that specifies HOL terms for some *) 390(* Boolean variables in the formula, similar to 'prop_formula_of_term' *) 391(* (but the other way round). *) 392 393fun term_of_prop_formula True = \<^term>\<open>True\<close> 394 | term_of_prop_formula False = \<^term>\<open>False\<close> 395 | term_of_prop_formula (BoolVar i) = Free ("v" ^ string_of_int i, HOLogic.boolT) 396 | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm) 397 | term_of_prop_formula (Or (fm1, fm2)) = 398 HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) 399 | term_of_prop_formula (And (fm1, fm2)) = 400 HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); 401 402end; 403