;; ---------------------------------------------------------------------------
;;     ~/events/toktrans-1.events
;; ---------------------------------------------------------------------------; 
(enable-theory tokens)

;; This is the token transformation function that discards tokens. 
;; "discard" is the name of the token transformation function. It takes 
;; as parameters the token sequence and a list of token names to be removed.

(defn discard (toks discard-list)
 (if (nlistp toks)
     toks
     (if (member (token-name (car toks)) discard-list)
	 (discard (cdr toks) discard-list)
	 (cons (car toks)
	       (discard (cdr toks) discard-list)))))

;; The first correctness predicate states that any tokens not on the discard
;; list remain unchanged and are in the same order as before the application 
;; of discard.

(defn non-discards-undisturbed (toks1 toks2 discard-list)
  (if (nlistp toks1)
      (nlistp toks2)
      (if (not (member (token-name (car toks1)) discard-list))
      	  (and (equal (car toks1) (car toks2))
               (non-discards-undisturbed (cdr toks1) (cdr toks2) discard-list))
	  (non-discards-undisturbed (cdr toks1) toks2 discard-list))))

(prove-lemma discard-does-not-disturb-non-discards (rewrite)
 (non-discards-undisturbed toks (discard toks discard-list) discard-list))

;; The second predicate states that after application of discard, no
;; tokens with a name on the discard list remain.

(defn no-discards-left (toks discard-list)
  (if (nlistp toks)
      T
      (if (member (token-name (car toks)) discard-list)
	  F
	  (no-discards-left (cdr toks) discard-list))))

;; The main theorem for toktrans-1 is trivially proven.

(prove-lemma toktrans-1-main-theorem (rewrite)
 (no-discards-left (discard toks discard-list) discard-list))