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

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 `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 `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

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 `isodata`,
the `isodata` design notes should be read as well.

(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 )

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) ist , thenold must return a non-multiple value. Ifold 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 ist ,old must be guard-verified.In the rest of this documentation page:

- Let
x1 , ...,xn be the arguments ofold , wheren > 0.- Let
m > 0 be the number of results ofold .- Let
old-guard<x1,...,xn> be the guard term ofold .- If
old is not recursive, letold-body<x1,...,xn>be the body ofold .- If
old is recursive, letold-body<x1,...,xn, (old update1-x1<x1,...,xn> ... update1-xn<x1,...,xn>) ... (old updater-x1<x1,...,xn> ... updater-xn<x1,...,xn>)>be the body ofold , wherer > 0 is the number of recursive calls in the body ofold and eachupdatek-xi<x1,...,xn> is thei -th actual argument passed to thek -th recursive call. Furthermore, letcontextk<x1,...,xn> be the context (i.e. controlling tests) in which thek -th recursive call occurs, and letmeasure<x1,...,xn> be the measure term ofold .In the

isodata design notes, referenced by theexpdata design notes,old is denoted byf when:predicate isnil , andp when:predicate ist .

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 ofold whose representation is transformed according tosurjk .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 ifm is 1.Each

surjk denotes the surjective mapping to apply to the arguments and results inarg/res-listk . Eachsurjk 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 thename input of that call. The domains and conversions recorded under that name specify: the recognizer of the old representation (domb ), which we calloldp here; the recognizer of the new representation (doma ), which we callnewp here; the surjective conversion from the new to the old representation (alpha ), which we callback here; and the right inverse conversion from the old to the new representation (beta ), which we callforth here. Botholdp andnewp must be unary. If the generated function is guard-verified (which is determined by the:verify-guards input; see below), the call ofdefsurjmust have:guard-thms equal tot , 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, wherename andthm-names consist of suitably fresh names, and whereguard-thms ist if the generated function is guard-verified (which is determined by the:verify-guards input; see below) andnil otherwise. A list(newp oldp back forth) abbreviates(newp oldp back forth :hints nil) . Theexpdata transformation generates this call ofdefsurj, and uses it in the same way as it uses a call referenced bysurj whensurj is a symbol; however, this generateddefsurjcall is local to theencapsulategenerated byexpdata , and cannot be therefore referenced after the call ofexpdata .The lists

arg/res-list1 , ...,arg/res-listq are pairwise disjoint, i.e. eachxi and:result appears in at most one of those lists.In the rest of this documentation page, for each

i from 1 ton , letoldpi ,newpi ,forthi , andbacki be:

- The
oldp ,newp ,forth , andback of the (pre-existing or locally generated)defsurjspecified bysurjk , ifxi is inarg/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, ifxi is not in anyarg/res-listk .Furthermore, for each

j from 1 tom , letoldp_rj ,newp_rj ,forth_rj , andback_rj be:

- The
oldp ,newp ,forth , andback of the (pre-existing or locally generated)defsurjspecified bysurjk , if:resultj is inarg/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 anyarg/res-listk .In the

isodata design notes, referenced by theexpdata 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. Thesurjmaps input currently supported byexpdata 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 , andbacki is used for the partition consisting of argumentxi .- The surjective mapping consisting of
oldp_rj ,newp_rj ,forth_rj , andback_rj is used for the partition consisting of resultj .- The identity surjective mapping is used for the partitions of all the results, if
:result is not in anyarg/res-listk .In the

expdata design notes, the resulting surjecive mapping over all function arguments is denoted as consisting of the domainsA andA' and the conversions\alpha and\alpha' , and the resulting surjective mapping over all function results is denoted as consisting of the domainsB andB' and the conversions\beta and\beta' . The design notes allow these domains and conversions to be specified via (the design notes counterparts of) eitherdefinjordefsurj(in opposite directions); for the currently implementedexpdata , onlydefsurjmay be used.

Selects between the two variants of this transformation:

t , to select the variant in whichold is treated like a predicate that recognizes argument tuples that are all in the old representation.nil , to select the variant in whichold is treated as a function that operates only on argument tuples that are all in the old representation.This input may be

t only ifsurjmaps does not include:result .In the

isodata design notes, referenced by theexpdata design notes, the sections with `Function' in their title refer to the case in which:predicate isnil , while the sections with `Predicate' in their title refer to the case in which:predicate ist .

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.

Determines whether

new is enabled.It must be one of the following:

t , to enable it.nil , to disable it.:auto , to enable it iffold is enabled.

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 andnew . A keyword:kwd specifies the theorem nameoldkwdnew , in the same package asnew .- 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.

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 benil . At most one of these two inputs may bet at any time.

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 andold . A keyword:kwd specifies the theorem namenewkwdold , in the same package asnew .- 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.

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 benil . At most one of these two inputs may bet at any time.

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 ofnew followed by-new-representation , in the same package asnew .- 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.

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 .

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 functionold are verified.

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 to prove the applicability conditions.

It must be one of the following:

- A keyword-value list
(appcond1 hints1 appcond2 hints2 ...) , where eachappcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and eachhintsk is a list of hints of the kind that may appear just after:hints in adefthm. The hintshintsk are used to prove applicability conditionappcondk . Theappcond1 ,appcond2 , ... keywords must be all distinct. Anappcondk 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 adefthm. In this case, these same hints are used to prove every applicability condition,.

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 ofexpdata . This is the default value of the:info , to print, besides any error output and the results, also some additional information about the internal operations ofexpdata .: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, unlessnil .

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 ifnil (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:result or:info or:all ; no ACL2 output is printed for the event expansion even if:all (because the event expansion is not submitted). If the call ofexpdata is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

In order for

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

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 theisodata design notes, referenced by theexpdata design notes,.This applicability condition is present if and only if

surjmaps includes some:resultj .

old holds only on argument tuples such thatx1 , ...,xn are all in the old representation:(implies (old x1 ... xn) (and (oldp1 x1) ... (oldpn xn)))This corresponds to

pA in theisodata design notes, referenced by theexpdata design notes,.This applicability condition is present if and only if

:predicate ist .

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 theisodata design notes, referenced by theexpdata design notes,.This applicability condition is present if and only if

old is recursive.

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 theisodata design notes, referenced by theexpdata 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 isnil .

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 theisodata design notes, referenced by theexpdata 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 ist .

Unless `defsurj`s,
there are additional applicability conditions
that pertain to the locally generated `defsurj`s.
These additional applicability conditions are described
in the documentation of `defsurj`.

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 ofnew ismeasure<(back1 x1),...,(backn xn)> and the well-founded relation ofnew is the same asold .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 ist the guard consists of the new representation; when:predicate isnil , the guard consists of the argument tuples that are in the surjection's preimage of the guard ofold .In the

isodata design notes, referenced by theexpdata design notes,new is denoted byf' when:predicate isnil , andp' when:predicate ist .Note that:

- When
:predicate ist ,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 whichold holds.- When
:predicate isnil ,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) thatold maps the corresponding argument tuple in the old representation (where `corresponding' here means in the surjection's image).

Theorem that relates

new toold :;; 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 theexpdata design notes,new-to-old is denoted byf'f when:predicate isnil , and'pp when:predicate ist .

Theorem that relates

old tonew :;; 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 theexpdata design notes,old-to-new is denoted byff' when:predicate isnil , andpp' when:predicate ist .

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 theexpdata design notes,newp-of-new is denoted byf'A'B' .This is generated if and only if

surjmaps includes some:resultj .

A theory invariant is also generated to prevent
both

A call of

A call of

- Expdata-implementation
- Implementation of
`expdata`.