9 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement |
9 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement |
10 |
10 |
11 *** Proof tools *** |
11 *** Proof tools *** |
12 |
12 |
13 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision |
13 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision |
14 procedure for linear arithmetic. Currently it is used only for type `nat' in |
14 procedure for linear arithmetic. Currently it is used for types `nat' and |
15 HOL (see below) but can, should and will be instantiated for other types and |
15 `int' in HOL (see below) but can, should and will be instantiated for other |
16 logics as well. |
16 types and logics as well. |
17 |
17 |
18 *** General *** |
18 *** General *** |
19 |
19 |
20 * in locales, the "assumes" and "defines" parts may be omitted if empty; |
20 * in locales, the "assumes" and "defines" parts may be omitted if empty; |
21 |
21 |
22 * new print_mode "xsymbols" for extended symbol support |
22 * new print_mode "xsymbols" for extended symbol support |
23 (e.g. genuiely long arrows) |
23 (e.g. genuiely long arrows) |
24 |
24 |
25 *** HOL *** |
25 *** HOL *** |
26 |
26 |
27 * There are now two decision procedures for linear arithmetic over nat: |
27 * There are now decision procedures for linear arithmetic over nat and int: |
28 1. nat_arith_tac copes with arbitrary propositional formulae (quantified |
28 1. nat_arith_tac copes with arbitrary formulae involving `=', `<', `<=', 0, |
29 formulae are treated as atomic) involving `=', `<', `<=', 0, Suc, `+' and `-' |
29 Suc, `+' and `-'; other subterms are treated as atomic; subformulae not |
30 (other operators are treated as atomic). It has to be invoked by hand and is |
30 involving type `nat' are ignored; quantified subformulae are ignored unless |
31 a little bit slow. |
31 they are positive universal or negative existential. The tactic has to be |
32 2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it does not do |
32 invoked by hand and can be a little bit slow. In particular, the running time |
33 much propositional reasoning (hence the premises and the conclusion should be |
33 is exponential in the number of occurrences of `-'. |
34 as atomic as possible) and does not know about `-' either. It is fast and is |
34 2. fast_nat_arith_tac is a cut-down version of nat_arith_tac: it only takes |
|
35 (negated) (in)equalities among the premises and the conclusion into account |
|
36 (i.e. no compound formulae) and does not know about `-'. It is fast and is |
35 used automatically by the simplifier. |
37 used automatically by the simplifier. |
|
38 3. int_arith_tac behaves like nat_arith_tac but applies to inequalities over |
|
39 `int'; it also knows about unary `-'; binary `-' does not cause a blow-up. |
|
40 4. fast_int_arith_tac is related to int_arith_tac like fast_nat_arith_tac is |
|
41 related to nat_arith_tac. |
|
42 NB: At the moment, these decision procedures do not cope with mixed nat/int |
|
43 formulae such as `m < n ==> int(m) < int(n)'. |
36 |
44 |
37 *** Internal programming interfaces *** |
45 *** Internal programming interfaces *** |
38 |
46 |
39 * tuned current_goals_markers semantics: begin / end goal avoids |
47 * tuned current_goals_markers semantics: begin / end goal avoids |
40 printing empty lines; |
48 printing empty lines; |