(in-package "ACL2")

(encapsulate 
 () ;we're not constraining any function symbols
 (defun foo (x) x)
 (defthm foo-idempotent
   (equal (foo (foo x))
          (foo x))))

(defthm foo-test
  (equal (foo (foo (foo x)))
         (foo x)))

(encapsulate 
 (
  ((bar *) => *)
  ) ;we're constraining the function symbol BAR
 (local (defun bar (x) x))
 (defthm bar-idempotent
   (equal (bar (bar x))
          (bar x))))

(defthm bar-test
  (equal (bar (bar (bar x)))
         (bar x)))

(encapsulate (((negate *) => *)
              ((pred *) => *)
              ) ;we're constraining the function symbols NEGATE and PRED
             
             (local (defun negate (x) x))

             (local (defun pred (x) 
                      (declare (ignore x))
                      t))

             (defthm negate-twice
               (implies (pred x)
                        (equal (negate (negate x))
                               x))))

;using encapsulate just lets me hide the helper lemma HACK
(encapsulate ()
             (local (defthm hack
                      (implies (and (equal (negate (negate x)) (negate (negate y)))
                                    (pred x)
                                    (pred y))
                               (equal (equal x y)
                                      t))))

             (defthm cancel-negations
               (implies (and (pred x) (pred y))
                        (equal (equal (negate x) (negate y))
                               (equal x y)))))
           
(defun my-negate (x)
  (- x))

(defthm my-negate-twice
  (implies (rationalp x)
           (equal (my-negate (my-negate x))
                  x)))

(in-theory (disable my-negate))

(defthm cancel-my-negations
  (implies (and (rationalp x) (rationalp y))
           (equal (equal (my-negate x) (my-negate y))
                  (equal x y)))
  :hints (("Goal" :in-theory (disable cancel-negations)
           :use (:functional-instance cancel-negations (negate my-negate) (pred rationalp)))))



(include-book "even")

(encapsulate (((counter-trace *) => *))

             (local (defun counter-trace (time)
                      (declare (ignore time))
                      0))

             (defthm counter-trace-of-0-is-even
               (even-nat (counter-trace 0)))

             (defthm counter-trace-remains-even
               (implies (and (integerp n)
                             (< 0 n)
                             (even-nat (counter-trace (+ -1 n))))
                        (even-nat (counter-trace n))))
             )



(defun time-induct (n)
  (if (zp n)
      n
    (time-induct (+ -1 n))))

(in-theory (disable counter-trace-remains-even 
                    counter-trace-of-0-is-even))

(defthm counter-trace-always-even-nat
  (implies (natp time)
           (even-nat (counter-trace time)))
  :hints (("subgoal *1/2" :use ((:instance counter-trace-remains-even
                                          (n time))
                                (:instance counter-trace-of-0-is-even
                                           )
                                ))
          ("subgoal *1/1" :use ((:instance counter-trace-of-0-is-even
                                          )
                                ))
          ("Goal" 
           :induct (time-induct time)))
  )