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