integer-type-set-test

other

(in-package "ACL2")

foo-thmencapsulate

(encapsulate ((foo (x) t))
  (local (defun foo (x) x))
  (defthm foo-thm (implies x (foo x))))

other

(set-backchain-limit 0)

lemma-1theorem

(defthm lemma-1
  (implies (and (rationalp x) (integerp (* 1/2 x)))
    (foo (integerp x)))
  :rule-classes nil)

lemma-2theorem

(defthm lemma-2
  (implies (and (rationalp x) (integerp (* 2 x)))
    (foo (integerp (* 4 x))))
  :rule-classes nil)

lemma-3theorem

(defthm lemma-3
  (implies (and (rationalp x) (integerp (* 2 x)))
    (foo (integerp (+ -1 (* 4 x)))))
  :rule-classes nil)

lemma-4theorem

(defthm lemma-4
  (implies (and (rationalp x) (integerp (+ 1 x)))
    (foo (integerp (+ 2 x))))
  :rule-classes nil)

lemma-5theorem

(defthm lemma-5
  (implies (and (rationalp x) (integerp (+ 1 x)))
    (foo (integerp x)))
  :rule-classes nil)

lemma-6theorem

(defthm lemma-6
  (implies (and (rationalp x) (integerp (+ -1/2 x)))
    (foo (integerp (+ 1/2 x))))
  :rule-classes nil)

lemma-7theorem

(defthm lemma-7
  (implies (and (rationalp x) (integerp (* 2 x)))
    (foo (not (integerp (+ 1/2 (* 4 x))))))
  :rule-classes nil)

not-integerpfunction

(defun not-integerp (x) (not (integerp x)))

not-integerp-implies-not-integerptheorem

(defthm not-integerp-implies-not-integerp
  (implies (not (integerp x)) (not-integerp x)))

in-theory

(in-theory (disable not-integerp))

lemma-8theorem

(defthm lemma-8
  (implies (and (rationalp x) (integerp (+ 1/2 x)))
    (foo (not-integerp x)))
  :rule-classes nil)