;;; Solution to exercises in Chapter 11, "Using Macros to Mimic VHDL",
;;; by Dominique Borrione, Philippe Georgelin, and Vanderlei
;;; Rodrigues, in "Computer-Aided Reasoning: ACL2 Case Studies",
;;; edited by M. Kaufmann, P. Manolios, J Moore (Kluwer, 2000,
;;; p.167-182).

(in-package "ACL2")

(include-book "fact")  ;; The solution to exercise 1 requires the 
                       ;; definition of fact-put from this book.

;;; Exercise 1
;;; ==========

;;; The definition of insert-value is found in file vhdl.lisp, and
;;; theorems are listed below.  The first three theorems are also 
;;; found in file fact-proof.lisp.

(defthm insert-value_consp
  (implies (consp st)
	   (consp (insert-value n new_value st))))

(defthm length_insert-value
  (equal (len (insert-value n new_value st))
	 (len st)))


(defthm lemma_nth_insert-value1
  (implies (and (integerp n) 
		(<= 0 n) 
		(consp st) 
		(< n (len st)))
	   (equal (nth n (insert-value n val st))
		  val)))

(defthm fact-put_consp
  (implies (consp st)
	   (consp (fact-put new var st))))

(defthm length_fact-put
  (equal (len (fact-put new var st))
	 (len st)))

(defthm lemma_fact-get_fact-put
  (implies (and (< (fact-get-nth var) (len st)) 
		(consp st))
	   (equal (fact-get (fact-put new var st) var)
		  new)))

;;; Exercise 2
;;; ==========

;;; The constant *fact-update-signals* is the source code for function
;;; fact-update-signals, as it is generated by the translator from
;;; VHDL to ACL2.  The command :props fact-update-signal displays
;;; several informations about this function, including the rewrite
;;; rule it generates and its source code.  However, the source code
;;; shown by :props has all macros expanded, including the Lisp
;;; special forms COND, LET, etc.  Therefore, this code is less
;;; readable than the code stored in *fact-update-signals*.

;;; Exercises 3 and 4
;;; =================

;;; Run the files as indicated in the book, observe and understand