; ****************** 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

;; ABSTRACT DATA TYPES and OBSERVATIONAL EQUIVALENCE

; We will only briefly talk about this topic, which is very important,
; but needs more time to do it justice.

; The topic has to do with the concepts of modularity, compositionality,
; and interfaces, which are fundamental to software and system design.
; What is modularity? Think of it as the property which allows to use
; a piece of software (or any other system) without knowing (or caring
; about) how exactly the software is implemented. You do this all the
; time: you use software libraries, without knowing how the functions
; in these libraries are implemented. All you need to know is _what_
; a function does, and how to call it (i.e., its signature). You don't
; care how it's implemented internally.

; An abstract data type is like a library, or a "class". It has a set
; of methods / functions that you can call. Each such function has a
; certain signature, and you know the signature, otherwise how could
; you call the function? But also, you know _what_ the function is
; supposed to do. Usually, this _what_ (the specification) is only
; described informally, e.g., in English comments. In this courrse,
; we will describe it formally.

; To make all this concrete, we will illustrate it using an example:
; STACKS!

; What is a stack? It's a data structure, which allows you to "push"
; elements onto it, "pop" the top element, etc. Let's define stacks
; and then illustrate how the concepts of abstract data types come
; into play.


; I want what constitutes an element to be a "parameter", i.e., I want
; everything I do after this to not depend on what an element is.  To
; have a concrete, executable implementation I'll just define element
; to be all.

(defdata element all)

; I am representing a stack using a list, but, again, I want
; everything I do later on to not depend on this representation.
(defdata stack (listof element))

; I will use data definitions to capture interesting special cases of
; stacks, including empty and non-empty stacks.
(defdata empty-stack nil)
(defdata non-empty-stack (cons element stack))

; Empty, non-empty stacks are stacks: they are "subtypes".
; The definitions below are really theorems (check the output of ACL2s):
(defdata-subtype empty-stack stack)
(defdata-subtype non-empty-stack stack)

; Now I will define stack operations. Think of the signature as the
; publicly viewable part of my library. The function body is an
; implementation choice that the user of the library does not have
; access to.

; The push operation inserts e on the top of the stack s
(definec stack-push (e :element s :stack) :non-empty-stack
  (cons e s))

; For pop, I have to make a decision. Do I allow stack-pop to be
; called on empty stacks? I decided to not allow that.

; The pop operation removes the top element of a non-empty stack 
(definec stack-pop (s :non-empty-stack) :stack
  (rest s))

; Similarly, we do not allow stack-head to be called on empty stacks.

; The head of a non-empty stack
(definec stack-head (s :non-empty-stack) :element
  (first s))

; How do I get my hands (as a user) on a stack in the first place?

; Stack creation: returns an empty stack
(definec new-stack () :empty-stack 
  nil)

; Auxiliary definitions

(defthm stack-tlp (equal (stackp l) (tlp l)))
(defmacro stack (a) `(listof ,a))


#|
* ALGEBRAIC DATA TYPES

While we now have an implementation, we do not have an
implementation-independent characterization of stacks. In fact, we
will see two such characterizations.

What the user of our library will be able to see is the following:
|#

; 1.The subtype theorems:

(defdata-subtype empty-stack stack)
(defdata-subtype non-empty-stack stack)

; 2. The following signatures:

(sig stack-push (:a (stack :a)) => (stack :a))
(sig stack-pop ((stack :a)) => (stack :a)
     :satisfies (non-empty-stackp x1))
(sig stack-head ((stack :a)) => :a
     :satisfies (non-empty-stackp x1))

; 3. The following theorems:

(thm (empty-stackp (new-stack)))
(thm (booleanp (elementp x)))
(thm (implies (and (elementp x) (stackp s))
              (non-empty-stackp (stack-push e s))))

#|
Notice that the users do not see the data definition of a stack,
because how we represent stacks is implementation-dependent. 
They also do not see the data definition of element, since that 
can be any recognizer.
|#

; 4. The (algebraic) properties that stacks satisfy:

(defthm pop-push
  (implies (and (stackp s)
                (elementp e))
           (equal (stack-pop (stack-push e s))
                  s)))

(defthm stack-head-stack-push
  (implies (and (stackp s)
                (elementp e))
           (equal (stack-head (stack-push e s))
                  e)))

(defthm push-pop
  (implies (and (stackp s)
                (not (empty-stackp s)))
           (equal (stack-push (stack-head s) (stack-pop s))
                  s)))

(defthm empty-stack-new-stack
  (implies (and (empty-stackp s)
                (stackp s))
           (equal (new-stack)
                  s)))



#|
* Redundancy & Independence

Independence: 
Are the algebraic properties defined above "independent"? We characterize
properties as either being "redundant", meaning that they can be derived
from existing properties, or "independent", meaning that they are not
provable from existing properties.

Here is an example of a redundant property:
|#

(thm (implies (and (stackp s) (elementp e))
              (stackp (stack-push e (stack-push e s)))))

#|
The above theorem does not allow us to prove anything new, as it
follows from the theorems we already know!

Here's a slightly more interesting example of a redundant property:
|#

(thm (implies (and (stackp s) (elementp e1) (elementp e2))
              (equal (stack-pop (stack-pop (stack-push e2 (stack-push e1 s))))
                     s)))

#|
Why is the above property redundant? Because we can prove it using the existing
algebraic properties:

(stack-pop (stack-pop (stack-push e2 (stack-push e1 s))))
= { property pop-push }
(stack-pop (stack-push e1 s))
= { property pop-push }
s

So all we needed to prove the above is property pop-push, which
we applied twice. In essence, we can view the above algebraic properties
as axioms about our library, which we take to hold for granted.
Then we can prove more properties about our library, using these axioms.

(NOTE: In the above "proof" what we are really proving is that _any functions_
stack-push and stack-pop which satisfy the pop-push theorem, also satisfy
the above theorem. This is a property that cannot be expressed in ACL2s
(nor in first-order logic) as it involves quantification over functions.)

Independence:
How does one show that a property is independent? The answer is to
come up with two implementations, one which satisfies all the
properties and one which satisfies all properties except the one under
consideration.

Since we already have an implementation that satisfies all the
properties, to show that some property above is independent of the
rest, come up with an implementation that satisfies the rest of the
properties, but not the one in question.

Let's try that for property pop-push. We want to show that it's independent
from the other three.

One idea is to have pop just return s. Let's try that:
|#

(definec stack-pop2 (s :non-empty-stack) :stack
  s)

#|
We now have to prove that our new implementation (the one which has
stack-pop2 instead of stack-pop, and all other functions stay the same)
satisfies the 3 properties other than pop-push:

These two will still hold, since they don't involve stack-pop2:

(defthm stack-head-stack-push
  (implies (and (stackp s)
                (elementp e))
           (equal (stack-head (stack-push e s))
                  e)))

(defthm empty-stack-new-stack
  (implies (and (empty-stackp s)
                (stackp s))
           (equal (new-stack)
                  s)))
|#

;; But now this property no longer holds:
(must-fail
(defthm push-pop2
  (implies (and (stackp s)
                (not (empty-stackp s)))
           (equal (stack-push (stack-head s) (stack-pop2 s))
                  s)))
)
;; for example, if s = (1 2) then
;; (stack-push (stack-head s) (stack-pop2 s)) = (1 1 2)
;; which is different from s.

#|
So we need to change something else also.
Here is one solution. Define stack-push2 as follows:
|#

(definec stack-push2 (e :element s :stack) :stack
  (if (and (consp s) (equal e (first s)))
      s
    (cons e s)))

;; Now we have to prove these 2 properties:
(defthm stack-head-stack-push2
  (implies (and (stackp s)
                (elementp e))
           (equal (stack-head (stack-push2 e s))
                  e)))

(defthm push2-pop2
  (implies (and (stackp s)
                (not (empty-stackp s)))
           (equal (stack-push2 (stack-head s) (stack-pop2 s))
                  s)))#|ACL2s-ToDo-Line|#


;; Do this for other properties as an exercise.