Generate the theorem about a formal parameter of a target function.
(atc-gen-formal-thm fn fn-guard fn-formals formal type defobj-pred prec-tags names-to-avoid wrld) → (mv event name updated-names-to-avoid)
The theorem asserts that, under the guard, the formal satisfies the type recognizer from the shallow embedding (e.g. sintp). This property is used in proofs that build on this theorem.
The theorem is proved in the theory that consists of just the guard function, the star wrapper, and the defobject predicate if the formal refers to an external object. This is because the recognizer predicate is either directly in a conjunct in the guard, possibly wrapped by star, or in the definition of the defobject predicate that is in a conjunct of the guard.
Function:
(defun atc-gen-formal-thm (fn fn-guard fn-formals formal type defobj-pred prec-tags names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (symbol-listp fn-formals) (symbolp formal) (typep type) (symbolp defobj-pred) (atc-string-taginfo-alistp prec-tags) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-formal-thm)) (declare (ignorable __function__)) (b* ((name (pack fn '- formal)) ((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix name nil names-to-avoid wrld)) (pred (atc-type-to-recognizer type prec-tags)) (formula (cons 'implies (cons (cons fn-guard fn-formals) (cons (cons pred (cons formal 'nil)) 'nil)))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons fn-guard (cons 'star (and defobj-pred (list defobj-pred)))) 'nil)) 'nil))) 'nil)) ((mv event &) (evmac-generate-defthm name :formula formula :hints hints :enable nil))) (mv event name names-to-avoid))))
Theorem:
(defthm pseudo-event-formp-of-atc-gen-formal-thm.event (b* (((mv acl2::?event ?name ?updated-names-to-avoid) (atc-gen-formal-thm fn fn-guard fn-formals formal type defobj-pred prec-tags names-to-avoid wrld))) (pseudo-event-formp event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-formal-thm.name (b* (((mv acl2::?event ?name ?updated-names-to-avoid) (atc-gen-formal-thm fn fn-guard fn-formals formal type defobj-pred prec-tags names-to-avoid wrld))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-formal-thm.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv acl2::?event ?name ?updated-names-to-avoid) (atc-gen-formal-thm fn fn-guard fn-formals formal type defobj-pred prec-tags names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)