Establish a mapping between two domains.

A mapping between two domains (i.e. predicates)

This macro attempts to verify that two specified conversions are mappings between two specified domains i.e. that they map values in one domain to values in the other domain. Optionally, the macro also attempts to verify additional properties of the conversions that imply injectivity and/or surjectivity. The verification amounts to proving the applicability conditions below as theorems, from which additional theorems are automatically proved.

The domains, conversions, and theorems are recorded in the ACL2 world, under a specified name that can be referenced from other tools (e.g. APT transformations).

The domains may have multiple arguments, and the conversions may have multiple arguments and results. In this case, the domains are subsets of cartesian products of the ACL2 universe of values, and the conversions map tuples to tuples, as shown in the `Generalization to Tuples' page of the design notes.

(defmapping name doma domb alpha beta :beta-of-alpha-thm ... :alpha-of-beta-thm ... :guard-thms ... :unconditional ... :thm-names ... :thm-enable ... :hints ... :print ... :show-only ... )

Name under which the domains, conversions, and theorems are recorded in the world.

It must be a symbol that is not a keyword.

Denote the domain

A , the domainB , the conversion\alpha fromA toB , and the conversion\beta fromB toA .Each must be one of the following:

- The name of a logic-mode function. This function must have no input or output stobjs. If the
:guard-thms input ist , then this function must be guard-verified.- A closed lambda expression that only references logic-mode functions. This lambda expression must have no input or output stobjs. If the
:guard-thms input ist , then the body of this lambda expression must only call guard-verified functions, except possibly in the:logic subterms ofmbe s or viaec-call . As an abbreviation, the namemac of a macro stands for the lambda expression(lambda (z1 z2 ...) (mac z1 z2 ...)) , wherez1 ,z2 , ... are the required parameters ofmac ; that is, a macro name abbreviates its eta-expansion (considering only the macro's required parameters).Let

n be the arity ofdoma , andm be the arity ofdomb . Then:alpha must taken arguments and returnm results;beta must takem arguments and returnn results;doma anddomb must return one result.

Determines whether the

:beta-of-alpha applicability condition is generated or not, which in turn determines whether certain theorems are generated or not.It must be one of the following:

t , to generate them.nil , to not generate them.

Determines whether the

:alpha-of-beta applicability condition is generated or not, which in turn determines whether certain theorems are generated or not.It must be one of the following:

t , to generate them.nil , to not generate them.

Determines whether the

...-guard applicability conditions are present or not, and generated as theorems.It must be one of the following:

t , to check and generate them.nil , to not check and generate them.

Determines whether some of the applicability conditions and generated theorems are unconditional, i.e. without hypotheses (see the `Variant: Unconditional Theorems' page of the design notes, and the `Applicability Conditions' and `Generated Events' sections below).

It must be one of the following:

t , for unconditional (i.e. stronger) theorems.nil , for conditional (i.e. normal) theorems.It may be

t only if:beta-of-alpha-thm ist or:alpha-of-beta-thm ist .

Non-default names for the generated theorems.

It must be a keyword-value list

(thm1 name1 ... thmp namep) , where eachthmk is a keyword that identifies one of the generated theorems below, and eachnamek is a valid fresh theorem name.

Determines which of the generated theorems must be enabled.

It must be one of the following:

nil , to enable none of them.:all , to enable all of them.:all-nonguard , to enable all of them except for the...-guard theorems.- A non-empty list
(thm1 ... thmp) , where eachthmk is a keyword that identifies one of the generated theorems below, to enable the theorems identified by the keywords. Only keywords for theorems that are generated (based on the:beta-of-alpha-thm ,:alpha-of-beta-thm , and:guard-thms inputs) may be in this list.As explained under `Generated Events', the theorems are generated as rewrite rules, if they are valid rewrite rules. The enablement specified by

:thm-enable applies only to those theorems that are rewrite rules; it is ignored for theorems that are not rewrite rules.Note that the first and last option could be described as a single one, namely as a possibly empty list of theorem keywords, where the empty list

nil enables no theorem. The:all option is provided for completeness, but the:all-nonguard may be more useful: in general, the...-guard theorems do not look like useful rewrite rules, while the other theorems generally do.If

:guard-thms isnil , then the:all and:all-nonguard options are equivalent.

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 ofdefmapping . 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 ofdefmapping .: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

defmapping is redundant, an indication to that effect is printed on the screen, unlessnil .

Determines whether the event expansion of

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

In order for

The conversion

\alpha maps the domainA to the domainB :;; when m = 1: (implies (doma a1 ... an) (domb (alpha a1 ... an))) ;; when m > 1: (implies (doma a1 ... an) (mv-let (b1 ... bm) (alpha a1 ... an) (domb b1 ... bm)))This corresponds to

\alpha{}A in the design notes.

The conversion

\beta maps the domainB to the domainA :;; when n = 1: (implies (domb b1 ... bm) (doma (beta b1 ... bm))) ;; when n > 1: (implies (domb b1 ... bm) (mv-let (a1 ... an) (beta b1 ... bm) (doma a1 ... an)))This corresponds to

\beta{}B in the design notes.

The conversion

\beta is left inverse of\alpha , i.e. the conversion\alpha is right inverse of\beta :;; when m = n = 1 and :unconditional is nil: (implies (doma a) (equal (beta (alpha a)) a)) ;; when m = n = 1 and :unconditional is t: (equal (beta (alpha a)) a) ;; when m = 1 and n > 1 and :unconditional is nil: (implies (doma a1 ... an) (mv-let (aa1 ... aan) (beta (alpha a1 ... an)) (and (equal aa1 a1) ... (equal aan an)))) ;; when m = 1 and n > 1 and :unconditional is t: (mv-let (aa1 ... aan) (beta (alpha a1 ... an)) (and (equal aa1 a1) ... (equal aan an))) ;; when m > 1 and n = 1 and :unconditional is nil: (implies (doma a) (mv-let (b1 ... bm) (alpha a) (equal (beta b1 ... bm) a))) ;; when m > 1 and n = 1 and :unconditional is t: (mv-let (b1 ... bm) (alpha a) (equal (beta b1 ... bm) a)) ;; when m > 1 and n > 1 and :unconditional is nil: (implies (doma a1 ... an) (mv-let (b1 ... bm) (alpha a1 ... an) (mv-let (aa1 ... aan) (beta b1 ... bm) (and (equal aa1 a1) ... (equal aan an))))) ;; when m > 1 and n > 1 and :unconditional is t: (mv-let (b1 ... bm) (alpha a1 ... an) (mv-let (aa1 ... aan) (beta b1 ... bm) (and (equal aa1 a1) ... (equal aan an))))This corresponds to

\beta{}\alpha or\beta{}\alpha' in the design notes.This applicability condition is present if and only if

:beta-of-alpha-thm ist .

The conversion

\alpha is left inverse of\beta , i.e. the conversion\beta is right inverse of\alpha :;; when n = m = 1 and :unconditional is nil: (implies (domb b) (equal (alpha (beta b)) b)) ;; when n = m = 1 and :unconditional is t: (equal (alpha (beta b)) b) ;; when n = 1 and m > 1 and :unconditional is nil: (implies (domb b1 ... bm) (mv-let (bb1 ... bbm) (alpha (beta b1 ... bm)) (and (equal bb1 b1) ... (equal bbm bm)))) ;; when n = 1 and m > 1 and :unconditional is t: (mv-let (bb1 ... bbm) (alpha (beta b1 ... bm)) (and (equal bb1 b1) ... (equal bbm bm))) ;; when n > 1 and m = 1 and :unconditional is nil: (implies (domb b) (mv-let (a1 ... an) (beta b) (equal (alpha a1 ... an) b))) ;; when n > 1 and m = 1 and :unconditional is t: (mv-let (a1 ... an) (beta b) (equal (alpha a1 ... an) b)) ;; when n > 1 and m > 1 and :unconditional is nil: (implies (domb b1 ... bm) (mv-let (a1 ... an) (beta b1 ... bm) (mv-let (bb1 ... bbm) (alpha a1 ... an) (and (equal bb1 b1) ... (equal bbm bm))))) ;; when n > 1 and m > 1 and :unconditional is t: (mv-let (a1 ... an) (beta b1 ... bm) (mv-let (bb1 ... bbm) (alpha a1 ... an) (and (equal bb1 b1) ... (equal bbm bm))))This corresponds to

\alpha{}\beta or\alpha{}\beta' in the design notes.This applicability condition is present if and only if

:alpha-of-beta-thm ist .

The

The

The

The

The domain

A is well-defined everywhere:doma-guard<a1,...,an>where

doma-guard<a1,...,an> is: the guard term ofdoma , ifdoma is a function; the guard obligation of the body ofdoma , ifdoma is a lambda expression.This corresponds to

G{}A in the design notes.This applicability condition is present if and only if

:guard-thms ist .

The domain

B is well-defined everywhere:domb-guard<b1,...,bm>where

domb-guard<b1,...,bm> is: the guard term ofdomb , ifdomb is a function; the guard obligation of the body ofdomb , ifdomb is a lambda expression.This corresponds to

G{}B in the design notes.This applicability condition is present if and only if

:guard-thms ist .

The conversion

\alpha is well-defined at least over the domainA :(implies (doma a1 ... an) alpha-guard<a1,...,an>)where

alpha-guard<a1,...,an> is: the guard term ofalpha , ifalpha is a function; the guard obligation of the body ofalpha , ifalpha is a lambda expression.This corresponds to

G{}\alpha in the design notes.This applicability condition is present if and only if

:guard-thms ist .

The conversion

\beta is well-defined at least over the domainB :(implies (domb b1 ... bm) beta-guard<b1,...,bm>)where

beta-guard<b1,...,bm> is: the guard term ofbeta , ifbeta is a function; the guard obligation of the body ofbeta , ifbeta is a lambda expression.This corresponds to

G{}\beta in the design notes.This applicability condition is present if and only if

:guard-thms ist .

Unless overridden via the

The theorems are generated as rewrite rules
if they are valid rewrite rules;
otherwise, they are generated with no rule classes.
The macros `defthmr` and

A theorem for each applicability condition. The

:beta-of-alpha theorem is generated if and only if the:beta-of-alpha-thm input ist . The:alpha-of-beta theorem is generated if and only if the:alpha-of-beta-thm input ist . The...-guard theorems are generated if and only if the:guard-thms input ist .

The conversion

\alpha is injective:;; when :unconditional is nil: (defthmr name.alpha-injective (implies (and (doma a1 ... an) (doma aa1 ... aan)) (equal (equal (alpha a1 ... an) (alpha aa1 ... aan)) (and (equal a1 aa1) ... (equal an aan))))) ;; when :unconditional is t: (defthmr name.alpha-injective (equal (equal (alpha a1 ... an) (alpha aa1 ... aan)) (and (equal a1 aa1) ... (equal an aan))))This corresponds to

\alpha{}i or\alpha{}i' in the design notes.This theorem is automatically proved from the applicability conditions.

This theorem is generated if and only if the

:beta-of-alpha-thm input ist .

The conversion

\beta is injective over the domainB :;; when :unconditional is nil: (defthmr name.beta-injective (implies (and (domb b1 ... bm) (domb bb1 ... bbm)) (equal (equal (beta b1 ... bm) (beta bb1 ... bbm)) (and (equal b1 bn1) ... (equal bm bbm))))) ;; when :unconditional is t: (defthmr name.beta-injective (equal (equal (beta b1 ... bm) (beta bb1 ... bbm)) (and (equal b1 bn1) ... (equal bm bbm))))This corresponds to

\beta{}i or\beta{}i' in the design notes.This theorem is automatically proved from the applicability conditions.

This theorem is generated if and only if the

:alpha-of-beta-thm input ist .

A call of

A call of

- Defsurj
- Establish a surjective mapping between two domains.
- Defiso
- Establish an isomorphic mapping between two domains.
- Defmapping-implementation
- Implementation of
`defmapping`. - Definj
- Establish an injective mapping between two domains.