Generate a theorem.

Example:

(defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y)))) ; show some output :print-flg t)

General Forms:

(DEFTHM? name (IMPLIES hyps (equiv term ?)) :hints hints :prove-assumptions prove-flg ; t or nil, default t :print-flg print-flg ; t or nil, default nil :simplify-hyps-p flg ; t, nil, or :no-split; default t ) (DEFTHM? name (equiv term ?) :hints hints :prove-assumptions prove-flg ; t or nil, default t :print-flg print-flg ; t or nil, default nil :simplify-hyps-p flg ; t, nil, or :no-split; default t )

where

If the given

In general, simplification may generate assumptions because of force.
By default, an attempt is made to prove these assumptions, which must succeed
or else this event fails. However, if

See rewrite$ for a flexible, convenient interface to the ACL2 rewriter that can be called programmatically. Also see symsim.

Here are some examples, including the one above. Try them out and see what happens.

; Doesn't simplify, so fails: (defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand (true-listp x)))) :pbt 0 ; The following creates one event, but maybe we'd prefer cases to be ; broken out into separate events. That comes next. (defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand (append x y)))) :pbt 0 :pe :here :pe APP-SIMPLIFY :u (defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y)))) ; show some extra output; this is optional :print-flg t) :pe :here :u