Lift check-type-definition-in-recursion to lists.
(check-type-definition-list-in-recursion typedefs ctxt) → (mv err? obligs)
Accumulate all the proof obligations.
Function:
(defun check-type-definition-list-in-recursion (typedefs ctxt) (declare (xargs :guard (and (type-definition-listp typedefs) (contextp ctxt)))) (declare (xargs :guard (and (subsetp-equal (type-definition-list->name-list typedefs) (context->types ctxt)) (null (context->functions ctxt)) (omap::emptyp (context->variables ctxt)) (null (context->obligation-vars ctxt)) (null (context->obligation-hyps ctxt))))) (let ((__function__ 'check-type-definition-list-in-recursion)) (declare (ignorable __function__)) (b* (((when (endp typedefs)) (mv nil nil)) ((mv err? obligs) (check-type-definition-in-recursion (car typedefs) ctxt)) ((when err?) (mv err? nil)) ((mv err? more-obligs) (check-type-definition-list-in-recursion (cdr typedefs) ctxt)) ((when err?) (mv err? nil))) (mv nil (append obligs more-obligs)))))
Theorem:
(defthm proof-obligation-listp-of-check-type-definition-list-in-recursion.obligs (b* (((mv ?err? ?obligs) (check-type-definition-list-in-recursion typedefs ctxt))) (proof-obligation-listp obligs)) :rule-classes :rewrite)
Theorem:
(defthm check-type-definition-list-in-recursion-of-type-definition-list-fix-typedefs (equal (check-type-definition-list-in-recursion (type-definition-list-fix typedefs) ctxt) (check-type-definition-list-in-recursion typedefs ctxt)))
Theorem:
(defthm check-type-definition-list-in-recursion-type-definition-list-equiv-congruence-on-typedefs (implies (type-definition-list-equiv typedefs typedefs-equiv) (equal (check-type-definition-list-in-recursion typedefs ctxt) (check-type-definition-list-in-recursion typedefs-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-type-definition-list-in-recursion-of-context-fix-ctxt (equal (check-type-definition-list-in-recursion typedefs (context-fix ctxt)) (check-type-definition-list-in-recursion typedefs ctxt)))
Theorem:
(defthm check-type-definition-list-in-recursion-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-type-definition-list-in-recursion typedefs ctxt) (check-type-definition-list-in-recursion typedefs ctxt-equiv))) :rule-classes :congruence)