		Search-engine friendly clone of the ACL2 documentation.

Defmapping

Establish a mapping between two domains.

Introduction

A mapping between two domains (i.e. predicates) A and B consists of two conversions (i.e. functions) \alpha and \beta. The domains and conversions are illustrated in these design notes, which use this notation. Each of the conversions may be injective, surjective, both (i.e. bijective), or neither.

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.

General Form

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

Inputs

name

Name under which the domains, conversions, and theorems are recorded in the world.
It must be a symbol that is not a keyword.

doma
domb
alpha
beta

Denote the domain A, the domain B, the conversion \alpha from A to B, and the conversion \beta from B to A.
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 is t, 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 is t, then the body of this lambda expression must only call guard-verified functions, except possibly in the :logic subterms of mbes or via ec-call. As an abbreviation, the name mac of a macro stands for the lambda expression (lambda (z1 z2 ...) (mac z1 z2 ...)), where z1, z2, ... are the required parameters of mac; that is, a macro name abbreviates its eta-expansion (considering only the macro's required parameters).
Let n be the arity of doma, and m be the arity of domb. Then: alpha must take n arguments and return m results; beta must take m arguments and return n results; doma and domb must return one result.

:beta-of-alpha-thm — default nil

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.

:alpha-of-beta-thm — default nil

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.

:guard-thms — default t

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.

:unconditional — default nil

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 is t or :alpha-of-beta-thm is t.

:thm-names — default nil

Non-default names for the generated theorems.
It must be a keyword-value list (thm1 name1 ... thmp namep), where each thmk is a keyword that identifies one of the generated theorems below, and each namek is a valid fresh theorem name.

:thm-enable — default nil

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 each thmk 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 is ('nil'), then the :all and :all-nonguard options are equivalent.

: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 defmapping. 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 defmapping.
: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, unless :print is nil.

:show-only — default nil

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

Applicability Conditions

In order for defmapping 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 defmapping is called, using the hints optionally supplied as the :hints input described in the `Inputs' section.

:alpha-image

The conversion \alpha maps the domain A to the domain B:
;; 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.

:beta-image

The conversion \beta maps the domain B to the domain A:
;; 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.

:beta-of-alpha

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 is t.

:alpha-of-beta

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 is t.

The :beta-of-alpha applicability condition (when present) implies the injectivity of \alpha. See the \alpha{}i and \alpha{}i' theorems in the design notes, and the generated theorem :alpha-injective below.

The :alpha-of-beta applicability condition (when present) implies the injectivity of \beta. See the \beta{}i and \beta{}i' theorems in the design notes, and the generated theorem :beta-injective below.

The :alpha-image applicability condition (always present) and the :alpha-of-beta applicabilty condition (when present) imply the surjectivity of \alpha. See the \alpha{}s and \alpha{}s' theorems in the design notes.

The :beta-image applicability condition (always present) and the :beta-of-alpha applicabilty condition (when present) imply the surjectivity of \beta. See the \beta{}s and \beta{}s' theorems in the design notes.

:doma-guard

The domain A is well-defined everywhere:
doma-guard<a1,...,an>
where doma-guard<a1,...,an> is: the guard term of doma, if doma is a function; the guard obligation of the body of doma, if doma is a lambda expression.
This corresponds to G{}A in the design notes.
This applicability condition is present if and only if :guard-thms is t.

:domb-guard

The domain B is well-defined everywhere:
domb-guard<b1,...,bm>
where domb-guard<b1,...,bm> is: the guard term of domb, if domb is a function; the guard obligation of the body of domb, if domb is a lambda expression.
This corresponds to G{}B in the design notes.
This applicability condition is present if and only if :guard-thms is t.

:alpha-guard

The conversion \alpha is well-defined at least over the domain A:
(implies (doma a1 ... an)
         alpha-guard<a1,...,an>)
where alpha-guard<a1,...,an> is: the guard term of alpha, if alpha is a function; the guard obligation of the body of alpha, if alpha is a lambda expression.
This corresponds to G{}\alpha in the design notes.
This applicability condition is present if and only if :guard-thms is t.

:beta-guard

The conversion \beta is well-defined at least over the domain B:
(implies (domb b1 ... bm)
         beta-guard<b1,...,bm>)
where beta-guard<b1,...,bm> is: the guard term of beta, if beta is a function; the guard obligation of the body of beta, if beta is a lambda expression.
This corresponds to G{}\beta in the design notes.
This applicability condition is present if and only if :guard-thms is t.

Generated Events

Unless overridden via the :thm-names input, the name of each generated theorem consists of the input name of defmapping, followed by ., followed by the identifying keyword (without :) below.

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 defthmdr are used to generate the theorems.

:alpha-image
:beta-image
:beta-of-alpha
:alpha-of-beta
:doma-guard
:domb-guard
:alpha-guard
:beta-guard

A theorem for each applicability condition. The :beta-of-alpha theorem is generated if and only if the :beta-of-alpha-thm input is t. The :alpha-of-beta theorem is generated if and only if the :alpha-of-beta-thm input is t. The ...-guard theorems are generated if and only if the :guard-thms input is t.

:alpha-injective

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 is t.

:beta-injective

The conversion \beta is injective over the domain B:
;; 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 is t.

Redundancy

A call of defmapping is redundant if and only if it is identical to a previous successful call of defmapping 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 defmapping whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

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.