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