realpart - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "complex"))

local

(local (include-book "imagpart"))

realpart-when-rationalptheorem

(defthm realpart-when-rationalp
  (implies (real/rationalp x) (equal (realpart x) x)))

realpart-redeftheorem

(defthmd realpart-redef
  (equal (realpart x) (- x (* #C(0 1) (imagpart x))))
  :hints (("Goal" :use realpart-imagpart-elim)))

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)))))

realpart-of--theorem

(defthm realpart-of--
  (equal (realpart (- x)) (- (realpart 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)))))))))

realpart-of-*-of-itheorem

(defthm realpart-of-*-of-i
  (implies (real/rationalp x)
    (equal (realpart (* #C(0 1) x)) 0))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (enable realpart-redef))))

realpart-of-*-when-rationalp-arg1theorem

(defthm realpart-of-*-when-rationalp-arg1
  (implies (real/rationalp x)
    (equal (realpart (* x y)) (* x (realpart y))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :use ((:instance complex-split (x y))))))

realpart-of-*-when-rationalp-arg2theorem

(defthm realpart-of-*-when-rationalp-arg2
  (implies (real/rationalp y)
    (equal (realpart (* x y)) (* y (realpart x))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (disable realpart-of-*-when-rationalp-arg1)
     :use ((:instance realpart-of-*-when-rationalp-arg1 (x y) (y x))))))