Turn a named formula into a theorem event.
(named-formula-to-thm-event name formula hints rule-classes enabled local names-to-avoid wrld) → (mv thm-event thm-name)
If the name of the formula is not in use and not among the names to avoid,
it is used as the name of the theorem event.
Otherwise, it is made fresh by appending
(defun named-formula-to-thm-event (name formula hints rule-classes enabled local names-to-avoid wrld) (declare (xargs :guard (and (symbolp name) (true-listp hints) (booleanp enabled) (booleanp local) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'named-formula-to-thm-event)) (declare (ignorable __function__)) (b* ((defthm/defthmd (theorem-intro-macro enabled)) (name (if (keywordp name) (intern (symbol-name name) "ACL2") name)) ((mv thm-name &) (fresh-logical-name-with-$s-suffix name nil names-to-avoid wrld)) (thm-event (cons defthm/defthmd (cons thm-name (cons formula (cons ':hints (cons hints (cons ':rule-classes (cons rule-classes 'nil)))))))) (thm-event (if local (cons 'local (cons thm-event 'nil)) thm-event))) (mv thm-event thm-name))))