src/HOL/Tools/prop_logic.ML
author blanchet
Fri Sep 12 11:16:47 2014 +0200 (2014-09-12)
changeset 58322 f13f6e27d68e
parent 55436 9781e17dcc23
child 61332 22378817612f
permissions -rw-r--r--
fixed spellings
     1 (*  Title:      HOL/Tools/prop_logic.ML
     2     Author:     Tjark Weber
     3     Copyright   2004-2009
     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 
    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
    43 end;
    44 
    45 structure Prop_Logic : PROP_LOGIC =
    46 struct
    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 
    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 double-negation elimination.                                      *)
    66 (* ------------------------------------------------------------------------- *)
    67 
    68 fun SNot True = False
    69   | SNot False = True
    70   | SNot (Not fm) = fm
    71   | SNot fm = Not fm;
    72 
    73 fun 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 
    79 fun 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 
    90 fun 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 
   100 fun 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 
   112 fun 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 
   124 fun exists xs = Library.foldl SOr (False, xs);
   125 
   126 (* ------------------------------------------------------------------------- *)
   127 (* all: computes the conjunction over a list 'xs' of propositional formulas  *)
   128 (* ------------------------------------------------------------------------- *)
   129 
   130 fun all xs = Library.foldl SAnd (True, xs);
   131 
   132 (* ------------------------------------------------------------------------- *)
   133 (* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
   134 (* ------------------------------------------------------------------------- *)
   135 
   136 fun 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 
   143 local
   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
   150 in
   151   fun is_nnf True = true
   152     | is_nnf False = true
   153     | is_nnf fm = is_conj_disj fm
   154 end;
   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 
   162 local
   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
   170 in
   171   fun is_cnf True = true
   172     | is_cnf False = true
   173     | is_cnf fm = is_conj fm
   174 end;
   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 
   184 fun 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 
   219 fun 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 
   255 fun 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 
   319 fun eval a True = true
   320   | eval a 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 
   341 fun 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 True}, _)) table = (True, table)
   354       | aux (Const (@{const_name False}, _)) table = (False, table)
   355       | aux (Const (@{const_name Not}, _) $ x) table = apfst Not (aux x table)
   356       | aux (Const (@{const_name HOL.disj}, _) $ 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 HOL.conj}, _) $ 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 
   393 fun term_of_prop_formula True = @{term True}
   394   | term_of_prop_formula False = @{term False}
   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 
   402 end;