summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 05 Jan 1999 17:30:07 +0100 | |

changeset 6063 | aa2ac7d21792 |

parent 6062 | ede9fea461f5 |

child 6064 | 0786b5afd8ee |

*** empty log message ***

--- a/NEWS Tue Jan 05 17:28:46 1999 +0100 +++ b/NEWS Tue Jan 05 17:30:07 1999 +0100 @@ -11,9 +11,9 @@ *** Proof tools *** * Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision -procedure for linear arithmetic. Currently it is used only for type `nat' in -HOL (see below) but can, should and will be instantiated for other types and -logics as well. +procedure for linear arithmetic. Currently it is used for types `nat' and +`int' in HOL (see below) but can, should and will be instantiated for other +types and logics as well. *** General *** @@ -24,15 +24,23 @@ *** HOL *** -* There are now two decision procedures for linear arithmetic over nat: -1. nat_arith_tac copes with arbitrary propositional formulae (quantified -formulae are treated as atomic) involving `=', `<', `<=', 0, Suc, `+' and `-' -(other operators are treated as atomic). It has to be invoked by hand and is -a little bit slow. -2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it does not do -much propositional reasoning (hence the premises and the conclusion should be -as atomic as possible) and does not know about `-' either. It is fast and is +* There are now decision procedures for linear arithmetic over nat and int: +1. nat_arith_tac copes with arbitrary formulae involving `=', `<', `<=', 0, +Suc, `+' and `-'; other subterms are treated as atomic; subformulae not +involving type `nat' are ignored; quantified subformulae are ignored unless +they are positive universal or negative existential. The tactic has to be +invoked by hand and can be a little bit slow. In particular, the running time +is exponential in the number of occurrences of `-'. +2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it only takes +(negated) (in)equalities among the premises and the conclusion into account +(i.e. no compound formulae) and does not know about `-'. It is fast and is used automatically by the simplifier. +3. int_arith_tac behaves like nat_arith_tac but applies to inequalities over +`int'; it also knows about unary `-'; binary `-' does not cause a blow-up. +4. fast_int_arith_tac is related to int_arith_tac like fast_nat_arith_tac is +related to nat_arith_tac. +NB: At the moment, these decision procedures do not cope with mixed nat/int +formulae such as `m < n ==> int(m) < int(n)'. *** Internal programming interfaces ***