		Search-engine friendly clone of the ACL2 documentation.

Expdata

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

Introduction

This transformation changes the representation of one or more of a function's arguments and results into an expanded representation in the sense that the same element in the old representation may correspond to multiple elements in the new representation. This is more general than isodata, where old and new representation are isomorphic: in expdata, there is a surjection from the new representation to the old representation. The expdata transformation is useful to carry out certain data type refinements (when synthesizing programs), or perhaps also to raise the level of abstraction of certain types (when analyzing programs); however, its usefulness in program analysis is not as obvious as isodata, given that isomorphisms are inherently invertible while mere surjections are not.

For a given (user-specified) surjective conversion from the new representation to the old representation there may be different possible right inverse conversions from the old representation to the new representation. Different such inverse conversions could be used in different parts of the new function generated by expdata. The current version of this transformation, for simplicity, use the same (user-specified) inverse conversion; future versions of expdata may support different conversions, which may be necessary to make expdata more practically useful. Thus, the current version of expdata is very similar to isodata, except that the conversions are not necessarily isomorphisms.

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 surjection, 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 in the surjection's preimage of 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 in the surjection's preimage of 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 results in the new representation that are in the surjection's preimage.

The expdata 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. Given that, as noted above, the current version of expdata is very similar to isodata, the expdata design notes mostly refer to the isodata design notes; thus, the isodata design notes should be read as well.

General Form

(expdata old
         surjmaps
         :predicate           ; default nil
         :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
  )

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, referenced by the expdata design notes, old is denoted by f when :predicate is nil, and p when :predicate is t.

surjmaps

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 surj) ... (arg/res-listq surjq)), where:
Each arg/res-listk denotes the subset of the arguments and results of old whose representation is transformed according to surjk.
It must be one of the following:
A non-empty list without duplicates of elements among x1, ... xn, :result1, ..., :resultm, in any order.
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 surjk denotes the surjective mapping to apply to the arguments and results in arg/res-listk. Each surjk specifies old and new representations and the surjection between them, along with a right inverse of the surjection.
It must be one of the following:
A symbol that references a previous successful call of defsurj, 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 (domb), which we call oldp here; the recognizer of the new representation (doma), which we call newp here; the surjective conversion from the new to the old representation (alpha), which we call back here; and the right inverse conversion from the old to the new representation (beta), which we call forth 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 defsurj must have :guard-thms equal to t, i.e. it must have proved and recorded the guard-related theorems.
A list (newp oldp back forth :hints hints) such that the call (defsurj name newp oldp back forth :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 (newp oldp back forth) abbreviates (newp oldp back forth :hints nil). The expdata transformation generates this call of defsurj, and uses it in the same way as it uses a call referenced by surj when surj is a symbol; however, this generated defsurj call is local to the encapsulate generated by expdata, and cannot be therefore referenced after the call of expdata.
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) defsurj specified by surjk, 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 surjective 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) defsurj specified by surjk, 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 surjective mapping over all values, if :resultj is not in any arg/res-listk.
In the isodata design notes, referenced by the expdata 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 same concepts apply to surjective mappings. The surjmaps input currently supported by expdata 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 surjective mapping consisting of oldpi, newpi, forthi, and backi is used for the partition consisting of argument xi.
The surjective mapping consisting of oldp_rj, newp_rj, forth_rj, and back_rj is used for the partition consisting of result j.
The identity surjective mapping is used for the partitions of all the results, if :result is not in any arg/res-listk.
In the expdata design notes, the resulting surjecive mapping over all function arguments is denoted as consisting of the domains A and A' and the conversions \alpha and \alpha', and the resulting surjective mapping over all function results is denoted as consisting of the domains B and B' and the conversions \beta and \beta'. The design notes allow these domains and conversions to be specified via (the design notes counterparts of) either definj or defsurj (in opposite directions); for the currently implemented expdata, only defsurj may be used.

: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 surjmaps does not include :result.
In the isodata design notes, referenced by the expdata 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.

: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 surjmaps 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 surjmaps 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 expdata. 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 expdata.
: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 expdata 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 expdata 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 expdata is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Applicability Conditions

In order for expdata 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 expdata 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, referenced by the expdata design notes,.
This applicability condition is present if and only if surjmaps 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, referenced by the expdata 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, referenced by the expdata 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, referenced by the expdata 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, referenced by the expdata 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 surj1, ..., surjq are all names of pre-existing defsurjs, there are additional applicability conditions that pertain to the locally generated defsurjs. These additional applicability conditions are described in the documentation of defsurj.

Generated Events

new

Expanded 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 surjmaps includes no :resultj:
(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      old-body<(back1 x1),...,(backn xn)>
    nil)) ; or (mv nil ... nil)

;; when old is not recursive,
;; :predicate is nil,
;; m = 1,
;; and surjmaps includes :result1 (or :result):

(defun new (x1 ... xn)
  (if (mbt$ (and (newp1 x1)
                 ...
                 (newpn xn)))
      (forth_r1 old-body<(back1 x1),...,(backn xn)>)
    nil))

;; when old is not recursive,
;; :predicate is nil,
;; m > 1,
;; and surjmaps 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)))
    (mv nil ... nil)))

;; 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 surjmaps 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)>))>
    nil)) ; or (mv nil ... nil)

;; when old is recursive,
;; :predicate is nil,
;; m = 1,
;; and surjmaps 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)>)))>)
    nil))

;; when old is recursive,
;; :predicate is nil,
;; m > 1,
;; and surjmaps 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 (forth_r1 y1) ... (forth_rm ym))),
                 ...
                 (mv-let (y1 ... ym)
                   (new (forth1 updater-x1<(back1 x1),
                                           ...,
                                           (backn xn)>)
                        ...
                        (forthn updater-xn<(back1 x1),
                                           ...,
                                           (backn xn)>))
                   (mv (forth_r1 y1) ... (forth_rm ym)))>
        (mv (forth_r1 y1) ... (forth_rm ym)))
    (mv nil ... nil)))

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 in the surjection's preimage of the guard of old.

In the isodata design notes, referenced by the expdata 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 in the surjection's preimage of 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 corresponding value (where `corresponding' here means in the surjection's preimage) that old maps the corresponding argument tuple in the old representation (where `corresponding' here means in the surjection's image).

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 surjmaps 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 surjmaps includes :result1 (or :result):
(implies (and (newp1 x1)
              ...
              (newp1 xn))
         (equal (new x1 ... xn)
                (forth_r1 (old (back1 x1) ... (backn xn)))))

;; when :predicate is nil,
;; m > 1,
;; and surjmaps includes some :resultj:
(implies (and (newp1 x1)
              ...
              (newp1 xn))
         (and (equal (mv-nth 0 (new x1 ... xn))
                     (forth_r1 (mv-nth 0 (old (back1 x1)
                                              ...
                                              (backn xn)))))
              ...
              (equal (mv-nth m-1 (new x1 ... xn))
                     (forth_rm (mv-nth m-1 (old (back1 x1)
                                                ...
                                                (backn xn)))))))

In the isodata design notes, referenced by the expdata 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 surjmaps 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 surjmaps 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 surjmaps includes some :resultj:
(defthm old-to-new
  (implies (and (oldp1 x1)
                ...
                (oldpn xn))
           (and (equal (mv-nth 0 (old x1 ... xn))
                       (back_r1 (mv-nth 0 (new (forth1 x1)
                                               ...
                                               (forthn xn)))))
                ...
                (equal (mv-nth m-1 (old x1 ... xn))
                       (back_rm (mv-nth m-1 (new (forth1 x1)
                                                 ...
                                                 (forthn xn))))))))

In the isodata design notes, referenced by the expdata 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, referenced by the expdata design notes, newp-of-new is denoted by f'A'B'.
This is generated if and only if surjmaps 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 expdata is redundant if and only if it is identical to a previous successful call of expdata 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 expdata whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

Expdata-implementation: Implementation of expdata.