simplify-defuns

(defun simplify-term1
  (ttree term
    hyps
    equiv
    thints
    prove-assumptions
    ctx
    wrld
    state)
  (prog2$ (semi-initialize-brr-wormhole state)
    (let* ((ens (ens state)) (saved-pspv (make-pspv ens
            wrld
            state
            :displayed-goal term
            :user-supplied-term term
            :orig-hints thints))
        (new-lit (fcons-term* 'equal (fcons-term* 'hide 'xxx) term))
        (current-clause (add-literal new-lit (dumb-negate-lit-lst hyps) t)))
      (er-let* ((pair (find-applicable-hint-settings *initial-clause-id*
             current-clause
             nil
             saved-pspv
             ctx
             thints
             wrld
             nil
             state)))
        (let ((hint-settings (car pair)) (thints (cdr pair)))
          (mv-let (hint-settings state)
            (cond ((null hint-settings) (mv nil state))
              (t (thanks-for-the-hint nil hint-settings nil state)))
            (er-let* ((pspv (load-hint-settings-into-pspv t
                   hint-settings
                   saved-pspv
                   nil
                   wrld
                   ctx
                   state)))
              (cond ((intersectp-eq '(:do-not-induct :do-not :induct :use :cases :by)
                   (strip-cars hint-settings)) (er soft
                    ctx
                    "It makes no sense for SIMPLIFY-TERM to be given hints for ~
                  "Goal" that include any of :do-not-induct, :do-not, ~
                  :induct, :use, :cases, or :by.  The hint ~p0 is therefore ~
                  illegal."
                    (cons "Goal" hint-settings)))
                (t (pprogn (initialize-proof-tree *initial-clause-id*
                      (list (list (implicate (conjoin hyps) term)))
                      ctx
                      state)
                    (let* ((rcnst (change rewrite-constant
                           (access prove-spec-var pspv :rewrite-constant)
                           :force-info (if (ffnnamep-lst 'if current-clause)
                             'weak
                             t))) (pts nil))
                      (mv-let (contradictionp type-alist fc-pair-lst)
                        (forward-chain current-clause
                          pts
                          (access rewrite-constant rcnst :force-info)
                          nil
                          wrld
                          ens
                          (access rewrite-constant rcnst :oncep-override)
                          state)
                        (declare (ignore fc-pair-lst))
                        (cond (contradictionp (er soft
                              ctx
                              "Contradiction found in hypotheses using type-set ~
                          reasoning!"))
                          (t (sl-let (contradictionp simplify-clause-pot-lst)
                              (setup-simplify-clause-pot-lst current-clause
                                (pts-to-ttree-lst pts)
                                nil
                                type-alist
                                rcnst
                                wrld
                                state
                                (initial-step-limit wrld state))
                              (cond (contradictionp (er soft
                                    ctx
                                    "Contradiction found in hypotheses using linear ~
                             reasoning!"))
                                (t (let ((local-rcnst (change rewrite-constant
                                         rcnst
                                         :current-literal (make current-literal :not-flg nil :atm term))) (gstack (initial-gstack 'simplify-clause nil current-clause)))
                                    (sl-let (rewritten-term ttree)
                                      (rewrite-entry (rewrite term nil 1)
                                        :rdepth (rewrite-stack-limit wrld)
                                        :obj '?
                                        :fnstack nil
                                        :ancestors nil
                                        :step-limit step-limit
                                        :pre-dwp nil
                                        :backchain-limit 500
                                        :geneqv (cadr (car (last (getprop equiv 'congruences nil 'current-acl2-world wrld))))
                                        :pequiv-info nil)
                                      (sl-let (bad-ass ttree)
                                        (resume-suspended-assumption-rewriting ttree
                                          nil
                                          gstack
                                          simplify-clause-pot-lst
                                          local-rcnst
                                          wrld
                                          state
                                          step-limit)
                                        (cond (bad-ass (er soft
                                              ctx
                                              "Generated false assumption, ~p0!  So, ~
                                   rewriting is aborted, just as it would be ~
                                   in the course of a regular ACL2 proof."
                                              bad-ass))
                                          (prove-assumptions (mv-let (pairs pspv state)
                                              (process-assumptions 0
                                                (change prove-spec-var
                                                  saved-pspv
                                                  :tag-tree (set-cl-ids-of-assumptions ttree *initial-clause-id*))
                                                wrld
                                                state)
                                              (er-let* ((ttree (accumulate-ttree-and-step-limit-into-state (access prove-spec-var pspv :tag-tree)
                                                     step-limit
                                                     state)) (thints (value thints)))
                                                (er-let* ((new-ttree (prove-loop1 1 nil pairs pspv thints ens wrld ctx state)))
                                                  (value (cons rewritten-term (cons-tag-trees ttree new-ttree)))))))
                                          (t (value (cons rewritten-term ttree))))))))))))))))))))))))

(defun simplify-term*
  (remaining-iters ttree
    term
    hyps
    equiv
    thints
    prove-assumptions
    ctx
    wrld
    state)
  (if (zp remaining-iters)
    (value (list* term t ttree))
    (er-let* ((term-ttree (simplify-term1 ttree
           term
           hyps
           equiv
           thints
           prove-assumptions
           ctx
           wrld
           state)))
      (if (equal term (car term-ttree))
        (value (list* term nil ttree))
        (simplify-term* (1- remaining-iters)
          (cdr term-ttree)
          (car term-ttree)
          hyps
          equiv
          thints
          prove-assumptions
          ctx
          wrld
          state)))))

(defun simplify-term
  (repeat-limit translate-flg
    inhibit-output
    form
    hyps
    equiv
    hints
    prove-assumptions
    ctx
    wrld
    state)
  (state-global-let* ((inhibit-output-lst (if inhibit-output
         (union-eq '(proof-tree prove) (@ inhibit-output-lst))
         (@ inhibit-output-lst))))
    (let ((name-tree 'simplify-term))
      (er-let* ((thints (translate-hints name-tree hints ctx wrld state)) (thyps (if translate-flg
              (translate-term-lst hyps t t t ctx wrld state)
              (value hyps)))
          (term (if translate-flg
              (translate form t t t ctx wrld state)
              (value form))))
        (simplify-term* repeat-limit
          nil
          term
          hyps
          equiv
          thints
          prove-assumptions
          ctx
          wrld
          state)))))

(defun strip-leading-percent-from-symbol
  (sym)
  (let* ((name (symbol-name sym)) (len (length name)))
    (if (and (not (int= len 0)) (eq (char name 0) #\%))
      (intern-in-package-of-symbol (subseq name 1 len) sym)
      sym)))

(defun strip-leading-percent-from-symbol-list
  (sym-list acc)
  (if (endp sym-list)
    acc
    (strip-leading-percent-from-symbol-list (cdr sym-list)
      (cons (strip-leading-percent-from-symbol (car sym-list))
        acc))))

(defun percentify (name) (concatenate 'string "%" name))

(defun sublis-fn!
  (alist term)
  (mv-let (erp new-term)
    (sublis-fn alist term nil)
    (assert$ (null erp) new-term)))

(defun %f-is-f-lemmas-rev
  (%f f
    formals-decls
    orig-body
    untranslated-new-body
    translated-new-body
    counter
    old-theory
    wrld)
  (let* ((%f-name (symbol-name %f)) (f-name (symbol-name f))
      (%%f-name (percentify %f-name))
      (%%f (intern-in-package-of-symbol %%f-name %f))
      (f-body-is-%f-body_s (intern-in-package-of-symbol (concatenate 'string f-name "-BODY-IS-" %f-name "-BODY_S")
          %f))
      (%%f-is-f (intern-in-package-of-symbol (concatenate 'string %%f-name "-IS-" f-name)
          %f))
      (f-is-%f (intern-in-package-of-symbol (concatenate 'string f-name "-IS-" %f-name)
          %f))
      (new-theory (intern (concatenate 'string
            "THEORY-"
            (coerce (explode-atom (1+ counter) 10) 'string))
          "ACL2"))
      (recp (getprop %f 'recursivep nil 'current-acl2-world wrld))
      (formals (car formals-decls))
      (%%f-formals (cons %%f formals))
      (%f-formals (cons %f formals))
      (f-formals (cons f formals))
      (equal-bodies (and (not recp) (equal untranslated-new-body orig-body))))
    `((local (deftheory ,NEW-THEORY
         (union-theories '(,F-IS-%F) (theory ',OLD-THEORY)))) (defthm ,F-IS-%F
        (equal ,F-FORMALS ,%F-FORMALS)
        :hints (,(IF RECP
     `("Goal" :BY (:FUNCTIONAL-INSTANCE ,%%F-IS-F (,%%F ,%F)) :DO-NOT
       '(PREPROCESS) :EXPAND (,%F-FORMALS))
     `("Goal" :EXPAND
       ((:FREE ,FORMALS ,%F-FORMALS) (:FREE ,FORMALS ,F-FORMALS)) :IN-THEORY
       (THEORY ',OLD-THEORY) :DO-NOT '(PREPROCESS)
       ,@(AND (NOT EQUAL-BODIES) `(:USE ,F-BODY-IS-%F-BODY_S))))))
      ,@(COND
   (RECP
    `((LOCAL
       (DEFTHM ,%%F-IS-F (EQUAL ,%%F-FORMALS ,F-FORMALS) :HINTS
               (("Goal" :IN-THEORY
                 (UNION-THEORIES '((:INDUCTION ,%%F)) (THEORY ',OLD-THEORY))
                 :DO-NOT '(PREPROCESS) :EXPAND (,%%F-FORMALS ,F-FORMALS)
                 :INDUCT T))))
      (LOCAL
       (DEFUN ,%%F ,FORMALS
         ,@(CDR FORMALS-DECLS)
         ,(UNTRANSLATE (SUBLIS-FN! (LIST (CONS %F %%F)) TRANSLATED-NEW-BODY)
                       NIL WRLD)))))
   (EQUAL-BODIES NIL)
   (T
    `((LOCAL
       (DEFTHM ,F-BODY-IS-%F-BODY_S (EQUAL ,UNTRANSLATED-NEW-BODY ,ORIG-BODY)
               :HINTS (("Goal" :DO-NOT '(PREPROCESS))) :RULE-CLASSES NIL))))))))

(defun get-state-value
  (sym state)
  (if (f-boundp-global sym state)
    (f-get-global sym state)
    nil))

(defun simplify-repeat-limit
  (state)
  (or (get-state-value 'simplify-repeat-limit state) 3))

(defun simplify-inhibit
  (state)
  (let ((val (get-state-value 'simplify-inhibit state)))
    (case val
      ((t) nil)
      ((nil) '(prove proof-tree warning observation event summary))
      (otherwise val))))

(defun simplify-defun
  (info def lemmas counter old-theory ens wrld state)
  (let* ((fn (cadr def)) (new-fn (strip-leading-percent-from-symbol fn))
      (orig-body (car (last def))))
    (if (eq new-fn fn)
      (mv nil nil lemmas counter old-theory state)
      (mv-let (erp simp state)
        (pprogn (fms "~x0"
            (list (cons #\0 (cadr def)))
            *standard-co*
            state
            nil)
          (simplify-term (simplify-repeat-limit state)
            t
            (simplify-inhibit state)
            orig-body
            nil
            'equal
            nil
            t
            'simplify-defun
            wrld
            state))
        (if erp
          (mv-let (erp val state)
            (er soft
              'simplify-defun
              "Simplification failed for the definition of ~x0."
              fn)
            (declare (ignore erp val))
            (mv t nil nil counter old-theory state))
          (let* ((new-body (car simp)) (untranslated-new-body (untranslate new-body nil wrld))
              (new-body-stripped (strip-percents new-body))
              (untranslated-new-body-stripped (untranslate new-body-stripped nil wrld))
              (formals-decls (butlast (cddr def) 1))
              (new-lemmas (if (eq info 'mut-rec)
                  nil
                  (%f-is-f-lemmas-rev fn
                    new-fn
                    formals-decls
                    orig-body
                    untranslated-new-body
                    new-body
                    counter
                    old-theory
                    wrld)))
              (first-new-lemma (car new-lemmas))
              (new-theory-p (case-match first-new-lemma
                  (('local ('deftheory . &)) t)
                  (& nil)))
              (new-theory (if new-theory-p
                  (cadr (cadr first-new-lemma))
                  old-theory))
              (new-counter (if new-theory-p
                  (1+ counter)
                  counter)))
            (mv nil
              `(,(IF (ENABLED-RUNEP (LIST :DEFINITION FN) ENS WRLD)
     'DEFUN
     'DEFUND) ,NEW-FN
                ,@FORMALS-DECLS
                ,UNTRANSLATED-NEW-BODY-STRIPPED)
              (append new-lemmas lemmas)
              new-counter
              new-theory
              state)))))))

(defun mut-rec-formals
  (defs formals)
  (if (endp defs)
    formals
    (let* ((def (car defs)) (new-formals (and (true-listp def) (caddr def)))
        (formals-okp (if formals
            (equal formals new-formals)
            (and (consp new-formals)
              new-formals
              (null (cdr new-formals))))))
      (and formals-okp (mut-rec-formals (cdr defs) new-formals)))))

(defun f-is-%f-list
  (defs formals acc)
  (if (endp defs)
    acc
    (f-is-%f-list (cdr defs)
      formals
      (let* ((%f (cadar defs)) (f (strip-leading-percent-from-symbol %f)))
        (if (eq %f f)
          acc
          (cons `(equal (,F ,@FORMALS) (,%F ,@FORMALS)) acc))))))

(defun f-is-%f-base-lemmas
  (f-is-%f-list formals zp-formals acc)
  (if (endp f-is-%f-list)
    acc
    (f-is-%f-base-lemmas (cdr f-is-%f-list)
      formals
      zp-formals
      (cons (let* ((equality (car f-is-%f-list)) (f (car (cadr equality)))
            (%f (car (caddr equality)))
            (lemma-name (intern (concatenate 'string
                  (symbol-name f)
                  "-IS-"
                  (symbol-name %f)
                  "-BASE")
                "ACL2")))
          `(local (defthm ,LEMMA-NAME
              (implies ,ZP-FORMALS ,EQUALITY)
              :hints (("Goal" :expand ((,F ,@FORMALS) (,%F ,@FORMALS)))))))
        acc))))

(defun f-is-%f-induction-step-lemmas
  (f-is-%f-list formals hyp acc)
  (if (endp f-is-%f-list)
    acc
    (f-is-%f-induction-step-lemmas (cdr f-is-%f-list)
      formals
      hyp
      (cons (let* ((equality (car f-is-%f-list)) (f (car (cadr equality)))
            (%f (car (caddr equality)))
            (lemma-name (intern (concatenate 'string
                  (symbol-name f)
                  "-IS-"
                  (symbol-name %f)
                  "-INDUCTION_STEP")
                "ACL2"))
            (f-formals (cons f formals))
            (%f-formals (cons %f formals)))
          `(local (defthm ,LEMMA-NAME
              (implies ,HYP (equal ,F-FORMALS ,%F-FORMALS))
              :instructions (:promote (:dv 1)
                :x-dumb :nx :x-dumb :top (:s :normalize nil
                  :backchain-limit 1000
                  :expand :lambdas :repeat 4)))))
        acc))))

(defun f-is-%f-lemmas-mut-rec
  (f-is-%f-list formals acc)
  (if (endp f-is-%f-list)
    acc
    (f-is-%f-lemmas-mut-rec (cdr f-is-%f-list)
      formals
      (cons (let* ((equality (car f-is-%f-list)) (f (car (cadr equality)))
            (%f (car (caddr equality)))
            (lemma-name (intern (concatenate 'string
                  (symbol-name f)
                  "-IS-"
                  (symbol-name %f))
                "ACL2")))
          `(defthm ,LEMMA-NAME
            (equal (,F ,@FORMALS) (,%F ,@FORMALS))
            :hints (("Goal" :do-not '(preprocess)))))
        acc))))

(defun mutual-recursion-lemmas
  (formals f-is-%f-list counter old-theory)
  (let* ((%%p-name (concatenate 'string
         *%%p*
         (coerce (explode-atom counter 10) 'string))) (%%p (intern %%p-name "ACL2"))
      (%%p-formals (cons %%p formals))
      (%%p-property (intern (concatenate 'string %%p-name "-PROPERTY") "ACL2"))
      (%%p-base (intern (concatenate 'string %%p-name "-BASE") "ACL2"))
      (%%p-induction-step (intern (concatenate 'string %%p-name "-INDUCTION_STEP")
          "ACL2"))
      (not-zp-formal `(not (zp ,@FORMALS)))
      (formal (car formals))
      (%%p-formal-minus-1 `(,%%P (1- ,FORMAL)))
      (induction-hyp `(and ,NOT-ZP-FORMAL ,%%P-FORMAL-MINUS-1))
      (%%p-holds (intern (concatenate 'string %%p-name "-HOLDS") "ACL2"))
      (%%p-implies-f-is-%f-theory (intern (concatenate 'string %%p-name "-IMPLIES-F-IS-%F-THEORY")
          "ACL2"))
      (new-theory (intern (concatenate 'string
            "THEORY-"
            (coerce (explode-atom (1+ counter) 10) 'string))
          "ACL2")))
    `((local (deftheory ,NEW-THEORY
         (union-theories (set-difference-theories (current-theory :here)
             (current-theory ',%%P-HOLDS))
           (theory ',OLD-THEORY)))) (encapsulate nil
        (local (in-theory (union-theories '(,%%P-HOLDS)
              (theory ',%%P-IMPLIES-F-IS-%F-THEORY))))
        ,@(F-IS-%F-LEMMAS-MUT-REC F-IS-%F-LIST FORMALS NIL))
      (local (defthm ,%%P-HOLDS
          ,%%P-FORMALS
          :hints (("Goal" :induct (%%sub1-induction ,@FORMALS)
             :do-not '(preprocess)
             :in-theory (union-theories '(,%%P-BASE ,%%P-INDUCTION-STEP
                 (:induction %%sub1-induction))
               (theory 'minimal-theory))))))
      (local (encapsulate nil
          (local (in-theory (disable ,%%P ,%%P-BASE)))
          (local (deflabel %%induction-start))
          ,@(F-IS-%F-INDUCTION-STEP-LEMMAS F-IS-%F-LIST FORMALS INDUCTION-HYP NIL)
          (defthm ,%%P-INDUCTION-STEP
            (implies ,INDUCTION-HYP ,%%P-FORMALS)
            :instructions (:promote :x-dumb (:s :normalize nil)))))
      (local (encapsulate nil
          (local (in-theory (disable ,%%P-PROPERTY)))
          ,@(F-IS-%F-BASE-LEMMAS F-IS-%F-LIST FORMALS `(ZP ,@FORMALS) NIL)
          (defthm ,%%P-BASE
            (implies (zp ,@FORMALS) ,%%P-FORMALS)
            :instructions (:promote :x-dumb (:s :normalize nil)))))
      (local (deftheory ,%%P-IMPLIES-F-IS-%F-THEORY
          (union-theories (set-difference-theories (current-theory :here)
              (current-theory ',%%P))
            (theory 'minimal-theory))))
      (local (defthm ,%%P-PROPERTY
          (implies (,%%P ,@FORMALS) (%%and-tree ,@F-IS-%F-LIST))
          :hints (("Goal" :in-theory (union-theories '(,%%P) (theory 'minimal-theory))))))
      (local (defun ,%%P
          ,FORMALS
          (declare (xargs :normalize nil))
          (%%and-tree ,@F-IS-%F-LIST))))))

(defun my-translate-rule-class-alist
  (token alist seen orig-name corollary ctx wrld state)
  (cond ((null alist) (value (alist-to-keyword-alist seen nil)))
    (t (er-let* ((val (case (car alist)
             (:corollary (value corollary))
             (:hints (value nil))
             (:instructions (value nil))
             (:otf-flg (value (cadr alist)))
             (:trigger-fns (value (reverse (strip-leading-percent-from-symbol-list (cadr alist) nil))))
             (:trigger-terms (er-let* ((terms (translate-term-lst (cadr alist) t t t ctx wrld state)))
                 (value (strip-percents-lst terms nil))))
             (:typed-term (er-let* ((term (translate (cadr alist) t t t ctx wrld state)))
                 (value (strip-percents term))))
             (:backchain-limit-lst (value (cadr alist)))
             (:match-free (value (cadr alist)))
             (:clique (let ((clique (cond ((null (cadr alist)) nil)
                      ((atom (cadr alist)) (strip-leading-percent-from-symbol (cadr alist)))
                      (t (strip-leading-percent-from-symbol-list (cadr alist) nil)))))
                 (value clique)))
             (:type-set (value (cadr alist)))
             (otherwise (er soft
                 ctx
                 "The key ~x0 is not yet implemented for rule class ~
                   translation."
                 (car alist))))))
        (my-translate-rule-class-alist token
          (cddr alist)
          (if val
            (let ((new-seen (cons (cons (car alist) val) seen)))
              (if (eq (car alist) :corollary)
                (cons (cons :hints `(("Goal" :use (,TOKEN ,ORIG-NAME))))
                  new-seen)
                new-seen))
            seen)
          orig-name
          corollary
          ctx
          wrld
          state)))))

(defun my-translate-rule-class1
  (name class ctx wrld state)
  (let ((orig-corollary (cadr (assoc-keyword :corollary (cdr class)))))
    (er-let* ((corollary (cond (orig-corollary (translate orig-corollary t t t ctx wrld state))
           (t (value nil)))) (alist (my-translate-rule-class-alist (car class)
            (cdr class)
            nil
            name
            (and corollary
              (untranslate (strip-percents corollary) t wrld))
            ctx
            wrld
            state)))
      (value (cons (car class) alist)))))

(defun my-translate-rule-class
  (name x ctx wrld state)
  (cond ((symbolp x) (value x))
    (t (my-translate-rule-class1 name x ctx wrld state))))

(defun my-translate-rule-classes1
  (name classes ctx wrld state)
  (cond ((atom classes) (value nil))
    (t (er-let* ((class (my-translate-rule-class name (car classes) ctx wrld state)) (rst (my-translate-rule-classes1 name
              (cdr classes)
              ctx
              wrld
              state)))
        (value (cons class rst))))))

(defun my-translate-rule-classes
  (name classes ctx wrld state)
  (cond ((atom classes) (value classes))
    (t (my-translate-rule-classes1 name classes ctx wrld state))))

(defun strip-percents-from-lemma
  (lemma ctx wrld state)
  (case-match lemma
    ((defthm name formula . other) (cond ((member-eq defthm '(defthm defthmd)) (let ((new-name (strip-leading-percent-from-symbol name)))
            (if (eq name new-name)
              (value nil)
              (let ((rcs (cadr (assoc-keyword :rule-classes other))))
                (er-let* ((term (translate formula t t t ctx wrld state)) (classes (my-translate-rule-classes name rcs ctx wrld state)))
                  (value `(,DEFTHM ,NEW-NAME
                      ,(UNTRANSLATE (STRIP-PERCENTS TERM) T WRLD)
                      :hints (("Goal" :use ,NAME))
                      ,@(AND CLASSES (LIST :RULE-CLASSES CLASSES)))))))))
        (t (value nil))))
    (& (value nil))))

(defun strip-percents-from-lemmas
  (lemmas acc ctx wrld state)
  (if (endp lemmas)
    (value (reverse acc))
    (er-let* ((new-lemma (strip-percents-from-lemma (car lemmas) ctx wrld state)))
      (strip-percents-from-lemmas (cdr lemmas)
        (if new-lemma
          (cons new-lemma acc)
          acc)
        ctx
        wrld
        state))))

(defun simplify-defuns
  (defs all-defs acc lemmas counter old-theory ens wrld state)
  (cond ((endp defs) (let ((formals (mut-rec-formals all-defs nil)))
        (if formals
          (let* ((new-lemmas (mutual-recursion-lemmas formals
                 (f-is-%f-list all-defs formals nil)
                 counter
                 old-theory)) (new-deftheory (cadr (car new-lemmas))))
            (mv nil
              (cons 'mutual-recursion (reverse acc))
              (append new-lemmas lemmas)
              (1+ counter)
              (cadr new-deftheory)
              state))
          (mv-let (erp val state)
            (er soft
              'simplify-defuns
              "Did not find a unique singleton list of formals for the ~
                     mutual-recursion nest starting with:~%~x0."
              (car all-defs))
            (declare (ignore erp val))
            (mv t nil nil counter old-theory state)))))
    (t (mv-let (erp def new-lemmas counter new-theory state)
        (simplify-defun 'mut-rec
          (car defs)
          lemmas
          counter
          old-theory
          ens
          wrld
          state)
        (if erp
          (mv t nil nil counter new-theory state)
          (simplify-defuns (cdr defs)
            all-defs
            (if def
              (cons def acc)
              acc)
            new-lemmas
            counter
            new-theory
            ens
            wrld
            state))))))

(defun simplify-form
  (form lemmas counter old-theory ens wrld state)
  (let ((car-form (and (consp form) (car form))))
    (case car-form
      ((defun defund) (simplify-defun nil
          form
          lemmas
          counter
          old-theory
          ens
          wrld
          state))
      (mutual-recursion (simplify-defuns (cdr form)
          (cdr form)
          nil
          lemmas
          counter
          old-theory
          ens
          wrld
          state))
      (defuns (mv-let (erp val state)
          (er soft
            'simplify-form
            "Simplify-form does not yet handle DEFUNS, but it ~
                           could.")
          (declare (ignore erp val))
          (mv t nil nil counter old-theory state)))
      (otherwise (mv nil nil lemmas counter old-theory state)))))

(defun simplify-forms
  (forms defs lemmas counter old-theory ens wrld state)
  (cond ((endp forms) (pprogn (newline *standard-co* state)
        (mv nil
          (reverse defs)
          (case-match lemmas
            ((('local ('deftheory . &)) . &) (cdr lemmas))
            (& lemmas))
          state)))
    (t (mv-let (erp simp-form lemmas new-counter new-theory state)
        (simplify-form (car forms)
          lemmas
          counter
          old-theory
          ens
          wrld
          state)
        (cond (erp (mv t nil nil state))
          (simp-form (simplify-forms (cdr forms)
              (cons simp-form defs)
              lemmas
              new-counter
              new-theory
              ens
              wrld
              state))
          (t (simplify-forms (cdr forms)
              defs
              lemmas
              new-counter
              new-theory
              ens
              wrld
              state)))))))

(defun final-deftheory-1
  (lemmas acc)
  (cond ((endp lemmas) acc)
    ((eq (caar lemmas) 'defthm) (final-deftheory-1 (cdr lemmas) (cons (cadar lemmas) acc)))
    ((eq (caar lemmas) 'encapsulate) (final-deftheory-1 (cdr lemmas)
        (final-deftheory-1 (cddar lemmas) acc)))
    (t (final-deftheory-1 (cdr lemmas) acc))))

(defun final-deftheory
  (lemmas)
  `(deftheory %-removal-theory
    (union-theories ',(FINAL-DEFTHEORY-1 LEMMAS NIL)
      (theory 'minimal-theory))))

(defun initial-equality-events
  (in-defs out-defs)
  (declare (ignore out-defs))
  (list (car in-defs)
    '(local (defun %%sub1-induction
        (n)
        (if (zp n)
          n
          (%%sub1-induction (1- n)))))
    '(local (defun %%and-tree-fn
        (args len)
        (declare (xargs :mode :program))
        (if (< len 20)
          (cons 'and args)
          (let* ((len2 (floor len 2)))
            (list 'and
              (%%and-tree-fn (take len2 args) len2)
              (%%and-tree-fn (nthcdr len2 args) (- len len2)))))))
    '(local (defmacro %%and-tree
        (&rest args)
        (%%and-tree-fn args (length args))))))

(defun write-lemma-file
  (infile outfile initial-events ctx state)
  (er-let* ((in-lemmas (read-list infile ctx state)) (out-lemmas (strip-percents-from-lemmas in-lemmas
          nil
          ctx
          (w state)
          state)))
    (write-list (cons (car in-lemmas) (append initial-events out-lemmas))
      outfile
      ctx
      state)))

(defun write-lemma-files
  (thm-file-pairs erp ctx state)
  (if (endp thm-file-pairs)
    (mv erp nil state)
    (mv-let (erp val state)
      (write-lemma-file (caar thm-file-pairs)
        (cadar thm-file-pairs)
        (cddar thm-file-pairs)
        ctx
        state)
      (declare (ignore val))
      (write-lemma-files (cdr thm-file-pairs) erp ctx state))))

(defun transform-defuns-fn
  (in-defs-file out-defs-file
    equalities-file
    extra-initial-events-for-defs
    extra-initial-events-for-lemmas
    thm-file-pairs
    state)
  (let ((ctx 'transform-defuns) (first-lemma '(local (deftheory theory-0 (theory 'minimal-theory)))))
    (mv-let (erp in-defs state)
      (read-list in-defs-file ctx state)
      (if erp
        (silent-error state)
        (mv-let (erp out-defs lemmas state)
          (if (or out-defs-file equalities-file)
            (simplify-forms in-defs
              nil
              (list first-lemma)
              0
              'theory-0
              (ens state)
              (w state)
              state)
            (mv nil nil nil state))
          (if erp
            (silent-error state)
            (er-progn (if out-defs-file
                (write-list (append (list (car in-defs)
                      '(set-ignore-ok t)
                      '(set-irrelevant-formals-ok t)
                      '(set-bogus-mutual-recursion-ok t))
                    extra-initial-events-for-defs
                    out-defs)
                  out-defs-file
                  ctx
                  state)
                (value nil))
              (if equalities-file
                (write-list (append (initial-equality-events in-defs out-defs)
                    extra-initial-events-for-lemmas
                    (reverse (cons (final-deftheory lemmas) lemmas)))
                  equalities-file
                  ctx
                  state)
                (value nil))
              (write-lemma-files thm-file-pairs nil ctx state))))))))