simplify-thm - ACL2 Book

Included Books

bash

other

(in-package "ACL2")

other

(program)

other

(set-state-ok t)

include-book

(include-book "bash")

incatmacro

(defmacro incat
  (sym &rest strings)
  `(intern-in-package-of-symbol (concatenate 'string . ,STRINGS)
    ,SYM))

smpl-clause-to-theoremfunction

(defun smpl-clause-to-theorem
  (clause)
  `(implies (and . ,(DUMB-NEGATE-LIT-LST (BUTLAST CLAUSE 1)))
    ,(CAR (LAST CLAUSE))))

smpl-clauses-to-theoremsfunction

(defun smpl-clauses-to-theorems
  (clauses)
  (if (atom clauses)
    nil
    (cons (smpl-clause-to-theorem (car clauses))
      (smpl-clauses-to-theorems (cdr clauses)))))

smpl-to-theoremsfunction

(defun smpl-to-theorems
  (term hints state)
  (er-let* ((clauses (simplify-with-prover term hints 'smpl-to-theorems state)))
    (value (smpl-clauses-to-theorems clauses))))

smpl-clauses-to-defthmsfunction

(defun smpl-clauses-to-defthms
  (namebase n clauses args)
  (if (atom clauses)
    nil
    (cons `(defthm ,(INCAT NAMEBASE (SYMBOL-NAME NAMEBASE) "-" (EXPLODE-ATOM N 10))
        ,(CAR CLAUSES) . ,ARGS)
      (smpl-clauses-to-defthms namebase (1+ n) (cdr clauses) args))))

simplify-thm-fnfunction

(defun simplify-thm-fn
  (namebase form smpl-hints args state)
  (er-let* ((forms (smpl-to-theorems form smpl-hints state)))
    (value (smpl-clauses-to-defthms namebase 0 forms args))))