		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-old-to-list-of-mv-nth

Generate a local theorem saying that a call of old can be decomposed via mv-nths and re-composed via list.

Signature
(isodata-gen-old-to-list-of-mv-nth old$ old-fn-unnorm-name m names-to-avoid wrld) → (mv old-to-list-of-mv-nth-name old-to-list-of-mv-nth-event updated-names-to-avoid)
Arguments: old$ — Guard (symbolp old$).; old-fn-unnorm-name — Guard (symbolp old-fn-unnorm-name).; m — Guard (natp m).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: old-to-list-of-mv-nth-name — A symbolp.; old-to-list-of-mv-nth-event — A pseudo-event-formp.; updated-names-to-avoid — A symbol-listp.

This is similar to isodata-gen-new-to-list-of-mv-nth.

Definitions and Theorems

Function: isodata-gen-old-to-list-of-mv-nth

(defun isodata-gen-old-to-list-of-mv-nth
       (old$ old-fn-unnorm-name
             m names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbolp old-fn-unnorm-name)
                             (natp m)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'isodata-gen-old-to-list-of-mv-nth))
  (declare (ignorable __function__))
  (b*
   (((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix 'old-to-list-of-mv-nth
                                        nil names-to-avoid wrld))
    (x1...xn (formals old$ wrld))
    (old-call (cons old$ x1...xn))
    (mv-nth-terms (loop$ for i from 0 to (1- m)
                         collect
                         (cons 'mv-nth
                               (cons i (cons old-call 'nil)))))
    (formula (cons 'equal
                   (cons old-call
                         (cons (cons 'list mv-nth-terms) 'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons (cons 'quote
                    (cons (cons old$
                                (cons old-fn-unnorm-name '(mv-nth)))
                          'nil))
              'nil)))
      'nil))
    ((mv event &)
     (evmac-generate-defthm name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (mv name event names-to-avoid))))