		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-vartys inner-diffp 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-vartys — Guard (ident-type-mapp inner-vartys).; inner-diffp — Guard (booleanp inner-diffp).; gin — Guard (simpadd0-ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (simpadd0-goutp 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 ldm-expr maps a parenthesized expression to the same as the inner expression. Thus, the theorem for the parenthesized expression follows 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-vartys inner-diffp gin)
 (declare (xargs :guard (and (exprp inner)
                             (exprp inner-new)
                             (pseudo-event-form-listp inner-events)
                             (symbolp inner-thm-name)
                             (ident-type-mapp inner-vartys)
                             (booleanp inner-diffp)
                             (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
                             :vartys inner-vartys
                             :diffp inner-diffp)))
    (hints
        (cons (cons '"Goal"
                    (cons ':in-theory
                          (cons ''((:e 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-vartys
          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)
            :vartys inner-vartys
            :diffp inner-diffp)))))

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-vartys inner-diffp 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-vartys inner-diffp 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-vartys inner-diffp gin)))
      (expr-unambp expr))))