Measure for recurring over type structures.
Function:
(defun type-count (x) (declare (xargs :guard (typep x))) (let ((__function__ 'type-count)) (declare (ignorable __function__)) (case (type-kind x) (:boolean 1) (:character 1) (:string 1) (:integer 1) (:set (+ 2 (type-count (type-set->element x)))) (:sequence (+ 2 (type-count (type-sequence->element x)))) (:map (+ 3 (type-count (type-map->domain x)) (type-count (type-map->range x)))) (:option (+ 2 (type-count (type-option->base x)))) (:defined 1))))
Theorem:
(defthm natp-of-type-count (b* ((count (type-count x))) (natp count)) :rule-classes :type-prescription)
Theorem:
(defthm type-count-of-type-fix-x (equal (type-count (type-fix x)) (type-count x)))
Theorem:
(defthm type-count-type-equiv-congruence-on-x (implies (type-equiv x x-equiv) (equal (type-count x) (type-count x-equiv))) :rule-classes :congruence)
Theorem:
(defthm type-count-of-type-set (implies t (< (+ (type-count element)) (type-count (type-set element)))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-set->element (implies (equal (type-kind x) :set) (< (type-count (type-set->element x)) (type-count x))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-sequence (implies t (< (+ (type-count element)) (type-count (type-sequence element)))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-sequence->element (implies (equal (type-kind x) :sequence) (< (type-count (type-sequence->element x)) (type-count x))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-map (implies t (< (+ (type-count domain) (type-count range)) (type-count (type-map domain range)))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-map->domain (implies (equal (type-kind x) :map) (< (type-count (type-map->domain x)) (type-count x))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-map->range (implies (equal (type-kind x) :map) (< (type-count (type-map->range x)) (type-count x))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-option (implies t (< (+ (type-count base)) (type-count (type-option base)))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-option->base (implies (equal (type-kind x) :option) (< (type-count (type-option->base x)) (type-count x))) :rule-classes :linear)