author | nipkow |

Thu Jan 14 14:29:52 1999 +0100 (1999-01-14) | |

changeset 6131 | 2d9e609abcdb |

parent 6130 | 30b84ad2131d |

child 6132 | 6f049245afad |

More Arith.

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