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