		Search-engine friendly clone of the ACL2 documentation.
Defbyte-ihs-theorems-implementation
Defbyte-ihs-theorems-fn

Event generated by defbyte-ihs-theorems.
Signature
(defbyte-ihs-theorems-fn type wrld) → event
Arguments: wrld — Guard (plist-worldp wrld).
Returns: event — A ACL2::pseudo-event-formp.
Definitions and Theorems

Function: defbyte-ihs-theorems-fn
(defun defbyte-ihs-theorems-fn (type wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defbyte-ihs-theorems-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp type))
     (raise
      "The TYPE input must be a symbol, ~
                but it is ~x0 instead."
      type))
    (defbyte-table (table-alist *defbyte-table-name* wrld))
    (defbyte-pair (assoc-eq type defbyte-table))
    ((unless defbyte-pair)
     (raise
      "The TYPE input ~x0 must name a type ~
                previously introduced via DEFBYTE, ~
                but this is not the case."
      type))
    (defbyte-info (cdr defbyte-pair))
    (size (defbyte-info->size defbyte-info))
    (signed (defbyte-info->signed defbyte-info))
    (fty-table (get-fixtypes-alist wrld))
    (fty-info (find-fixtype type fty-table))
    (bytep (fixtype->pred fty-info))
    (loghead/logext (if signed 'logext 'loghead))
    (type-ihs-theorems (acl2::packn-pos (list type '-ihs-theorems)
                                        bytep))
    (short (cat "Theorems about @(tsee acl2::"
                (str::downcase-string (symbol-name type))
                ") and IHS functions."))
    (bytep-of-loghead/logext-of-size
         (acl2::packn-pos (list bytep '-of-
                                loghead/logext '-of-
                                size)
                          bytep))
    (loghead/logext-of-size-when-bytep
         (acl2::packn-pos (list loghead/logext '-of-
                                size '-when-
                                bytep)
                          bytep))
    (logtail-of-size-when-bytep
         (acl2::packn-pos (list 'logtail-of- size '-when- bytep)
                          bytep))
    (x (intern-in-package-of-symbol "X" bytep))
    (event
     (cons
      'defsection
      (cons
       type-ihs-theorems
       (cons
        ':parents
        (cons
         (cons type
               '(defbyte-standard-instances-ihs-theorems))
         (cons
          ':short
          (cons
           short
           (cons
            '(local (include-book "arithmetic-5/top"
                                  :dir :system))
            (cons
             (cons
              'defrule
              (cons
                  bytep-of-loghead/logext-of-size
                  (cons (cons bytep
                              (cons (cons loghead/logext
                                          (cons size (cons x 'nil)))
                                    'nil))
                        (cons ':enable (cons bytep 'nil)))))
             (cons
              (cons
               'defrule
               (cons
                loghead/logext-of-size-when-bytep
                (cons
                 (cons
                  'implies
                  (cons
                   (cons bytep (cons x 'nil))
                   (cons
                        (cons 'equal
                              (cons (cons loghead/logext
                                          (cons size (cons x 'nil)))
                                    (cons x 'nil)))
                        'nil)))
                 (cons ':enable (cons bytep 'nil)))))
              (cons
               (cons
                'defrule
                (cons
                 logtail-of-size-when-bytep
                 (cons
                  (cons
                   'implies
                   (cons
                    (cons bytep (cons x 'nil))
                    (cons
                     (cons
                      'equal
                      (cons
                       (cons 'logtail
                             (cons size (cons x 'nil)))
                       (cons
                        (if signed
                         (cons
                             'if
                             (cons (cons '< (cons x '(0))) '(-1 0)))
                         0)
                        'nil)))
                     'nil)))
                  (cons ':enable (cons bytep 'nil)))))
               'nil))))))))))))
   event)))