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