Enhanced variant of measured-subset.
This returns the same result as measured-subset,
but it is guard-verified
and includes a run-time check (which should always succeed) on the result
that allows us to prove the return type theorem
without strengthening the guard on
(defun measured-subset+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'measured-subset+)) (declare (ignorable __function__)) (if (not (irecursivep+ fn wrld)) (raise "The function ~x0 is not recursive." fn) (b* ((justification (getpropc fn 'justification nil wrld)) ((unless (weak-justification-p justification)) (raise "Internal error: ~ the JUSTIFICATION property ~x0 of ~x1 is not well-formed." justification fn)) (measured-subset (access justification justification :subset)) ((unless (symbol-listp measured-subset)) (raise "Internal error: ~ the measured subset ~x0 of ~x1 is not a true list of symbols." measured-subset fn))) measured-subset))))
(defthm symbol-listp-of-measured-subset+ (b* ((measured-subset (measured-subset+ fn wrld))) (symbol-listp measured-subset)) :rule-classes :rewrite)