Filtering...

forcing-types

books/arithmetic-5/lib/basic-ops/forcing-types

Included Books

building-blocks
other
(in-package "ACL2")
include-book
(include-book "building-blocks")
default-plus-1theorem
(defthm default-plus-1
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (+ x y)
      (if (acl2-numberp x)
        (+ x y)
        (if (acl2-numberp y)
          y
          0)))))
default-plus-2theorem
(defthm default-plus-2
  (implies (syntaxp (not (proveably-acl2-numberp 'y `((y . ,Y)) mfc state)))
    (equal (+ x y)
      (if (acl2-numberp y)
        (+ x y)
        (if (acl2-numberp x)
          x
          0)))))
default-minustheorem
(defthm default-minus
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (- x)
      (if (acl2-numberp x)
        (- x)
        0))))
default-times-1theorem
(defthm default-times-1
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (* x y)
      (if (acl2-numberp x)
        (* x y)
        0))))
default-times-2theorem
(defthm default-times-2
  (implies (syntaxp (not (proveably-acl2-numberp 'y `((y . ,Y)) mfc state)))
    (equal (* x y)
      (if (acl2-numberp y)
        (* x y)
        0))))
default-dividetheorem
(defthm default-divide
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (/ x)
      (if (acl2-numberp x)
        (/ x)
        0))))
default-rational-denominatortheorem
(defthm default-rational-denominator
  (implies (syntaxp (not (proveably-rational 'x `((x . ,X)) mfc state)))
    (equal (denominator x)
      (if (rationalp x)
        (denominator x)
        1))))
default-rational-numeratortheorem
(defthm default-rational-numerator
  (implies (syntaxp (not (proveably-rational 'x `((x . ,X)) mfc state)))
    (equal (numerator x)
      (if (rationalp x)
        (numerator x)
        0))))
default-less-than-1theorem
(defthm default-less-than-1
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (< x y)
      (if (acl2-numberp x)
        (< x y)
        (< 0 y)))))
default-less-than-2theorem
(defthm default-less-than-2
  (implies (syntaxp (not (proveably-acl2-numberp 'y `((y . ,Y)) mfc state)))
    (equal (< x y)
      (if (acl2-numberp y)
        (< x y)
        (< x 0)))))
default-expt-1theorem
(defthm default-expt-1
  (implies (syntaxp (not (proveably-acl2-numberp 'x `((x . ,X)) mfc state)))
    (equal (expt x n)
      (if (acl2-numberp x)
        (expt x n)
        (if (zip n)
          1
          0)))))
default-expt-2theorem
(defthm default-expt-2
  (implies (syntaxp (not (proveably-integer 'n `((n . ,N)) mfc state)))
    (equal (expt x n)
      (if (integerp n)
        (expt x n)
        1))))