author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 33243  17014b1b9353 
child 38549  d0385f2764d8 
permissions  rwrr 
14452  1 
(* Title: HOL/Tools/prop_logic.ML 
2 
Author: Tjark Weber 

31220  3 
Copyright 20042009 
14452  4 

5 
Formulas of propositional logic. 

6 
*) 

7 

8 
signature PROP_LOGIC = 

9 
sig 

10 
datatype prop_formula = 

11 
True 

12 
 False 

13 
 BoolVar of int (* NOTE: only use indices >= 1 *) 

14 
 Not of prop_formula 

15 
 Or of prop_formula * prop_formula 

16 
 And of prop_formula * prop_formula 

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 doublenegation *) 
14452  22 

14681  23 
val indices : prop_formula > int list (* set of all variable indices *) 
15301  24 
val maxidx : prop_formula > int (* maximal variable index *) 
14452  25 

26 
val exists : prop_formula list > prop_formula (* finite disjunction *) 

27 
val all : prop_formula list > prop_formula (* finite conjunction *) 

28 
val dot_product : prop_formula list * prop_formula list > prop_formula 

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  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  39 
(* propositional representation of HOL terms *) 
33243  40 
val prop_formula_of_term : term > int Termtab.table > prop_formula * int Termtab.table 
20442  41 
(* HOL term representation of propositional formulae *) 
33243  42 
val term_of_prop_formula : prop_formula > term 
14452  43 
end; 
44 

45 
structure PropLogic : PROP_LOGIC = 

46 
struct 

47 

48 
(*  *) 

14753  49 
(* prop_formula: formulas of propositional logic, built from Boolean *) 
14452  50 
(* variables (referred to by index) and True/False using *) 
51 
(* not/or/and *) 

52 
(*  *) 

53 

54 
datatype prop_formula = 

55 
True 

56 
 False 

57 
 BoolVar of int (* NOTE: only use indices >= 1 *) 

58 
 Not of prop_formula 

59 
 Or of prop_formula * prop_formula 

60 
 And of prop_formula * prop_formula; 

61 

62 
(*  *) 

63 
(* The following constructor functions make sure that True and False do not *) 

64 
(* occur within any of the other connectives (i.e. Not, Or, And), and *) 

65 
(* perform doublenegation elimination. *) 

66 
(*  *) 

67 

68 
(* prop_formula > prop_formula *) 

69 

70 
fun SNot True = False 

71 
 SNot False = True 

72 
 SNot (Not fm) = fm 

73 
 SNot fm = Not fm; 

74 

75 
(* prop_formula * prop_formula > prop_formula *) 

76 

77 
fun SOr (True, _) = True 

78 
 SOr (_, True) = True 

79 
 SOr (False, fm) = fm 

80 
 SOr (fm, False) = fm 

81 
 SOr (fm1, fm2) = Or (fm1, fm2); 

82 

83 
(* prop_formula * prop_formula > prop_formula *) 

84 

85 
fun SAnd (True, fm) = fm 

86 
 SAnd (fm, True) = fm 

87 
 SAnd (False, _) = False 

88 
 SAnd (_, False) = False 

89 
 SAnd (fm1, fm2) = And (fm1, fm2); 

90 

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  104 
(* indices: collects all indices of Boolean variables that occur in a *) 
14452  105 
(* propositional formula 'fm'; no duplicates *) 
106 
(*  *) 

107 

108 
(* prop_formula > int list *) 

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  114 
 indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) 
115 
 indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); 

14452  116 

117 
(*  *) 

118 
(* maxidx: computes the maximal variable index occuring in a formula of *) 

119 
(* propositional logic 'fm'; 0 if 'fm' contains no variable *) 

120 
(*  *) 

121 

122 
(* prop_formula > int *) 

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  155 

156 
(*  *) 

31220  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  179 
(* (i.e., a conjunction of disjunctions of literals). 'is_cnf' *) 
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  198 
(* nnf: computes the negation normal form of a formula 'fm' of propositional *) 
31220  199 
(* logic (i.e., only variables may be negated, but not subformulas). *) 
200 
(* Simplification (cf. 'simplify') is performed as well. Not *) 

201 
(* surprisingly, 'is_nnf o nnf' always returns 'true'. 'nnf fm' returns *) 

202 
(* 'fm' if (and only if) 'is_nnf fm' returns 'true'. *) 

14452  203 
(*  *) 
204 

205 
(* prop_formula > prop_formula *) 

206 

31220  207 
fun nnf fm = 
208 
let 

209 
fun 

210 
(* constants *) 

211 
nnf_aux True = True 

212 
 nnf_aux False = False 

213 
(* variables *) 

214 
 nnf_aux (BoolVar i) = (BoolVar i) 

215 
(* 'or' and 'and' as outermost connectives are left untouched *) 

216 
 nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2) 

217 
 nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2) 

218 
(* 'not' + constant *) 

219 
 nnf_aux (Not True) = False 

220 
 nnf_aux (Not False) = True 

221 
(* 'not' + variable *) 

222 
 nnf_aux (Not (BoolVar i)) = Not (BoolVar i) 

223 
(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) 

224 
 nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) 

225 
 nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) 

226 
(* doublenegation elimination *) 

227 
 nnf_aux (Not (Not fm)) = nnf_aux fm 

228 
in 

229 
if is_nnf fm then 

230 
fm 

231 
else 

232 
nnf_aux fm 

233 
end; 

14452  234 

235 
(*  *) 

31220  236 
(* cnf: computes the conjunctive normal form (i.e., a conjunction of *) 
237 
(* disjunctions of literals) of a formula 'fm' of propositional logic. *) 

238 
(* Simplification (cf. 'simplify') is performed as well. The result *) 

239 
(* is equivalent to 'fm', but may be exponentially longer. Not *) 

240 
(* surprisingly, 'is_cnf o cnf' always returns 'true'. 'cnf fm' returns *) 

241 
(* 'fm' if (and only if) 'is_cnf fm' returns 'true'. *) 

14452  242 
(*  *) 
243 

244 
(* prop_formula > prop_formula *) 

245 

246 
fun cnf fm = 

247 
let 

31220  248 
(* function to push an 'Or' below 'And's, using distributive laws *) 
249 
fun cnf_or (And (fm11, fm12), fm2) = 

250 
And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) 

251 
 cnf_or (fm1, And (fm21, fm22)) = 

252 
And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) 

253 
(* neither subformula contains 'And' *) 

254 
 cnf_or (fm1, fm2) = 

255 
Or (fm1, fm2) 

256 
fun cnf_from_nnf True = True 

14939  257 
 cnf_from_nnf False = False 
258 
 cnf_from_nnf (BoolVar i) = BoolVar i 

31220  259 
(* 'fm' must be a variable since the formula is in NNF *) 
260 
 cnf_from_nnf (Not fm) = Not fm 

261 
(* 'Or' may need to be pushed below 'And' *) 

14939  262 
 cnf_from_nnf (Or (fm1, fm2)) = 
31220  263 
cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) 
264 
(* 'And' as outermost connective is left untouched *) 

265 
 cnf_from_nnf (And (fm1, fm2)) = 

266 
And (cnf_from_nnf fm1, cnf_from_nnf fm2) 

14452  267 
in 
31220  268 
if is_cnf fm then 
269 
fm 

270 
else 

271 
(cnf_from_nnf o nnf) fm 

14452  272 
end; 
273 

274 
(*  *) 

31220  275 
(* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *) 
276 
(* of propositional logic. Simplification (cf. 'simplify') is performed *) 

277 
(* as well. 'defcnf' may introduce auxiliary Boolean variables to avoid *) 

278 
(* an exponential blowup of the formula. The result is equisatisfiable *) 

279 
(* (i.e., satisfiable if and only if 'fm' is satisfiable), but not *) 

280 
(* necessarily equivalent to 'fm'. Not surprisingly, 'is_cnf o defcnf' *) 

281 
(* always returns 'true'. 'defcnf fm' returns 'fm' if (and only if) *) 

282 
(* 'is_cnf fm' returns 'true'. *) 

14452  283 
(*  *) 
284 

16909
acbc7a9c3864
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents:
16907
diff
changeset

285 
(* prop_formula > prop_formula *) 
14452  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  290 
else 
291 
let 

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  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  298 
(* replaces 'And' by an auxiliary variable (and its definition) *) 
299 
(* prop_formula > prop_formula * prop_formula list *) 

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  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  304 
(* Note that definitions are in NNF, but not CNF. *) 
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  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  309 
val (fm1', defs1) = defcnf_or fm1 
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  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  314 
 defcnf_or fm = 
315 
(fm, []) 

316 
(* prop_formula > prop_formula *) 

317 
fun defcnf_from_nnf True = True 

318 
 defcnf_from_nnf False = False 

319 
 defcnf_from_nnf (BoolVar i) = BoolVar i 

320 
(* 'fm' must be a variable since the formula is in NNF *) 

321 
 defcnf_from_nnf (Not fm) = Not fm 

322 
(* 'Or' may need to be pushed below 'And' *) 

323 
(* 'Or' of literal and 'And': use distributivity *) 

324 
 defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) = 

325 
And (defcnf_from_nnf (Or (BoolVar i, fm1)), 

326 
defcnf_from_nnf (Or (BoolVar i, fm2))) 

327 
 defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) = 

328 
And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)), 

329 
defcnf_from_nnf (Or (Not (BoolVar i), fm2))) 

330 
 defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) = 

331 
And (defcnf_from_nnf (Or (fm1, BoolVar i)), 

332 
defcnf_from_nnf (Or (fm2, BoolVar i))) 

333 
 defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) = 

334 
And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))), 

335 
defcnf_from_nnf (Or (fm2, Not (BoolVar i)))) 

336 
(* all other cases: turn the formula into a disjunction of literals, *) 

337 
(* adding definitions as necessary *) 

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  340 
val (fm, defs) = defcnf_or (Or x) 
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  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  345 
(* 'And' as outermost connective is left untouched *) 
346 
 defcnf_from_nnf (And (fm1, fm2)) = 

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  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  351 

352 
(*  *) 

14753  353 
(* eval: given an assignment 'a' of Boolean values to variable indices, the *) 
14452  354 
(* truth value of a propositional formula 'fm' is computed *) 
355 
(*  *) 

356 

357 
(* (int > bool) > prop_formula > bool *) 

358 

359 
fun eval a True = true 

360 
 eval a False = false 

361 
 eval a (BoolVar i) = (a i) 

362 
 eval a (Not fm) = not (eval a fm) 

363 
 eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2) 

364 
 eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2); 

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  384 
val next_idx_is_valid = Unsynchronized.ref false 
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  388 
Unsynchronized.inc next_idx 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
16913
diff
changeset

389 
else ( 
33029  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  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  428 
(*  *) 
429 
(* term_of_prop_formula: returns a HOL term that corresponds to a *) 

430 
(* propositional formula, with Boolean variables replaced by Free's *) 

431 
(*  *) 

432 

433 
(* Note: A more generic implementation should take another argument of type *) 

434 
(* Term.term Inttab.table (or so) that specifies HOL terms for some *) 

435 
(* Boolean variables in the formula, similar to 'prop_formula_of_term' *) 

436 
(* (but the other way round). *) 

437 

438 
(* prop_formula > Term.term *) 

439 
fun term_of_prop_formula True = 

31220  440 
HOLogic.true_const 
441 
 term_of_prop_formula False = 

442 
HOLogic.false_const 

443 
 term_of_prop_formula (BoolVar i) = 

444 
Free ("v" ^ Int.toString i, HOLogic.boolT) 

445 
 term_of_prop_formula (Not fm) = 

446 
HOLogic.mk_not (term_of_prop_formula fm) 

447 
 term_of_prop_formula (Or (fm1, fm2)) = 

448 
HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) 

449 
 term_of_prop_formula (And (fm1, fm2)) = 

450 
HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); 

20442  451 

14452  452 
end; 