def-functional-instance

(in-package "ACL2")

(defxdoc def-functional-instance
  :parents (functional-instantiation)
  :short "Functionally instantiate a pre-existing theorem to prove a new one."
  :long "<p>Usage:</p>

@({
 (def-functional-instance new-thm-name
   orig-thm-name
   ((orig-fn substitute-fn) ...)
   :hints (...)                   ;; optional
   :rule-classes rule-classes)    ;; optional
})

<p>Def-functional-instance attempts to define a new theorem based on
functionally instantiating an existing one with a user-provided function
substitution.  It looks up the body of the theorem named ORIG-THM-NAME in the
ACL2 world and applies the functional substitution, replacing each ORIG-FN with
SUBSTITUTE-FN in the theorem body.  It then submits this as a new theorem named
NEW-THM-NAME with a hint to prove it using a functional instance of the
original theorem.  This theorem has either the given rule-classes or, if this
argument is omitted, the rule-classes of the original theorem.</p>

<p>Sometimes further hints are needed to show that the functional instantiation
is valid.  These may be given by the :hints keyword.  Note, however, that there
is already a hint provided at "goal", so that if one of the user-provided
hints uses this as its subgoal specifier, this hint will be ignored.  The extra
hints given should either be computed hints or reference later subgoals.</p>")