Number of
This is useful as a measure for certain recursive functions.
We prove some theorems about the results of these counting functions. Additional similar theorems could be added as needed.
Function:
(defun jstatem-count-ifs (statem) (declare (xargs :guard (jstatemp statem))) (let ((__function__ 'jstatem-count-ifs)) (declare (ignorable __function__)) (jstatem-case statem :locvar 0 :expr 0 :return 0 :throw 0 :break 0 :continue 0 :if (1+ (jblock-count-ifs statem.then)) :ifelse (1+ (+ (jblock-count-ifs statem.then) (jblock-count-ifs statem.else))) :while (jblock-count-ifs statem.body) :do (jblock-count-ifs statem.body) :for (jblock-count-ifs statem.body))))
Function:
(defun jblock-count-ifs (block) (declare (xargs :guard (jblockp block))) (let ((__function__ 'jblock-count-ifs)) (declare (ignorable __function__)) (cond ((endp block) 0) (t (+ (jstatem-count-ifs (car block)) (jblock-count-ifs (cdr block)))))))
Theorem:
(defthm return-type-of-jstatem-count-ifs.count (b* ((common-lisp::?count (jstatem-count-ifs statem))) (natp count)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-jblock-count-ifs.count (b* ((common-lisp::?count (jblock-count-ifs block))) (natp count)) :rule-classes :rewrite)
Theorem:
(defthm jblock-count-ifs-of-cons (equal (jblock-count-ifs (cons statem block)) (+ (jstatem-count-ifs statem) (jblock-count-ifs block))))
Theorem:
(defthm jblock-count-ifs-of-append (equal (jblock-count-ifs (append block1 block2)) (+ (jblock-count-ifs block1) (jblock-count-ifs block2))))
Theorem:
(defthm jstatem-count-ifs-of-return (equal (jstatem-count-ifs (jstatem-return expr?)) 0))
Theorem:
(defthm jblock-count-ifs-of-jstatem-if->then-decreases (implies (jstatem-case statem :if) (< (jblock-count-ifs (jstatem-if->then statem)) (jstatem-count-ifs statem))) :rule-classes :linear)
Theorem:
(defthm jblock-count-ifs-of-jstatem-ifelse->then-decreases (implies (jstatem-case statem :ifelse) (< (jblock-count-ifs (jstatem-ifelse->then statem)) (jstatem-count-ifs statem))) :rule-classes :linear)
Theorem:
(defthm jblock-count-ifs-of-jstatem-ifelse->else-decreases (implies (jstatem-case statem :ifelse) (< (jblock-count-ifs (jstatem-ifelse->else statem)) (jstatem-count-ifs statem))) :rule-classes :linear)
Theorem:
(defthm jblock-count-ifs-of-take-not-increases (<= (jblock-count-ifs (take n block)) (jblock-count-ifs block)) :rule-classes :linear)
Theorem:
(defthm jblock-count-ifs-of-nthcdr-not-increases (<= (jblock-count-ifs (nthcdr n block)) (jblock-count-ifs block)) :rule-classes :linear)
Theorem:
(defthm jstatem-count-ifs-of-car-not-increases (<= (jstatem-count-ifs (car block)) (jblock-count-ifs block)) :rule-classes :linear)
Theorem:
(defthm jblock-count-ifs-of-cdr-not-increases (<= (jblock-count-ifs (cdr block)) (jblock-count-ifs block)) :rule-classes :linear)
Theorem:
(defthm jblock-count-ifs-positive-when-nth-ifelse (implies (jstatem-case (nth i block) :ifelse) (> (jblock-count-ifs block) 0)) :rule-classes :linear)