More Arith.
authornipkow
Thu Jan 14 14:29:52 1999 +0100 (1999-01-14)
changeset 61312d9e609abcdb
parent 6130 30b84ad2131d
child 6132 6f049245afad
More Arith.
NEWS
     1.1 --- a/NEWS	Thu Jan 14 13:20:02 1999 +0100
     1.2 +++ b/NEWS	Thu Jan 14 14:29:52 1999 +0100
     1.3 @@ -30,22 +30,22 @@
     1.4  *** HOL ***
     1.5  
     1.6  * There are now decision procedures for linear arithmetic over nat and int:
     1.7 -1. nat_arith_tac copes with arbitrary formulae involving `=', `<', `<=', 0,
     1.8 -Suc, `+' and `-'; other subterms are treated as atomic; subformulae not
     1.9 -involving type `nat' are ignored; quantified subformulae are ignored unless
    1.10 -they are positive universal or negative existential. The tactic has to be
    1.11 -invoked by hand and can be a little bit slow. In particular, the running time
    1.12 -is exponential in the number of occurrences of `-'.
    1.13 -2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it only takes
    1.14 -(negated) (in)equalities among the premises and the conclusion into account
    1.15 -(i.e. no compound formulae) and does not know about `-'. It is fast and is
    1.16 +
    1.17 +1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
    1.18 +`-', `Suc' and numerical constants; other subterms are treated as atomic;
    1.19 +subformulae not involving type `nat' or `int' are ignored; quantified
    1.20 +subformulae are ignored unless they are positive universal or negative
    1.21 +existential. The tactic has to be invoked by hand and can be a little bit
    1.22 +slow. In particular, the running time is exponential in the number of
    1.23 +occurrences of `-' on `nat'.
    1.24 +
    1.25 +2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
    1.26 +(in)equalities among the premises and the conclusion into account (i.e. no
    1.27 +compound formulae) and does not know about `-' on `nat'. It is fast and is
    1.28  used automatically by the simplifier.
    1.29 -3. int_arith_tac behaves like nat_arith_tac but applies to inequalities over
    1.30 -`int';  it also knows about unary `-'; binary `-' does not cause a blow-up.
    1.31 -4. fast_int_arith_tac is related to int_arith_tac like fast_nat_arith_tac is
    1.32 -related to nat_arith_tac.
    1.33 +
    1.34  NB: At the moment, these decision procedures do not cope with mixed nat/int
    1.35 -formulae such as `m < n ==> int(m) < int(n)'.
    1.36 +formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
    1.37  
    1.38  *** Internal programming interfaces ***
    1.39