|
|
|---|
|
|
|
|---|
Functionally instantiate a pre-existing theorem to prove a new one.
Usage:
(def-functional-instance new-thm-name orig-thm-name ((orig-fn substitute-fn) ...) :hints (...) ;; optional :rule-classes rule-classes) ;; optional
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.
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.