rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

where is -convertible toA

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* by seq [new ]

* >> ext

* : >> ext

*

* :,,: >>

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

by lemma **theorem** [new **x**]

*
**x**:**C** >> **T** ext **t**

whereCis the conclusion of the complete theoremtheorem.

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

*

whereCis the conclusion of the complete theorem,theorem, andext-termis the term extracted from that theorem.

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* >>

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* >>

wherej<i

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

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

* >> ext

.`
H, x:T, >>
ext t
by compute hyp i using S `

* H, x:, >> ext t

`
`

wherex:Tis the hypothesis, whereSis obtained fromTby ``tagging'' some of its subterms, and where is generated by the system by performing some computation steps on subterms ofT, as indicated by the tags. A subtermtis tagged by replacing it by[[*;t]] or[[n;t]], wherenis a positive integer constant. The latter tag causestto be computed fornsteps, and the former causes computation to proceed as far as possible. There are some somewhat complicated restrictions on what subterms ofAmay be tagged, but most users will likely find it sufficient to know that any subterm ofTmay be tagged that does not occur within the scope of a binding variable occurrence inT. An application of one of these rules will fail if the tagging is illegal, or if removing the tags fromSdoes not yield a term equal toT. 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

where the equality oftand can be deduced from assumptions that are equalities overT(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

Thearith 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 byarith by giving an informal account of the procedure whicharith uses to decide whether or notCfollows fromH.The terms that

arithunderstands are those denoting arithmetic relations, namely terms of the form,s<tor the negation of a term of this form. As the only equalitiess=tin intarithconcerns itself with are those of the form, we will drop thes=tin intin intand write onlyin the rest of this description. Fors=tariththe negation of anarithmetic 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 byarith.The

arithrule may be used to justify goals of the form

, , >> | |,where each and is a term denoting an arithmetic relation. If

arithcan 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 conveniencearithwill 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.

Arithbegins by normalizing the relevant formulas of the goal according to the following conventions:

- Rewrite each relation of the form
as the equivalent. A conclusions<t|t<sCfollows from such an assumption if it follows from eithers<tort<s; hencearithtries 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.
Arithuses 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
pand are nonconstant polynomials in canonical form,cand are constants, and is one of<,=or ( is equivalent to ).- Replace each nonconstant polynomial
pby a new variable, with each occurrence ofpbeing replaced by the same variable. This amounts to treating each nonconstant polynomial as an atom. Now each formula is of the form .Arithnow 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--calledtrivial monotonicityaxioms (canddare 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

arithrule and a proof of its correctness, see the article by Tat-hung Chan in [Constable, Johnson, & Eichenlaub 82].

`
`

Thu Sep 14 08:45:18 EDT 1995