10 text {* |
10 text {* |
11 The {\tt arith} tactic is used frequently throughout the Isabelle |
11 The {\tt arith} tactic is used frequently throughout the Isabelle |
12 distribution. This file merely contains some additional tests and special |
12 distribution. This file merely contains some additional tests and special |
13 corner cases. Some rather technical remarks: |
13 corner cases. Some rather technical remarks: |
14 |
14 |
15 {\tt fast_arith_tac} is a very basic version of the tactic. It performs no |
15 \verb!fast_arith_tac! is a very basic version of the tactic. It performs no |
16 meta-to-object-logic conversion, and only some splitting of operators. |
16 meta-to-object-logic conversion, and only some splitting of operators. |
17 {\tt simple_arith_tac} performs meta-to-object-logic conversion, full |
17 \verb!simple_arith_tac! performs meta-to-object-logic conversion, full |
18 splitting of operators, and NNF normalization of the goal. The {\tt arith} |
18 splitting of operators, and NNF normalization of the goal. The {\tt arith} |
19 tactic combines them both, and tries other tactics (e.g.~{\tt presburger}) |
19 tactic combines them both, and tries other tactics (e.g.~{\tt presburger}) |
20 as well. This is the one that you should use in your proofs! |
20 as well. This is the one that you should use in your proofs! |
21 |
21 |
22 An {\tt arith}-based simproc is available as well (see {\tt |
22 An {\tt arith}-based simproc is available as well |
23 Fast_Arith.lin_arith_prover}), which---for performance reasons---however |
23 (see \verb!Fast_Arith.lin_arith_prover!), |
24 does even less splitting than {\tt fast_arith_tac} at the moment (namely |
24 which---for performance reasons---however |
|
25 does even less splitting than \verb!fast_arith_tac! at the moment (namely |
25 inequalities only). (On the other hand, it does take apart conjunctions, |
26 inequalities only). (On the other hand, it does take apart conjunctions, |
26 which {\tt fast_arith_tac} currently does not do.) |
27 which \verb!fast_arith_tac! currently does not do.) |
27 *} |
28 *} |
28 |
29 |
29 (* |
30 (* |
30 ML {* set trace_arith; *} |
31 ML {* set trace_arith; *} |
31 *) |
32 *) |