• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • 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
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • 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.