Simplify given term and hypotheses.

Example:

(symsim (append x y) ((not (atom x)) (not (cdr x))) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y)))))

yields

Simplified term: (CONS (CAR X) Y) Simplified hyps: ((CONSP X) (NOT (CDR X)))~/ General Form: (symsim term hyps :hints hints :inhibit-output inhibit-flg ; t, :prove, :all, or nil, default t :prove-assumptions prove-flg ; t, nil, or (default) any other value :print-flg print-flg ; t or nil, default nil :simplify-hyps-p flg ; t, nil, or :no-split; default t )

where

Prover output is inhibited if

See rewrite$ for a flexible, convenient interface to the ACL2
rewriter that can be called programmatically. Also see defthm?, which
is related to

(symsim (append x y) nil :hints (("Goal" :expand ((true-listp x) (append x y) (append (cdr x) y))))) ; Generates three cases: (symsim (append x y) ((true-listp x)) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y) (append (cdr x) y))))) ; Let's illustrate the role of FORCE. The following rule ; forces append to open up, and comes into play below. (defthm true-listp-expand-append (implies (and (force (true-listp x)) x) (equal (append x y) (cons (car x) (append (cdr x) y))))) ; Generates assumption forced by preceding rule. (symsim (append x y) ((not (atom x)))) ; But now we fail; but why? See next form. (symsim (append x y) ((consp x)) :prove-assumptions t) ; Let's not inhibit output. Then we can see the failed forcing round. (symsim (append x y) ((consp x)) :prove-assumptions t :inhibit-output nil) ; As above, but doesn't deal with generated forced assumptions at all (just ; drops them on the floor). (symsim (append x y) ((consp x)) :prove-assumptions nil)