1(*  Title:      HOL/Tools/prop_logic.ML
2    Author:     Tjark Weber
3    Copyright   2004-2009
4
5Formulas of propositional logic.
6*)
7
8signature PROP_LOGIC =
9sig
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
18  val SNot: prop_formula -> prop_formula
19  val SOr: prop_formula * prop_formula -> prop_formula
20  val SAnd: prop_formula * prop_formula -> prop_formula
21  val simplify: prop_formula -> prop_formula  (* eliminates True/False and double-negation *)
22
23  val indices: prop_formula -> int list  (* set of all variable indices *)
24  val maxidx: prop_formula -> int       (* maximal variable index *)
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
30  val is_nnf: prop_formula -> bool  (* returns true iff the formula is in negation normal form *)
31  val is_cnf: prop_formula -> bool  (* returns true iff the formula is in conjunctive normal form *)
32
33  val nnf: prop_formula -> prop_formula  (* negation normal form *)
34  val cnf: prop_formula -> prop_formula  (* conjunctive normal form *)
35  val defcnf: prop_formula -> prop_formula  (* definitional cnf *)
36
37  val eval: (int -> bool) -> prop_formula -> bool  (* semantics *)
38
39  (* propositional representation of HOL terms *)
40  val prop_formula_of_term: term -> int Termtab.table -> prop_formula * int Termtab.table
41  (* HOL term representation of propositional formulae *)
42  val term_of_prop_formula: prop_formula -> term
43end;
44
45structure Prop_Logic : PROP_LOGIC =
46struct
47
48(* ------------------------------------------------------------------------- *)
49(* prop_formula: formulas of propositional logic, built from Boolean         *)
50(*               variables (referred to by index) and True/False using       *)
51(*               not/or/and                                                  *)
52(* ------------------------------------------------------------------------- *)
53
54datatype 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 double-negation elimination.                                      *)
66(* ------------------------------------------------------------------------- *)
67
68fun SNot True = False
69  | SNot False = True
70  | SNot (Not fm) = fm
71  | SNot fm = Not fm;
72
73fun SOr (True, _) = True
74  | SOr (_, True) = True
75  | SOr (False, fm) = fm
76  | SOr (fm, False) = fm
77  | SOr (fm1, fm2) = Or (fm1, fm2);
78
79fun SAnd (True, fm) = fm
80  | SAnd (fm, True) = fm
81  | SAnd (False, _) = False
82  | SAnd (_, False) = False
83  | SAnd (fm1, fm2) = And (fm1, fm2);
84
85(* ------------------------------------------------------------------------- *)
86(* simplify: eliminates True/False below other connectives, and double-      *)
87(*      negation                                                             *)
88(* ------------------------------------------------------------------------- *)
89
90fun simplify (Not fm) = SNot (simplify fm)
91  | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2)
92  | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
93  | simplify fm = fm;
94
95(* ------------------------------------------------------------------------- *)
96(* indices: collects all indices of Boolean variables that occur in a        *)
97(*      propositional formula 'fm'; no duplicates                            *)
98(* ------------------------------------------------------------------------- *)
99
100fun indices True = []
101  | indices False = []
102  | indices (BoolVar i) = [i]
103  | indices (Not fm) = indices fm
104  | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2)
105  | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2);
106
107(* ------------------------------------------------------------------------- *)
108(* maxidx: computes the maximal variable index occurring in a formula of     *)
109(*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
110(* ------------------------------------------------------------------------- *)
111
112fun maxidx True = 0
113  | maxidx False = 0
114  | maxidx (BoolVar i) = i
115  | maxidx (Not fm) = maxidx fm
116  | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2)
117  | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
118
119(* ------------------------------------------------------------------------- *)
120(* exists: computes the disjunction over a list 'xs' of propositional        *)
121(*      formulas                                                             *)
122(* ------------------------------------------------------------------------- *)
123
124fun exists xs = Library.foldl SOr (False, xs);
125
126(* ------------------------------------------------------------------------- *)
127(* all: computes the conjunction over a list 'xs' of propositional formulas  *)
128(* ------------------------------------------------------------------------- *)
129
130fun all xs = Library.foldl SAnd (True, xs);
131
132(* ------------------------------------------------------------------------- *)
133(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
134(* ------------------------------------------------------------------------- *)
135
136fun dot_product (xs, ys) = exists (map SAnd (xs ~~ ys));
137
138(* ------------------------------------------------------------------------- *)
139(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e.,  *)
140(*         only variables may be negated, but not subformulas).              *)
141(* ------------------------------------------------------------------------- *)
142
143local
144  fun is_literal (BoolVar _) = true
145    | is_literal (Not (BoolVar _)) = true
146    | is_literal _ = false
147  fun is_conj_disj (Or (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2
148    | is_conj_disj (And (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2
149    | is_conj_disj fm = is_literal fm
150in
151  fun is_nnf True = true
152    | is_nnf False = true
153    | is_nnf fm = is_conj_disj fm
154end;
155
156(* ------------------------------------------------------------------------- *)
157(* is_cnf: returns 'true' iff the formula is in conjunctive normal form      *)
158(*         (i.e., a conjunction of disjunctions of literals). 'is_cnf'       *)
159(*         implies 'is_nnf'.                                                 *)
160(* ------------------------------------------------------------------------- *)
161
162local
163  fun is_literal (BoolVar _) = true
164    | is_literal (Not (BoolVar _)) = true
165    | is_literal _ = false
166  fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2
167    | is_disj fm = is_literal fm
168  fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2
169    | is_conj fm = is_disj fm
170in
171  fun is_cnf True = true
172    | is_cnf False = true
173    | is_cnf fm = is_conj fm
174end;
175
176(* ------------------------------------------------------------------------- *)
177(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
178(*      logic (i.e., only variables may be negated, but not subformulas).    *)
179(*      Simplification (cf. 'simplify') is performed as well. Not            *)
180(*      surprisingly, 'is_nnf o nnf' always returns 'true'. 'nnf fm' returns *)
181(*      'fm' if (and only if) 'is_nnf fm' returns 'true'.                    *)
182(* ------------------------------------------------------------------------- *)
183
184fun nnf fm =
185  let
186    fun
187      (* constants *)
188        nnf_aux True = True
189      | nnf_aux False = False
190      (* variables *)
191      | nnf_aux (BoolVar i) = (BoolVar i)
192      (* 'or' and 'and' as outermost connectives are left untouched *)
193      | nnf_aux (Or  (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2)
194      | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2)
195      (* 'not' + constant *)
196      | nnf_aux (Not True) = False
197      | nnf_aux (Not False) = True
198      (* 'not' + variable *)
199      | nnf_aux (Not (BoolVar i)) = Not (BoolVar i)
200      (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
201      | nnf_aux (Not (Or  (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
202      | nnf_aux (Not (And (fm1, fm2))) = SOr  (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
203      (* double-negation elimination *)
204      | nnf_aux (Not (Not fm)) = nnf_aux fm
205  in
206    if is_nnf fm then fm
207    else nnf_aux fm
208  end;
209
210(* ------------------------------------------------------------------------- *)
211(* cnf: computes the conjunctive normal form (i.e., a conjunction of         *)
212(*      disjunctions of literals) of a formula 'fm' of propositional logic.  *)
213(*      Simplification (cf. 'simplify') is performed as well. The result     *)
214(*      is equivalent to 'fm', but may be exponentially longer. Not          *)
215(*      surprisingly, 'is_cnf o cnf' always returns 'true'. 'cnf fm' returns *)
216(*      'fm' if (and only if) 'is_cnf fm' returns 'true'.                    *)
217(* ------------------------------------------------------------------------- *)
218
219fun cnf fm =
220  let
221    (* function to push an 'Or' below 'And's, using distributive laws *)
222    fun cnf_or (And (fm11, fm12), fm2) =
223          And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
224      | cnf_or (fm1, And (fm21, fm22)) =
225          And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
226    (* neither subformula contains 'And' *)
227      | cnf_or (fm1, fm2) = Or (fm1, fm2)
228    fun cnf_from_nnf True = True
229      | cnf_from_nnf False = False
230      | cnf_from_nnf (BoolVar i) = BoolVar i
231    (* 'fm' must be a variable since the formula is in NNF *)
232      | cnf_from_nnf (Not fm) = Not fm
233    (* 'Or' may need to be pushed below 'And' *)
234      | cnf_from_nnf (Or (fm1, fm2)) =
235        cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
236    (* 'And' as outermost connective is left untouched *)
237      | cnf_from_nnf (And (fm1, fm2)) =
238        And (cnf_from_nnf fm1, cnf_from_nnf fm2)
239  in
240    if is_cnf fm then fm
241    else (cnf_from_nnf o nnf) fm
242  end;
243
244(* ------------------------------------------------------------------------- *)
245(* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *)
246(*      of propositional logic. Simplification (cf. 'simplify') is performed *)
247(*      as well. 'defcnf' may introduce auxiliary Boolean variables to avoid *)
248(*      an exponential blowup of the formula.  The result is equisatisfiable *)
249(*      (i.e., satisfiable if and only if 'fm' is satisfiable), but not      *)
250(*      necessarily equivalent to 'fm'. Not surprisingly, 'is_cnf o defcnf'  *)
251(*      always returns 'true'. 'defcnf fm' returns 'fm' if (and only if)     *)
252(*      'is_cnf fm' returns 'true'.                                          *)
253(* ------------------------------------------------------------------------- *)
254
255fun defcnf fm =
256  if is_cnf fm then fm
257  else
258    let
259      val fm' = nnf fm
260      (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
261      val new = Unsynchronized.ref (maxidx fm' + 1)
262      fun new_idx () = let val idx = !new in new := idx+1; idx end
263      (* replaces 'And' by an auxiliary variable (and its definition) *)
264      fun defcnf_or (And x) =
265            let
266              val i = new_idx ()
267            in
268              (* Note that definitions are in NNF, but not CNF. *)
269              (BoolVar i, [Or (Not (BoolVar i), And x)])
270            end
271        | defcnf_or (Or (fm1, fm2)) =
272            let
273              val (fm1', defs1) = defcnf_or fm1
274              val (fm2', defs2) = defcnf_or fm2
275            in
276              (Or (fm1', fm2'), defs1 @ defs2)
277            end
278        | defcnf_or fm = (fm, [])
279      fun defcnf_from_nnf True = True
280        | defcnf_from_nnf False = False
281        | defcnf_from_nnf (BoolVar i) = BoolVar i
282      (* 'fm' must be a variable since the formula is in NNF *)
283        | defcnf_from_nnf (Not fm) = Not fm
284      (* 'Or' may need to be pushed below 'And' *)
285      (* 'Or' of literal and 'And': use distributivity *)
286        | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) =
287            And (defcnf_from_nnf (Or (BoolVar i, fm1)),
288                 defcnf_from_nnf (Or (BoolVar i, fm2)))
289        | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) =
290            And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)),
291                 defcnf_from_nnf (Or (Not (BoolVar i), fm2)))
292        | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) =
293            And (defcnf_from_nnf (Or (fm1, BoolVar i)),
294                 defcnf_from_nnf (Or (fm2, BoolVar i)))
295        | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) =
296            And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))),
297                 defcnf_from_nnf (Or (fm2, Not (BoolVar i))))
298      (* all other cases: turn the formula into a disjunction of literals, *)
299      (*                  adding definitions as necessary                  *)
300        | defcnf_from_nnf (Or x) =
301            let
302              val (fm, defs) = defcnf_or (Or x)
303              val cnf_defs = map defcnf_from_nnf defs
304            in
305              all (fm :: cnf_defs)
306            end
307      (* 'And' as outermost connective is left untouched *)
308        | defcnf_from_nnf (And (fm1, fm2)) =
309            And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
310    in
311      defcnf_from_nnf fm'
312    end;
313
314(* ------------------------------------------------------------------------- *)
315(* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
316(*      truth value of a propositional formula 'fm' is computed              *)
317(* ------------------------------------------------------------------------- *)
318
319fun eval _ True = true
320  | eval _ False = false
321  | eval a (BoolVar i) = (a i)
322  | eval a (Not fm) = not (eval a fm)
323  | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2)
324  | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2);
325
326(* ------------------------------------------------------------------------- *)
327(* prop_formula_of_term: returns the propositional structure of a HOL term,  *)
328(*      with subterms replaced by Boolean variables.  Also returns a table   *)
329(*      of terms and corresponding variables that extends the table that was *)
330(*      given as an argument.  Usually, you'll just want to use              *)
331(*      'Termtab.empty' as value for 'table'.                                *)
332(* ------------------------------------------------------------------------- *)
333
334(* Note: The implementation is somewhat optimized; the next index to be used *)
335(*       is computed only when it is actually needed.  However, when         *)
336(*       'prop_formula_of_term' is invoked many times, it might be more      *)
337(*       efficient to pass and return this value as an additional parameter, *)
338(*       so that it does not have to be recomputed (by folding over the      *)
339(*       table) for each invocation.                                         *)
340
341fun prop_formula_of_term t table =
342  let
343    val next_idx_is_valid = Unsynchronized.ref false
344    val next_idx = Unsynchronized.ref 0
345    fun get_next_idx () =
346      if !next_idx_is_valid then
347        Unsynchronized.inc next_idx
348      else (
349        next_idx := Termtab.fold (Integer.max o snd) table 0;
350        next_idx_is_valid := true;
351        Unsynchronized.inc next_idx
352      )
353    fun aux (Const (\<^const_name>\<open>True\<close>, _)) table = (True, table)
354      | aux (Const (\<^const_name>\<open>False\<close>, _)) table = (False, table)
355      | aux (Const (\<^const_name>\<open>Not\<close>, _) $ x) table = apfst Not (aux x table)
356      | aux (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ x $ y) table =
357          let
358            val (fm1, table1) = aux x table
359            val (fm2, table2) = aux y table1
360          in
361            (Or (fm1, fm2), table2)
362          end
363      | aux (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ x $ y) table =
364          let
365            val (fm1, table1) = aux x table
366            val (fm2, table2) = aux y table1
367          in
368            (And (fm1, fm2), table2)
369          end
370      | aux x table =
371          (case Termtab.lookup table x of
372            SOME i => (BoolVar i, table)
373          | NONE =>
374              let
375                val i = get_next_idx ()
376              in
377                (BoolVar i, Termtab.update (x, i) table)
378              end)
379  in
380    aux t table
381  end;
382
383(* ------------------------------------------------------------------------- *)
384(* term_of_prop_formula: returns a HOL term that corresponds to a            *)
385(*      propositional formula, with Boolean variables replaced by Free's     *)
386(* ------------------------------------------------------------------------- *)
387
388(* Note: A more generic implementation should take another argument of type  *)
389(*       Term.term Inttab.table (or so) that specifies HOL terms for some    *)
390(*       Boolean variables in the formula, similar to 'prop_formula_of_term' *)
391(*       (but the other way round).                                          *)
392
393fun term_of_prop_formula True = \<^term>\<open>True\<close>
394  | term_of_prop_formula False = \<^term>\<open>False\<close>
395  | term_of_prop_formula (BoolVar i) = Free ("v" ^ string_of_int i, HOLogic.boolT)
396  | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm)
397  | term_of_prop_formula (Or (fm1, fm2)) =
398      HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
399  | term_of_prop_formula (And (fm1, fm2)) =
400      HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
401
402end;
403