Index of /users/moore/acl2/v3-3/distrib/acl2-sources/books/arithmetic-2/meta

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[   ] Makefile                24-Nov-2001 11:26  1.5K  
[   ] cancel-terms-helper...> 15-Feb-2007 20:02   10K  
[   ] cancel-terms-meta.lisp  15-Nov-2005 13:44   18K  
[   ] collect-terms-meta.lisp 24-Nov-2001 11:30  5.4K  
[   ] common-meta.lisp        06-Nov-2002 15:05   25K  
[   ] expt-helper.lisp        15-Nov-2005 13:43  2.9K  
[   ] expt.lisp               05-Jan-2003 20:09   11K  
[   ] integerp-meta.lisp      06-Nov-2002 14:33   21K  
[   ] integerp.lisp           06-Nov-2002 14:33  3.2K  
[   ] mini-theories.lisp      15-Nov-2005 13:43  1.9K  
[   ] non-linear.lisp         06-Nov-2002 14:33   13K  
[   ] numerator-and-denomi..> 24-Nov-2001 11:32  2.3K  
[   ] post.lisp               06-Nov-2002 14:33  4.6K  
[   ] pre.lisp                24-Nov-2001 11:33  2.0K  
[   ] top.lisp                06-Nov-2002 14:33  6.0K  


1. Introduction

See top.lisp for a summary of the theories contained in this library
and how to use them.

These books contain a port of some experimental arithmetic libraries
to ACL2 v2-6.  They are, I believe, superior to what had been shipped
with ACL2 in the past; but they have not been extensively tested in
this configuration.  In particular, the original libraries depend upon
some extensions to the linear-arithmetic decision procedure which has
not yet been integrated into the main development branch of ACL2, and
so there may be some unanticipated weaknesses.



2. Overview


Basic Books:

  pre.lisp
  post.lisp 

    These books contain some basic normalization and rewrite rules.

  expt.lisp

    This book contains some simple rules for manipulating expressions
    involving expt.  Most of them should not require any attention from
    the user, but see the comment at the beginning of the book regarding
    strong-expt-rules.

  numerator-and-denominator.lisp

    A small book containing a few rules about numerator and
    denominator.  This book does not pretend to be complete and should
    be expanded.  Suggestions are welcome.

  mini-theories.lisp

    A very small book containing some rules which are occasionally
    useful, but which fit nowhere else.  In particular, the rule
    rewrite-linear-equalities-to-iff should be kept in mind.

  integerp.lisp

    This book contains a set of rules about when a term is or is not an
    integer.  The need for this book reveals a weakness in ACL2's
    type-prescription reasoning.

  non-linear.lisp

    This book contains some rules intended to mitigate the absence of
    the extensions to the linear-arithmetic decision procedure
    mentioned above.  Most of these rules suffer from the
    free-variable problem, but are still useful.

    There is also a set of rules, gathered into the theory
    ratio-theory-of-1.  they are occasionaly useful, but can cause
    thrashing of the linear-arithmetic decision procedure and so are
    disabled by default.



Books with Meta Rules:

  The next four books provide a more complex set of rules for
  manipulating arithmetic expressions.  Extensive use is made of the
  newly augmented meta rules.  They are documented internally,
  but see the regular ACL2 documentaion on meta rules also.

  common-meta.lisp

    This book provides several functions and utilities for the next
    two books.

  collect-terms-meta.lisp

    This book contains some meta-rules which collect "like" terms
    in a sum or product.

  cancel-terms-meta.lisp

    This book contains some meta-rules which cancel "like" terms
    on either side of an (in)equality.

  integerp-meta.lisp

    This book of meta-rules does not depend on the other three books.
    We reccomend this as a first book to look at if you are interested
    in the design and writing of meta functions, rather than just
    there use.  Although the meta rule defined here is more complex
    than the ones in collect-terms-meta.lisp, it is all in one book
    and does not use any macros to generate theorems or functions.


Top:

  top.lisp

    This book gathers all the other books together into one easy to
    include package.  It also contains a list (with descriptions) of
    the various theories and setting available to the user of these
    books and is therefore a useful starting point for exploration.