1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
\DOC ASM_ARITH_TAC
\TYPE {ASM_ARITH_TAC : tactic}
\SYNOPSIS
Tactic for proving arithmetic goals needing basic rearrangement and linear
inequality reasoning only, using assumptions
\DESCRIBE
{ASM_ARITH_TAC} will automatically prove goals that require basic algebraic
normalization and inequality reasoning over the natural numbers. For nonlinear
equational reasoning use {NUM_RING} and derivatives. Unlike plain {ARITH_TAC},
{ASM_ARITH_TAC} uses any assumptions that are not universally quantified as
additional hypotheses.
\FAILURE
Fails if the automated methods do not suffice.
\EXAMPLE
This example illustrates how {ASM_ARITH_TAC} uses assumptions while {ARITH_TAC}
does not. Of course, this is for illustration only: plain {ARITH_TAC} would
solve the entire goal before application of {STRIP_TAC}.
{
# g `1 <= 6 * x /\ 2 * x <= 3 ==> x = 1`;;
Warning: Free variables in goal: x
val it : goalstack = 1 subgoal (1 total)
`1 <= 6 * x /\ 2 * x <= 3 ==> x = 1`
# e STRIP_TAC;;
val it : goalstack = 1 subgoal (1 total)
0 [`1 <= 6 * x`]
1 [`2 * x <= 3`]
`x = 1`
# e ARITH_TAC;;
Exception: Failure "linear_ineqs: no contradiction".
# e ASM_ARITH_TAC;;
val it : goalstack = No subgoals
}
\USES
Solving basic arithmetic goals.
\SEEALSO
ARITH_RULE, ARITH_TAC, INT_ARITH_TAC, NUM_RING, REAL_ARITH_TAC.
\ENDDOC
|
