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

author | nipkow |

Thu, 14 Jan 1999 14:29:52 +0100 | |

changeset 6131 | 2d9e609abcdb |

parent 6130 | 30b84ad2131d |

child 6132 | 6f049245afad |

More Arith.

--- a/NEWS Thu Jan 14 13:20:02 1999 +0100 +++ b/NEWS Thu Jan 14 14:29:52 1999 +0100 @@ -30,22 +30,22 @@ *** HOL *** * 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 + +1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+', +`-', `Suc' and numerical constants; other subterms are treated as atomic; +subformulae not involving type `nat' or `int' 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 `-' on `nat'. + +2. fast_arith_tac is a cut-down version of 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 `-' on `nat'. 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)'. +formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'. *** Internal programming interfaces ***