;; ---------------------------------------------------------------------------
;; ~/events/lists.events
;; ---------------------------------------------------------------------------
;; These are some functions on lists, adapted from the CLInc list library.

(defn last (x)
  (if (nlistp x)
      x
      (if (nlistp (cdr x))
	  x
	  (last (cdr x)))))

;; ------------- length and lemmata on length -----------------

(defn length (l) 
  (if (not (listp l))
      0 
      (add1 (length (cdr l)))))

(prove-lemma equal-length-0 (rewrite)
  (equal (equal (length l) 0)
	 (not (listp l)))
  ((enable length)))

(prove-lemma length-nlistp (rewrite)
  (implies (nlistp x)
	   (equal (length x) 0))
  ((enable length)))

(prove-lemma length-cons (rewrite)
  (equal (length (cons a x))
	 (add1 (length x)))
  ((enable length)))

(prove-lemma lessp-length-cons (rewrite)
  (equal (lessp (length z) (length (cons v z)))
	 t)
 ((enable length-cons)))

(prove-lemma lessp-length-cdr (rewrite)
 (implies (listp x)
	  (lessp (length (cdr x))
		 (length x)))
 ((do-not-induct t)))

;; The function plist constructs a proper (i.e. nil as last cdr) list out of l.

(defn plist (l)
  (if (not (listp l))
      nil
      (cons (car l) (plist (cdr l)))))

(defn plistp (l)
  (if (not (listp l))
      (equal l nil)
      (plistp (cdr l))))

(prove-lemma plistp-nlistp (rewrite)
  (implies (nlistp l)
	   (equal (plistp l)
		  (equal l nil)))
  ((enable plistp)))

(prove-lemma equal-plist (rewrite)
  (implies (plistp l)
	   (equal (plist l) l))
  ((enable plistp plist)))

(prove-lemma plistp-cons (rewrite)
  (equal (plistp (cons a l))
	 (plistp l))
  ((enable plistp)))

; ---------- lemmata on append ----------

(prove-lemma plistp-append (rewrite)
  (equal (plistp (append a b))
	 (plistp b))
  ((enable plistp append)))

(prove-lemma append-left-id (rewrite)
  (implies (not (listp a))
	   (equal (append a b)
		  b))
  ((enable append)))

(prove-lemma append-nil (rewrite)
  (equal (append a nil)
	 (plist a))
  ((enable append plist)))

(prove-lemma append-append (rewrite)
 (equal (append (append a b) c)
	(append a (append b c))))

;; These are some definitions from the association list library.

(defn domain (map)
  (if (listp map)
      (if (listp (car map))
	  (cons (car (car map)) (domain (cdr map)))
	(domain (cdr map)))
    nil))

(disable domain)

(defn alistp (x)
  (if (listp x)
      (and (listp (car x))
	   (alistp (cdr x)))
    (equal x nil)))

(disable alistp)


(defn value (x map)
  (if (listp map)
      (if (and (listp (car map))
               (equal x (caar map)))
          (cdar map)
	(value x (cdr map)))
    0))

;; ---------- reverse and lemmata on reverse ----------

(defn reverse (l)
 (if (nlistp l)
     nil
     (append (reverse (cdr l)) (list (car l)))))

(prove-lemma plistp-reverse (rewrite)
  (plistp (reverse a)))

(prove-lemma reverse-append (rewrite)
  (equal (reverse (append a b))
	 (append (reverse b) (reverse a))))

(prove-lemma reverse-reverse (rewrite)
  (implies (plistp l)
	   (equal (reverse (reverse l)) l)))

;; This predicate returns true if all elements of the string are in vocab.

(defn is-string-in (string vocab)
  (if (nlistp string)
      T
      (and (member (car string) vocab)
	   (is-string-in (cdr string) vocab))))

; These two functions are needed for generating the tables

(defn position (x l)
  (if (listp l)
      (if (equal x (car l))
	  0
	  (add1 (position x (cdr l))))
      0))

(defn nth (n l)
  (if (listp l)
      (if (zerop n)
	  (car l)
	  (nth (sub1 n) (cdr l)))
      0))

(deftheory lists
 (REVERSE-REVERSE REVERSE-APPEND PLISTP-REVERSE REVERSE ALISTP 
  DOMAIN APPEND-NIL APPEND-LEFT-ID APPEND-APPEND PLISTP-APPEND 
  PLISTP-CONS EQUAL-PLIST PLISTP-NLISTP PLISTP PLIST LENGTH-CONS 
  LENGTH-NLISTP EQUAL-LENGTH-0 IS-STRING-IN LENGTH LAST VALUE
  NTH POSITION))
 
(disable-theory lists)