• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • 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
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • 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.