		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-defiso

Generate a local defiso.

Signature
(isodata-gen-defiso isomap verify-guards$ print$) → event
Arguments: isomap — Guard (isodata-isomapp isomap).; verify-guards$ — Guard (booleanp verify-guards$).; print$ — Guard (evmac-input-print-p print$).
Returns: event — Type (pseudo-event-formp event).

When the iso input is not a name, isodata internally generates and uses a defiso, so that the rest of the generated events can uniformly rely on a defiso that has established the isomorphic mapping.

This event is local to the encapsulate generated by isodata.

Since the defiso 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 isodata's :print input is :all, the we use :all for defiso's :print input as well.

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

Definitions and Theorems

Function: isodata-gen-defiso

(defun isodata-gen-defiso (isomap verify-guards$ print$)
 (declare (xargs :guard (and (isodata-isomapp isomap)
                             (booleanp verify-guards$)
                             (evmac-input-print-p print$))))
 (declare (xargs :guard (isodata-isomap->localp isomap)))
 (let ((__function__ 'isodata-gen-defiso))
  (declare (ignorable __function__))
  (b* (((isodata-isomap isomap) isomap)
       (name isomap.isoname)
       (doma isomap.oldp)
       (domb isomap.newp)
       (alpha isomap.forth)
       (beta isomap.back)
       (unconditional nil)
       (guard-thms verify-guards$)
       (nonguard-thm-names
            (list :alpha-image isomap.forth-image
                  :beta-image isomap.back-image
                  :beta-of-alpha isomap.back-of-forth
                  :alpha-of-beta isomap.forth-of-back
                  :alpha-injective isomap.forth-injective
                  :beta-injective isomap.back-injective))
       (guard-thm-names? (and guard-thms
                              (list :doma-guard isomap.oldp-guard
                                    :domb-guard isomap.newp-guard
                                    :alpha-guard isomap.forth-guard
                                    :beta-guard isomap.back-guard)))
       (thm-names (append nonguard-thm-names guard-thm-names?))
       (hints isomap.hints)
       (print (if (eq print$ :all) :all :error)))
   (cons
    'local
    (cons
     (cons
      'defiso
      (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-isodata-gen-defiso

(defthm pseudo-event-formp-of-isodata-gen-defiso
  (b* ((event (isodata-gen-defiso isomap verify-guards$ print$)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)