Expand-measure
ACL2::measure function for proving termination of function
expand.
- Signature
(expand-measure expand-args) → m
- Arguments
- expand-args — Guard (ex-args-p expand-args).
- Returns
- m — Type (nat-listp m).
The measure is using the lexicographical order (see mutual-recursion), using a list of three arguments, where the priority
goes from the first argument to the second, and then to the third.
The first argument is wrld-fn-len which appears in ex-args.
It is necessary for decreasing the measure when we are expanding a function
that is not in fn-lst (see ex-args). The second argument is a
summation of fn-lvls which also appears in ex-args. This list
remembers how many levels are left for each function. Since functions not
in fn-lst are added to fn-lvls with 0 level, this argument
doesn't decrease in that case. This is why it's necessary to have the first
argument wrld-fn-len. The third argument is the ACL2-count of
current term-lst (also see ex-args). This argument decreases
every time the recursive function expand goes into expand the cdr of term-lst.
Definitions and Theorems
Function: expand-measure
(defun expand-measure (expand-args)
(declare (xargs :guard (ex-args-p expand-args)))
(let ((acl2::__function__ 'expand-measure))
(declare (ignorable acl2::__function__))
(b* ((expand-args (ex-args-fix expand-args))
((ex-args a) expand-args)
(lvl-sum (sum-lvls a.fn-lvls)))
(list a.wrld-fn-len
lvl-sum (acl2-count a.term-lst)))))
Theorem: nat-listp-of-expand-measure
(defthm nat-listp-of-expand-measure
(b* ((m (expand-measure expand-args)))
(nat-listp m))
:rule-classes :rewrite)
