Examples illustrating `simplify-defun-sk`.

The examples below are deliberately quite trivial, in order to make clear
how

(defthm member-equal-fix-true-list (iff (member-equal a (fix-true-list lst)) (member-equal a lst)))

We start with the following basic example. The keywords can all be omitted with minimal change to the outcome, but we include them as a way to introduce some of the simplest keywords.

(defun-sk foo (lst) (exists x (member-equal x (fix-true-list lst)))) ; redundant (see above) (defthm member-equal-fix-true-list (iff (member-equal a (fix-true-list lst)) (member-equal a lst))) (simplify-defun-sk foo :new-name foo-simp :thm-name foo-simplified :function-disabled nil :thm-enable t :skolem-name foo-simp-sk)

ACL2 responds to the call above of

(DEFUN-SK FOO-SIMP (LST) (EXISTS (X) (MEMBER-EQUAL X LST)) :QUANT-OK T :SKOLEM-NAME FOO-SIMP-SK)

You can add

To see the full expansion produced by the call of

(ENCAPSULATE NIL ... ; helpful stuff local to the encapsulate (DEFUN-SK FOO-SIMP ...) ; as shown above ... ; local helper events, not shown here (DEFTHM FOO-SIMPLIFIED ; the value of keyword argument :thm-name (IFF (FOO LST) (FOO-SIMP LST)) :HINTS ...) (IN-THEORY (DISABLE FOO-SIMP)))

Notice that new function symbol

On the other hand, if you want less output, not more, use

ACL2 !>(simplify-defun-sk foo :new-name foo-simp :thm-name foo-simplified :function-disabled t :thm-enable t :skolem-name foo-simp-sk :print nil) T ACL2 !>:pe foo-simp d 4:x(SIMPLIFY-DEFUN-SK FOO :NEW-NAME ...) >L d (DEFUN FOO-SIMP (LST) (DECLARE (XARGS :NON-EXECUTABLE T :MODE :LOGIC)) (PROG2$ (THROW-NONEXEC-ERROR 'FOO-SIMP (LIST LST)) (LET ((X (FOO-SIMP-SK LST))) (MEMBER-EQUAL X LST)))) ACL2 !>

The following trivial example illustrates the use of assumptions.

(defthm fix-true-list-is-identity (implies (true-listp x) (equal (fix-true-list x) x))) (defun-sk foo (lst1 lst2) (forall x (equal (member-equal x (fix-true-list lst1)) (member-equal x (fix-true-list lst2))))) (simplify-defun-sk foo :assumptions ((and (true-listp lst1) (true-listp lst2))))

Here is the result. Notice that since we did not specify

(DEFUN-SK FOO$1 (LST1 LST2) (FORALL (X) (EQUAL (MEMBER-EQUAL X LST1) (MEMBER-EQUAL X LST2))) :QUANT-OK T)

Notice that the body was simplified under the given assumption that
`true-listp`; without any such
assumption, no simplification would have taken place.

The following example has a non-trivial guard, and illustrates that
the value of keyword

(defun-sk foo (lst1 lst2) (declare (xargs :guard (and (true-listp lst1) (true-listp lst2)) :verify-guards nil)) (forall x (equal (member-equal x (fix-true-list lst1)) (member-equal x (fix-true-list lst2))))) (simplify-defun-sk foo :assumptions :guard)

Here is the result. Notice that the simplified body is the same as before.

(DEFUN-SK FOO$1 (LST1 LST2) (DECLARE (XARGS :NON-EXECUTABLE NIL)) (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LST1) (TRUE-LISTP LST2)) :VERIFY-GUARDS NIL)) (FORALL (X) (EQUAL (MEMBER-EQUAL X LST1) (MEMBER-EQUAL X LST2))) :QUANT-OK T)

Unlike `simplify-defun`, `defun-sk` does not support recursion.

Consider the preceding example, but where we verify guards before attempting simplification, as follows.

(verify-guards foo) (simplify-defun-sk foo :assumptions :guard)

The new `defun-sk` form is the same as before. However, this time
the new function symbol is guard-verified. If we use
`verify-guards` event is generated for the
new function symbol.

(VERIFY-GUARDS FOO$1 :HINTS (("Goal" :USE (:GUARD-THEOREM FOO))))

This illustrates that by default, guard verification will be attempted for
the new function symbol exactly when the original function symbol is
guard-verified. However, that default behavior can be overridden by using the

(simplify-defun-sk foo :assumptions :guard :verify-guards nil)

In this case, guard verification will not be attempted for the new function symbol.

(simplify-defun-sk foo :assumptions :guard :guard-hints (("Goal" :in-theory (enable append))))

Then in place of the default `verify-guards`, as displayed above, the guard hints supplied in our

(VERIFY-GUARDS FOO$1 :HINTS (("Goal" :IN-THEORY (ENABLE APPEND))))

Next, we discuss two features of `simplify-defun`.

The macro

(include-book "simplify-defun-sk") (include-book "kestrel/soft/top" :dir :system) (defunvar ?foo (*) => *) (defun-sk2 spec[?foo] (?foo) () (forall (x) (equal (?foo x) (* x 2)))) (simplify-defun-sk spec[?foo])

The resulting definition benefits from simplification of

(DEFUN-SK2 SPEC[?FOO]$1 (?FOO) NIL (FORALL (X) (EQUAL (?FOO X) (* 2 X))) :QUANT-OK T)

A second capability offered by

; Start a fresh ACL2 session. (include-book "simplify-defun-sk") (defthm member-equal-fix-true-list (iff (member-equal a (fix-true-list lst)) (member-equal a lst))) (defun-sk foo (lst) (forall x (not (member-equal x (fix-true-list lst))))) (simplify-defun-sk foo :rewrite :direct)

As a result of the

(DEFUN-SK FOO$1 (LST) (FORALL (X) (NOT (MEMBER-EQUAL X LST))) :QUANT-OK T :REWRITE :DIRECT)

As for `forall`.

By default, simplification done on behalf of `defthmd`
(not because it helps our proofs to disable it, but because that will help us
to illustrate the

; Start a fresh ACL2 session. (include-book "simplify-defun-sk") (defthmd member-equal-fix-true-list (iff (member-equal a (fix-true-list lst)) (member-equal a lst))) (defun-sk foo (lst) (exists x (member-equal x (fix-true-list lst)))) (simplify-defun-sk foo :theory (enable member-equal-fix-true-list))

If we omit the

For convenience,

(simplify-defun-sk foo :enable (member-equal-fix-true-list))

Like `simplify-defun`, value of the

The handling of patterns is the same as for

; Start a fresh ACL2 session. (include-book "simplify-defun-sk") ; Books included above define set-equiv as an equivalence relation, ; and provide some nice congruence rules. (defthm set-equiv-fix-true-list (set-equiv (fix-true-list lst) lst)) (defun-sk foo (lst1 lst2) (exists x (iff (and (member-equal x (fix-true-list lst1)) (member-equal x (fix-true-list lst2))) t))) (simplify-defun-sk foo :simplify-body (and (member-equal x @) (member-equal x (fix-true-list lst2))))

The result is below. Notice that simplification has taken place at the
subterm labeled with

(DEFUN-SK FOO$1 (LST1 LST2) (EXISTS (X) (IFF (AND (MEMBER-EQUAL X LST1) (MEMBER-EQUAL X (FIX-TRUE-LIST LST2))) T)) :QUANT-OK T)

It is interesting to note that our original lemma,

; Start a fresh ACL2 session. (include-book "simplify-defun-sk") (defthm member-equal-fix-true-list (iff (member-equal a (fix-true-list lst)) (member-equal a lst))) (defun-sk foo (lst1 lst2) (exists x (and (member-equal x (fix-true-list lst1)) (member-equal x (fix-true-list lst2))))) (simplify-defun-sk foo :simplify-body (and (member-equal x @) (member-equal x (fix-true-list lst2))))