		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 arg-types-compst all-params all-args) → (mv thm-events thm-names)
Arguments: args — Guard (symbol-listp args).; arg-types — Guard (true-listp arg-types).; arg-types-compst — Guard (true-listp arg-types-compst).; 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, arg-types and arg-types-compst inputs are the corresponding outputs of simpadd0-gen-from-params.

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 is an int value, then reading the parameter from the computation state succeeds and yields an int value.

Definitions and Theorems

Function: simpadd0-gen-param-thms

(defun simpadd0-gen-param-thms
       (args arg-types
             arg-types-compst all-params all-args)
 (declare (xargs :guard (and (symbol-listp args)
                             (true-listp arg-types)
                             (true-listp arg-types-compst)
                             (c::param-declon-listp all-params)
                             (symbol-listp all-args))))
 (declare (xargs :guard (and (equal (len arg-types) (len args))
                             (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 (car arg-types)
                         (cons (car arg-types-compst) 'nil)))
             'nil))))
    (hints
     '(("Goal"
         :in-theory
         '(init-scope-thm (:e ident)
                          (:e c$::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
                          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-list-fix-of-cons (:e c::ident)
                          (:e c::ident-fix$inline)
                          (:e c::identp)
                          (:t c::objdesign-auto)
                          omap::assoc omap::head
                          omap::tail omap::mfix-when-mapp
                          omap::mapp-non-nil-implies-not-emptyp
                          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 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)
                              (cdr arg-types-compst)
                              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
                             arg-types-compst 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
                             arg-types-compst 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
                             arg-types-compst 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))