Major Section: TAU-SYSTEM
General Form: (in-tau-intervalp e x)
Here, x should be an interval (see tau-intervalp). This function
returns t or nil indicating whether e, which is generally but not
necessarily a number, is an element of interval x. By that is meant that
e satisfies the domain predicate of the interval and lies between the two
bounds.
Suppose x is an interval with the components dom, lo-rel, lo,
hi-rel and hi. Suppose (<? rel u v) means (< u v)
when rel is true and (<= u v) otherwise, with appropriate
treatment of infinities.
Then for e to be in interval x, it must be the case that e
satisfies the domain predicate dom (where where dom=nil means
there is no restriction on the domain) and (<? lo-rel lo e) and
(<? hi-rel e hi). [Note: ``Appropriate treatment of
infinities'' is slightly awkward if both infinities are represented by the
same object, nil. However, this is handled by coercing e to a
number after checking that it is in the domain. By this trick, ``<?''
is presented with at most one ``infinity'' and it is always negative
when in the first argument and positive when in the second.]
Note that every element in an INTEGERP interval is contained in the
analogous RATIONALP interval (i.e., the interval obtained by just
replacing the domain INTEGERP by RATIONALP). That is because every
integer is a rational. Similarly, every rational is an ACL2 number.
Note that an interval in which the relations are weak and the bounds are equal rationals is the ``unit'' or ``identity'' interval containing exactly that rational.
Note that an interval in which the relations are strong and the bounds are equal rationals is empty: it contains no objects.
Note that the interval (make-tau-interval nil nil nil nil nil) is the
``universal interval:'' it contains all ACL2 objects. It contains all
numbers because they statisfy the non-existent domain restriction and lie
between minus infinity and plus infinity. It contains all non-numbers
because the interval contains 0 and ACL2's inequalities coerce
non-numbers to 0. The universal interval is useful if you are defining a
bounder (see bounders) for a function and do not wish to address a certain
case: return the universal interval.
Recall that make-tau-interval constructs intervals. Using make-tau-interval
we give several self-explanatory examples of in-tau-intervalp:
(in-tau-intervalp 3 (make-tau-interval 'INTEGERP nil 0 nil 10)) = t (in-tau-intervalp 3 (make-tau-interval 'RATIONALP nil 0 nil 10)) = t (in-tau-intervalp 3 (make-tau-interval NIL nil 0 nil 10)) = t (in-tau-intervalp -3 (make-tau-interval 'INTEGERP nil 0 nil 10)) = nil (in-tau-intervalp 30 (make-tau-interval 'INTEGERP nil 0 nil 10)) = nil (in-tau-intervalp 3/5 (make-tau-interval 'INTEGERP nil 0 nil 10)) = nil (in-tau-intervalp 3/5 (make-tau-interval 'RATIONALP nil 0 nil 10)) = t (in-tau-intervalp #c(3 5) (make-tau-interval 'RATIONALP nil 0 nil 10)) = nil (in-tau-intervalp #c(3 5) (make-tau-interval 'ACL2-NUMBERP nil 0 nil 10)) = t (in-tau-intervalp 'ABC (make-tau-interval NIL nil 0 nil 10)) = t
