		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop-measure-thm

Generate type prescription theorem asserting that the measure of the recursive function fn yields a natural number.

Signature
(atc-gen-loop-measure-thm fn fn-appconds appcond-thms measure-of-fn measure-formals names-to-avoid wrld) → (mv event name updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; fn-appconds — Guard (symbol-symbol-alistp fn-appconds).; appcond-thms — Guard (keyword-symbol-alistp appcond-thms).; measure-of-fn — Guard (symbolp measure-of-fn).; measure-formals — Guard (symbol-listp measure-formals).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: event — Type (pseudo-event-formp event).; name — Type (symbolp name).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

This is like the applicability condition, except that it uses the generated measure function (to treat the measure as a black box, as discussed in atc-gen-loop-measure-fn), and that it is a type prescription rule (which seems needed, as opposed a rewrite rule, based on proof experiments).

Definitions and Theorems

Function: atc-gen-loop-measure-thm

(defun atc-gen-loop-measure-thm
       (fn fn-appconds appcond-thms measure-of-fn
           measure-formals names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (symbol-symbol-alistp fn-appconds)
                             (keyword-symbol-alistp appcond-thms)
                             (symbolp measure-of-fn)
                             (symbol-listp measure-formals)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (declare (xargs :guard (irecursivep+ fn wrld)))
 (let ((__function__ 'atc-gen-loop-measure-thm))
  (declare (ignorable __function__))
  (b*
   ((appcond-thm (cdr (assoc-eq (cdr (assoc-eq fn fn-appconds))
                                appcond-thms)))
    (natp-of-measure-of-fn-thm
         (packn-pos (list 'natp-of-measure-of- fn)
                    fn))
    ((mv natp-of-measure-of-fn-thm
         names-to-avoid)
     (fresh-logical-name-with-$s-suffix natp-of-measure-of-fn-thm
                                        nil names-to-avoid wrld))
    ((mv natp-of-measure-of-fn-thm-event &)
     (evmac-generate-defthm
      natp-of-measure-of-fn-thm
      :formula (cons 'natp
                     (cons (cons measure-of-fn measure-formals)
                           'nil))
      :rule-classes :type-prescription
      :enable nil
      :hints
      (cons
       (cons
            '"Goal"
            (cons ':in-theory
                  (cons (cons 'quote
                              (cons (cons measure-of-fn 'nil) 'nil))
                        (cons ':use (cons appcond-thm 'nil)))))
       'nil))))
   (mv natp-of-measure-of-fn-thm-event
       natp-of-measure-of-fn-thm
       names-to-avoid))))

Theorem: pseudo-event-formp-of-atc-gen-loop-measure-thm.event

(defthm pseudo-event-formp-of-atc-gen-loop-measure-thm.event
 (b*
  (((mv acl2::?event
        ?name ?updated-names-to-avoid)
    (atc-gen-loop-measure-thm fn
                              fn-appconds appcond-thms measure-of-fn
                              measure-formals names-to-avoid wrld)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-loop-measure-thm.name

(defthm symbolp-of-atc-gen-loop-measure-thm.name
 (b*
  (((mv acl2::?event
        ?name ?updated-names-to-avoid)
    (atc-gen-loop-measure-thm fn
                              fn-appconds appcond-thms measure-of-fn
                              measure-formals names-to-avoid wrld)))
  (symbolp name))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-loop-measure-thm.updated-names-to-avoid

(defthm
    symbol-listp-of-atc-gen-loop-measure-thm.updated-names-to-avoid
  (implies (symbol-listp names-to-avoid)
           (b* (((mv acl2::?event
                     ?name ?updated-names-to-avoid)
                 (atc-gen-loop-measure-thm
                      fn
                      fn-appconds appcond-thms measure-of-fn
                      measure-formals names-to-avoid wrld)))
             (symbol-listp updated-names-to-avoid)))
  :rule-classes :rewrite)