• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
        • Simplify-defun
        • Isodata
          • Isodata-implementation
            • Isodata-event-generation
            • Isodata-fn
            • Isodata-input-processing
              • Isodata-symbol-isomap-alistp
              • Isodata-isomapp
                • Isodata-isomap
                • Make-isodata-isomap
                • Honsed-isodata-isomap
                • Change-isodata-isomap
                • Make-honsed-isodata-isomap
                • Isodata-isomap->oldp-guard
                • Isodata-isomap->oldp
                • Isodata-isomap->newp-guard
                • Isodata-isomap->newp
                • Isodata-isomap->localp
                • Isodata-isomap->isoname
                • Isodata-isomap->hints
                • Isodata-isomap->forth-of-back
                • Isodata-isomap->forth-injective
                • Isodata-isomap->forth-image
                • Isodata-isomap->forth-guard
                • Isodata-isomap->forth
                • Isodata-isomap->back-of-forth
                • Isodata-isomap->back-injective
                • Isodata-isomap->back-image
                • Isodata-isomap->back-guard
                • Isodata-isomap->back
              • Isodata-pos-isomap-alistp
              • Isodata-process-iso
              • Isodata-process-inputs
              • Isodata-process-arg/res-list-iso
              • Isodata-process-isomaps
              • Isodata-fresh-defiso-thm-names
              • Isodata-process-arg/res-list
              • Isodata-process-arg/res-list-iso-list
              • Isodata-process-res
              • Isodata-fresh-defiso-name-with-*s-suffix
              • Isodata-process-newp-of-new-name
              • Isodata-process-isomaps-ress
              • Isodata-process-isomaps-args
              • Isodata-process-arg/res-list-iso-add-ress
              • Isodata-process-arg/res-list-iso-add-args
              • Isodata-process-old
              • Isodata-process-undefined
              • Isodata-process-arg/res-list-aux
              • Isodata-isomap-listp
              • Isodata-fresh-defiso-name-with-*s-suffix-aux
            • Isodata-macro-definition
        • Tailrec
        • Schemalg
        • Restrict
        • Expdata
        • Casesplit
        • Simplify-term
        • Simplify-defun-sk
        • Parteval
        • Solve
        • Wrap-output
        • Propagate-iso
        • Simplify
        • Finite-difference
        • Drop-irrelevant-params
        • Copy-function
        • Lift-iso
        • Rename-params
        • Utilities
        • Simplify-term-programmatic
        • Simplify-defun-sk-programmatic
        • Simplify-defun-programmatic
        • Simplify-defun+
        • Common-options
        • Common-concepts
      • Std/util
      • Defdata
      • Defrstobj
      • Seq
      • Match-tree
      • Defrstobj
      • With-supporters
      • Def-partial-measure
      • Template-subst
      • Soft
      • Defthm-domain
      • Event-macros
      • Def-universal-equiv
      • Def-saved-obligs
      • With-supporters-after
      • Definec
      • Sig
      • Outer-local
      • Data-structures
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Isodata-input-processing

Isodata-isomapp

Information about an isomorphic mapping according to which (some of) the target function's arguments and results are transformed.

(isodata-isomapp x) is a std::defaggregate of the following fields.

  • isoname — Name of the defiso.
        Invariant (symbolp isoname).
  • localp — Flag saying whether the defiso is locally generated or not.
        Invariant (booleanp localp).
  • oldp — Recognizer of the old representation.
        Invariant (pseudo-termfnp oldp).
  • newp — Recognizer of the new representation.
        Invariant (pseudo-termfnp newp).
  • forth — Conversion from old to new representation.
        Invariant (pseudo-termfnp forth).
  • back — Conversion from new to old representation.
        Invariant (pseudo-termfnp back).
  • forth-image — Name of the :alpha-image theorem of the defiso.
        Invariant (symbolp forth-image).
  • back-image — Name of the :beta-image theorem of the defiso.
        Invariant (symbolp back-image).
  • back-of-forth — Name of the :beta-of-alpha theorem of the defiso.
        Invariant (symbolp back-of-forth).
  • forth-of-back — Name of the :alpha-of-beta theorem of the defiso.
        Invariant (symbolp forth-of-back).
  • forth-injective — Name of the :alpha-injective theorem of the defiso.
        Invariant (symbolp forth-injective).
  • back-injective — Name of the :beta-injective theorem of the defiso.
        Invariant (symbolp back-injective).
  • oldp-guard — Name of the :doma-guard theorem of the defiso, if present (otherwise nil).
        Invariant (symbolp oldp-guard).
  • newp-guard — Name of the :domb-guard theorem of the defiso, if present (otherwise nil).
        Invariant (symbolp newp-guard).
  • forth-guard — Name of the :alpha-guard theorem of the defiso, if present (otherwise nil).
        Invariant (symbolp forth-guard).
  • back-guard — Name of the :beta-guard theorem of the defiso, if present (otherwise nil).
        Invariant (symbolp back-guard).
  • hints — Optional hints for the defiso, if locally generated (otherwise nil).
        Invariant (keyword-value-listp hints).

Source link: isodata-isomapp

This aggregate is somewhat similar to defmapping-infop, and in fact it corresponds either to an existing defiso that is referenced in an isok input of isodata, or to a locally generated defiso that is determined in the isok input of isodata. However, this aggregate is not stored in any table; it has some fields in common (except for their names) with defmapping-infop, but it has a few extra fields and omits a few fields. This aggregate is only for isodata's internal use.

Subtopics

Isodata-isomap
Raw constructor for isodata-isomapp structures.
Make-isodata-isomap
Constructor macro for isodata-isomapp structures.
Honsed-isodata-isomap
Raw constructor for honsed isodata-isomapp structures.
Change-isodata-isomap
A copying macro that lets you create new isodata-isomapp structures, based on existing structures.
Make-honsed-isodata-isomap
Constructor macro for honsed isodata-isomapp structures.
Isodata-isomap->oldp-guard
Access the oldp-guard field of a isodata-isomapp structure.
Isodata-isomap->oldp
Access the oldp field of a isodata-isomapp structure.
Isodata-isomap->newp-guard
Access the newp-guard field of a isodata-isomapp structure.
Isodata-isomap->newp
Access the newp field of a isodata-isomapp structure.
Isodata-isomap->localp
Access the localp field of a isodata-isomapp structure.
Isodata-isomap->isoname
Access the isoname field of a isodata-isomapp structure.
Isodata-isomap->hints
Access the hints field of a isodata-isomapp structure.
Isodata-isomap->forth-of-back
Access the forth-of-back field of a isodata-isomapp structure.
Isodata-isomap->forth-injective
Access the forth-injective field of a isodata-isomapp structure.
Isodata-isomap->forth-image
Access the forth-image field of a isodata-isomapp structure.
Isodata-isomap->forth-guard
Access the forth-guard field of a isodata-isomapp structure.
Isodata-isomap->forth
Access the forth field of a isodata-isomapp structure.
Isodata-isomap->back-of-forth
Access the back-of-forth field of a isodata-isomapp structure.
Isodata-isomap->back-injective
Access the back-injective field of a isodata-isomapp structure.
Isodata-isomap->back-image
Access the back-image field of a isodata-isomapp structure.
Isodata-isomap->back-guard
Access the back-guard field of a isodata-isomapp structure.
Isodata-isomap->back
Access the back field of a isodata-isomapp structure.