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