		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-defsurj

Generate a local defsurj.

Signature
(expdata-gen-defsurj surjmap verify-guards$ print$) → event
Arguments: surjmap — Guard (expdata-surjmapp surjmap).; verify-guards$ — Guard (booleanp verify-guards$).; print$ — Guard (evmac-input-print-p print$).
Returns: event — Type (pseudo-event-formp event).

When the surj input is not a name, expdata internally generates and uses a defsurj, so that the rest of the generated events can uniformly rely on a defsurj that has established the surjective mapping.

This event is local to the encapsulate generated by expdata.

Since the defsurj is local, we normally do not want to print its result or info output. But we want to print errors. So we pass :error as the :print input. However, if expdata's :print input is :all, the we use :all for defsurj's :print input as well.

This is also used for the identity surjective mapping, which is also locally generated.

Definitions and Theorems

Function: expdata-gen-defsurj

(defun expdata-gen-defsurj (surjmap verify-guards$ print$)
 (declare (xargs :guard (and (expdata-surjmapp surjmap)
                             (booleanp verify-guards$)
                             (evmac-input-print-p print$))))
 (declare (xargs :guard (expdata-surjmap->localp surjmap)))
 (let ((__function__ 'expdata-gen-defsurj))
  (declare (ignorable __function__))
  (b*
   (((expdata-surjmap surjmap) surjmap)
    (name surjmap.surjname)
    (doma surjmap.newp)
    (domb surjmap.oldp)
    (alpha surjmap.back)
    (beta surjmap.forth)
    (unconditional nil)
    (guard-thms verify-guards$)
    (nonguard-thm-names
         (list :alpha-image surjmap.back-image
               :beta-image surjmap.forth-image
               :alpha-of-beta surjmap.back-of-forth
               :beta-injective surjmap.forth-injective))
    (guard-thm-names? (and guard-thms
                           (list :doma-guard surjmap.newp-guard
                                 :domb-guard surjmap.oldp-guard
                                 :alpha-guard surjmap.back-guard
                                 :beta-guard surjmap.forth-guard)))
    (thm-names (append nonguard-thm-names guard-thm-names?))
    (hints surjmap.hints)
    (print (if (eq print$ :all) :all :error)))
   (cons
    'local
    (cons
     (cons
      'defsurj
      (cons
       name
       (cons
        doma
        (cons
         domb
         (cons
          alpha
          (cons
           beta
           (cons
            ':unconditional
            (cons
             unconditional
             (cons
              ':guard-thms
              (cons
               guard-thms
               (cons
                ':thm-names
                (cons
                  thm-names
                  (cons ':hints
                        (cons hints
                              (cons ':print
                                    (cons print 'nil))))))))))))))))
     'nil)))))

Theorem: pseudo-event-formp-of-expdata-gen-defsurj

(defthm pseudo-event-formp-of-expdata-gen-defsurj
  (b* ((event (expdata-gen-defsurj surjmap verify-guards$ print$)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)