+ =====================================================================	+
| LIBRARY	: decision						|
|									|
| DESCRIPTION   : Co-operating decision procedures.			|
|									|
| AUTHOR	: R.J.Boulton						|
| DATE		: 1995							|
|									|
| MODIFIED      : R.J.Boulton						|
| DATE		: 3 September 1996					|
+ =====================================================================	+

The decision library contains co-operating decision procedures for
quantifier-free formulas built up from linear natural number arithmetic,
propositional logic, and the equational theories of pairs, recursive types,
and uninterpreted function symbols. Subterms from other theories may also
be accepted if they do not contribute to the truth of the formula. Formulas
that when placed in prenex normal form contain only universal quantifiers
are accepted in addition to quantifier-free formulas. The procedure is
based on the approach of Nelson and Oppen:

   G. Nelson and D. C. Oppen
   "Simplification by Cooperating Decision Procedures"
   ACM Transactions on Programming Languages and Systems, 1(2):245-257,
   October 1979.

The procedure either proves that the formula is equal to false or raises an
exception. There is some incompleteness in the procedures. Properties of
the natural numbers that depend fundamentally on the discreteness of the
naturals are not proved. Nor are acyclicity properties of recursive types
(e.g. lists). There is also much scope for improvements to the efficiency.

The most important ML structure for the procedure is decisionLib which
contains the following identifiers:

   DECIDE_CONV : conv
   DECIDE : term -> thm
   DECIDE_TAC : tactic
   DECISION_TAC : conv -> (term -> bool) -> tactic
   show_proving : bool ref

(The type `conv' is an abbreviation for `term -> thm'.)

DECIDE_CONV is the main decision procedure. It takes a term t and attempts
to prove the theorem |- t = T, where T is the truth value true. DECIDE is a
variant of DECIDE_CONV that proves |- t instead of |- t = T.

DECIDE_TAC is a tactic that uses DECIDE_CONV to attempt to prove the
conclusion of the current goal in the context of any assumptions that are
free of lambda abstractions (and hence of quantifiers). To select different
assumptions use `DECISION_TAC DECIDE_CONV p' where p is a predicate that
returns true when applied to the required assumptions.

The procedure normalizes the negation of the formula to be proved and then
attempts to prove that the result is false. To see the formulas the
procedure is trying to refute and the equations between variables that are
exchanged by the component procedures, set the reference variable
show_proving to true.

Initially lists are the only recursive type handled by the procedure, but
it may be extended to handle the equational theories of types defined using
the HOL define_type function, including selectors (e.g. HD and TL for lists)
and discriminators (e.g. NULL) defined for such types. Amongst others, the
structure DecideTypes contains the following identifiers:

   add_type : thm HOLTypeInfo.hol_type_info -> unit
   delete_type : string -> unit

The function add_type extends the decision procedure with a new type. The
function delete_type removes the named type from the procedure. The type
information required by add_type can be obtained using the following
function in the structure HOLTypeInfo:

   define_type_info : {name : string,
                       type_spec : term frag list,
                       fixities : fixity list,
                       selectors : (string * string list) list,
                       discriminators : (string * string) list}
                      -> thm hol_type_info

The fields `name', `type_spec', and `fixities' of the argument are identical
to those of the HOL define_type function. The other fields specify the names
of the selector and discriminator functions. Each is a list of pairs in
which the first component should be the name of one of the constructors.

The function assumes that there are no selectors for a constructor that
doesn't appear in the list, so it is not necessary to include an entry for
a nullary constructor. For other constructors there must be one selector
name for each argument and they should be given in the correct order. The
function ignores any item in the list with a constructor name that does not
belong to the type. The discriminators are optional. The constructor,
selector and discriminator names must all be distinct.

Here is an example, a type of Lisp s-expressions:

   define_type_info
      {name = "sexp",
       type_spec = `sexp = Nil | Atom of 'a | Cons of sexp => sexp`,
       fixities = [Prefix,Prefix,Prefix],
       selectors = [("Atom",["Tok"]),("Cons",["Car","Cdr"])],
       discriminators = [("Nil","Nilp"),("Atom","Atomp"),("Cons","Consp")]};

Ideally, define_type_info should be used in place of define_type. It then
defines the type and the selectors and discriminators, and returns the type
information required by the decision procedure. 

For details of the implementation of the decision procedure, see the
following paper:

   R. J. Boulton
   "Combining Decision Procedures in the HOL System"
   In E. T. Schubert, P. J. Windley and J. Alves-Foss (editors),
   "Proceedings of the 8th International Workshop on Higher Order Logic
    Theorem Proving and Its Applications", Aspen Grove, UT, USA,
   September 1995, pages 75-89. Volume 971 of Lecture Notes in Computer
   Science, Springer-Verlag.

Some examples can be found in the file examples.sml in this directory.