Event form to introduce additional return type theorems for the conversions from natural numbers to digits.
(defthm-dab-return-types-fn eq-thm-name prefix topic topicp parents parentsp short shortp long longp wrld) → event
Function:
(defun defthm-dab-return-types-fn (eq-thm-name prefix topic topicp parents parentsp short shortp long longp wrld) (declare (xargs :guard (and (symbolp eq-thm-name) (symbolp prefix) (symbolp topic) (booleanp topicp) (symbol-listp parents) (booleanp parentsp) (stringp short) (booleanp shortp) (stringp long) (booleanp longp) (plist-worldp wrld)))) (let ((__function__ 'defthm-dab-return-types-fn)) (declare (ignorable __function__)) (b* ((equality (formula eq-thm-name nil wrld)) (dab-digit-listp-call (cadr equality)) (base (cadr dab-digit-listp-call)) (var (caddr dab-digit-listp-call)) (term (caddr equality)) (nat=>bendian*-thm-name (packn (list prefix '-nat=>bendian*))) (nat=>bendian+-thm-name (packn (list prefix '-nat=>bendian+))) (nat=>bendian-thm-name (packn (list prefix '-nat=>bendian))) (nat=>lendian*-thm-name (packn (list prefix '-nat=>lendian*))) (nat=>lendian+-thm-name (packn (list prefix '-nat=>lendian+))) (nat=>lendian-thm-name (packn (list prefix '-nat=>lendian))) (nat=>bendian*-call (fcons-term* 'nat=>bendian* base 'nat)) (nat=>bendian+-call (fcons-term* 'nat=>bendian+ base 'nat)) (nat=>bendian-call (fcons-term* 'nat=>bendian base 'width 'nat)) (nat=>lendian*-call (fcons-term* 'nat=>lendian* base 'nat)) (nat=>lendian+-call (fcons-term* 'nat=>lendian+ base 'nat)) (nat=>lendian-call (fcons-term* 'nat=>lendian base 'width 'nat)) (nat=>bendian*-term (fsubcor-var (list var) (list nat=>bendian*-call) term)) (nat=>bendian+-term (fsubcor-var (list var) (list nat=>bendian+-call) term)) (nat=>bendian-term (fsubcor-var (list var) (list nat=>bendian-call) term)) (nat=>lendian*-term (fsubcor-var (list var) (list nat=>lendian*-call) term)) (nat=>lendian+-term (fsubcor-var (list var) (list nat=>lendian+-call) term)) (nat=>lendian-term (fsubcor-var (list var) (list nat=>lendian-call) term)) (theorems (cons (cons 'defthm (cons nat=>bendian*-thm-name (cons (untranslate nat=>bendian*-term t wrld) (cons ':hints (cons (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons 'return-type-of-nat=>bendian* (cons (cons 'base (cons base 'nil)) 'nil))) (cons (cons ':instance (cons eq-thm-name (cons (cons var (cons nat=>bendian*-call 'nil)) 'nil))) 'nil)) '(:in-theory nil)))) 'nil) 'nil))))) (cons (cons 'defthm (cons nat=>bendian+-thm-name (cons (untranslate nat=>bendian+-term t wrld) (cons ':hints (cons (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons 'return-type-of-nat=>bendian+ (cons (cons 'base (cons base 'nil)) 'nil))) (cons (cons ':instance (cons eq-thm-name (cons (cons var (cons nat=>bendian+-call 'nil)) 'nil))) 'nil)) '(:in-theory nil)))) 'nil) 'nil))))) (cons (cons 'defthm (cons nat=>bendian-thm-name (cons (untranslate nat=>bendian-term t wrld) (cons ':hints (cons (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons 'return-type-of-nat=>bendian (cons (cons 'base (cons base 'nil)) 'nil))) (cons (cons ':instance (cons eq-thm-name (cons (cons var (cons nat=>bendian-call 'nil)) 'nil))) 'nil)) '(:in-theory nil)))) 'nil) 'nil))))) (cons (cons 'defthm (cons nat=>lendian*-thm-name (cons (untranslate nat=>lendian*-term t wrld) (cons ':hints (cons (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons 'return-type-of-nat=>lendian* (cons (cons 'base (cons base 'nil)) 'nil))) (cons (cons ':instance (cons eq-thm-name (cons (cons var (cons nat=>lendian*-call 'nil)) 'nil))) 'nil)) '(:in-theory nil)))) 'nil) 'nil))))) (cons (cons 'defthm (cons nat=>lendian+-thm-name (cons (untranslate nat=>lendian+-term t wrld) (cons ':hints (cons (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons 'return-type-of-nat=>lendian+ (cons (cons 'base (cons base 'nil)) 'nil))) (cons (cons ':instance (cons eq-thm-name (cons (cons var (cons nat=>lendian+-call 'nil)) 'nil))) 'nil)) '(:in-theory nil)))) 'nil) 'nil))))) (cons (cons 'defthm (cons nat=>lendian-thm-name (cons (untranslate nat=>lendian-term t wrld) (cons ':hints (cons (cons (cons '"Goal" (cons ':use (cons (cons (cons ':instance (cons 'return-type-of-nat=>lendian (cons (cons 'base (cons base 'nil)) 'nil))) (cons (cons ':instance (cons eq-thm-name (cons (cons var (cons nat=>lendian-call 'nil)) 'nil))) 'nil)) '(:in-theory nil)))) 'nil) 'nil))))) 'nil)))))))) (if topicp (cons 'defsection (cons topic (append (and parentsp (list :parents parents)) (append (and shortp (list :short short)) (append (and longp (list :long long)) theorems))))) (cons 'encapsulate (cons 'nil theorems))))))