		Search-engine friendly clone of the ACL2 documentation.

Defflatsum

Introduce a fixtype for the flat (i.e. not tagged) sum of disjoint fixtypes.

Introduction

This is a very preliminary tool for now. In particular, it does not perform a thorough input validation.

deftagsum introduces a tagged sum of fixtypes, some of which may partially or totally overlap (the tags distinguish them in the sum); it is like a disjoint union in set theory. In contrast, this defflatsum macro introduces a flat (i.e. untagged) sum of fixtypes; it is like a union in set theory. However, the summand fixtypes must be pairwise disjoint, so that the union is actually disjoint.

General Form

(defflatsum type
            (:kwd1 type1)
            ...
            (:kwdn typen)
            :pred ...
            :fix ...
            :equiv ...
            :parents ...
            :short ...
            :long ...
            :prepwork ...
  )

Inputs

:type

A symbol that specifies the name of the new fixtype.

(:kwd1 type1)
...
(:kwdn typen)

Two or more doublets, one for each summand. The first component of each doublet is a keyword that identifies the summand; all these keywords must be distinct. The second component of each doublet is an existing fixtype that is a summand; these fixtypes must be pairwise disjoint.

:pred

A symbol that specifies the name of the fixtype's recognizer. If this is nil (the default), the name of the recognizer is type followed by -p.

:fix

A symbol that specifies the name of the fixtype's fixer. If this is nil (the default), the name of the fixer is type followed by -fix.

:equiv

A symbol that specifies the name of the fixtype's equivalence. If this is nil (the default), the name of the equivalence is type followed by -equiv.

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the fixtype.

:prepwork

A list of preparatory event forms. See the `Generated Events' section.

Applicability Conditions

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

The fixtypes type1, ..., typen must be pairwise disjoint. Currently this proof obligation is not quite explicated as a theorem to be proved, but the generated defflexsum will likely fail if the pairwise disjointness does not hold.

Generated Events

This macro generates a defflexsum with some accompanying theorems:

(defflexsum type
  (:kwd1 :fields ((get :type type1 :acc-body x))
         :ctor-body get
         :cond (type1p x))
  (:kwd2 :fields ((get :type type2 :acc-body x))
         :ctor-body get
         :cond (type2p x))
  ...
  (:kwdn :fields ((get :type typen :acc-body x))
         :ctor-body get)
  :prepwork ...
  ///
  (defthm typep-when-type1p
    (implies (type1p x)
             (typep x)))
  (defthm typep-when-type2p
    (implies (type2p x)
             (typep x)))
  ...
  (defthm typep-when-typenp
    (implies (typenp x)
             (typep x))))

Note that the last summand does not have :cond, while all the previous ones do.

If a :prepwork is supplied to defflatsum, it is copied to the generated defflexsum. Otherwise, the defflexsum is generated with a default :prepwork that locally enables all the predicates and fixers.

Subtopics

Defflatsum-implementation: Implementation of defflatsum.