Mutually recursive functions that check the absence of function definitions in statements, blocks, cases, and function definitions.
Function:
(defun statement-nofunp (stmt) (declare (xargs :guard (statementp stmt))) (let ((__function__ 'statement-nofunp)) (declare (ignorable __function__)) (statement-case stmt :block (block-nofunp stmt.get) :variable-single t :variable-multi t :assign-single t :assign-multi t :funcall t :if (block-nofunp stmt.body) :for (and (block-nofunp stmt.init) (block-nofunp stmt.update) (block-nofunp stmt.body)) :switch (and (swcase-list-nofunp stmt.cases) (block-option-nofunp stmt.default)) :leave t :break t :continue t :fundef nil)))
Function:
(defun statement-list-nofunp (stmts) (declare (xargs :guard (statement-listp stmts))) (let ((__function__ 'statement-list-nofunp)) (declare (ignorable __function__)) (or (endp stmts) (and (statement-nofunp (car stmts)) (statement-list-nofunp (cdr stmts))))))
Function:
(defun block-nofunp (block) (declare (xargs :guard (blockp block))) (let ((__function__ 'block-nofunp)) (declare (ignorable __function__)) (statement-list-nofunp (block->statements block))))
Function:
(defun block-option-nofunp (block?) (declare (xargs :guard (block-optionp block?))) (let ((__function__ 'block-option-nofunp)) (declare (ignorable __function__)) (block-option-case block? :some (block-nofunp block?.val) :none t)))
Function:
(defun swcase-nofunp (case) (declare (xargs :guard (swcasep case))) (let ((__function__ 'swcase-nofunp)) (declare (ignorable __function__)) (block-nofunp (swcase->body case))))
Function:
(defun swcase-list-nofunp (cases) (declare (xargs :guard (swcase-listp cases))) (let ((__function__ 'swcase-list-nofunp)) (declare (ignorable __function__)) (or (endp cases) (and (swcase-nofunp (car cases)) (swcase-list-nofunp (cdr cases))))))
Function:
(defun fundef-nofunp (fundef) (declare (xargs :guard (fundefp fundef))) (let ((__function__ 'fundef-nofunp)) (declare (ignorable __function__)) (block-nofunp (fundef->body fundef))))
Theorem:
(defthm return-type-of-statement-nofunp.yes/no (b* ((?yes/no (statement-nofunp stmt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-statement-list-nofunp.yes/no (b* ((?yes/no (statement-list-nofunp stmts))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-nofunp.yes/no (b* ((?yes/no (block-nofunp block))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-option-nofunp.yes/no (b* ((?yes/no (block-option-nofunp block?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-nofunp.yes/no (b* ((?yes/no (swcase-nofunp case))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-list-nofunp.yes/no (b* ((?yes/no (swcase-list-nofunp cases))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-fundef-nofunp.yes/no (b* ((?yes/no (fundef-nofunp fundef))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm statement-nofunp-of-statement-fix-stmt (equal (statement-nofunp (statement-fix stmt)) (statement-nofunp stmt)))
Theorem:
(defthm statement-list-nofunp-of-statement-list-fix-stmts (equal (statement-list-nofunp (statement-list-fix stmts)) (statement-list-nofunp stmts)))
Theorem:
(defthm block-nofunp-of-block-fix-block (equal (block-nofunp (block-fix block)) (block-nofunp block)))
Theorem:
(defthm block-option-nofunp-of-block-option-fix-block? (equal (block-option-nofunp (block-option-fix block?)) (block-option-nofunp block?)))
Theorem:
(defthm swcase-nofunp-of-swcase-fix-case (equal (swcase-nofunp (swcase-fix case)) (swcase-nofunp case)))
Theorem:
(defthm swcase-list-nofunp-of-swcase-list-fix-cases (equal (swcase-list-nofunp (swcase-list-fix cases)) (swcase-list-nofunp cases)))
Theorem:
(defthm fundef-nofunp-of-fundef-fix-fundef (equal (fundef-nofunp (fundef-fix fundef)) (fundef-nofunp fundef)))
Theorem:
(defthm statement-nofunp-statement-equiv-congruence-on-stmt (implies (statement-equiv stmt stmt-equiv) (equal (statement-nofunp stmt) (statement-nofunp stmt-equiv))) :rule-classes :congruence)
Theorem:
(defthm statement-list-nofunp-statement-list-equiv-congruence-on-stmts (implies (statement-list-equiv stmts stmts-equiv) (equal (statement-list-nofunp stmts) (statement-list-nofunp stmts-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-nofunp-block-equiv-congruence-on-block (implies (block-equiv block block-equiv) (equal (block-nofunp block) (block-nofunp block-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-option-nofunp-block-option-equiv-congruence-on-block? (implies (block-option-equiv block? block?-equiv) (equal (block-option-nofunp block?) (block-option-nofunp block?-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-nofunp-swcase-equiv-congruence-on-case (implies (swcase-equiv case case-equiv) (equal (swcase-nofunp case) (swcase-nofunp case-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-nofunp-swcase-list-equiv-congruence-on-cases (implies (swcase-list-equiv cases cases-equiv) (equal (swcase-list-nofunp cases) (swcase-list-nofunp cases-equiv))) :rule-classes :congruence)
Theorem:
(defthm fundef-nofunp-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (fundef-nofunp fundef) (fundef-nofunp fundef-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-option-nofunp-when-blockp (implies (blockp block) (equal (block-option-nofunp block) (block-nofunp block))))