26 Isabelle's arithmetic decision procedure, the method |
26 Isabelle's arithmetic decision procedure, the method |
27 \methdx{arith}. Linear arithmetic comprises addition, subtraction |
27 \methdx{arith}. Linear arithmetic comprises addition, subtraction |
28 and multiplication by constant factors; subterms involving other operators |
28 and multiplication by constant factors; subterms involving other operators |
29 are regarded as variables. The procedure can be slow, especially if the |
29 are regarded as variables. The procedure can be slow, especially if the |
30 subgoal to be proved involves subtraction over type \isa{nat}, which |
30 subgoal to be proved involves subtraction over type \isa{nat}, which |
31 causes case splits. |
31 causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith} |
|
32 can deal with quantifiers (this is known as ``Presburger Arithmetic''), |
|
33 whereas on type \isa{real} it cannot. |
32 |
34 |
33 The simplifier reduces arithmetic expressions in other |
35 The simplifier reduces arithmetic expressions in other |
34 ways, such as dividing through by common factors. For problems that lie |
36 ways, such as dividing through by common factors. For problems that lie |
35 outside the scope of automation, HOL provides hundreds of |
37 outside the scope of automation, HOL provides hundreds of |
36 theorems about multiplication, division, etc., that can be brought to |
38 theorems about multiplication, division, etc., that can be brought to |