		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Gen-param-thms

Generate theorems about the parameters of a function.

Signature
(gen-param-thms arg-types-compst all-arg-types all-params all-args init-scope-thm const-new thm-index) → (mv thm-events thm-names updated-thm-index)
Arguments: 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).; init-scope-thm — Guard (symbolp init-scope-thm).; const-new — Guard (symbolp const-new).; thm-index — Guard (posp thm-index).
Returns: thm-events — Type (pseudo-event-form-listp thm-events).; thm-names — Type (symbol-listp thm-names).; updated-thm-index — Type (posp updated-thm-index).

The args and arg-types-compst inputs are the corresponding outputs of gen-from-params; these are cdred in the recursion. The all-arg-types input is the arg-types output of 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: gen-param-thms

(defun gen-param-thms
       (arg-types-compst all-arg-types all-params all-args
                         init-scope-thm const-new thm-index)
 (declare (xargs :guard (and (true-listp arg-types-compst)
                             (true-listp all-arg-types)
                             (c::param-declon-listp all-params)
                             (symbol-listp all-args)
                             (symbolp init-scope-thm)
                             (symbolp const-new)
                             (posp thm-index))))
 (let ((__function__ 'gen-param-thms))
  (declare (ignorable __function__))
  (b*
   (((when (endp arg-types-compst))
     (mv nil nil (pos-fix thm-index)))
    (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
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
            'quote
            (cons (cons init-scope-thm
                        '((:e ident)
                          c::push-frame
                          c::compustate-has-var-with-type-p
                          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
                          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)
                          (:e c::type-fix)))
                  'nil))
         'nil)))
      'nil))
    ((mv thm-name thm-index)
     (gen-thm-name const-new thm-index))
    (thm-event
         (cons 'defruled
               (cons thm-name
                     (cons formula
                           (cons ':hints (cons hints 'nil))))))
    ((mv more-thm-events
         more-thm-names thm-index)
     (gen-param-thms (cdr arg-types-compst)
                     all-arg-types all-params all-args
                     init-scope-thm const-new thm-index)))
   (mv (cons thm-event more-thm-events)
       (cons thm-name more-thm-names)
       thm-index))))

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

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

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

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

Theorem: posp-of-gen-param-thms.updated-thm-index

(defthm posp-of-gen-param-thms.updated-thm-index
  (b* (((mv ?thm-events
            ?thm-names ?updated-thm-index)
        (gen-param-thms arg-types-compst
                        all-arg-types all-params all-args
                        init-scope-thm const-new thm-index)))
    (posp updated-thm-index))
  :rule-classes (:rewrite :type-prescription))

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

(defthm len-of-gen-param-thms.thm-names
  (b* (((mv ?thm-events
            ?thm-names ?updated-thm-index)
        (gen-param-thms arg-types-compst
                        all-arg-types all-params all-args
                        init-scope-thm const-new thm-index)))
    (equal (len thm-names)
           (len thm-events))))

Theorem: param-thm-list-lemma

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