Nonemptyp
Oset non-emptiness predicate defined with an existential quantifier.
When this predicate holds,
it provides an under-specified witness member of the set,
which is useful in certain proofs,
via the rules provided here.
The rule emptyp-to-not-nonemptyp resp. not-emptyp-to-nonemptyp
is useful to rewrite the emptiness resp. non-emptiness of a set
to the non-membership resp. membership of a witness in the set
(by also enabling nonemptyp).
Although head could be such a witness,
it seems to require a :use hint to be brought to ACL2's attention,
and its (non-)membership gets quickly rewritten away
by the in-head rule, which must be thus disabled for this purpose
(even though it may still be useful for other heads in the proof).
Furthermore, head may interact with other rules,
depending on the form of the term that denotes the set.
In contrast, nonempty-witness is abstract.
Thus this approach should provide more proof control.
The rule not-emptyp-to-nonemptyp
has more restricted applicability than emptyp-to-not-nonempty,
in case one wants to leave alone
emptyp not preceded by not.
The forward chaining rule nonemptyp-witness-from-not-emptyp
is useful to inject a witness member into a proof,
when a set is known to be non-empty in a hypothesis.
The implication rules
nonemptyp-when-not-emptyp and not-emptyp-when-nonemptyp
are mainly used to prove not-emptyp-to-nonemptyp,
but they could be useful when they provide the desired backchaining.
All these rules are disabled by default.
This file is not included in [books]/std/osets/top.lisp.
It must be included explicitly when needed.
Definitions and Theorems
Theorem: nonemptyp-suff
(defthm nonemptyp-suff
(implies (in elem set) (nonemptyp set)))
Theorem: nonemptyp-when-not-emptyp
(defthm nonemptyp-when-not-emptyp
(implies (not (emptyp set))
(nonemptyp set)))
Theorem: not-emptyp-when-nonemptyp
(defthm not-emptyp-when-nonemptyp
(implies (nonemptyp set)
(not (emptyp set))))
Theorem: not-emptyp-to-nonemptyp
(defthm not-emptyp-to-nonemptyp
(equal (not (emptyp set))
(nonemptyp set)))
Theorem: emptyp-to-not-nonemptyp
(defthm emptyp-to-not-nonemptyp
(equal (emptyp set)
(not (nonemptyp set))))
Theorem: nonemptyp-witness-from-not-emptyp
(defthm nonemptyp-witness-from-not-emptyp
(implies (not (emptyp set))
(in (nonemptyp-witness set) set))
:rule-classes ((:forward-chaining :trigger-terms ((emptyp set)))))
