		Search-engine friendly clone of the ACL2 documentation.

Proof-automation

Bash-term-to-dnf

Bash-term-to-dnf is a tool that simplifies a term, producing a list of clauses such that if all output clauses are theorems, then so is the input term.

This utility is defined in community book "misc/bash.lisp". We assume here familiarity with the bash tool defined in that book, focusing below on how the present tool differs from that one.

If you submit (bash-term-to-dnf term) then the result is a list of goals produced by ACL2's simplification process, much as for the result of (bash term); see bash. However, unlike bash, bash-term-to-dnf returns a list of clauses, where each clause is a list of terms that represents the disjunction of those terms, and the list of clauses is implicitly conjoined.

Again: For related utilities, see simp and bash.

Example

First we execute:

(include-book "misc/bash" :dir :system)

Then:

ACL2 !>(bash-term-to-dnf
        '(implies (true-listp x) (equal (append x y) zzz))
        '(("Goal" :expand ((true-listp x)
                           (true-listp (cdr x))
                           (append x y))))
        nil t state)
 (((EQUAL Y ZZZ))
  ((NOT (CONSP X))
   (NOT (CONSP (CDR X)))
   (NOT (TRUE-LISTP (CDDR X)))
   (EQUAL (LIST* (CAR X)
                 (CADR X)
                 (APPEND (CDDR X) Y))
          ZZZ))
  ((NOT (CONSP X))
   (CDR X)
   (EQUAL (CONS (CAR X) Y) ZZZ)))
ACL2 !>

General Form:

(bash-term-to-dnf form hints verbose untranslate-flg state)

returns a list of clauses, each of which is a list of terms, where:

form is a user-level (untranslated) term;
hints, if supplied, is a hints structure (as for defthm);
verbose is nil by default, in which case output is inhibited; on the other extreme, if verbose is :all then a warning is printed when no simplification takes place; and
untranslate-flg is nil by default, in which case each term in each returned clause is a term in internal (translated) form and otherwise, each such term is in user-level (untranslated) form;

If each returned clause (viewed as a disjunction) is a theorem, then the input form is a theorem.