		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-param-thms

Generate theorems about the parameters of a function.

Signature
(simpadd0-gen-param-thms args arg-types-compst all-arg-types all-params all-args) → (mv thm-events thm-names)
Arguments: args — Guard (symbol-listp args).; arg-types-compst — Guard (true-listp arg-types-compst).; all-arg-types — Guard (true-listp all-arg-types).; all-params — Guard (c::param-declon-listp all-params).; all-args — Guard (symbol-listp all-args).
Returns: thm-events — Type (pseudo-event-form-listp thm-events).; thm-names — Type (symbol-listp thm-names).

The args and arg-types-compst inputs are the corresponding outputs of simpadd0-gen-from-params; these are cdred in the recursion. The all-arg-types input is the arg-types output of simpadd0-gen-from-params; it stays the same during the recursion.

We return the theorem events, along with the theorem names.

The theorem names are used locally in an enclosing theorem, so they do not need to be particularly unique. But we should check and disambiguate them more thoroughly.

For each parameter of the function, we generate a theorem saying that, in the computation state resulting from pushing the initial scope to the frame stack, if the value corresponding to the parameter has a certain type, then reading the parameter from the computation state succeeds and yields a value of that type.

Definitions and Theorems

Function: simpadd0-gen-param-thms

(defun simpadd0-gen-param-thms
       (args arg-types-compst
             all-arg-types all-params all-args)
 (declare (xargs :guard (and (symbol-listp args)
                             (true-listp arg-types-compst)
                             (true-listp all-arg-types)
                             (c::param-declon-listp all-params)
                             (symbol-listp all-args))))
 (declare (xargs :guard (equal (len arg-types-compst)
                               (len args))))
 (let ((__function__ 'simpadd0-gen-param-thms))
  (declare (ignorable __function__))
  (b*
   (((when (endp args)) (mv nil nil))
    (arg (car args))
    (formula
     (cons
      'b*
      (cons
       (cons
        (cons
         'compst
         (cons
          (cons
           'c::push-frame
           (cons
            (cons
             'c::frame
             (cons
              'fun
              (cons
               (cons
                'list
                (cons
                    (cons 'c::init-scope
                          (cons (cons 'quote (cons all-params 'nil))
                                (cons (cons 'list all-args) 'nil)))
                    'nil))
               'nil)))
            '(compst0)))
          'nil))
        'nil)
       (cons (cons 'implies
                   (cons (cons 'and all-arg-types)
                         (cons (car arg-types-compst) 'nil)))
             'nil))))
    (hints
     '(("Goal"
         :in-theory
         '(init-scope-thm (:e ident)
                          (:e ldm-ident)
                          c::push-frame c::objdesign-of-var
                          c::objdesign-of-var-aux
                          c::compustate-frames-number
                          c::top-frame c::read-object
                          c::scopep-of-update (:e c::scopep)
                          c::compustate->frames-of-compustate
                          c::frame->scopes-of-frame
                          c::frame-fix-when-framep
                          c::frame-list-fix-of-cons
                          c::mapp-when-scopep c::framep-of-frame
                          c::objdesign-auto->frame-of-objdesign-auto
                          c::objdesign-auto->name-of-objdesign-auto
                          c::objdesign-auto->scope-of-objdesign-auto
                          c::return-type-of-objdesign-auto
                          c::scope-fix-when-scopep c::scope-fix
                          c::scope-list-fix-of-cons (:e c::ident)
                          (:e c::ident-fix$inline)
                          (:e c::identp)
                          (:t c::objdesign-auto)
                          omap::assoc-of-update
                          simpadd0-param-thm-list-lemma nfix fix
                          len car-cons cdr-cons commutativity-of-+
                          acl2::fold-consts-in-+
                          acl2::len-of-append acl2::len-of-rev
                          acl2::rev-of-cons (:e acl2::fast-<<)
                          unicity-of-0 (:e rev)
                          (:t len)))))
    (thm-name (packn-pos (list arg '-param-thm) arg))
    (thm-event
         (cons 'defruled
               (cons thm-name
                     (cons formula
                           (cons ':hints (cons hints 'nil))))))
    ((mv more-thm-events more-thm-names)
     (simpadd0-gen-param-thms (cdr args)
                              (cdr arg-types-compst)
                              all-arg-types all-params all-args)))
   (mv (cons thm-event more-thm-events)
       (cons thm-name more-thm-names)))))

Theorem: pseudo-event-form-listp-of-simpadd0-gen-param-thms.thm-events

(defthm
      pseudo-event-form-listp-of-simpadd0-gen-param-thms.thm-events
 (b* (((mv ?thm-events ?thm-names)
       (simpadd0-gen-param-thms args arg-types-compst
                                all-arg-types all-params all-args)))
   (pseudo-event-form-listp thm-events))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-simpadd0-gen-param-thms.thm-names

(defthm symbol-listp-of-simpadd0-gen-param-thms.thm-names
 (b* (((mv ?thm-events ?thm-names)
       (simpadd0-gen-param-thms args arg-types-compst
                                all-arg-types all-params all-args)))
   (symbol-listp thm-names))
 :rule-classes :rewrite)

Theorem: len-of-simpadd-gen-param-thms.thm-names

(defthm len-of-simpadd-gen-param-thms.thm-names
 (b* (((mv ?thm-events ?thm-names)
       (simpadd0-gen-param-thms args arg-types-compst
                                all-arg-types all-params all-args)))
   (equal (len thm-names)
          (len thm-events))))

Theorem: simpadd0-param-thm-list-lemma

(defthm simpadd0-param-thm-list-lemma
  (equal (nth (len l) (append (rev l) (list x)))
         x))