		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-fn-guard

Generate a local function for the guard of fn.

Signature
(atc-gen-fn-guard fn names-to-avoid state) → (mv local-event name updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: local-event — Type (pseudo-event-formp local-event).; name — Type (symbolp name).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

This is used only in theorems, so there is no need to guard-verify it.

Definitions and Theorems

Function: atc-gen-fn-guard

(defun atc-gen-fn-guard (fn names-to-avoid state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbolp fn)
                              (symbol-listp names-to-avoid))))
  (let ((__function__ 'atc-gen-fn-guard))
    (declare (ignorable __function__))
    (b* ((wrld (w state))
         (name (pack fn "-GUARD"))
         ((mv name names-to-avoid)
          (fresh-logical-name-with-$s-suffix name 'function
                                             names-to-avoid wrld))
         (guard (uguard+ fn wrld))
         ((mv event &)
          (evmac-generate-defun name
                                :formals (formals+ fn wrld)
                                :body (untranslate$ guard t state)
                                :verify-guards nil
                                :enable nil)))
      (mv event name names-to-avoid))))

Theorem: pseudo-event-formp-of-atc-gen-fn-guard.local-event

(defthm pseudo-event-formp-of-atc-gen-fn-guard.local-event
  (b* (((mv ?local-event
            ?name ?updated-names-to-avoid)
        (atc-gen-fn-guard fn names-to-avoid state)))
    (pseudo-event-formp local-event))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-fn-guard.name

(defthm symbolp-of-atc-gen-fn-guard.name
  (b* (((mv ?local-event
            ?name ?updated-names-to-avoid)
        (atc-gen-fn-guard fn names-to-avoid state)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-fn-guard.updated-names-to-avoid

(defthm symbol-listp-of-atc-gen-fn-guard.updated-names-to-avoid
  (implies (symbol-listp names-to-avoid)
           (b* (((mv ?local-event
                     ?name ?updated-names-to-avoid)
                 (atc-gen-fn-guard fn names-to-avoid state)))
             (symbol-listp updated-names-to-avoid)))
  :rule-classes :rewrite)