Next: 18. The Proof Commands
Up: 3. Reference Manual
Previous: 3. Reference Manual
Subsections
17. The IMPS Special Forms
In this chapter, we document a number of user forms for defining and
modifying IMPS objects, for loading sections and files, and for
presenting expressions. We will use the following template to
describe each one of these forms.
 Positional Arguments.
 This is a list of arguments that must
occur in the order given, and must precede the modifier arguments and
the keyword arguments. All IMPS definition forms have a name as
first argument or, a list of names as first argument.
 Modifier Arguments.
 Each modifier argument is a single symbol
called the modifier.
 Keyword Arguments.
 Each keyword argument is a list whose first
element is a symbol called the keyword. Keyword arguments
have one of two forms:
 (keyword argcomponent).
 (keyword
.
Note: By default, nearly every special form in this chapter is allowed
to have a keyword argument of the form
where syntaxname is the name of a syntax (e.g., stringsyntax or sexpsyntax) which specifies what syntax to
use when reading the form. If this keyword argument is missing, the
current syntax is used when reading the form.
Modifier and keyword arguments can occur in any order.
 Description.
 A brief description of the definition form.
 Remarks:
 Hints or observations that we think you should find useful.
 Examples.
 Some example forms.
defalgebraicprocessor
 cancellative. This modifier argument tells the simplifier
to do multiplicative cancellation.
 (language languagename). Required.
 (base specforms). Required.
 (exponent specforms). Instructs processor how to
simplify exponents if there are any.
 (coefficient specforms). Instructs processor how to
simplify coefficients for modules.
In all of the above cases, specforms is either a name of an
algebraic processor or is a list with keyword arguments and modifier
arguments of its own. The keyword arguments for specforms are:
 (scalars numericaltype).
 (operations
.
operationalist is a
list of entries (operationtype operator). operationtype is one of the symbols
+ *  / ^ sub zero unit
. operator is the name of a constant in the processor language.
The modifier arguments for specforms are:
 usenumeralsforgroundterms.
 commutes.
This form builds an object called a processor for algebraic simplification. Processors are used by IMPS to generate algebraic and order simplification procedures used by the
simplifier for the following purposes:
 To utilize theoryspecific information of an algebraic nature in
performing simplification. For example, the expression x+xx should
simplify to x, or x<x+1 should simplify to true.
 To reduce any expression built from formal constants whose value
can be algebraically computed from the values of the components. Thus
the expression 2+3 should reduce to 5.
In order for simplification to reduce expressions involving only
formal constants (for instance, 2+3), a processor associates such
IMPS terms to executable T expressions involving algebraic procedures
and objects from some data type S. This type is specified by
the scalars declaration of the defalgebraicprocessor
form. We refer to this data type as a numerical type. Each
formal constant o which denotes an algebraic function (such as +or ) is associated to an operation f(o) on the data type. This
correspondence is specified by the operations keyword of
processor. Finally, certain terms must be associated to elements of
S. This is accomplished by a predicate and two mappings
constructed by IMPS when the processor is built:
 A predicate that singles out certain terms as numerical
constants. These are called numerical terms. For the processor
used in the theory horealarithmetic the numerical constants
are those formal constants whose names are rational numbers.
 A function
which maps certain elements of S to terms.
 A function
which maps certain terms to S.
The simplifier uses these functions to reduce
expressions containing numerical terms, according to the following
rule: If f denotes a processor operation, and s,t denote numerical
terms, and o(s,t) is defined, then o(s,t) is replaced by
T(f(o)(N(s),N(t))).
Evaluating a defalgebraicprocessor form by itself will not
affect theory simplification in any way. To add algebraic
simplification to a theory, evaluate the form deftheoryprocessors. It is also important to note that an
algebraic processor can only be installed in the simplifier when
certain theorems generated by the processor are valid in the theory.
(defalgebraicprocessor RRALGEBRAICPROCESSOR
(language numericalstructures)
(base ((scalars *rationaltype*)
(operations
(+ +)
(* *)
( )
(^ ^)
(/ /)
(sub sub))
usenumeralsforgroundterms
commutes)))
(defalgebraicprocessor VECTORSPACEALGEBRAICPROCESSOR
(language realvectorlanguage)
(base ((operations
(+ ++)
(* **)
(zero v0))))
(coefficient rralgebraicprocessor))
defatomicsort
 sortname. The name of the atomic sort to be
defined. sortname also is the name of the newly built definition.
 quasisortstring.
 (theory theoryname). Required.
 (usages
.
 (witness witnessexprstring).
This form creates a new atomic sort
called sortname from a unary predicate p of sort
specified by quasisortstring and adds a set of
new theorems with usage list
.
The new atomic sort and new theorems are added to the
theory T named theoryname provided:
 sortname is not the name of any current
atomic sort of T or of a structural supertheory of T; and
 the formula
is known to be a
theorem of T.
If there is a witness argument, the systems tries to verify
condition (2) by simplifying p(a), where a is the expression
specified by witnessexprstring.
(defatomicsort NN
"lambda(x:zz, 0<=x)"
(theory horealarithmetic)
(witness "0"))
defbnf
 name. A symbol to serve as the name of the theory that will be
created as a consequence of this defform. In addition, a second
implementation object with this name is also created; it represents the
BNF definition itself together with the axioms and theorems that it
generates.
 (theory theoryname). Required. The theory that will be
conservatively extended by adding the new datatype. We will refer to
this theory as the underlying theory.
 (basetype typename). Required. The name of the new data
type.
 (sorts (
) ... (
)).
Subsorts of the new datatype. All these subsorts must be included
within the new base type. Thus, the enclosing sort of the first
subsort must be the new base type, and the enclosing sort of a later
subsort must be either the base type or a previously mentioned subsort
of it.
 (atoms (
) ... (
)). Individual constants declared to
belong to the base type (or one of its subsorts).
 (constructors (
(
...
) (selectors s_{1} ...s_{n1}))).
Function constants declared to construct elements of the new type (or
its subsorts). Each range sort must be the new base type or one of its
subsorts. Each domain sort may belong to the underlying theory, or
alternatively it may be the new base or one of its subsorts. It may
not be a higher sort involving the new type.
 (sortinclusions (
) ... (
)). Declare that every
element of subsort is also a member of supersort. This is
not needed when subsort is a syntactic subsort of supersort
in the sense that there are zero or more intermediate sorts
such that the enclosing sort of subsort is
,
the enclosing sort of
is supersort, and
the enclosing sort of
is
for each i with
.
The purpose of the defbnf form is to define a new recursive data type to
be added (as a conservative extension) to some existing theory. The members of
the new data type are the atoms in the declaration together with the objects
returned (``constructed'') by the constructor functions. We will use the
to refer to the base type; symbols such as
will stand for any
sort included in the base type (such as the base sort
itself); will be used for any sort of the underlying theory.
The logical content of a data type definition of this kind is determined by two
main ideas:
 No Confusion. If c_{0} and c_{1} are two different constructor
functions, then the range of c_{0} is disjoint from the range of c_{1}.
If a and b are two atoms, then .
Moreover
.
 No Junk. Everything in
apart from the atoms is generated
by the constructor functions. This is in fact a form of induction. It
allows us to infer that a property holds of all members of the data
type on two assumptions:
 1.
 The property holds true of each atom;
 2.
 The property holds true of a value returned by any constructor
function c, assuming that it holds true of those arguments that
belong to
(rather than to some sort
of the underlying
theory).
The implementation ensures that the resulting theory will be a model
conservative extension of the underlying theory. That is, given any model
M of the underlying theory, we can augment M with a new domain to
interpret
and provide interpretations of the new vocabulary so that
the resulting M' is a model of extended theory.
In the case where
contains no subtype, it is clear that to ensure
conservatism, it is enough to establish that
will be nonempty. The
syntax of the declaration suffices to determine whether this condition is
met: either there must be an atom, or else at least one constructor function
must take all of its arguments from types
of the underlying theory.
If
does have subtypes, the implementation must establish that each
subtype is nonempty. That will hold if there is an ordering of the new
sorts
such that, for each ,
at least one of the
following conditions holds:
 1.
 There is an atom declared to be of sort ;
or
 2.
 There is a sort
occurring earlier in the ordering, and
is declared to be included within ;
or
 3.
 There is at least one constructor c declared with range sort
,
and every domain sort of c is either some
belonging to the underlying theory or some
occurring
earlier in the ordering that .
When this condition is not met, the implementation raises an error and
identifies the uninhabited sort (or sorts) for the user.
The BNF mechanism generates six categories
of axioms:
 Constructor definedness
 A constructor is welldefined for every
selection of arguments of the syntactically declared sorts.
 Disjointness
 If a and b are atoms and c_{0} and c_{1} are
constructors, then ,
,
and
is disjoint from
.
 Selector/constructor
 If s is the th selector for the
constructor c, then
.
Moreover, if
,
then
for some .
 Sort Inclusions

,
when
is specified as included within .
 Induction
 The type
is the smallest containing the atoms and
closed under the constructor functions in the sense given above (``No
Junk'').
 Case Analysis
 If
,
where
is the new type
or one of its subsorts, then one of the following holds:
 1.
 x is one of the atoms declared with sort ;
 2.
 x is in the range of some constructor declared with range ;
 3.

,
where either
is the enclosing sort of
,
or else the inclusion of
within
is
declared as a sort inclusion.
Strictly speaking this should be a theorem rather than an axiom, as
it follows from the induction principle.
A data type introduced via the BNF
mechanism justifies a schema for defining functions by primitive recursion.
Roughly speaking, a function g of sort
is uniquely
determined if a sort
is given, together with the following:
 For each atom, a value of sort ;
 For each constructor c, with sort
a functional
of sort
is given. The primitive recursively defined function g will have the
property that
is quasiequal to
Thus in effect
says how to combine the results of the
recursive calls (for arguments in the primary type) with the values
of the parameters (from sorts
of the underlying theory).
A number of consequences of the axioms are
installed.
The simplest example possible is:
(defbnf nat
(theory puregenerictheory1)
(basetype nat)
(atoms (zero nat))
(constructors (succ (nat nat) (selectors pred))))
The axioms generated from this definition are displayed in
Figure 17.1 on page .
Figure 17.1:
Axioms for Nat, as Introduced by BNF
bnf data type nat:

As a more complicated example, consider a programming language with phrases of
three kinds, namely identifiers, expressions, and statements. The data type to
be introduced corresponds to set of phrases of all three syntactic categories;
each syntactic category will be represented by a subsort. A BNF for the
language might take the form given in Figure 17.2, with x ranging
over numbers and s ranging over strings. A corresponding IMPS def form is
shown in Figure 17.3, where it is assumed that the underlying
theory Stringtheory contains a sort string representing
ASCII strings, as well as containing R.
Figure 17.2:
BNF Syntax for a Small Programming Language

Figure 17.3:
IMPS defbnf Form for Programming Language Syntax

defcartesianproduct
 name. A symbol to name the product sort.
 (
.
sortname is the name of a sort
 (constructor constructorname).
 (accessors
.
 (theory theoryname). Required.
This form creates a new atomic sort
called name. This
sort can be regarded as the cartesian product of the sorts
The sort actually created is a subsort of the
function sort
 constructorname is the name of the canonical
``ntuple'' mapping:

is the name of the canonical projection onto the
ith coordinate:
(defcartesianproduct complex
(rr rr)
(constructor make%complex)
(accessors real imaginary)
(theory horealarithmetic))
defcompoundmacete
None.
This form adds a compound macete with the
given name and components. See the section on macetes for the
semantics of macetes.
(defcompoundmacete FRACTIONALEXPRESSIONMANIPULATION
(repeat
betareduce
additionoffractions
multiplicationoffractions
multiplicationoffractionsleft
multiplicationoffractionsright
equalityoffractions
leftdenominatorremovalforequalities
rightdenominatorremovalforequalities
strictinequalityoffractions
rightdenominatorremovalforstrictinequalities
leftdenominatorremovalforstrictinequalities
inequalityoffractions
rightdenominatorremovalforinequalities
leftdenominatorremovalforinequalities))
(defcompoundmacete ELIMINATEIOTAMACETE
(sequential
(sound
tr%abstractionforiotabody
betareduce
betareduce)
(series
tr%definediotaexpressionelimination
tr%negateddefinediotaexpressionelimination
tr%leftiotaexpressionequationelimination
tr%rightiotaexpressionequationelimination)
betareduce))
defconstant
 constantname. The name of the constant to be defined.
constantname is also the name of the newlybuilt definition.
 definingexprstring.
 (theory theoryname). Required.
 (sort sortstring).
 (usages
.
This form creates a new constant c called
constantname and a new axiom of the form c =e with usage
list
,
where e is
the expression specified by definingexprstring. The sort
of c is the sort specified by sortstring if there
is a sort argument and otherwise is the sort of e. The new
constant and new axiom are added to the theory T named theoryname provided:
 constantname is not the name of any current constant
of T or of a structural supertheory of T; and
 the formula
is known to be a
theorem of T.
(defconstant ABS
"lambda(r:rr, if(0<=r,r,r))"
(theory horealarithmetic))
(defconstant >
"lambda(x,y:rr,y<x)"
(theory horealarithmetic)
(usages rewrite))
(defconstant POWER%OF%TWO
"lambda(x:zz,2^x)"
(sort "[zz,zz]")
(theory horealarithmetic))
defimportedrewriterules
 (sourcetheory sourcetheoryname).
 (sourcetheories
.
This form imports into the theory named
theoryname all the transportable rewrite rules installed in
the theory named sourcetheoryname (or in the theories named
).
definductor
 inductorname.
 inductionprinciple. Can be a string representing the
induction principle in the current syntax or a name of a theorem.
 (theory theoryname). Required.
 (translation name). name is the name of a theory
interpretation. If this keyword is present, the formula used in
constructing the induction principle is actually the translation of
inductionprinciple.
 (basecasehook name). name is the name of a macete
or a command.
 (inductionstephook name). name is the name of a macete
or a command.
 (dontunfold
.
name is the name of a recursive constant in
the theory or the symbol
#t
. This form instructs the inductor not to
unfold the recursive constant named name when processing the
induction step. If #t
is specified, then no recursive definitions will
be unfolded in the induction step.
The induction principle used for
constructing an inductor must satisfy a number of requirements.
This form builds an inductor from the
formula
represented by inductionprinciple or if the
translation keyword is present, from the translation of
under the translation named by name. The basecase
and inductionstep hooks are macetes or commands that provide additional
handling for the base and induction cases.
(definductor TRIVIALINTEGERINDUCTOR
"forall(s:[zz,prop],m:zz,
forall(t:zz,m<=t implies s(t))
iff
(s(m) and
forall(t:zz,m<=t implies (s(t) implies s(t+1)))))"
(theory horealarithmetic))
(definductor NATURALNUMBERINDUCTOR
"forall(s:[nn,prop],
forall(t:nn, s(t))
iff
(s(0) and forall(t:nn,s(t) implies s(t+1))))"
(theory horealarithmetic))
(definductor INTEGERINDUCTOR
induct
(theory horealarithmetic)
(basecasehook unfolddefinedconstantsrepeatedly))
(definductor SMINDUCT
"forall(p:[state,prop],
forall(s:state, accessible(s) implies p(s))
iff
(forall(s:state, initial(s) implies p(s)) and
forall(s_1, s_2:state, a:action,
(accessible(s_1) and p(s_1) and tr(s_1, a, s_2))
implies
p(s_2))))"
(theory horealarithmetic)
(basecasehook
eliminatenonrecursivedefinitionsandsimplify))
(definductor SEQUENCEINDUCTOR
"forall(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1], f_seq_q(s) implies p(s))
iff
(p(nil(ind_1)) and
forall(s:[nn,ind_1], e:ind_1,
f_seq_q(s) and p(s) implies p(cons{e,s}))))"
(theory sequences)
(basecasehook simplify))
deflanguage
 (embeddedlanguages
.
name is the name of a
language or theory.
 (embeddedlanguage name). name is the name of a
language or theory.
 (basetypes
.
 (sorts
.
sortspec is a list of the form
(sort enclosingsort), called a sortspecification. sort must be a symbol, and
enclosingsort must satisfy one of the following:
 It occurs in a previous sort specification.
 It is a sort in one of the embedded languages.
 It is a compound sort which can be built up from sorts of the
preceding kinds.
 (extensible
.
typesortalist is a list of
the form (numericaltypename sort). numericaltypename is the name of a numerical type, that is, a
class of objects defined in T. For example, *integertype* and
*rationaltype* are names of numerical types. This keyword
argument is used for defining selfextending languages. This is a
language that incorporates new formal symbols when the expression
reader encounters numerical objects of the given type.
 (constants
.
constantspec is a list
(constantname sortorcompoundsort).
This form builds a language with name
languagename satisfying the following properties:
 This language contains the sorts and constants
given by the sort and constant specification subforms.
 It contains the languages named
as sublanguages.
 If the language contains the extensible keyword, then the
language may contain an infinite number of constants; these constants
are in onetoone correspondence with elements of the numerical types
present in the typesortalist.
(deflanguage NUMERICALSTRUCTURES
(extensible (*integertype* zz) (*rationaltype* qq))
(sorts (rr ind) (qq rr) (zz qq))
(constants
(^ (rr zz rr))
(+ (rr rr rr))
(* (rr rr rr))
(sub (rr rr rr))
( (rr rr))
(/ (rr rr rr))
(<= (rr rr prop))
(< (rr rr prop))))
(deflanguage METRICSPACESLANGUAGE
(embeddedlanguage horealarithmetic)
(basetypes pp)
(constants
(dist (pp pp rr))))
(deflanguage REALVECTORLANGUAGE
(embeddedlanguage horealarithmetic)
(basetypes uu)
(constants
(++ (uu uu uu))
(v0 uu)
(** (rr uu uu))))
(deflanguage HAMSANDWICHLANGUAGE
(basetypes sandwich)
(embeddedlanguage horealarithmetic)
(constants
(ham%sandwich sandwich)
(tuna%sandwich sandwich)
(refrigerator (sandwich unit%sort))))
deforderprocessor
 (algebraicprocessor name). The name of an algebraic
processor.
 (operations
.
operationalist is a
list of entries (operationtype operator), where operationtype is one of: <, <=. operator is the name of a
constant in the language of the associated algebraic processor.
 (discretesorts
.
This form builds an object called an order processor for simplification
of formulas involving order relations. Processors are used by IMPS to generate algebraic and order simplification procedures used by the
simplifier for the following purposes:
 To utilize theoryspecific information of an algebraic nature in
performing simplification. For example, the expression x+xx should
simplify to x, or x<x+1 should simplify to true.
 To reduce any formula built from formal constants whose value
can be algebraically computed from the values of the components. Thus
the expression 2<3 should reduce to true.
(deforderprocessor RRORDER
(algebraicprocessor rralgebraicprocessor)
(operations (< <) (<= <=))
(discretesorts zz))
defprimitiverecursiveconstant
 constant name: The name of the function (or predicate) constant
to be introduced by the defform.
 bnf: The BNF object furnishing the primitive
recursive schema for the definition (see defbnf). The base type
of this BNF will also be the domain of the constant.
 (theory theoryname): Required. The theory to which the defined
constant will be added. This may be an extension of the theory of the
BNF with respect to which the recursion is performed.
 (rangesort rangesortform): Required. This specifies the
range of the function or predicator being introduced; since the domain
will be the base sort of the BNF, this fixes the sort of the
constant.
 (atomname value): Required, one for each
BNF atom. This specifies one base case of the recursive definition.
 (constructorname varnames operatorbody ): Required, one for each BNF constructor. This specifies one
recursive step of the recursive definition. The operatorbody
specifies how the results of the recursive subcalls should be combined
(possibly with parameters not belonging to the datatype) to produce the
value of the recursive operator for an argument of this form.
Each BNF is automatically equipped with a
principle of definition by structural (primitive) recursion. A defprimitiverecursiveconstant form instantiates this principle by
stipulating the intended range sort, the values for atoms of the BNF
data type, and how the recursively defined operator combines its results on
the arguments of each datatype constructor.
See, for instance, the compiler exercise file.
defquasiconstructor
 name. The name of the quasiconstructor.
 lambdaexprstring.
 (language languagename). Required. languagename
may also be the name of a theory.
 (fixedtheories
.
This form builds a quasiconstructor
named name from the schema specified by lambdaexprstring, which is a lambdaexpression in the
language named languagename. The sorts in the theories named
,
...
are
held fixed.
(defquasiconstructor PREDICATETOINDICATOR
"lambda(s:[uu,prop],
lambda(x:uu, if(s(x),an%individual, ?unit%sort)))"
(language indicators)
(fixedtheories thekerneltheory))
(defquasiconstructor GROUP
"lambda(a:sets[gg],
mul%:[gg,gg,gg],
e%:gg,
inv%:[gg,gg],
forall(x,y:gg,
(x in a and y in a) implies mul%(x,y) in a) and
e% in a and
forall(x:gg, x in gg% implies inv%(x) in gg%) and
forall(x:gg, x in a implies mul%(e%,x)=x) and
forall(x:gg, x in a implies mul%(x,e%)=x) and
forall(x:gg, x in a implies mul%(inv%(x),x)=e%) and
forall(x:gg, x in a implies mul%(x,inv%(x))=e%) and
forall(x,y,z:gg,
(x in a) and (y in a) and (z in a)
implies
mul%(mul%(x,y),z) = mul%(x,mul%(y,z))))"
(language groups))
defrecordtheory
 theoryname. The name of a theory.
 (type symbol). Required.
 (accessors
.
accessorspec is a list
NO DESCRIPTION.
(defrecordtheory ENTITIESANDLEVELS
(type access)
(accessors
(read "prop")
(write "prop")))
defrecursiveconstant
 names. The name or lists of names of the constant or
constants to be defined.
 definingfunctionalstrings. A string or list of strings
specifying the defining functionals of the definition.
 (theory theoryname). Required.
 (usages
.
 (definitionname defname). The name of the definition.
Let T be the theory named theoryname;
,...,
be the names given by names; and
be the functionals specified by the strings in definingfunctionalstrings. This form creates a list of new
constants
called
,...,
and a set of new
axioms with usage list
,...,
.
The axioms say that
are a minimal fixed
point of the family
of functionals. The new
constants and new axioms are added to T provided:
 each
is not the name of any current
constant of T or of a structural supertheory of T; and
 each functional f_{i} is known to be monotone in T.
If the definitionname keyword is present, the name of the
definition is defname; otherwise, it is
.
(defrecursiveconstant SUM
"lambda(sigma:[zz,zz,[zz,rr],rr],
lambda(m,n:zz,f:[zz,rr],
if(m<=n,sigma(m,n1,f)+f(n),0)))"
(theory horealarithmetic)
(definitionname sum))
(defrecursiveconstant (EVEN ODD)
("lambda(even,odd:[nn,prop],
lambda(n:nn, if_form(n=0, truth, odd(n1))))"
"lambda(even,odd:[nn,prop],
lambda(n:nn, if_form(n=0, falsehood, even(n1))))")
(theory horealarithmetic)
(definitionname evenodd))
(defrecursiveconstant OMEGA%EMBEDDING
"lambda(f:[nn,nn], a:sets[nn],
lambda(k:nn,
if(k=0,
iota(n:nn, n in a and
forall(m:nn, m<n implies not(m in a))),
lambda(z:nn,
iota(n:nn, n in a and z<n
forall(m:nn, (z<m and m<n) implies
(not(m in a)))))(f(k1)))))"
(theory horealarithmetic)
(definitionname omega%embedding))
defrenamer
 name. A symbol naming the renamer.
 (pairs
.
pair is of the form
(oldname newname).
This form defines a T procedure named
name which, given a symbol x, returns the symbol y if (xy) is one of the pairs, and otherwise returns x.
(defrenamer SBRENAMER
(pairs
(last%a%index last%b%index)
(a%inf b%inf)
(a%even b%even)
(a%odd b%odd)))
defschematicmacete
 macetename. A symbol naming the schematic macete.
 formula. A string representing the formula using the current syntax.
 null. The presence of this modifier means the macete is
nondirectional. This means that schematic macete which is built uses a
matching and substitution procedure which does not obey the variable
capturing protections and other restrictions of normal matching and
substitution.
 transportable. The presence of this modifier means the macete is transportable.
 (theory theorylanguagename). Required. The name of
the language in which expression should be read in.
(defschematicmacete ABSTRACTIONFORDIFFPROD
"with(a,b:rr,y:rr,
diff(lambda(x:rr,a*b))(y)=
diff(lambda(x:rr,
lambda(x:rr,a)(x)*lambda(x:rr,b)(x)))(y))"
null
(theory calculustheory))
defscript
 scriptname. The name of the new command being created.
 N. The number of arguments required by the script.
 (
.
A proof script consisting of 0 or more
forms.
 (retrievalprotocol proc). proc is the name of an
Emacs procedure which IMPS uses to interactively request command
arguments from the user. The default procedure is generalargumentretrievalprotocol which requires the user to supply
all the arguments in the minibuffer.
 (applicabilityrecognizer proc). proc is the name
of a T predicate or is the symbol
#t
. The inclusion of this
argument will cause the command name to appear as a selection in the
command menu whenever the current sequent node satisfies the
predicate. Supplying #t
as an argument is equivalent to
supplying a predicate which is always true.
This form is used to build a new command named scriptname. This
new command can be used in either interactive mode or in script mode. The
script defining the command is a list of forms, each of which is a
command form or a keyword form. See a description of the
proof script language in Chapter 12.
(defscript EPSILON/NARGUMENT 1
((instantiateuniversalantecedent
"with(p:prop, forall(eps:rr, 0<eps implies p))" ($1))))
defsection
 (componentsections
.
 (files
.
This form builds a section which, when loaded, loads the sections with
names
and then loads the files with specifications
.
A section can be
loaded with the form loadsection.
(defsection BASICREALARITHMETIC
(componentsections reals)
(files
(imps theories/reals/somelemmas)
(imps theories/reals/arithmeticmacetes)
(imps theories/reals/numbertheory)))
(defsection FUNDAMENTALCOUNTINGTHEOREM
(componentsections
basiccardinality
basicgrouptheory)
(files
(imps theories/groups/groupcardinality)
(imps theories/groups/countingtheorem)))
defsublanguage
 (superlanguage superlanguagename). Required.
The name of the language containing the sublanguage.
 (languages
.
 (sorts
.
 (constants
.
This form finds the smallest sublanguage of the language L named
superlanguagename which contains the sublanguages of Lnamed language
,
..., language
;
the atomic sorts of L named sort
,
..., sort
;
and the constants of L named
.
Each of
may be the name of
a theory instead of a language.
(defsublanguage REALVECTORLANGUAGE
(superlanguage vectorspacesoverrrlanguage)
(languages horealarithmetic)
(sorts uu)
(constants ++ v0 **))
deftheorem
 name. The name of the theorem which may be ().
 formulaspec. A string representing the formula using the
current syntax or the name of a theorem.
 reverse.
 lemma. Not loaded when quickloading.
 (theory theoryname). Required. The name of the theory
in which to install the theorem.
 (usages
.
 (translation translationname). The name of a theory
interpretation.
 (macete macetename). The name of a bidirectional macete.
 (hometheory hometheoryname). The name of the home
theory of the formula specified by formulaspec.
 (proof proofspec).
This form installs a theorem in three
steps. Let
be the theory interpretation named translationname when there is a translation argument, and let
M be the bidirectional macete named macetename when there is
a macete argument. Also, let T be the theory named theoryname, and let H be the theory named by hometheoryname. If there is no hometheory argument, then
H is the source theory of
if there is a translation
argument and otherwise H=T. Finally, let
be the formula
specified by formulaspec in H.
Step 1. IMPS verifies that
is a theorem of H.
If proofspec is the symbol existingtheorem, IMPS checks to see that
is alphaequivalent to some existing
theorem of H. If the theorem is being installed in ``batch mode''
(see Section 12.3.1), IMPS verifies that is a theorem of H by running the script proofspec.
Otherwise, IMPS simply checks that
is a formula in H,
and it is assumed that the user has verified that
is a
theorem of H.
Step 2. The theorem
to be installed is generated from
as follows:
 If there is no translation or macete
argument and T=H, then
.
 If there is no translation or macete
argument and T is a subtheory of H,
is a formula of Twhich is the result of generalizing the constants of H which are not
in T (assuming each sort of T is also a sort of H).
 If there is a translation argument but no macete
argument, then
is the translation of
by .
 If there is a macete argument but no translation
argument, then
is the result of applying M to .
 If there is both a translation and macete argument,
then
is the result of applying M to the translation of
by .
Step 3.
is installed as a theorem in T with usage
list
,
,
.
If the modifier argument reverse is present, evaluating this
form is equivalent to evaluating the form without reverse
followed by evaluating the form again without reverse but with:
 name changed to the concatenation of rev% with
name, and
 formulaspec changed to a string which specifies
the ``reverse'' of the formula specified by formulaspec.
In other words, the reverse argument allows you to install both
a theorem and its reverse. It is very useful for building a macete
(or transportable macete) and its reverse by evaluating one form. Of
course, it would not be wise to use the reverse argument when
rewrite is a usage.
(deftheorem ABSISTOTAL
"total_q(abs,[rr,rr])"
(theory horealarithmetic)
(usages drconvergence)
(proof
(
(unfoldsingledefinedconstant (0) abs)
insistentdirectinference
betareducerepeatedly
)))
(deftheorem RIGHTCANCELLATIONLAW
leftcancellationlaw
(theory groups)
(translation mulreverse)
(proof existing theorem))
(deftheorem FUNDAMENTALCOUNTINGTHEOREM
"f_indic_q{gg%subgroup}
implies
f_card{gg%subgroup} =
f_card{stabilizer(zeta)}*f_card{orbit(zeta)}"
;; "forall(zeta:uu,
;; f_indic_q{gg%subgroup}
;; implies
;; f_card{gg%subgroup} =
;; f_card{stabilizer(zeta)}*f_card{orbit(zeta)})"
(theory groupactions)
(hometheory countingtheoremtheory))
deftheory
 (language languagename).
 (componenttheories
.
 (axioms
.
axiomspec is a list
where name, a symbol, is the optional name of the axiom and formulastring is a string representing the axiom in the syntax of
the language of the theory.
 (distinctconstants
.
distinct is a list
This form builds a theory named theoryname. The language of this theory is the union of the language
languagename and the languages of the component theories. The
axioms of the theory are the formulas represented by the strings in
the list axiomspec. The distinctconstants list
implicitly adds new axioms asserting that the constants in each list
distinct are not equal.
(deftheory METRICSPACES
(componenttheories horealarithmetic)
(language metricspaceslanguage)
(axioms
(positivityofdistance
"forall(x,y:pp, 0<=dist(x,y))"
transportablemacete)
(pointseparationfordistance
"forall(x,y:pp, x=y iff dist(x,y)=0)"
transportablemacete)
(symmetryofdistance
"forall(x,y:pp, dist(x,y) = dist(y,x))"
transportablemacete)
(triangleinequalityfordistance
"forall(x,y,z:pp, dist(x,z)<=dist(x,y)+dist(y,z))")))
(deftheory VECTORSPACESOVERRR
(language realvectorlanguage)
(componenttheories generictheory1)
(axioms
("forall(x,y,z:uu, (x++y)++z=x++(y++z))")
("forall(x,y:uu, x++y=y++x)")
("forall(x:uu, x++v0=x)")
("forall(x,y:rr, z:uu, (x*y)**z=x**(y**z))")
("forall(x,y:uu,a:rr,a**(x++y)=(a**x)++(a**y))")
("forall(a,b:rr, x:uu,(a+b)**x=(a**x)++(b**x))")
("forall(x:uu, 0**x=v0)")
("forall(x:uu, 1**x=x)")))
deftheoryensemble
 ensemblename. The name of the theory ensemble. This will also
be the name of the base theory unless the basetheory
keyword argument is provided.
 (basetheory theoryname) theoryname is the name
of the base theory of the ensemble. If this keyword argument is not
included then the base theory is that theory with the name
ensemblename.
 (fixedtheories
.
The theories listed are not
replicated when the theory replicas and multiples are built. If this
argument is not provided, then the fixed theories are those in the
global fixed theories list at the time the form is evaluated.
 (replicarenamer procname). procname is the name
of a procedure of one integer argument, used to name sorts and
constants of theory replicas. The default procedure is to subscript
the corresponding sort and constant of the base theory.
This form builds a theory ensemble such
that
 1.
 The base theory is the theory with name theoryname if the basetheory keyword argument is provided or ensemblename
otherwise.
 2.
 The fixed theories are those given in the fixedtheories keyword
argument list if the fixedtheories keyword argument is provided
or those theories in the global fixed theories list at the time the
form is evaluated.
If there is already a theory ensemble with
name ensemblename but with different fixedtheories set or
different renamer an error will result.
(deftheoryensemble METRICSPACES)
deftheoryensembleinstances
 ensemblename. An error will result if no ensemble exists
with ensemblename.
This form is used to build translations
from selected theory multiples and to transport natively defined
constants and sorts from these multiples. To describe the
effects of evaluating this form, we consider a number of cases and
subcases determined by the presence of certain keyword arguments.
 (targettheories
.
Let
be the theory with
name
In this case, evaluation of the form builds
translations and transports natively defined constants and sorts by
these translations from selected theory multiples into the theory
union
The theory multiples
that are selected as translation source theories are determined by the
multiples or permutations keyword arguments as follows:
 (targetmultiple n). This case can be reduced to
the case of the (targettheories
argument by letting
be the name of the ith theory replica.
(deftheoryensembleinstances METRICSPACES
(targettheories horealarithmetic metricspaces)
(multiples 1 2)
(sorts (pp rr pp))
(constants (dist "lambda(x,y:rr,abs(xy))" dist)))
deftheoryensemblemultiple
 ensemblename. An error will result if no ensemble exists
with ensemblename.
 N. An integer.
Builds a theory which is an Nmultiple
of the theory ensemble base, together with N theory
interpretations from the base theory into the multiple. All
existing definitions of the base theory are translated via these
interpretations. The Nmultiple is constructed to be a subtheory
of the (N+1)multiple.
(deftheoryensemblemultiple metricspaces 2)
deftheoryensembleoverloadings
 ensemblename. An error will result if no ensemble exists
with ensemblename.

Each N is an integer
Installs overloadings for constants
natively defined in the theory multiples
(deftheoryensembleoverloadings metricspaces 1 2)
deftheoryinstance
 name. The name of the theory to be created.
 (source sourcetheoryname). Required.
 (target targettheoryname). Required.
 (translation transname). Required.
 (fixedtheories
.
 (renamer renamer). Name of a renaming procedure.
 (newtranslationname newtransname). Name of the
the translation to be created.
Let T_{0} and
be
the source and target theories, respectively, of the translation
named transname. Also, let T_{1} and
be the theories named sourcetheoryname and targettheoryname, respectively. Lastly, let
be the set of
theories named
.
Suppose that T_{0} and
are subtheories of T_{1} and
,
respectively, and that every member of
is a
subtheory of T_{1}. The theory named name is an extension Uof
built as follows. First, the primitive vocabulary
of T_{1} which is outside of T_{0} and
is added to the language
of
;
the vocabulary is renamed using the value of renamer. Next, the translations of the axioms of T_{1} which are
outside of T_{0} and
are added to the axioms of
;
the axioms are renamed using the value of renamer. U is union of the resulting theory and the members of
. The translation
from T_{1} to U extending
is
created with name newtransname.
(deftheoryinstance METRICSPACESCOPY
(source metricspaces)
(target thekerneltheory)
(translation thekerneltranslation)
(fixedtheories horealarithmetic))
(deftheoryinstance VECTORSPACESOVERRR
(source vectorspaces)
(target horealarithmetic)
(translation fieldstorr)
(renamer vsrenamer))
deftheoryprocessors
 (algebraicsimplifier
.
Each entry spec
is a list
where processorname is the name of an algebraic processor and
are constant names denoting functions. We will say that the operators
are within the scope of the specified processor.
 (algebraicordersimplifier
.
Each spec
is a list
where processorname is the name of an order processor and
are constant names denoting twoplace predicates. We will say that
the predicates
are within the scope of the
specified order processor.
 (algebraictermcomparator
.
spec is just
the name of an algebraic or order processor. We will
say that the equality constructor is within the scope of the specified
processor.
This form causes the simplifier of the theory named theoryname
to simplify certain terms using the specified algebraic and order
processors as follows:
 All applications of an operator or predicate within the scope
of a processor are handled by that processor. An operation or
predicate may be within the scope of more than one processor.
 All equalities are handled by processors which contain the
equality constructor within its scope.
(deftheoryprocessors HOREALARITHMETIC
(algebraicsimplifier
(rralgebraicprocessor * ^ +  / sub))
(algebraicordersimplifier (rrorder < <=))
(algebraictermcomparator rrorder))
(deftheoryprocessors VECTORSPACESOVERRR
(algebraicsimplifier
(vectorspacealgebraicprocessor ** ++))
(algebraictermcomparator
vectorspacealgebraicprocessor))
deftranslation
 name: The name of the translation.
 force.
 forceunderquickload.
 dontenrich.
 (source sourcetheoryname). Required.
 (target targettheoryname). Required.
 (assumptions
.
 (fixedtheories
.
 (sortpairs
.
Each
sortpairspec has one of the following forms:
 (sortname sortname).
 (sortname sortstring).
 (sortname (pred exprstring)).
 (sortname (indic exprstring)).
 (constantpairs
,
where
constpairspec has one of the following forms:
 (constantname constantname).
 (constantname exprstring).
 (coretranslation coretranslationname). The name of a
theory interpretation.
 (theoryinterpretationcheck checkmethod).
This form builds a translation named name from the source theory S named sourcetheoryname to
the target theory T named targettheoryname. (The target
context in T is the set of assumptions specified by
,
,
.) The
translation is specified by the set of fixed theories, the set of sort
pairs, and the set of constant pairs.
If there is a coretranslation argument, an extension of the
translation named coretranslationname is build using the
information given by the other arguments. The argument theoryinterpretationcheck tells IMPS how to check if the
translation is a theory interpretation (relative to the set of
assumptions).
If the modifier argument force is present, the obligations of
the translation are not generated, and thereby the translation is
forced to be a theory interpretation. Similarly, if the modifier
argument forceunderquickload is present and the switch quickload? is set to true, the obligations of the translation are
not generated. The former lets you build a theory interpretation when
the obligations are very hard to prove, and the latter is useful for
processing the defform faster, when it has been previously determined
that the translation is indeed a theory interpretation.
If the modifier argument dontenrich is present, the translation
will not be enriched. A translation is enriched at various times to
take into account new definitions in the source and target theories.
If one expects there to be many untranslated definitions after
enrichment, it may be computationally beneficial to use this modifier
argument.
(deftranslation MONOIDTHEORYTOADDITIVERR
(source monoidtheory)
(target horealarithmetic)
(fixedtheories horealarithmetic)
(sortpairs
(uu rr))
(constantpairs
(e 0)
(** +))
(theoryinterpretationcheck usingsimplification))
(deftranslation MULREVERSE
(source groups)
(target groups)
(fixedtheories horealarithmetic)
(constantpairs
(mul "lambda(x,y:gg, y mul x)"))
(theoryinterpretationcheck usingsimplification))
(deftranslation GROUPS>SUBGROUP
force
(source groups)
(target groups)
(assumptions
"with(a:sets[gg], nonempty_indic_q{a})"
"with(a:sets[gg],
forall(g,h:gg,
(g in a) and (h in a)
implies
(g mul h) in a))"
"with(a:sets[gg],
forall(g:gg, (g in a) implies (inv(g) in a)))")
(fixedtheories horealarithmetic)
(sortpairs
(gg (indic "with(a:sets[gg], a)")))
(constantpairs
(mul "with(a:sets[gg],
lambda(x,y:gg,
if((x in a) and (y in a), x mul y, ?gg)))")
(inv "with(a:sets[gg],
lambda(x:gg, if(x in a, inv(x), ?gg)))"))
(theoryinterpretationcheck usingsimplification))
deftransportedsymbols
 names. The name or lists of names of defined atomic
sorts and constants to be transported.
 (translation translationname). Required.
 (renamer renamer.) Name of a renaming procedure.
Let T and T' be the source and
target theories, respectively, of the translation
named translationname, and let
,...,
be the symbols whose names are given by names. For each
which is a defined symbol in T, this form creates
a corresponding new defined symbol
in
T' by translating the defining object of
via
.
If
already translates
to some
defined symbol, the new symbol is not created.
(deftransportedsymbols
(last%a%index a%inf a%even a%odd)
(translation schroederbernsteinsymmetry)
(renamer sbrenamer))
(deftransportedsymbols
(prec%increasing prec%majorizes prec%sup)
(translation orderreverse)
(renamer firstrenamer))
defoverloading
 symbol. A symbol to overload (that is, to have multiple
meanings which are determined by context.)

theorynamepair is a list (theoryname symbolname).
(defoverloading *
(horealarithmetic *)
(normedlinearspaces **))
defparsesyntax
 constantname. This is a symbol or a list of symbols.
 (token spec). spec is a symbol or a string. If this
argument is omitted, by default it is constantname.
 (leftmethod procname). procname is the name of a
procedure for left parsing of the token.
 (nullmethod procname). procname is the name of a
procedure for null parsing of the token.
 (table tablename). tablename is the name of the
parsetable being changed. If this argument is omitted, the default value
is the global parse table *parse*.
 (binding N). Required. N is the binding or
precedence of the token.
This form allows you to set (or reset)
the parse syntax of a constant. In particular, you can change the
precedence, parsing method, and token representation of a constant.
The most common parsing methods are:
 infixoperatormethod. For example multiplication and addition use this method.
 prefixoperatormethod. comb, the binomial coefficient
function, uses this method.
 postfixoperatormethod. ! uses this method.
Note that an operator can have both a nullmethod and a leftmethod.
(defparsesyntax +
(leftmethod infixoperatormethod)
(binding 100))
(defparsesyntax factorial
(token !)
(leftmethod postfixoperatormethod)
(binding 160))
defprintsyntax
 constantname. This is a symbol.
 tex. If this argument is present, then the syntax is added
to the global TEX print table.
 (token spec). spec is a symbol, a string or a list
of such. If this argument is omitted, by default it is constantname.
 (method procname). procname is the name of a
procedure for printing of the token.
 (table tablename). tablename is the name of the
parsetable being changed. If this argument is omitted, and the tex modifier argument is not given, the default value is the global
print table *form*.
 (binding N). Required. N is the binding or
precedence of the token.
This form allows you to set (or reset)
the print syntax of a constant. In particular, you can change the
precedence, parsing method, and token representation of a constant.
(defprintsyntax +
(method presentbinaryinfixoperator)
(binding 100))
(defprintsyntax factorial
(token !)
(method presentpostfixoperator)
(binding 160))
loadsection
 reload. Causes the section to be reloaded if
the section has already been loaded.
 reloadfilesonly. Causes the files of the section (but
not the component sections) to be reloaded if the section has already
been loaded.
 quickload. Causes the section to be quickloaded.
None.
If there are no modifier arguments, this
form will simply load the component sections and files of the section
named sectionname which have not been loaded.
includefiles
None.
 reload. Causes a file to be reloaded if
the file has already been loaded.
 quickload. Causes the files to be quickloaded.
 (files
.
If there are no modifier arguments, this
form will simply load the files with specifications
which have not been
loaded.
viewexpr
 expressionstring. A string representing the expression to
be built and viewed.
 fullyparenthesize. Causes the expression to be viewed
fully parenthesized.
 fully. Same as fullyparenthesize.
 noquasiconstructors. Causes the expression to be
viewed without quasiconstructor abbreviations.
 noqcs. Same as noquasiconstructors.
 tex. Causes the expression to be xviewed (i.e., printed
in TEX and displayed in an X window TEX previewer).
 (language languagename). languagename is the name of a
language or theory in which to build the expression.
Next: 18. The Proof Commands
Up: 3. Reference Manual
Previous: 3. Reference Manual
System Administrator
20000723