src/HOL/Tools/prop_logic.ML
author wenzelm
Thu Mar 27 14:41:09 2008 +0100 (2008-03-27)
changeset 26424 a6cad32a27b0
parent 22441 7da872d34ace
child 31220 f1c0ed85a33b
permissions -rw-r--r--
eliminated theory ProtoPure;
     1 (*  Title:      HOL/Tools/prop_logic.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2004-2005
     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 	val simplify : prop_formula -> prop_formula  (* eliminates True/False and double-negation *)
    23 
    24 	val indices : prop_formula -> int list  (* set of all variable indices *)
    25 	val maxidx  : prop_formula -> int       (* maximal variable index *)
    26 
    27 	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
    28 	val all         : prop_formula list -> prop_formula  (* finite conjunction *)
    29 	val dot_product : prop_formula list * prop_formula list -> prop_formula
    30 
    31 	val is_nnf : prop_formula -> bool  (* returns true iff the formula is in negation normal form *)
    32 	val is_cnf : prop_formula -> bool  (* returns true iff the formula is in conjunctive normal form *)
    33 
    34 	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    35 	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
    36 	val auxcnf : prop_formula -> prop_formula  (* cnf with auxiliary variables *)
    37 	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
    38 
    39 	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
    40 
    41 	(* propositional representation of HOL terms *)
    42 	val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
    43 	(* HOL term representation of propositional formulae *)
    44 	val term_of_prop_formula : prop_formula -> Term.term
    45 end;
    46 
    47 structure PropLogic : PROP_LOGIC =
    48 struct
    49 
    50 (* ------------------------------------------------------------------------- *)
    51 (* prop_formula: formulas of propositional logic, built from Boolean         *)
    52 (*               variables (referred to by index) and True/False using       *)
    53 (*               not/or/and                                                  *)
    54 (* ------------------------------------------------------------------------- *)
    55 
    56 	datatype prop_formula =
    57 		  True
    58 		| False
    59 		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    60 		| Not of prop_formula
    61 		| Or of prop_formula * prop_formula
    62 		| And of prop_formula * prop_formula;
    63 
    64 (* ------------------------------------------------------------------------- *)
    65 (* The following constructor functions make sure that True and False do not  *)
    66 (* occur within any of the other connectives (i.e. Not, Or, And), and        *)
    67 (* perform double-negation elimination.                                      *)
    68 (* ------------------------------------------------------------------------- *)
    69 
    70 	(* prop_formula -> prop_formula *)
    71 
    72 	fun SNot True     = False
    73 	  | SNot False    = True
    74 	  | SNot (Not fm) = fm
    75 	  | SNot fm       = Not fm;
    76 
    77 	(* prop_formula * prop_formula -> prop_formula *)
    78 
    79 	fun SOr (True, _)   = True
    80 	  | SOr (_, True)   = True
    81 	  | SOr (False, fm) = fm
    82 	  | SOr (fm, False) = fm
    83 	  | SOr (fm1, fm2)  = Or (fm1, fm2);
    84 
    85 	(* prop_formula * prop_formula -> prop_formula *)
    86 
    87 	fun SAnd (True, fm) = fm
    88 	  | SAnd (fm, True) = fm
    89 	  | SAnd (False, _) = False
    90 	  | SAnd (_, False) = False
    91 	  | SAnd (fm1, fm2) = And (fm1, fm2);
    92 
    93 (* ------------------------------------------------------------------------- *)
    94 (* simplify: eliminates True/False below other connectives, and double-      *)
    95 (*      negation                                                             *)
    96 (* ------------------------------------------------------------------------- *)
    97 
    98 	(* prop_formula -> prop_formula *)
    99 
   100 	fun simplify (Not fm)         = SNot (simplify fm)
   101 	  | simplify (Or (fm1, fm2))  = SOr (simplify fm1, simplify fm2)
   102 	  | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
   103 	  | simplify fm               = fm;
   104 
   105 (* ------------------------------------------------------------------------- *)
   106 (* indices: collects all indices of Boolean variables that occur in a        *)
   107 (*      propositional formula 'fm'; no duplicates                            *)
   108 (* ------------------------------------------------------------------------- *)
   109 
   110 	(* prop_formula -> int list *)
   111 
   112 	fun indices True             = []
   113 	  | indices False            = []
   114 	  | indices (BoolVar i)      = [i]
   115 	  | indices (Not fm)         = indices fm
   116 	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
   117 	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
   118 
   119 (* ------------------------------------------------------------------------- *)
   120 (* maxidx: computes the maximal variable index occuring in a formula of      *)
   121 (*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
   122 (* ------------------------------------------------------------------------- *)
   123 
   124 	(* prop_formula -> int *)
   125 
   126 	fun maxidx True             = 0
   127 	  | maxidx False            = 0
   128 	  | maxidx (BoolVar i)      = i
   129 	  | maxidx (Not fm)         = maxidx fm
   130 	  | maxidx (Or (fm1, fm2))  = Int.max (maxidx fm1, maxidx fm2)
   131 	  | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
   132 
   133 (* ------------------------------------------------------------------------- *)
   134 (* exists: computes the disjunction over a list 'xs' of propositional        *)
   135 (*      formulas                                                             *)
   136 (* ------------------------------------------------------------------------- *)
   137 
   138 	(* prop_formula list -> prop_formula *)
   139 
   140 	fun exists xs = Library.foldl SOr (False, xs);
   141 
   142 (* ------------------------------------------------------------------------- *)
   143 (* all: computes the conjunction over a list 'xs' of propositional formulas  *)
   144 (* ------------------------------------------------------------------------- *)
   145 
   146 	(* prop_formula list -> prop_formula *)
   147 
   148 	fun all xs = Library.foldl SAnd (True, xs);
   149 
   150 (* ------------------------------------------------------------------------- *)
   151 (* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
   152 (* ------------------------------------------------------------------------- *)
   153 
   154 	(* prop_formula list * prop_formula list -> prop_formula *)
   155 
   156 	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
   157 
   158 (* ------------------------------------------------------------------------- *)
   159 (* is_nnf: returns 'true' iff the formula is in negation normal form (i.e.   *)
   160 (*         only variables may be negated, but not subformulas).              *)
   161 (* ------------------------------------------------------------------------- *)
   162 
   163 	local
   164 		fun is_literal (BoolVar _)       = true
   165 		  | is_literal (Not (BoolVar _)) = true
   166 		  | is_literal _                 = false
   167 		fun is_conj_disj (Or (fm1, fm2))  =
   168 			is_conj_disj fm1 andalso is_conj_disj fm2
   169 		  | is_conj_disj (And (fm1, fm2)) =
   170 			is_conj_disj fm1 andalso is_conj_disj fm2
   171 		  | is_conj_disj fm               =
   172 			is_literal fm
   173 	in
   174 		fun is_nnf True  = true
   175 		  | is_nnf False = true
   176 		  | is_nnf fm    = is_conj_disj fm
   177 	end;
   178 
   179 (* ------------------------------------------------------------------------- *)
   180 (* is_cnf: returns 'true' iff the formula is in conjunctive normal form      *)
   181 (*         (i.e. a conjunction of disjunctions).                             *)
   182 (* ------------------------------------------------------------------------- *)
   183 
   184 	local
   185 		fun is_literal (BoolVar _)       = true
   186 		  | is_literal (Not (BoolVar _)) = true
   187 		  | is_literal _                 = false
   188 		fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2
   189 		  | is_disj fm              = is_literal fm
   190 		fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2
   191 		  | is_conj fm               = is_disj fm
   192 	in
   193 		fun is_cnf True             = true
   194 		  | is_cnf False            = true
   195 		  | is_cnf fm               = is_conj fm
   196 	end;
   197 
   198 (* ------------------------------------------------------------------------- *)
   199 (* nnf: computes the negation normal form of a formula 'fm' of propositional *)
   200 (*      logic (i.e. only variables may be negated, but not subformulas).     *)
   201 (*      Simplification (c.f. 'simplify') is performed as well.               *)
   202 (* ------------------------------------------------------------------------- *)
   203 
   204 	(* prop_formula -> prop_formula *)
   205 
   206 	fun
   207 	(* constants *)
   208 	    nnf True                   = True
   209 	  | nnf False                  = False
   210 	(* variables *)
   211 	  | nnf (BoolVar i)            = (BoolVar i)
   212 	(* 'or' and 'and' as outermost connectives are left untouched *)
   213 	  | nnf (Or  (fm1, fm2))       = SOr  (nnf fm1, nnf fm2)
   214 	  | nnf (And (fm1, fm2))       = SAnd (nnf fm1, nnf fm2)
   215 	(* 'not' + constant *)
   216 	  | nnf (Not True)             = False
   217 	  | nnf (Not False)            = True
   218 	(* 'not' + variable *)
   219 	  | nnf (Not (BoolVar i))      = Not (BoolVar i)
   220 	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   221 	  | nnf (Not (Or  (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
   222 	  | nnf (Not (And (fm1, fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
   223 	(* double-negation elimination *)
   224 	  | nnf (Not (Not fm))         = nnf fm;
   225 
   226 (* ------------------------------------------------------------------------- *)
   227 (* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
   228 (*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
   229 (*      formula may be exponentially longer than 'fm'.                       *)
   230 (* ------------------------------------------------------------------------- *)
   231 
   232 	(* prop_formula -> prop_formula *)
   233 
   234 	fun cnf fm =
   235 	let
   236 		fun
   237 		(* constants *)
   238 		    cnf_from_nnf True             = True
   239 		  | cnf_from_nnf False            = False
   240 		(* literals *)
   241 		  | cnf_from_nnf (BoolVar i)      = BoolVar i
   242 		  | cnf_from_nnf (Not fm1)        = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
   243 		(* pushing 'or' inside of 'and' using distributive laws *)
   244 		  | cnf_from_nnf (Or (fm1, fm2))  =
   245 			let
   246 				fun cnf_or (And (fm11, fm12), fm2) =
   247 					And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
   248 				  | cnf_or (fm1, And (fm21, fm22)) =
   249 					And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
   250 				(* neither subformula contains 'and' *)
   251 				  | cnf_or (fm1, fm2) =
   252 					Or (fm1, fm2)
   253 			in
   254 				cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
   255 			end
   256 		(* 'and' as outermost connective is left untouched *)
   257 		  | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
   258 	in
   259 		(cnf_from_nnf o nnf) fm
   260 	end;
   261 
   262 (* ------------------------------------------------------------------------- *)
   263 (* auxcnf: computes the definitional conjunctive normal form of a formula    *)
   264 (*      'fm' of propositional logic, introducing auxiliary variables if      *)
   265 (*      necessary to avoid an exponential blowup of the formula.  The result *)
   266 (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
   267 (*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
   268 (*      on the observation that e.g. "fm1 OR (fm21 AND fm22)" is             *)
   269 (*      equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR   *)
   270 (*      aux)".                                                               *)
   271 (* ------------------------------------------------------------------------- *)
   272 
   273 (* ------------------------------------------------------------------------- *)
   274 (* Note: 'auxcnf' tends to use fewer variables and fewer clauses than        *)
   275 (*      'defcnf' below, but sometimes generates much larger SAT problems     *)
   276 (*      overall (hence it must sometimes generate longer clauses than        *)
   277 (*      'defcnf' does).  It is currently not quite clear to me if one of the *)
   278 (*      algorithms is clearly superior to the other, but I suggest using     *)
   279 (*      'defcnf' instead.                                                    *)
   280 (* ------------------------------------------------------------------------- *)
   281 
   282 	(* prop_formula -> prop_formula *)
   283 
   284 	fun auxcnf fm =
   285 	let
   286 		(* convert formula to NNF first *)
   287 		val fm' = nnf fm
   288 		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   289 		(* int ref *)
   290 		val new = ref (maxidx fm' + 1)
   291 		(* unit -> int *)
   292 		fun new_idx () = let val idx = !new in new := idx+1; idx end
   293 		(* prop_formula -> prop_formula *)
   294 		fun
   295 		(* constants *)
   296 		    auxcnf_from_nnf True  = True
   297 		  | auxcnf_from_nnf False = False
   298 		(* literals *)
   299 		  | auxcnf_from_nnf (BoolVar i) = BoolVar i
   300 		  | auxcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
   301 		(* pushing 'or' inside of 'and' using auxiliary variables *)
   302 		  | auxcnf_from_nnf (Or (fm1, fm2)) =
   303 			let
   304 				val fm1' = auxcnf_from_nnf fm1
   305 				val fm2' = auxcnf_from_nnf fm2
   306 				(* prop_formula * prop_formula -> prop_formula *)
   307 				fun auxcnf_or (And (fm11, fm12), fm2) =
   308 					(case fm2 of
   309 					(* do not introduce an auxiliary variable for literals *)
   310 					  BoolVar _ =>
   311 							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
   312 					| Not _ =>
   313 							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
   314 					| _ =>
   315 						let
   316 							val aux = BoolVar (new_idx ())
   317 						in
   318 							And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
   319 						end)
   320 				  | auxcnf_or (fm1, And (fm21, fm22)) =
   321 					(case fm1 of
   322 					(* do not introduce an auxiliary variable for literals *)
   323 					  BoolVar _ =>
   324 							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
   325 					| Not _ =>
   326 							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
   327 					| _ =>
   328 						let
   329 							val aux = BoolVar (new_idx ())
   330 						in
   331 							And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
   332 						end)
   333 				(* neither subformula contains 'and' *)
   334 				  | auxcnf_or (fm1, fm2) =
   335 					Or (fm1, fm2)
   336 			in
   337 				auxcnf_or (fm1', fm2')
   338 			end
   339 		(* 'and' as outermost connective is left untouched *)
   340 		  | auxcnf_from_nnf (And (fm1, fm2)) =
   341 				And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
   342 	in
   343 		auxcnf_from_nnf fm'
   344 	end;
   345 
   346 (* ------------------------------------------------------------------------- *)
   347 (* defcnf: computes the definitional conjunctive normal form of a formula    *)
   348 (*      'fm' of propositional logic, introducing auxiliary variables to      *)
   349 (*      avoid an exponential blowup of the formula.  The result formula is   *)
   350 (*      satisfiable if and only if 'fm' is satisfiable.  Auxiliary variables *)
   351 (*      are introduced as abbreviations for AND-, OR-, and NOT-nodes, based  *)
   352 (*      on the following equisatisfiabilities (+/- indicates polarity):      *)
   353 (*      LITERAL+       == LITERAL                                            *)
   354 (*      LITERAL-       == NOT LITERAL                                        *)
   355 (*      (NOT fm1)+     == aux AND (NOT aux OR fm1-)                          *)
   356 (*      (fm1 OR fm2)+  == aux AND (NOT aux OR fm1+ OR fm2+)                  *)
   357 (*      (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+)    *)
   358 (*      (NOT fm1)-     == aux AND (NOT aux OR fm1+)                          *)
   359 (*      (fm1 OR fm2)-  == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-)    *)
   360 (*      (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-)                  *)
   361 (*      Example:                                                             *)
   362 (*      NOT (a AND b) == aux1 AND (NOT aux1 OR aux2)                         *)
   363 (*                            AND (NOT aux2 OR NOT a OR NOT b)               *)
   364 (* ------------------------------------------------------------------------- *)
   365 
   366 	(* prop_formula -> prop_formula *)
   367 
   368 	fun defcnf fm =
   369 		if is_cnf fm then
   370 			fm
   371 		else let
   372 			(* simplify formula first *)
   373 			val fm' = simplify fm
   374 			(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   375 			(* int ref *)
   376 			val new = ref (maxidx fm' + 1)
   377 			(* unit -> int *)
   378 			fun new_idx () = let val idx = !new in new := idx+1; idx end
   379 			(* optimization for n-ary disjunction/conjunction *)
   380 			(* prop_formula -> prop_formula list *)
   381 			fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
   382 			| disjuncts fm1             = [fm1]
   383 			(* prop_formula -> prop_formula list *)
   384 			fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
   385 			| conjuncts fm1              = [fm1]
   386 			(* polarity -> formula -> (defining clauses, literal) *)
   387 			(* bool -> prop_formula -> prop_formula * prop_formula *)
   388 			fun
   389 			(* constants *)
   390 				defcnf' true  True  = (True, True)
   391 			| defcnf' false True  = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
   392 			| defcnf' true  False = (True, False)
   393 			| defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
   394 			(* literals *)
   395 			| defcnf' true  (BoolVar i)       = (True, BoolVar i)
   396 			| defcnf' false (BoolVar i)       = (True, Not (BoolVar i))
   397 			| defcnf' true  (Not (BoolVar i)) = (True, Not (BoolVar i))
   398 			| defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
   399 			(* 'not' *)
   400 			| defcnf' polarity (Not fm1) =
   401 				let
   402 					val (def1, aux1) = defcnf' (not polarity) fm1
   403 					val aux          = BoolVar (new_idx ())
   404 					val def          = Or (Not aux, aux1)
   405 				in
   406 					(SAnd (def1, def), aux)
   407 				end
   408 			(* 'or' *)
   409 			| defcnf' polarity (Or (fm1, fm2)) =
   410 				let
   411 					val fms          = disjuncts (Or (fm1, fm2))
   412 					val (defs, auxs) = split_list (map (defcnf' polarity) fms)
   413 					val aux          = BoolVar (new_idx ())
   414 					val def          = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
   415 				in
   416 					(SAnd (all defs, def), aux)
   417 				end
   418 			(* 'and' *)
   419 			| defcnf' polarity (And (fm1, fm2)) =
   420 				let
   421 					val fms          = conjuncts (And (fm1, fm2))
   422 					val (defs, auxs) = split_list (map (defcnf' polarity) fms)
   423 					val aux          = BoolVar (new_idx ())
   424 					val def          = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
   425 				in
   426 					(SAnd (all defs, def), aux)
   427 				end
   428 			(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
   429 			(* prop_formula -> prop_formula * prop_formula *)
   430 			fun defcnf_or (Or (fm1, fm2)) =
   431 				let
   432 					val (def1, aux1) = defcnf_or fm1
   433 					val (def2, aux2) = defcnf_or fm2
   434 				in
   435 					(SAnd (def1, def2), Or (aux1, aux2))
   436 				end
   437 			| defcnf_or fm =
   438 				defcnf' true fm
   439 			(* prop_formula -> prop_formula * prop_formula *)
   440 			fun defcnf_and (And (fm1, fm2)) =
   441 				let
   442 					val (def1, aux1) = defcnf_and fm1
   443 					val (def2, aux2) = defcnf_and fm2
   444 				in
   445 					(SAnd (def1, def2), And (aux1, aux2))
   446 				end
   447 			| defcnf_and (Or (fm1, fm2)) =
   448 				let
   449 					val (def1, aux1) = defcnf_or fm1
   450 					val (def2, aux2) = defcnf_or fm2
   451 				in
   452 					(SAnd (def1, def2), Or (aux1, aux2))
   453 				end
   454 			| defcnf_and fm =
   455 				defcnf' true fm
   456 		in
   457 			SAnd (defcnf_and fm')
   458 		end;
   459 
   460 (* ------------------------------------------------------------------------- *)
   461 (* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
   462 (*      truth value of a propositional formula 'fm' is computed              *)
   463 (* ------------------------------------------------------------------------- *)
   464 
   465 	(* (int -> bool) -> prop_formula -> bool *)
   466 
   467 	fun eval a True            = true
   468 	  | eval a False           = false
   469 	  | eval a (BoolVar i)     = (a i)
   470 	  | eval a (Not fm)        = not (eval a fm)
   471 	  | eval a (Or (fm1,fm2))  = (eval a fm1) orelse (eval a fm2)
   472 	  | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
   473 
   474 (* ------------------------------------------------------------------------- *)
   475 (* prop_formula_of_term: returns the propositional structure of a HOL term,  *)
   476 (*      with subterms replaced by Boolean variables.  Also returns a table   *)
   477 (*      of terms and corresponding variables that extends the table that was *)
   478 (*      given as an argument.  Usually, you'll just want to use              *)
   479 (*      'Termtab.empty' as value for 'table'.                                *)
   480 (* ------------------------------------------------------------------------- *)
   481 
   482 (* Note: The implementation is somewhat optimized; the next index to be used *)
   483 (*       is computed only when it is actually needed.  However, when         *)
   484 (*       'prop_formula_of_term' is invoked many times, it might be more      *)
   485 (*       efficient to pass and return this value as an additional parameter, *)
   486 (*       so that it does not have to be recomputed (by folding over the      *)
   487 (*       table) for each invocation.                                         *)
   488 
   489 	(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
   490 	fun prop_formula_of_term t table =
   491 	let
   492 		val next_idx_is_valid = ref false
   493 		val next_idx          = ref 0
   494 		fun get_next_idx () =
   495 			if !next_idx_is_valid then
   496 				inc next_idx
   497 			else (
   498 				next_idx          := Termtab.fold (curry Int.max o snd) table 0;
   499 				next_idx_is_valid := true;
   500 				inc next_idx
   501 			)
   502 		fun aux (Const ("True", _))         table =
   503 			(True, table)
   504 		  | aux (Const ("False", _))        table =
   505 			(False, table)
   506 		  | aux (Const ("Not", _) $ x)      table =
   507 			apfst Not (aux x table)
   508 		  | aux (Const ("op |", _) $ x $ y) table =
   509 			let
   510 				val (fm1, table1) = aux x table
   511 				val (fm2, table2) = aux y table1
   512 			in
   513 				(Or (fm1, fm2), table2)
   514 			end
   515 		  | aux (Const ("op &", _) $ x $ y) table =
   516 			let
   517 				val (fm1, table1) = aux x table
   518 				val (fm2, table2) = aux y table1
   519 			in
   520 				(And (fm1, fm2), table2)
   521 			end
   522 		  | aux x                           table =
   523 			(case Termtab.lookup table x of
   524 			  SOME i =>
   525 				(BoolVar i, table)
   526 			| NONE   =>
   527 				let
   528 					val i = get_next_idx ()
   529 				in
   530 					(BoolVar i, Termtab.update (x, i) table)
   531 				end)
   532 	in
   533 		aux t table
   534 	end;
   535 
   536 (* ------------------------------------------------------------------------- *)
   537 (* term_of_prop_formula: returns a HOL term that corresponds to a            *)
   538 (*      propositional formula, with Boolean variables replaced by Free's     *)
   539 (* ------------------------------------------------------------------------- *)
   540 
   541 (* Note: A more generic implementation should take another argument of type  *)
   542 (*       Term.term Inttab.table (or so) that specifies HOL terms for some    *)
   543 (*       Boolean variables in the formula, similar to 'prop_formula_of_term' *)
   544 (*       (but the other way round).                                          *)
   545 
   546 	(* prop_formula -> Term.term *)
   547 	fun term_of_prop_formula True             =
   548 			HOLogic.true_const
   549 		| term_of_prop_formula False            =
   550 			HOLogic.false_const
   551 		| term_of_prop_formula (BoolVar i)      =
   552 			Free ("v" ^ Int.toString i, HOLogic.boolT)
   553 		| term_of_prop_formula (Not fm)         =
   554 			HOLogic.mk_not (term_of_prop_formula fm)
   555 		| term_of_prop_formula (Or (fm1, fm2))  =
   556 			HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
   557 		| term_of_prop_formula (And (fm1, fm2)) =
   558 			HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
   559 
   560 end;