• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
              • Atc-event-and-code-generation
                • Atc-symbolic-computation-states
                • Atc-symbolic-execution-rules
                • Atc-gen-ext-declon-lists
                • Atc-function-and-loop-generation
                  • Atc-gen-cfun-correct-thm
                  • Atc-typed-formals
                  • Atc-gen-outer-bindings-and-hyps
                  • Atc-gen-fundef
                  • Atc-gen-exec-stmt-while-for-loop
                  • Atc-gen-context-preamble
                  • Atc-gen-pop-frame-thm
                  • Atc-gen-loop-correct-thm
                  • Atc-gen-init-scope-thms
                  • Atc-gen-fun-correct-thm
                  • Atc-gen-fn-result-thm
                  • Atc-gen-loop-body-correct-thm
                  • Atc-gen-loop
                  • Atc-gen-loop-test-correct-thm
                  • Atc-check-guard-conjunct
                  • Atc-find-affected
                  • Atc-gen-cfun-final-compustate
                  • Atc-gen-init-inscope-auto
                  • Atc-gen-init-inscope-static
                  • Atc-gen-push-init-thm
                  • Atc-gen-loop-measure-fn
                  • Atc-gen-fun-endstate
                  • Atc-gen-loop-termination-thm
                  • Atc-gen-formal-thm
                  • Atc-gen-loop-final-compustate
                  • Atc-gen-loop-measure-thm
                    • Atc-gen-object-disjoint-hyps
                    • Atc-loop-body-term-subst
                    • Atc-gen-omap-update-formals
                    • Atc-gen-loop-tthm-formula
                    • Atc-gen-init-inscope
                    • Atc-gen-fn-def*
                    • Atc-gen-param-declon-list
                    • Atc-formal-affectablep
                    • Atc-gen-cfun-fun-env-thm
                    • Atc-gen-add-var-formals
                    • Atc-gen-cfun-fun-env-thm-name
                    • Atc-gen-fn-guard
                    • Atc-filter-exec-fun-args
                    • Atc-gen-context-preamble-aux-aux
                    • Atc-typed-formals-to-extobjs
                    • Atc-formal-affectable-listp
                  • Atc-statement-generation
                  • Atc-gen-fileset
                  • Atc-gen-everything
                  • Atc-gen-obj-declon
                  • Atc-gen-fileset-event
                  • Atc-tag-tables
                  • Atc-expression-generation
                  • Atc-generation-contexts
                  • Atc-gen-wf-thm
                  • Term-checkers-atc
                  • Atc-variable-tables
                  • Term-checkers-common
                  • Atc-gen-init-fun-env-thm
                  • Atc-gen-appconds
                  • Read-write-variables
                  • Atc-gen-thm-assert-events
                  • Test*
                  • Atc-gen-prog-const
                  • Atc-gen-expr-bool
                  • Atc-theorem-generation
                  • Atc-tag-generation
                  • Atc-gen-expr-pure
                  • Atc-function-tables
                  • Atc-object-tables
                • Fty-pseudo-term-utilities
                • Atc-term-recognizers
                • Atc-input-processing
                • Atc-shallow-embedding
                • Atc-process-inputs-and-gen-everything
                • Atc-table
                • Atc-fn
                • Atc-pretty-printing-options
                • Atc-types
                • Atc-macro-definition
              • Atc-tutorial
            • Language
            • Representation
            • Transformation-tools
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • 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)