; ****************** BEGIN INITIALIZATION FOR ACL2s MODE ****************** ;
; (Nothing to see here!  Your actual file is after this initialization code);
(make-event
 (er-progn
  (set-deferred-ttag-notes t state)
  (value '(value-triple :invisible))))

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil);v4.0 change

;Common base theory for all modes.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s base theory book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/base-theory" :dir :system :ttags :all)


#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/custom" :dir :system :ttags :all)

;; guard-checking-on is in *protected-system-state-globals* so any
;; changes are reverted back to what they were if you try setting this
;; with make-event. So, in order to avoid the use of progn! and trust
;; tags (which would not have been a big deal) in custom.lisp, I
;; decided to add this here.
;; 
;; How to check (f-get-global 'guard-checking-on state)
;; (acl2::set-guard-checking :nowarn)
(acl2::set-guard-checking :all)

;Settings common to all ACL2s modes
(acl2s-common-settings)
;(acl2::xdoc acl2s::defunc) ;; 3 seconds is too much time to spare -- commenting out [2015-02-01 Sun]

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/acl2s-sigs" :dir :system :ttags :all)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s mode.") (value :invisible))

(acl2::xdoc acl2s::defunc) ; almost 3 seconds

; Non-events:
;(set-guard-checking :none)

(set-inhibit-warnings! "Invariant-risk" "theory")

(in-package "ACL2")
(redef+)
(defun print-ttag-note (val active-book-name include-bookp deferred-p state)
  (declare (xargs :stobjs state)
	   (ignore val active-book-name include-bookp deferred-p))
  state)

(defun print-deferred-ttag-notes-summary (state)
  (declare (xargs :stobjs state))
  state)

(defun notify-on-defttag (val active-book-name include-bookp state)
  (declare (xargs :stobjs state)
	   (ignore val active-book-name include-bookp))
  state)
(redef-)

(acl2::in-package "ACL2S")

; ******************* END INITIALIZATION FOR ACL2s MODE ******************* ;
;$ACL2s-SMode$;ACL2s

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;; LECTURE 31 CODE:  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



;; the pow example:

;; non-tail-recursive version:
(definec pow (x :rational p :nat) :rational
  (if (equal p 0)
      1
    (* x (pow x (- p 1)))))

;; tail-recursive version:
(definec pow-t (x :rational p :nat acc :rational) :rational
  (if (equal p 0)
      acc
    (pow-t x (- p 1) (* x acc))))

(definec pow* (x :rational p :nat) :rational
  (pow-t x p 1))

;; the lemma relating pow-t and pow:
(defthm pow-t-lemma
  (implies (and (rationalp x)
                (natp p)
                (rationalp acc))
           (equal (pow-t x p acc)
                  (* acc (pow x p)))))

;; the main theorem that pow* and pow are equivalent:
(defthm pow*-thm
  (implies (and (rationalp x)
                (natp p))
           (equal (pow* x p)
                  (pow  x p))))




;; the replace-all example:

;; preliminaries:
(definec aapp (x :tl y :tl) :tl
  (if (endp x) y
    (cons (car x) (aapp (cdr x) y))))

(definec rrev (x :tl) :tl
  (if (endp x) x
    (aapp (rrev (cdr x)) (list (car x)))))

(defthm aapp-associative
  (implies (and (tlp x) (tlp y) (tlp z))
           (equal (aapp (aapp x y) z)  (aapp x (aapp y z)))))

(defthm aapp-nil  (implies (tlp x)  (equal (aapp x nil) x)))

(defthm rrev-over-aapp
  (implies (and (tlp x) (tlp y))
           (equal (rrev (aapp x y))
                  (aapp (rrev y) (rrev x)))))

(defthm rrev-rrev  (implies (tlp x) (equal (rrev (rrev x)) x)))

(definec revt (x :tl acc :tl) :tl
  (if (endp x)
      acc
    (revt (cdr x) (cons (car x) acc))))

(definec rev* (x :tl) :tl
  (revt x nil))

(defthm revt-rev
  (implies (and (tlp l)
                (tlp a))
           (equal (revt l a)
                  (aapp (rrev l) a))))

(defthm rev*-rev
  (implies (tlp l)
           (equal (rev* l)
                  (rrev l))))


;; the replace-all function:
(definec replace-all (e :all f :all l :tl) :tl
  (cond ((endp l) l)
        ((equal e (first l))
         (cons f (replace-all e f (rest l))))
        (t (cons (first l) (replace-all e f (rest l))))))

;; it replaces all occurrences of e by f in list l:
(replace-all '(1) 2 '(1 (2) (1) 2 (1) 1))

;; tail-recursive version of replace-all, version 1:
(definec rt1 (e :all f :all l :tl acc :tl) :tl
  (cond ((endp l) (rev* acc))
        ((equal e (first l))
         (rt1 e f (rest l) (cons f acc)))
        (t (rt1 e f (rest l) (cons (first l) acc)))))

(definec r*1 (e :all f :all l :tl) :tl
  (rt1 e f l nil))


;; this goes through, but a thm wouldn't: try it!
(test?
 (implies (tlp l)
          (equal (r*1 e f l)
                 (replace-all e f l))))

(defthm rt1-lemma
  (implies (and (tlp l) (tlp acc))
           (equal (rt1 e f l acc)
                  (aapp (rrev acc) (replace-all e f l)))))

(defthm r*1-thm
  (implies (tlp l)
           (equal (r*1 e f l)
                  (replace-all e f l))))


;; tail-recursive version of replace-all, version 2:
(definec rt2 (e :all f :all l :tl acc :tl) :tl
  (cond ((endp l) acc)
        ((equal e (first l))
         (rt2 e f (rest l) (cons f acc)))
        (t (rt2 e f (rest l) (cons (first l) acc)))))

(definec r*2 (e :all f :all l :tl) :tl
  (rt2 e f (rev* l) nil))


;; this goes through, but a thm wouldn't: try it!
(test?
 (implies (tlp l)
          (equal (r*2 e f l)
                 (replace-all e f l))))

(defthm rt2-lemma
  (implies (and (tlp l) (tlp acc))
           (equal (rt2 e f l acc)
                  (aapp (rrev (replace-all e f l)) acc))))

(defthm r*2-thm
  (implies (tlp l)
           (equal (r*2 e f l)
                  (replace-all e f l))))


;; tail-recursive version of replace-all, version 3:
(definec r*3 (e :all f :all l :tl) :tl
  (rev* (rt2 e f l nil)))


;; this goes through, but a thm wouldn't: try it!
(test?
 (implies (tlp l)
          (equal (r*3 e f l)
                 (replace-all e f l))))

(defthm r*3-thm
  (implies (tlp l)
           (equal (r*3 e f l)
                  (replace-all e f l))))#|ACL2s-ToDo-Line|#




;; the add-lists example:

(defdata lor (listof rational))

(definec add-lists (x :lor y :lor) :lor
  (cond ((endp x) y)
        ((endp y) x)
        (t (cons (+ (car x) (car y))
                 (add-lists (cdr x) (cdr y))))))

(add-lists '(1 2 3) '(4 5))

;; Ask students to define add-lists-t. Try to get a wrong answer!
;; Refer to the recipe.

(definec add-lists-t (x :lor y :lor acc :lor) :lor
  (cond ((endp x) (aapp (rev* acc) y))
        ((endp y) (aapp (rev* acc) x))
        (t (add-lists-t (cdr x)
                        (cdr y)
                        (cons (+ (car x) (car y)) acc)))))

;; Notice the use of rev* above: we want execution to be fast.

;; Ask students to define add-lists*

(definec add-lists* (x :lor y :lor) :lor
  (add-lists-t x y nil))

;; Test the conjecture. If it fails, use the failed test to fix
;; add-lists-t unilt this goes through.

(test? (implies (and (lorp x) (lorp y))
                (equal (add-lists* x y)
                       (add-lists x y))))

;; Test the lemma. Fix it until it goes through. Notice the use of
;; rev below. We want to use the simple version when proving theorems. 

(test?
 (implies (and (lorp x) (lorp y) (lorp acc))
          (equal (add-lists-t x y acc)
                 (aapp (rrev acc) (add-lists x y)))))

;; Now we can prove theorems. Again, notice the use of rev, not rev*
;; when proving theorems.

(defthm add-lists-t-lemma
  (implies (and (lorp x) (lorp y) (lorp acc))
           (equal (add-lists-t x y acc)
                  (aapp (rrev acc) (add-lists x y)))))

;; And this goes through easily.

(defthm add-lists*-thm
  (implies (and (lorp x) (lorp y))
           (equal (add-lists* x y)
                  (add-lists x y))))