TUTORIAL5-MISCELLANEOUS-EXAMPLES

miscellaneous ACL2 examples 
Major Section:  TUTORIAL-EXAMPLES

The following examples are more advanced examples of usage of ACL2. They are included largely for reference, in case someone finds them useful.




FILE-READING-EXAMPLE

example of reading files in ACL2 
Major Section:  TUTORIAL5-MISCELLANEOUS-EXAMPLES

This example illustrates the use of ACL2's IO primitives to read the forms in a file. See io.

This example provides a solution to the following problem. Let's say that you have a file that contains s-expressions. Suppose that you want to build a list by starting with nil, and updating it ``appropriately'' upon encountering each successive s-expression in the file. That is, suppose that you have written a function update-list such that (update-list obj current-list) returns the list obtained by ``updating'' current-list with the next object, obj, encountered in the file. The top-level function for processing such a file, returning the final list, could be defined as follows. Notice that because it opens a channel to the given file, this function modifies state and hence must return state. Thus it actually returns two values: the final list and the new state. 



  (defun process-file (filename state)
    (mv-let
     (channel state)
     (open-input-channel filename :object state)
     (mv-let (result state)
             (process-file1 nil channel state) ;see below
             (let ((state (close-input-channel channel state)))
               (mv result state)))))
The function process-file1 referred to above takes the currently constructed list (initially, nil), together with a channel to the file being read and the state, and returns the final updated list. Notice that this function is tail recursive. This is important because many Lisp compilers will remove tail recursion, thus avoiding the potential for stack overflows when the file contains a large number of forms. 


  (defun process-file1 (current-list channel state)
    (mv-let (eofp obj state)
            (read-object channel state)
            (cond
             (eofp (mv current-list state))
             (t (process-file1 (update-list obj current-list)
                               channel state)))))



FUNCTIONAL-INSTANTIATION-EXAMPLE

a small proof demonstrating functional instantiation 
Major Section:  TUTORIAL5-MISCELLANEOUS-EXAMPLES

The example below demonstrates the use of functional instantiation, that is, the use of a generic result in proving a result about specific functions. In this example we constrain a function to be associative and commutative, with an identity or ``root,'' on a given domain. Next, we define a corresponding function that applies the constrained associative-commutative function to successive elements of a list. We then prove that the latter function gives the same value when we first reverse the elements of the list. Finally, we use functional instantiation to derive the corresponding result for the function that multiplies successive elements of a list.

Also see constraint for more about functional instance and see lemma-instance for general information about the use of previously-proved lemmas. 

(in-package "ACL2")


(encapsulate
 (((ac-fn * *) => *)
  ((ac-fn-domain *) => *)
  ((ac-fn-root) => *))
 (local (defun ac-fn (x y) (+ x y)))
 (local (defun ac-fn-root () 0))
 (local (defun ac-fn-domain (x) (acl2-numberp x)))
 (defthm ac-fn-comm
   (equal (ac-fn x y)
          (ac-fn y x)))
 (defthm ac-fn-assoc
   (equal (ac-fn (ac-fn x y) z)
          (ac-fn x (ac-fn y z))))
 (defthm ac-fn-id
   (implies (ac-fn-domain x)
            (equal (ac-fn (ac-fn-root) x)
                   x)))
 (defthm ac-fn-closed
   (and (ac-fn-domain (ac-fn x y))
        (ac-fn-domain (ac-fn-root)))))


(defun ac-fn-list (x)
  (if (atom x)
      (ac-fn-root)
    (ac-fn (car x)
           (ac-fn-list (cdr x)))))


(in-theory (disable (ac-fn-list)))


(defun ac-fn-domain-list (x)
  (if (atom x)
      t
    (and (ac-fn-domain (car x))
         (ac-fn-domain-list (cdr x)))))


(defun rev (x)
  (if (atom x)
      nil
    (append (rev (cdr x))
            (list (car x)))))


(defthm ac-fn-list-closed
   (ac-fn-domain (ac-fn-list x)))


(defthm ac-fn-list-append
  (implies (and (ac-fn-domain-list x)
                (ac-fn-domain-list y))
           (equal (ac-fn-list (append x y))
                  (ac-fn (ac-fn-list x)
                         (ac-fn-list y)))))


(defthm ac-fn-domain-list-rev
  (equal (ac-fn-domain-list (rev x))
         (ac-fn-domain-list x)))


(defthm ac-fn-list-rev
  (implies (ac-fn-domain-list x)
           (equal (ac-fn-list (rev x))
                  (ac-fn-list x))))


(defun times-list (x)
  (if (atom x)
      1
    (* (car x)
       (times-list (cdr x)))))


(defun acl2-number-listp (x)
  (if (atom x)
      t
    (and (acl2-numberp (car x))
         (acl2-number-listp (cdr x)))))


(defthm times-list-rev
  (implies (acl2-number-listp x)
           (equal (times-list (rev x))
                  (times-list x)))
  :hints (("Goal"
           :use
           ((:functional-instance
             ac-fn-list-rev
             ;; Instantiate the generic functions:
             (ac-fn (lambda (x y) (* x y)))
             (ac-fn-root (lambda () 1))
             (ac-fn-domain acl2-numberp)
             ;; Instantiate the other relevant functions:
             (ac-fn-list times-list)
             (ac-fn-domain-list acl2-number-listp))))))