In-tau-intervalp
Boolean membership in a tau interval
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 satisfy 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
