		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-prod-combination+theorem

Generate the combination for the fields of a product type or a case of a sum type, as well as a theorem about the predicate for the product or sum type applied to the constructor of the product type or the case of the sum type.

Signature
(deffoldred-gen-prod-combination+theorem type constr kind kind-fn prod suffix targets extra-args default combine fty-table) → (mv fn-term thm-events)
Arguments: type — Guard (symbolp type).; constr — Guard (symbolp constr).; kind — Guard (symbolp kind).; kind-fn — Guard (symbolp kind-fn).; prod — Guard (flexprod-p prod).; suffix — Guard (symbolp suffix).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; combine — Guard (symbolp combine).; fty-table — Guard (alistp fty-table).
Returns: thm-events — Type (acl2::pseudo-event-form-listp thm-events).

The type input is the name of the product type or sum type. The constr input is the name of the constructor of the product type or the case of the sum type; it is the same as type in the case of a product type, but in the case of a sum type it consists of type followed by the kind of the case of the sum. The kind input is nil if type is a product type, while it is the keyword kind of the summand if type is a sum type. The kind-fn input is the kind function if type is a sum type, otherwise it is nil.

The fn-term result is from deffoldred-gen-prod-combination: see that function for details. The theorem's formula involves the thm-term and field-names results of that function: this is the theorem <type>-<suffix>-of-<type> described in deffold-reduce.

If we are dealing with the summand of a sum type (which we can tell from whether the kind function kind-fn passed as input is not nil), and if that summand has no fields, then we generate a theorem of a different form, which is more amenable to rewriting in proofs.

Definitions and Theorems

Function: deffoldred-gen-prod-combination+theorem

(defun deffoldred-gen-prod-combination+theorem
       (type constr kind kind-fn prod suffix targets
             extra-args default combine fty-table)
 (declare (xargs :guard (and (symbolp type)
                             (symbolp constr)
                             (symbolp kind)
                             (symbolp kind-fn)
                             (flexprod-p prod)
                             (symbolp suffix)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (symbolp combine)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-gen-prod-combination+theorem))
  (declare (ignorable __function__))
  (b*
   ((fields (flexprod->fields prod))
    ((unless (flexprod-field-listp fields))
     (raise "Internal error: malformed fields ~x0."
            fields)
     (mv nil nil))
    ((mv fn-term
         thm-rhs field-names field-thm-events)
     (deffoldred-gen-prod-combination
          type fields kind kind-fn suffix targets
          extra-args default combine fty-table))
    (type-suffix (deffoldred-gen-fold-name type suffix))
    (extra-args-names (deffoldred-extra-args-to-names extra-args))
    ((mv thm-name thm-event)
     (if
      (and kind-fn (not fields))
      (b* ((kind (flexprod->kind prod))
           ((unless (or (not kind) (keywordp kind)))
            (raise "Internal error: malformed kind ~x0."
                   kind)
            (mv nil '(_)))
           (type-suffix-when-kind
                (acl2::packn-pos (list type-suffix '-when- kind)
                                 suffix)))
       (mv
        type-suffix-when-kind
        (cons
         'defruled
         (cons
          type-suffix-when-kind
          (cons
           (cons
            'implies
            (cons
               (cons 'equal
                     (cons (cons kind-fn (cons type 'nil))
                           (cons kind 'nil)))
               (cons (cons 'equal
                           (cons (cons type-suffix
                                       (cons type extra-args-names))
                                 (cons default 'nil)))
                     'nil)))
           (cons ':enable
                 (cons type-suffix 'nil)))))))
      (b* ((type-suffix-of-constr
                (acl2::packn-pos (list type-suffix '-of- constr)
                                 suffix))
           (thm-lhs (cons type-suffix
                          (cons (cons constr field-names)
                                extra-args-names))))
       (mv
        type-suffix-of-constr
        (cons
          'defruled
          (cons type-suffix-of-constr
                (cons (cons 'equal
                            (cons thm-lhs (cons thm-rhs 'nil)))
                      (if fields (cons ':expand (cons thm-lhs 'nil))
                        (cons ':enable
                              (cons type-suffix 'nil))))))))))
    (thm-events
     (cons
      thm-event
      (cons
           (cons 'add-to-ruleset
                 (cons (deffoldred-gen-ruleset-name suffix)
                       (cons (cons 'quote
                                   (cons (cons thm-name 'nil) 'nil))
                             'nil)))
           'nil))))
   (mv fn-term
       (append thm-events field-thm-events)))))

Theorem: pseudo-event-form-listp-of-deffoldred-gen-prod-combination+theorem.thm-events

(defthm
 pseudo-event-form-listp-of-deffoldred-gen-prod-combination+theorem.thm-events
 (b* (((mv ?fn-term ?thm-events)
       (deffoldred-gen-prod-combination+theorem
            type
            constr kind kind-fn prod suffix targets
            extra-args default combine fty-table)))
   (acl2::pseudo-event-form-listp thm-events))
 :rule-classes :rewrite)