rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H,x:A,
>> 
ext x by hyp x
where
is 
-convertible to A
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> T
ext (
.
(
.t)(
))
)(
)
[new 
] 
ext 
:
>> 
ext 
:
,
,
:
>> T ext t
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> T
ext t[term_of(theorem)/x]
by lemma theorem [new x]
*
x:C >> T ext t
where C is the conclusion of the complete theorem theorem.
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> T ext t by def theorem [new x] where C is the conclusion of the complete theorem, theorem, and ext-term is the term extracted from that theorem.
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> T ext t by explicit intro t rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> T in 
by cumulativity at 
where j<i
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> T[t/x]
ext s
by subst at 
t=
in 
over 
*
>> t = 
in 
*
>> T[
/x]
ext s
*
x:
>> T in 
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> T
ext t
by compute using S 
ext t
.
H, x:T, 
>> 
ext t
by compute hyp i using S
*
H, x:
, 
>> 
ext t
where x :T is thehypothesis, where S is obtained from T by ``tagging'' some of its subterms, and where
is generated by the system by performing some computation steps on subterms of T, as indicated by the tags. A subterm t is tagged by replacing it by [[*;t]] or [[n;t]], where n is a positive integer constant. The latter tag causes t to be computed for n steps, and the former causes computation to proceed as far as possible. There are some somewhat complicated restrictions on what subterms of A may be tagged, but most users will likely find it sufficient to know that any subterm of T may be tagged that does not occur within the scope of a binding variable occurrence in T. An application of one of these rules will fail if the tagging is illegal, or if removing the tags from S does not yield a term equal to T. For a more complete description of this rule, see appendix C. Note that many of the computation rules, such as the one for product, are instances of direct computation.
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> t = 
in T by equality
where the equality of t and
can be deduced from assumptions that are
equalities over T (or equalities over 
where 
is deducible
using only reflexivity, commutativity and transitivity)
using only reflexivity, commutativity and transitivity.
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> C by arith at 
The arith rule is used to justify conclusions which follow from hypotheses by a restricted form of arithmetic reasoning. Roughly speaking, arith knows about the ring axioms for integer multiplication and addition, the total order axioms of <, the reflexivity, symmetry and transitivity of equality, and a limited form of substitutivity of equality. We will describe the class of problems decidable by arith by giving an informal account of the procedure which arith uses to decide whether or not C follows from H.The terms that arith understands are those denoting arithmetic relations, namely terms of the form s<t, s=t in int or the negation of a term of this form. As the only equalities arith concerns itself with are those of the form s=t in int, we will drop the in int and write only s=t in the rest of this description. For arith the negation of an arithmetic relation
where
is one of < or = is of the form (
)->void, which we will write as
. As integer equality and less--than are decidable relations,
and
denote the same relation and will be treated identically by arith.
The arith rule may be used to justify goals of the form
,
,
>>
|
|
,
where each
and
is a term denoting an arithmetic relation. If arith can justify the goal it will produce subgoals requiring the user to show that the left-- and right--hand sides of each
denote integer terms. As a convenience arith will attempt to prove goals in which not all of the
are arithmetic relations; it simply ignores such disjuncts. If it is successful on such a goal, it will produce subgoals requiring the user to prove that each such disjunct is a type at the level given in the invocation of the rule.
Arith begins by normalizing the relevant formulas of the goal according to the following conventions:
- Rewrite each relation of the form
as the equivalent s<t|t<s. A conclusion C follows from such an assumption if it follows from either s<t or t<s; hence arith tries both cases. Henceforth, we assume that all negations of equalities have been eliminated from consideration.
- Replace all occurrences of terms which are not addition, subtraction or multiplication by a new variable. Multiple occurrences of the same term are replaced by the same variable. Arith uses only facts about addition, subtraction and multiplication, so it treats all other terms as atomic. At this point all terms are built from integer constants and integer variables using +, - and
.
- Rewrite all terms as polynomials in canonical form. The exact nature of the canonical form is irrelevant (the reader may think of it as the form used in high school algebra texts) but has the important property that any two equal terms are identical. Each term now has the form
, where p and
are nonconstant polynomials in canonical form, c and
are constants, and
is one of <, = or
(
is equivalent to
).
- Replace each nonconstant polynomial p by a new variable, with each occurrence of p being replaced by the same variable. This amounts to treating each nonconstant polynomial as an atom. Now each formula is of the form
. Arith now decides whether or not the conclusion follows from the hypotheses by using the total order axioms of <, the reflexivity, symmetry, transitivity and substitutivity of =, and the following so--called trivial monotonicity axioms (c and d are constants).
These rules capture all of the acceptable forms of reasoning which may be applied to formulas in canonical form.
For a detailed account of the arith rule and a proof of its correctness, see the article by Tat-hung Chan in [Constable, Johnson, & Eichenlaub 82].
