Filtering...

imagpart

books/kestrel/arithmetic-light/imagpart

Included Books

complex plus-and-minus minus
other
(in-package "ACL2")
local
(local (include-book "complex"))
local
(local (include-book "plus-and-minus"))
local
(local (include-book "minus"))
imagpart-when-rationalptheorem
(defthm imagpart-when-rationalp
  (implies (real/rationalp x) (equal (imagpart x) 0)))
local
(local (defthm complex-split
    (implies (acl2-numberp x)
      (equal (+ (realpart x) (* #C(0 1) (imagpart x))) x))
    :rule-classes nil
    :hints (("Goal" :use realpart-imagpart-elim))))
local
(local (defthmd --becomes-*-of--1 (equal (- x) (* -1 x))))
local
(local (defthm commutativity-2-of-*
    (equal (* x (* y z)) (* y (* x z)))
    :hints (("Goal" :use ((:instance associativity-of-*) (:instance associativity-of-* (x y) (y x)))
       :in-theory (disable associativity-of-*)))))
local
(local (defthm *-of---arg2
    (equal (* x (- y)) (- (* x y)))
    :hints (("Goal" :in-theory (enable --becomes-*-of--1)))))
imagpart-of--theorem
(defthm imagpart-of--
  (equal (imagpart (- x)) (- (imagpart x)))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :use ((:instance complex-split) (:instance complex-split (x (- x)))
       (:instance complex-equal
         (x1 (realpart x))
         (y1 (imagpart x))
         (x2 (- (realpart (- x))))
         (y2 (- (imagpart (- x)))))))))
imagpart-of-*-of-itheorem
(defthm imagpart-of-*-of-i
  (implies (real/rationalp x)
    (equal (imagpart (* #C(0 1) x)) x))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (disable complex-opener imagpart-complex)
     :use ((:instance imagpart-complex (y x)) (:instance complex-definition (y x))))))
imagpart-of-*-when-rationalp-arg1theorem
(defthm imagpart-of-*-when-rationalp-arg1
  (implies (real/rationalp x)
    (equal (imagpart (* x y)) (* x (imagpart y))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :use ((:instance complex-split (x y))))))
imagpart-of-*-when-rationalp-arg2theorem
(defthm imagpart-of-*-when-rationalp-arg2
  (implies (real/rationalp y)
    (equal (imagpart (* x y)) (* y (imagpart x))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (disable imagpart-of-*-when-rationalp-arg1)
     :use (:instance imagpart-of-*-when-rationalp-arg1 (x y) (y x)))))