		Search-engine friendly clone of the ACL2 documentation.

Isodata

APT isomorphic data transformation: change function arguments and results into isomorphic representations.

Introduction

This transformation changes the representation of one or more of a function's arguments and results into an isomorphic representation. This transformation is useful to carry out certain data type refinements (when synthesizing programs), or to raise the level of abstraction of certain types (when analyzing programs).

When at least one argument's representation is being changed, then by regarding the arguments whose representation is not changed as being changed via an indentity isomorphism, we can say that this transformation changes the representation of (the tuple of) all the function's arguments into a new representation that consists of (the tuple of) all the new function's arguments. In this case, there are two variants of this transformation:

When the function operates only on argument tuples in the old representation (i.e. when the function's guard is a subset of the old representation), the function is transformed to operate in the same way on exactly the argument tuples in the new representation that are isomorphic to the old guard.
When the function operates on at least all the tuples in the old representation (and possibly more) (i.e. the function's guard is a superset of the old representation), and is used as a predicate to recognize a subset of argument tuples all of which are in the old representation, the function is transformed to recognize exactly the argument tuples in the new representation that are isomorphic to the ones recognized by the old function.

These two variants involve slightly different applicability conditions and produce slightly different results. These two variants are selected via the :predicate input (see below).

If only the representation of some results (and of no arguments) is changed, then there is a single variant of this transformation, namely one that operates on the same tuples as the old function but returns isomorphic results in the new representation.

These isodata design notes, which use this notation, provide the mathematical concepts and template proofs upon which this transformation is based. These notes should be read alongside this reference documentation, which refers to the them in numerous places.

The isodata design notes cover isomorphic transformations compositionally established by partitioning arguments and results of old and new function and by establishing sub-mappings between the partitions (see the `Compositional Establishment of Isomorphic Mappings on Tuples' section in the design notes). The current implementation is more limited, supporting only a limited form of partition of the arguments (see below). There are plans to extend the implementation to match the coverage of the design notes, namely allowing arbitrary partitions of arguments and results.

General Form

(isodata old
         isomaps
         :predicate           ; default nil
         :undefined           ; default :auto
         :new-name            ; default :auto
         :new-enable          ; default :auto
         :old-to-new-name     ; default from table
         :old-to-new-enable   ; default from table
         :new-to-old-name     ; default from table
         :new-to-old-enable   ; default from table
         :newp-of-new-name    ; default :auto
         :newp-of-new-enable  ; default t
         :verify-guards       ; default :auto
         :untranslate         ; default :nice
         :hints               ; default nil
         :print               ; default :result
         :show-only           ; default nil
         :compatibility       ; default nil
  )

Inputs

old

Denotes the target function to transform.
It must be the name of a function, or a numbered name with a wildcard index that resolves to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that old is the name of the denoted function.
old must be in logic mode, be defined, and have no input or output stobjs. If the :predicate input (see below) is t, then old must return a non-multiple value. If old is recursive, it must be singly (not mutually) recursive, not have a :? measure, and not occur in its own termination theorem (i.e. not occur in the tests and arguments of its own recursive calls). If the :verify-guards input is t, old must be guard-verified.
In the rest of this documentation page:
Let x1, ..., xn be the arguments of old, where n > 0.
Let m > 0 be the number of results of old.
Let old-guard<x1,...,xn> be the guard term of old.
If old is not recursive, let
old-body<x1,...,xn>
be the body of old.
If old is recursive, let
old-body<x1,...,xn,
         (old update1-x1<x1,...,xn>
              ...
              update1-xn<x1,...,xn>)
         ...
         (old updater-x1<x1,...,xn>
              ...
              updater-xn<x1,...,xn>)>
be the body of old, where r > 0 is the number of recursive calls in the body of old and each updatek-xi<x1,...,xn> is the i-th actual argument passed to the k-th recursive call. Furthermore, let contextk<x1,...,xn> be the context (i.e. controlling tests) in which the k-th recursive call occurs, and let measure<x1,...,xn> be the measure term of old.
In the isodata design notes, old is denoted by f when :predicate is nil, and p when :predicate is t.

isomaps

Specifies the arguments and results of old that are transformed and the way in which they are transformed.
It must be a non-empty list of doublets ((arg/res-list1 iso1) ... (arg/res-listq isoq)), where:
Each arg/res-listk denotes the subset of the arguments and results of old whose representation is transformed according to isok.
It must be one of the following:
A list without duplicates of elements among x1, ... xn, :result1, ..., :resultm, in any order. The list is allowed to be empty (to facilitate iterative development), in which case the doublet does not induce any transformation.
A single element among x1, ... xn, :result1, ..., :resultm, abbreviating the singleton list with that element.
The single element :result, abbreviating the singleton list :result1. This is allowed only if m is 1.
Each isok denotes the isomorphic mapping to apply to the arguments and results in arg/res-listk. Each isok specifies old and new representations and the conversions between them.
It must be one of the following:
A symbol that references a previous successful call of defiso, i.e. the symbol must be the name input of that call. The domains and conversions recorded under that name specify: the recognizer of the old representation (doma), which we call oldp here; the recognizer of the new representation (domb), which we call newp here; the conversion from the old to the new representation (alpha), which we call forth here; and the conversion from the new to the old representation (beta), which we call back here. Both oldp and newp must be unary. If the generated function is guard-verified (which is determined by the :verify-guards input; see below), the call of defiso must have :guard-thms equal to t, i.e. it must have proved and recorded the guard-related theorems.
A list (oldp newp forth back :hints hints) such that the call (defiso name oldp newp forth back :guard-thms guard-thms :thm-names thm-names :hints hints) is successful, where name and thm-names consist of suitably fresh names, and where guard-thms is t if the generated function is guard-verified (which is determined by the :verify-guards input; see below) and nil otherwise. A list (oldp newp forth back) abbreviates (oldp newp forth back :hints nil). The isodata transformation generates this call of defiso, and uses it in the same way as it uses a call referenced by iso when iso is a symbol; however, this generated defiso call is local to the encapsulate generated by isodata, and cannot be therefore referenced after the call of isodata.
The lists arg/res-list1, ..., arg/res-listq are pairwise disjoint, i.e. each xi and :result appears in at most one of those lists.
In the rest of this documentation page, for each i from 1 to n, let oldpi, newpi, forthi, and backi be:
The oldp, newp, forth, and back of the (pre-existing or locally generated) defiso specified by isok, if xi is in arg/res-listk.
The functions (lambda (x) t), (lambda (x) t), (lambda (x) x), and (lambda (x) x) that form the identity isomorphic mapping over all values, if xi is not in any arg/res-listk.
Furthermore, for each j from 1 to m, let oldp_rj, newp_rj, forth_rj, and back_rj be:
The oldp, newp, forth, and back of the (pre-existing or locally generated) defiso specified by isok, if :resultj is in arg/res-listk.
The functions (lambda (x) t), (lambda (x) t), (lambda (x) x), and (lambda (x) x) that form the identity isomorphic mapping over all values, if :resultj is not in any arg/res-listk.
In the isodata design notes, the section `Compositional Establishment of Isomorphic Mappings on Tuples' describes the compositional establishment of an isomorphic mapping between the inputs of old and new function. The isomaps input currently supported by this transformation amounts to the following partitioning and sub-mappings:
The new function's arguments are the same (i.e. have the same names) as the old function's arguments, i.e. x1, ..., xn.
The new function has the same number of results as the old function.
The arguments are partitioned into n singleton partitions.
The results are partitioned into m singleton partitions.
The isomorphic mapping consisting of oldpi, newpi, forthi, and backi is used for the partition consisting of argument xi.
The isomorphic mapping consisting of oldp_rj, newp_rj, forth_rj, and back_rj is used for the partition consisting of result j.
The identity isomorphic mapping is used for the partitions of all the results, if :result is not in any arg/res-listk.
In the design notes, the resulting isomorphic mapping over all function arguments is denoted as consisting of the domains A and A' and the conversions \alpha and \alpha', and the resulting isomorphic mapping over all function results is denoted as consisting of the domains B and B' and the conversions \beta and \beta'.

:predicate — default nil

Selects between the two variants of this transformation:
t, to select the variant in which old is treated like a predicate that recognizes argument tuples that are all in the old representation.
nil, to select the variant in which old is treated as a function that operates only on argument tuples that are all in the old representation.
This input may be t only if isomaps does not include :result.
In the isodata design notes, the sections with `Function' in their title refer to the case in which :predicate is nil, while the sections with `Predicate' in their title refer to the case in which :predicate is t.

:undefined — default :auto

Denotes the value that the generated new function must return outside of the new domain.
It must be one of the following:
:auto, to use nil or (mv nil ... nil) for single-value and multi-value functions respectively.
:base-case-then, to search for a base-case within the domain of the new function. A base-case of a term may be be the whole term when the term does not include any recursive calls, or it may be a base-case of the `then' or `else' branch when the translated term is an `if'. This search for a base-case is biased toward `then' branches.
:base-case-else, to search for a base-case with a bias toward `else' branches.
Any other term. It must be a term that only references logic-mode functions and that includes no free variables other than x1, ..., xn. This term must have no output ACL2::stobjs. This term must return the same number of results as old. This term must not reference old.
If one wishes to use the term :auto as the undefined result, this may be accomplished by providing the quoted constant ':auto. The same applies for :base-case-then and :base-case-else.
Even if the generated function is guard-verified (which is determined by the :verify-guards input; see below), the undefined term need not be guard-verified. Since the term is governed by the negation of the guard (see the generated new function, below), the verification of its guards always succeeds trivially.
In the rest of this documentation page, let undefined be this term specified by :undefined.

:new-name — default :auto

Determines the name of the generated new function.
It must be one of the following:
:auto, to generate the name automatically as described in function-name-generation.
Any other symbol, to use as the name of the function.
In the rest of this documentation page, let new be the name of this function.

:new-enable — default :auto

Determines whether new is enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
:auto, to enable it iff old is enabled.

:old-to-new-name — default from table

Determines the name of the theorem that rewrites the old function in terms of the new function.
It must be one of the following:
A keyword, to use as separator between the names of old and new. A keyword :kwd specifies the theorem name oldkwdnew, in the same package as new.
Any other symbol, to use as the name of the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-to-new-name.
In the rest of this documentation page, let old-to-new be the name of this theorem.

:old-to-new-enable — default from table

Determines whether the old-to-new theorem is enabled.
It must be one of the following:
t, to enable the theorem.
nil, to disable the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-to-new-enable.
If this input is t, the :new-to-old-enable input must be nil. At most one of these two inputs may be t at any time.

:new-to-old-name — default from table

Determines the name of the theorem that rewrites the new function in terms of the old function.
It must be one of the following:
A keyword, to use as separator between the names of new and old. A keyword :kwd specifies the theorem name newkwdold, in the same package as new.
Any other symbol, to use as the name of the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-new-to-old-name.
In the rest of this documentation page, let new-to-old be the name of this theorem.

:new-to-old-enable — default from table

Determines whether the new-to-old theorem is enabled.
It must be one of the following:
t, to enable the theorem.
nil, to disable the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-new-to-old-enable.
If this input is t, the :old-to-new-enable input must be nil. At most one of these two inputs may be t at any time.

:newp-of-new-name — default :auto

Determines the name of the theorem asserting that new maps arguments in the new representation to results in the new representation.
It must be one of the following:
:auto, to use the concatenation of the name of new followed by -new-representation, in the same package as new.
Any other symbol, to use as the name of the theorem.
This input may be present only if isomaps includes some :resultj.
In the rest of this documentation page, let newp-of-new be the name of this theorem.

:newp-of-new-enable — default t

Determines whether newp-of-new is enabled.
It must be one of the following:
t, to enable the theorem.
nil, to disable the theorem.
This input may be present only if isomaps includes some :resultj.

:verify-guards — default :auto

Determines whether the guards of the generated functions are verified or not.
It must be one of the following:
t, to verify the guards.
nil, to not verify guards.
:auto, to verify the guards if and only if the guards of the target function old are verified.

:untranslate — default :nice

Specifies if and how the body of new should be turned from internal translated form to external untranslated form.
It must be an untranslate specifier; see that documentation topic for details.

:hints — default nil

Hints to prove the applicability conditions.
It must be one of the following:
A keyword-value list (appcond1 hints1 appcond2 hints2 ...), where each appcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and each hintsk is a list of hints of the kind that may appear just after :hints in a defthm. The hints hintsk are used to prove applicability condition appcondk. The appcond1, appcond2, ... keywords must be all distinct. An appcondk keyword is allowed only if the corresponding applicability condition is present, as specified in the `Applicability Conditions' section.
A list of hints of the kind that may appear just after :hints in a defthm. In this case, these same hints are used to prove every applicability condition,.

:print — default :result

Specifies what is printed on the screen (see screen printing).
It must be one of the following:
nil, to print nothing (not even error output).
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of isodata. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of isodata.
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.
If the call of isodata is redundant, an indication to that effect is printed on the screen, unless :print is nil.

:show-only — default nil

Determines whether the event expansion of isodata is submitted to ACL2 or just printed on the screen:
nil, to submit it.
t, to just print it. In this case: the event expansion is printed even if :print is nil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of isodata is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

:compatibility — default nil

This is a temporary option that is not documented because it should not be used, except in very specific transitional situations.

Applicability Conditions

In order for isodata to apply, in addition to the requirements on the inputs stated in the `Inputs' section, the following applicability conditions must be proved. The proofs are attempted when isodata is called, using the hints optionally supplied as the :hints input described in the `Inputs' section.

The following conditions must be proved in order for the transformation to apply.

:oldp-of-old

old maps arguments in the old representation to results in the old representation:
;; when m = 1:
(implies (and (oldp1 x1)
              ...
              (oldpn xn))
         (oldp_r1 (old x1 ... xn)))

;; when m > 1:
(implies (and (oldp1 x1)
              ...
              (oldpn xn))
         (mv-let (y1 ... ym)
           (old x1 ... xn)
           (and (oldp_r1 y1)
                ...
                (oldp_rm ym))))
This corresponds to fAB in the isodata design notes.
This applicability condition is present if and only if isomaps includes some :resultj.

:oldp-when-old

old holds only on argument tuples such that x1, ..., xn are all in the old representation:
(implies (old x1 ... xn)
         (and (oldp1 x1)
              ...
              (oldpn xn)))
This corresponds to pA in the isodata design notes.
This applicability condition is present if and only if :predicate is t.

:oldp-of-rec-call-args

The old representation is preserved on the arguments of the recursive calls of old:

(implies (and (oldp1 x1)
              ...
              (oldpn xn))
         (and (implies context1<x1,...,xn>
                       (and (oldp1 update1-x1<x1,...,xn>)
                            ...
                            (oldpn update1-xn<x1,...,xn>)))
              ...
              (implies contextr<x1,...,xn>
                       (and (oldp1 updater-x1<x1,...,xn>)
                            ...
                            (oldpn updater-xp<x1,...,xn>)))))

This corresponds to Ad in the isodata design notes.

This applicability condition is present if and only if old is recursive.

:old-guard

old is well-defined (according to its guard) only on tuples in the old representation:
(implies old-guard<x1,...,xn>
         (and (oldp1 x1)
              ...
              (oldpn xn)))
This corresponds to Gf in the isodata design notes.
This applicability condition is present if and only if the generated function is guard-verified (which is determined by the :verify-guards input; see above) and :predicate is nil.

:old-guard-pred

old is well-defined (according to its guard) on all tuples in the old representation:
(implies (and (oldp1 x1)
              ...
              (oldpn xn))
         old-guard<x1,...,xn>)
This corresponds to Gp in the isodata design notes.
This applicability condition is present if and only if the generated function is guard-verified (which is determined by the :verify-guards input; see above) and :predicate is t.

Unless iso1, ..., isoq are all names of pre-existing defisos, there are additional applicability conditions that pertain to the locally generated defisos. These additional applicability conditions are described in the documentation of defiso.

Generated Events

new

Isomorphic version of old:

;; when old is not recursive
;; and :predicate is t:
(defun new (x1 ... xn)
  (and (mbt$ (and (newp1 x1)
                  ...
                  (newpn xn)))
       old-body<(back1 x1),...,(backn xn)>))

;; when old is not recursive,
;; :predicate is nil:
;; and isomaps includes no :resultj:
(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      old-body<(back1 x1),...,(backn xn)>
    undefined))

;; when old is not recursive,
;; :predicate is nil,
;; m = 1,
;; and isomaps includes :result1 (or :result):
(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      (forth_r1 old-body<(back1 x1),...,(backn xn)>)
    undefined))
;; where forth_r1 is actually pushed into
;; the 'if' branches of old-body if it starts with 'if',
;; and recursively into their 'if' branches (if any)

;; when old is not recursive,
;; :predicate is nil,
;; m > 1,
;; and isomaps includes some :resultj:
(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      (mv-let (y1 ... ym)
        old-body<(back1 x1),...,(backn xn)>
        (mv (forth_r1 y1) ... (forth_rm ym)))
    undefined))

;; when old is recursive
;; and :predicate is t:
(defun new (x1 ... xn)
  (and (mbt$ (and (newp1 x1)
                  ...
                  (newpn xn)))
       old-body<(back1 x1),...,(backn xn),
                (new (forth1 update1-x1<(back1 x1),
                                        ...,
                                        (backn xn)>)
                     ...
                     (forthn update1-xn<(back1 x1),
                                        ...,
                                        (backn xn)>)),
                ...
                (new (forth1 updater-x1<(back1 x1),
                                        ...,
                                        (backn xn)>)
                     ...
                     (forthn updater-xn<(back1 x1),
                                        ...,
                                        (backn xn)>))>))

;; when old is recursive,
;; :predicate is nil,
;; and isomaps includes no :resultj:
(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      old-body<(back1 x1),...,(backn xn),
               (new (forth1 update1-x1<(back1 x1),
                                       ...,
                                       (backn xn)>)
                    ...
                    (forthn update1-xn<(back1 x1),
                                       ...,
                                       (backn xn)>)),
               ...
               (new (forth1 updater-x1<(back1 x1),
                                       ...,
                                       (backn xn)>)
                    ...
                    (forthn updater-xn<(back1 x1),
                                       ...,
                                       (backn xn)>))>
    undefined))

;; when old is recursive,
;; :predicate is nil,
;; m = 1,
;; and isomaps include :result1 (or :result):
(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      (forth_r1 old-body<(back1 x1),...,(backn xn),
                         (back_r1
                          (new (forth1 update1-x1<(back1 x1),
                                                  ...,
                                                  (backn xn)>)
                               ...
                               (forthn update1-xn<(back1 x1),
                                                  ...,
                                                  (backn xn)>))),
                         ...
                         (back_r1
                          (new (forth1 updater-x1<(back1 x1),
                                                  ...,
                                                  (backn xn)>)
                               ...
                               (forthn updater-xn<(back1 x1),
                                                  ...,
                                                  (backn xn)>)))>)
    undefined))
;; where forth_r1 is actually pushed into
;; the 'if' branches of old-body if it starts with 'if',
;; and recursively into their 'if' branches (if any)

;; when old is recursive,
;; :predicate is nil,
;; m > 1,
;; and isomaps includes some :resultj:
(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      (mv-let (y1 ... ym)
        old-body<(back1 x1),...,(backn xn),
                 (mv-let (y1 ... ym)
                   (new (forth1 update1-x1<(back1 x1),
                                           ...,
                                           (backn xn)>)
                        ...
                        (forthn update1-xn<(back1 x1),
                                           ...,
                                           (backn xn)>))
                   (mv (back_r1 y1) ... (back_rm ym))),
                 ...
                 (mv-let (y1 ... ym)
                   (new (forth1 updater-x1<(back1 x1),
                                           ...,
                                           (backn xn)>)
                        ...
                        (forthn updater-xn<(back1 x1),
                                           ...,
                                           (backn xn)>))
                   (mv (back_r1 y1) ... (back_rm ym)))>
        (mv (forth_r1 y1) ... (forth_rm ym)))
    undefined))

If old is recursive, the measure term of new is measure<(back1 x1),...,(backn xn)> and the well-founded relation of new is the same as old.

The guard of new is:

;; when :predicate is nil:
(and (newp1 x1)
     ...
     (newpn xn)
     old-guard<(back1 x1),...,(backn xn)>)

;; when :predicate is t:
(and (newp1 x1)
     ...
     (newpn xn))

That is, when :predicate is t the guard consists of the new representation; when :predicate is nil, the guard consists of the argument tuples that are isomorphic to the ones in the guard of old.

In the isodata design notes, new is denoted by f' when :predicate is nil, and p' when :predicate is t.

Note that:

When :predicate is t, new is defined to hold exactly on the argument tuples in the new representation that are isomorphic the argument tuples in the old representation on which old holds.
When :predicate is nil, new is defined to map each argument tuple in the new representation to the same or isomorphic value that old maps the isomorphic argument tuple in the old representation.

new-to-old

Theorem that relates new to old:

;; when :predicate is t:
(defthm new-to-old
  (implies (and (newp1 x1)
                ...
                (newpn xn))
           (equal (new x1 ... xn)
                  (old (back1 x1) ... (backn xn)))))

;; when :predicate is nil
;; and isomaps includes no :resultj:
(implies (and (newp1 x1)
              ...
              (newpn xn))
         (equal (new x1 ... xn)
                (old (back1 x1) ... (backn xn))))

;; when :predicate is nil,
;; m = 1,
;; and isomaps includes :result1 (or :result):
(implies (and (newp1 x1)
              ...
              (newpn xn))
         (equal (new x1 ... xn)
                (forth_r1 (old (back1 x1) ... (backn xn)))))

;; when :predicate is nil,
;; m > 1,
;; and isomaps includes some :resultj:
(implies (and (newp1 x1)
              ...
              (newpn xn))
         (equal (new x1 ... xn)
                (mv-let (y1 ... ym)
                  (old (back1 x1) ... (backn xn))
                  (mv (forth_r1 y1) ... (forth_rm ym)))))

In the isodata design notes, new-to-old is denoted by f'f when :predicate is nil, and 'pp when :predicate is t.

old-to-new

Theorem that relates old to new:

;; when :predicate is t:
(defthm old-to-new
  (implies (and (oldp1 x1)
                ...
                (oldpn xn))
           (equal (old x1 ... xn)
                  (new (forth1 x1) ... (forthn xn)))))

;; when :predicate is nil
;; and isomaps includes no :resultj:
(defthm old-to-new
  (implies (and (oldp1 x1)
                ...
                (oldpn xn))
           (equal (old x1 ... xn)
                  (new (forth1 x1) ... (forthn xn)))))

;; when :predicate is nil,
;; m = 1,
;; and isomaps includes :result1 (or :result):
(defthm old-to-new
  (implies (and (oldp1 x1)
                ...
                (oldpn xn))
           (equal (old x1 ... xn)
                  (back_r1 (new (forth1 x1) ... (forthn xn))))))

;; when :predicate is nil,
;; m > 1,
;; and isomaps includes some :resultj:
(defthm old-to-new
  (implies (and (oldp1 x1)
                ...
                (oldpn xn))
         (equal (old x1 ... xn)
                (mv-let (y1 ... ym)
                  (new (forth1 x1) ... (forthn xn))
                  (mv (back_r1 y1) ... (back_rm ym)))))

In the isodata design notes, old-to-new is denoted by ff' when :predicate is nil, and pp' when :predicate is t.

newp-of-new

Theorem asserting that new maps arguments in the new representation to results in the new representation:
;; when m = 1:
(defthm newp-of-new
  (implies (and (newp1 x1)
                ...
                (newpn xn))
           (newp_r1 (new x1 ... xn))))

;; when m > 1:
(defthm newp-of-new
  (implies (and (newp1 x1)
                ...
                (newpn xn))
           (mv-let (y1 ... ym)
             (new x1 ... xn)
             (and (newp_r1 y1)
                  ...
                  (newp_rm ym)))))
In the isodata design notes, newp-of-new is denoted by f'A'B'.
This is generated if and only if isomaps includes some :resultj.

A theory invariant is also generated to prevent both new-to-old and old-to-new from being enabled at the same time.

Redundancy

A call of isodata is redundant if and only if it is identical to a previous successful call of isodata whose :show-only input is not t, except that the two calls may differ in their :print and :show-only inputs. These inputs do not affect the generated events, and thus they are ignored for the purpose of redundancy.

A call of isodata whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

Isodata-implementation: Implementation of isodata.