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
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
Again: For related utilities, see simp and bash.
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 !>
(bash-term-to-dnf form hints verbose untranslate-flg state)returns a list of clauses, each of which is a list of terms, where: