Lift atc-process-function to lists.
(atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld) → (mv erp targets new-previous-structs new-previous-objs new-previous-fns new-uncalled-fns)
We thread the lists through.
If successful, we also return the target list itself, with a guaranteed symbol-listp type, so that calling code has that fact readily available.
Function:
(defun atc-process-target-list (targets previous-structs previous-objs previous-fns uncalled-fns wrld) (declare (xargs :guard (and (true-listp targets) (symbol-listp previous-structs) (symbol-listp previous-objs) (symbol-listp previous-fns) (symbol-listp uncalled-fns) (plist-worldp wrld)))) (let ((__function__ 'atc-process-target-list)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil nil nil) ((when (endp targets)) (retok nil previous-structs previous-objs previous-fns uncalled-fns)) ((erp target previous-structs previous-objs previous-fns uncalled-fns) (atc-process-target (car targets) previous-structs previous-objs previous-fns uncalled-fns wrld)) ((erp targets previous-structs previous-objs previous-fns uncalled-fns) (atc-process-target-list (cdr targets) previous-structs previous-objs previous-fns uncalled-fns wrld))) (retok (cons target targets) previous-structs previous-objs previous-fns uncalled-fns))))
Theorem:
(defthm symbol-listp-of-atc-process-target-list.targets (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (symbol-listp targets)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-process-target-list.new-previous-structs (implies (symbol-listp previous-structs) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (symbol-listp new-previous-structs))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-process-target-list.new-previous-objs (implies (symbol-listp previous-objs) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (symbol-listp new-previous-objs))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-process-target-list.new-previous-fns (implies (symbol-listp previous-fns) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (symbol-listp new-previous-fns))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-process-target-list.new-uncalled-fns (implies (symbol-listp uncalled-fns) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (symbol-listp new-uncalled-fns))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-atc-process-target-list.new-previous-structs (implies (true-listp previous-structs) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (true-listp new-previous-structs))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-atc-process-target-list.new-previous-objs (implies (true-listp previous-objs) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (true-listp new-previous-objs))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-atc-process-target-list.new-previous-fns (implies (true-listp previous-fns) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (true-listp new-previous-fns))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-atc-process-target-list.new-uncalled-fns (implies (true-listp uncalled-fns) (b* (((mv acl2::?erp ?targets ?new-previous-structs ?new-previous-objs ?new-previous-fns ?new-uncalled-fns) (atc-process-target-list targets previous-structs previous-objs previous-fns uncalled-fns wrld))) (true-listp new-uncalled-fns))) :rule-classes :type-prescription)