Event to generate operations on pointed integers of a given type.
(def-pointed-integer-operations type) → event
The enabled return type theorem for each writer has the star wrapper, because this is the kind of rule we want enabled for more strictly typed reasoning. We also add a disabled return type theorem without the wrapper, which may be useful for other purposes, namely when the star wrapper is enabled.
Function:
(defun def-pointed-integer-operations (type) (declare (xargs :guard (typep type))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'def-pointed-integer-operations)) (declare (ignorable __function__)) (b* ((type-string (integer-type-xdoc-string type)) (<type> (integer-type-to-fixtype type)) (<type>p (pack <type> 'p)) (<type>-fix (pack <type> '-fix)) (<type>-read (pack <type> '-read)) (<type>-write (pack <type> '-write)) (<type>p-of-<type>-write (pack <type> 'p-of- <type> '-write))) (cons 'progn (cons (cons 'define (cons <type>-read (cons (cons (cons 'x (cons (cons 'star (cons (cons <type>p '(x)) 'nil)) 'nil)) 'nil) (cons ':returns (cons (cons 'x (cons <type>p 'nil)) (cons ':short (cons (str::cat "Representation of a read of a pointed " type-string ".") (cons (cons <type>-fix '(x)) '(:prepwork ((local (in-theory (enable star)))) :hooks (:fix)))))))))) (cons (cons 'define (cons <type>-write (cons (cons (cons 'x (cons <type>p 'nil)) 'nil) (cons ':returns (cons (cons 'x (cons (cons 'star (cons (cons <type>p '(x)) 'nil)) 'nil)) (cons ':short (cons (str::cat "Representation of a write of a pointed " type-string ".") (cons (cons <type>-fix '(x)) (cons ':prepwork (cons '((local (in-theory (enable star)))) (cons ':hooks (cons '(:fix) (cons '/// (cons (cons 'more-returns (cons (cons 'x (cons <type>p 'nil)) 'nil)) (cons (cons 'in-theory (cons (cons 'disable (cons <type>p-of-<type>-write 'nil)) 'nil)) 'nil))))))))))))))) 'nil))))))
Theorem:
(defthm pseudo-event-formp-of-def-pointed-integer-operations (b* ((event (def-pointed-integer-operations type))) (pseudo-event-formp event)) :rule-classes :rewrite)
Theorem:
(defthm def-pointed-integer-operations-of-type-fix-type (equal (def-pointed-integer-operations (type-fix type)) (def-pointed-integer-operations type)))
Theorem:
(defthm def-pointed-integer-operations-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (def-pointed-integer-operations type) (def-pointed-integer-operations type-equiv))) :rule-classes :congruence)