Filtering...

forcing-types

books/arithmetic-5/lib/floor-mod/forcing-types

Included Books

building-blocks
other
(in-package "ACL2")
include-book
(include-book "../basic-ops/building-blocks")
default-floor-ratiotheorem
(defthm default-floor-ratio
  (implies (syntaxp (not (proveably-real/rational '(binary-* x (unary-/ y))
          `((x . ,X) (y . ,Y))
          mfc
          state)))
    (equal (floor x y)
      (if (real/rationalp (/ x y))
        (floor x y)
        0))))
default-floor-1theorem
(defthm default-floor-1
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (floor x y)
      (if (acl2-numberp x)
        (floor x y)
        0))))
default-floor-2theorem
(defthm default-floor-2
  (implies (syntaxp (not (proveably-acl2-numberp 'y `((y . ,Y)) mfc state)))
    (equal (floor x y)
      (if (acl2-numberp y)
        (floor x y)
        0))))
default-mod-ratiotheorem
(defthm default-mod-ratio
  (implies (syntaxp (not (proveably-real/rational '(binary-* x (unary-/ y))
          `((x . ,X) (y . ,Y))
          mfc
          state)))
    (equal (mod x y)
      (if (real/rationalp (/ x y))
        (mod x y)
        (if (acl2-numberp x)
          x
          0)))))
default-mod-1theorem
(defthm default-mod-1
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (mod x y)
      (if (acl2-numberp x)
        (mod x y)
        0))))
default-mod-2theorem
(defthm default-mod-2
  (implies (syntaxp (not (proveably-acl2-numberp 'y `((y . ,Y)) mfc state)))
    (equal (mod x y)
      (if (acl2-numberp y)
        (mod x y)
        (if (acl2-numberp x)
          x
          0)))))
default-logand-1theorem
(defthm default-logand-1
  (implies (syntaxp (not (proveably-integer 'x `((x . ,X)) mfc state)))
    (equal (logand x y)
      (if (integerp x)
        (logand x y)
        0))))
default-logand-2theorem
(defthm default-logand-2
  (implies (syntaxp (not (proveably-integer 'y `((y . ,Y)) mfc state)))
    (equal (logand x y)
      (if (integerp y)
        (logand x y)
        0))))
default-logior-1theorem
(defthm default-logior-1
  (implies (syntaxp (not (proveably-integer 'x `((x . ,X)) mfc state)))
    (equal (logior x y)
      (if (integerp x)
        (logior x y)
        (logior 0 y)))))
default-logior-2theorem
(defthm default-logior-2
  (implies (syntaxp (not (proveably-integer 'y `((y . ,Y)) mfc state)))
    (equal (logior x y)
      (if (integerp y)
        (logior x y)
        (logior x 0)))))
default-logxor-1theorem
(defthm default-logxor-1
  (implies (syntaxp (not (proveably-integer 'x `((x . ,X)) mfc state)))
    (equal (logxor x y)
      (if (integerp x)
        (logxor x y)
        (logxor 0 y)))))
default-logxor-2theorem
(defthm default-logxor-2
  (implies (syntaxp (not (proveably-integer 'y `((y . ,Y)) mfc state)))
    (equal (logxor x y)
      (if (integerp y)
        (logxor x y)
        (logxor x 0)))))
default-lognottheorem
(defthm default-lognot
  (implies (syntaxp (not (proveably-integer 'x `((x . ,X)) mfc state)))
    (equal (lognot x)
      (if (integerp x)
        (lognot x)
        -1))))