		Search-engine friendly clone of the ACL2 documentation.

Subst-free

Fundef-subst-free

Substitute expressions in for free variables appearing in a function definition.

Signature
(fundef-subst-free fundef subst bound-vars) → (mv result bound-vars)
Arguments: fundef — Guard (fundefp fundef).; subst — Guard (ident-expr-mapp subst).; bound-vars — Guard (ident-setp bound-vars).
Returns: result — Type (fundefp result).; bound-vars — Type (ident-setp bound-vars).

Definitions and Theorems

Function: fundef-subst-free

(defun fundef-subst-free (fundef subst bound-vars)
  (declare (xargs :guard (and (fundefp fundef)
                              (ident-expr-mapp subst)
                              (ident-setp bound-vars))))
  (b*
    (((fundef fundef) fundef)
     (spec (decl-spec-list-subst-free fundef.spec subst bound-vars))
     ((mv declor bound-vars param-bound-vars)
      (declor-subst-free fundef.declor subst bound-vars))
     (body-bound-vars (union bound-vars param-bound-vars))
     (attribs (attrib-spec-list-subst-free
                   fundef.attribs subst body-bound-vars))
     ((mv decls body-bound-vars)
      (decl-list-subst-free fundef.decls subst body-bound-vars))
     (body (stmt-subst-free fundef.body subst body-bound-vars)))
    (mv (make-fundef :extension fundef.extension
                     :spec spec
                     :declor declor
                     :asm? fundef.asm?
                     :attribs attribs
                     :decls decls
                     :body body)
        bound-vars)))

Theorem: fundefp-of-fundef-subst-free.result

(defthm fundefp-of-fundef-subst-free.result
  (b* (((mv ?result ?bound-vars)
        (fundef-subst-free fundef subst bound-vars)))
    (fundefp result))
  :rule-classes :rewrite)

Theorem: ident-setp-of-fundef-subst-free.bound-vars

(defthm ident-setp-of-fundef-subst-free.bound-vars
  (b* (((mv ?result ?bound-vars)
        (fundef-subst-free fundef subst bound-vars)))
    (ident-setp bound-vars))
  :rule-classes :rewrite)