		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-paren

Transform a parenthesized expression.

Signature
(simpadd0-expr-paren inner inner-new inner-events inner-thm-name inner-vars inner-diffp inner-falliblep gin) → (mv expr gout)
Arguments: inner — Guard (exprp inner).; inner-new — Guard (exprp inner-new).; inner-events — Guard (pseudo-event-form-listp inner-events).; inner-thm-name — Guard (symbolp inner-thm-name).; inner-vars — Guard (ident-setp inner-vars).; inner-diffp — Guard (booleanp inner-diffp).; inner-falliblep — Guard (booleanp inner-falliblep).; gin — Guard (simpadd0-ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (simpadd0-goutp gout).

The caller of this ACL2 function recursively transforms the inner expression, and passes to this function the possibly transformed expression, along with some of the simpadd0-gout components resulting from that transformation; it also passes a simpadd0-gin whose components have been updated from the aforementioned simpadd0-gout.

The resulting expression is obtained by parenthesizing the possibly transformed inner expression. We generate a theorem iff a theorem was generated for the inner expression, which we see from whether the theorem name is nil or not. The function c$::ldm-expr maps a parenthesized expression to the same as the inner expression. Thus, the theorem for the parenthesized expression follow directly from the one for the inner expression.

Definitions and Theorems

Function: simpadd0-expr-paren

(defun simpadd0-expr-paren
       (inner inner-new
              inner-events inner-thm-name inner-vars
              inner-diffp inner-falliblep gin)
 (declare (xargs :guard (and (exprp inner)
                             (exprp inner-new)
                             (pseudo-event-form-listp inner-events)
                             (symbolp inner-thm-name)
                             (ident-setp inner-vars)
                             (booleanp inner-diffp)
                             (booleanp inner-falliblep)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (and (expr-unambp inner)
                             (expr-unambp inner-new))))
 (let ((__function__ 'simpadd0-expr-paren))
  (declare (ignorable __function__))
  (b*
   ((expr (expr-paren inner))
    (expr-new (expr-paren inner-new))
    ((simpadd0-gin gin) gin)
    ((unless inner-thm-name)
     (mv expr-new
         (make-simpadd0-gout :events inner-events
                             :thm-name nil
                             :thm-index gin.thm-index
                             :names-to-avoid gin.names-to-avoid
                             :vars inner-vars
                             :diffp inner-diffp
                             :falliblep inner-falliblep)))
    (hints
        (cons (cons '"Goal"
                    (cons ':in-theory
                          (cons ''((:e c$::ldm-expr))
                                (cons ':use
                                      (cons inner-thm-name 'nil)))))
              'nil))
    ((mv thm-event thm-name thm-index)
     (simpadd0-gen-expr-pure-thm
          expr expr-new inner-falliblep inner-vars
          gin.const-new gin.thm-index hints)))
   (mv expr-new
       (make-simpadd0-gout
            :events (append inner-events (list thm-event))
            :thm-name thm-name
            :thm-index thm-index
            :names-to-avoid (cons thm-name gin.names-to-avoid)
            :vars inner-vars
            :diffp inner-diffp
            :falliblep inner-falliblep)))))

Theorem: exprp-of-simpadd0-expr-paren.expr

(defthm exprp-of-simpadd0-expr-paren.expr
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-paren inner inner-new
                             inner-events inner-thm-name inner-vars
                             inner-diffp inner-falliblep gin)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-expr-paren.gout

(defthm simpadd0-goutp-of-simpadd0-expr-paren.gout
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-paren inner inner-new
                             inner-events inner-thm-name inner-vars
                             inner-diffp inner-falliblep gin)))
    (simpadd0-goutp gout))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-simpadd0-expr-paren

(defthm expr-unambp-of-simpadd0-expr-paren
 (implies
   (expr-unambp inner-new)
   (b* (((mv ?expr ?gout)
         (simpadd0-expr-paren inner inner-new
                              inner-events inner-thm-name inner-vars
                              inner-diffp inner-falliblep gin)))
     (expr-unambp expr))))