; A Simple Ripple-Carry Adder in ACL2
; J Moore

(include-book "arithmetic-5/top" :dir :system)

(set-acl2s-random-testing-enabled nil)

; In this project I will represent binary numbers by
; lists of Ts and NILs. I will call such a list a ``Boolean
; vectors'' or ``bv'' for short.  In a bv, I will put the least
; significant digit first.  So the binary number 6, which might
; usually be written 110 will be the bv (NIL T T).

; First I will define the function that takes a bv
; and converts it to a natural number:

(defun N (bv)
  (if (endp bv)
    0
    (+ (if (first bv) 1 0)
       (* 2 (N (rest bv))))))

; For example,

(N '(nil t t))

; For testing purposes, it is convenient to have the inverse
; of N:

(defun V (n)
  (if (zp n)
    nil
    (cons (oddp n)
          (V (floor n 2)))))

; So for example,

(V 6)

; and

(V 123456789)

(N (V 12345689))

; To add in binary we must be able to add 3 binary digits together
; and get the new least significant digit and a carry out.

; a + b + c   = low-digit   carry out
; nil nil nil   nil         nil
; nil nil t     t           nil
; nil t   nil   t           nil
; nil t   t     nil         t
; t   nil nil   t           nil
; t   nil t     nil         t
; t   t   nil   nil         t
; t   t   t     t           t

; The following definitions would be much more elegant if I used 
; exclusive or, but I want to show how I can do everything with
; and, or, and not.

; Low-digit is T if exactly one of a, b, and c is T, or if all
; three are T.

(defun low-digit (a b c)
  (or (and a       (not b) (not c))
      (and (not a) b       (not c))
      (and (not a) (not b) c)
      (and a       b       c)))

; Carry-out is T if two or more of a, b, and c are T.

(defun carry-out (a b c)
  (or (and a b)
      (and a c)
      (and b c)))

(defun adder (A B c)
  (if (and (endp A) (endp B))
      (list c)
      (cons (low-digit (first A)
                       (first B) 
                       c)
            (adder (rest A) 
                   (rest B) 
                   (carry-out (first A)
                              (first B)
                              c)))))

(adder '(nil t t) '(t t nil) nil)

(N (adder (V 6) (V 3) nil))

(N (adder (V 1234) (V 6789) nil))

(+ 1234 6789 0)

(defthm adder-is-correct-lemma
  (implies (endp B)
           (equal (N (adder A B c))
                  (+ (N A) (if c 1 0)))))

(defthm adder-is-correct
  (equal (N (adder A B c))
         (+ (N A)
            (N B)
            (if c 1 0))))