(boot-strap nqthm)
;; ---------------------------------------------------------------------------
;; ~/events/numbers.events
;; ---------------------------------------------------------------------------
;;
;; This is the collection of theorems from the naturals library
;; needed for toktrans-4.
;;
;; ---------------------------------------------------------------------------
;; pick one of the following: Either the library or the easy lemmata and
;;                            the axioms
;; ---------------------------------------------------------------------------
;#|
; ------------------------ The naturals library ---------------------------
;;   from the nqthm-1992 examples/numbers directory
(note-lib "/usr1/name/weberwu/bm/nqthm-1992/examples/numbers/naturals") 
(enable-theory addition)
(enable-theory multiplication)
(enable-theory remainders)
(enable-theory quotients)

;; These cause a infinite rewrite loops and are disabled.
(disable DIFFERENCE-ADD1-ARG2)
(disable PLUS-ZERO-ARG2)
(disable PLUS-ADD1-ARG2)


;|#

#|
;; ---------------------------------------------------------------------------
;; These are lemmata extracted from the naturals library.
;; ---------------------------------------------------------------------------

(prove-lemma commutativity-of-plus (rewrite)
       (equal (plus x y) (plus y x)))

(prove-lemma equal-plus-0 (rewrite)
       (equal (equal (plus a b) 0)
	      (and (zerop a)
		   (zerop b))))

(prove-lemma plus-zero-arg2 (rewrite)
       (implies (zerop y)
		(equal (plus x y)
		       (fix x)))
       ((induct (plus x y))))

(prove-lemma times-zero (rewrite)
       (implies (zerop y)
		(equal (times x y) 0)))

(prove-lemma equal-times-0 (rewrite)
       (equal (equal (times x y) 0)
	      (or (zerop x)
		  (zerop y)))
       ((induct (times x y))))

;; Fix coerces non-numbers to zero.

(prove-lemma times-add1 (rewrite)
       (equal (times x (add1 y))
	      (if (numberp y)
		  (plus x (times x y)) 
		  (fix x))))

(prove-lemma plus-remainder-times-quotient (rewrite)
       (equal (plus (remainder x y) (times y (quotient x y)))
	      (fix x)))

(prove-lemma lessp-quotient (rewrite)
       (equal (lessp (quotient i j) i)
	      (and (not (zerop i))
		   (not (equal j 1)))))

(prove-lemma commutativity-of-times (rewrite)
       (equal (times y x) 
	      (times x y)))

(prove-lemma quotient-lessp-arg1 (rewrite)
       (implies (lessp a b)
		(equal (quotient a b) 0)))

;; ---------------------------------------------------------------------------
;; These are lemmata from the naturals library expressed as axioms.
;; ---------------------------------------------------------------------------

(add-axiom remainder-plus (rewrite)
 (implies (equal (remainder a c) 0)
	  (equal (remainder (plus b a) c)
			   (remainder b c))))

(add-axiom quotient-plus (rewrite)
	   (implies (equal (remainder a c) 0)
		    (equal (quotient (plus b a) c)
			   (plus (quotient a c) (quotient b c)))))

(add-axiom quotient-times-instance (rewrite)
	   (equal (quotient (times y x) y) 
		  (if (zerop y) 
		      0
		      (fix x)))))

(add-axiom remainder-times1-instance (rewrite)
       (and (equal (remainder (times x y) y) 0)
	    (equal (remainder (times x y) x) 0)))

;; ------------------------------------------------------------------
|#
;; ---------------------------------------------------------------------------
;;  ~/events/sets.events
;; ---------------------------------------------------------------------------
;; This is the set theory needed for the proof.
;; Major portions of it are taken from Matt Kaufmann's set library.
;; ---------------------------------------------------------------------------

;; The function subset should probably be named subbag.

(defn subsetp (a b)
  (if (nlistp a)
      T
      (and (member (car a) b)
	   (subsetp (cdr a) b))))

;; A proper set has no duplicates.

(defn setp (l)
  (if (not (listp l))
      t
      (and (not (member (car l) (cdr l)))
	   (setp (cdr l)))))

;; The cardinality of a set is just the length of the list representing it.

(defn card (l) 
  (if (listp l)
      (add1 (card (cdr l)))
      0))

;; The intersection of two sets is all elements that are members in both.

(defn intersection (x y)
  (if (listp x)
      (if (member (car x) y)
	  (cons (car x) (intersection (cdr x) y))
	  (intersection (cdr x) y))
      nil))

;; This function will make a proper set out of the elements of a list.

(defn mk-unique-set (set)
 (if (nlistp set)
     nil
     (union (car set) (mk-unique-set (cdr set)))))

(deftheory sets (subsetp setp card intersection mk-unique-set))

(disable-theory sets)




;; ---------------------------------------------------------------------------
;; ~/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)
;; ---------------------------------------------------------------------------
;; ~/events/grammar.events
;; ---------------------------------------------------------------------------

;; This the implementation of the grammar data type.

(enable-theory sets)
(enable-theory lists)

(add-shell mk-grammar Empty-Grammar is-Grammar
  ((sel-Nonterminals (none-of) zero)
   (sel-Terminals    (none-of) zero)
   (sel-Productions  (none-of) zero)
   (sel-Axiom        (none-of) zero)))

;; Using a shell for mk-prod keeps it from opening up.

(add-shell mk-prod Empty-Prod is-production
  ((sel-label (one-of numberp) Zero)
   (sel-lhs   (none-of)        Zero)
   (sel-rhs   (none-of)        Zero)))

(defn vocab (grammar)
 (union (sel-nonterminals grammar) (sel-terminals grammar)))

;; One needs to be able to access the production labelled label.

(defn prod-nr (prods label)
  (if (nlistp prods)
      nil
      (if (equal (sel-label (car prods)) label)
	  (car prods)
	  (prod-nr (cdr prods) label))))

;; These are the explicit fresh tokens.

(defn end-of-file () 'ef)

(defn dot () 'dot)

(defn left-hand-sides (prods)
 (if (nlistp prods)
     nil
     (union (sel-lhs (car prods)) (left-hand-sides (cdr prods)))))

(defn right-hand-sides (prods)
 (if (nlistp prods)
     nil
     (union (sel-rhs (car prods)) (right-hand-sides (cdr prods)))))

(defn all-but-axiom (prods axiom)
 (if (nlistp prods)
      prods
      (if (equal (sel-label (car prods)) axiom)
	  (cdr prods)
	  (cons (car prods) (all-but-axiom (cdr prods) axiom)))))

(defn no-unused-productions (prods axiom)
    (subsetp (left-hand-sides (all-but-axiom prods axiom))
             (right-hand-sides prods)))

(defn labels (prods)
  (if (nlistp prods)
      nil
      (append (list (sel-label (car prods))) (labels (cdr prods)))))

;; This function finds the label number for a production mk-prod (_,lhs, rhs).

(defn find-label (lhs rhs prods)
 (if (nlistp prods)
     'no-such-label
     (if (and (equal lhs (sel-lhs (car prods)))
	      (equal rhs (sel-rhs (car prods))))
	 (sel-label (car prods))
	 (find-label lhs rhs (cdr prods)))))

(defn is-wf-grammar (grammar)
 (let ((prods (sel-productions grammar))
       (nonts (sel-nonterminals grammar))
       (terms (sel-terminals grammar))
       (axiom (sel-axiom grammar)))
   (let ((vocab (union nonts terms))
	 (labs  (labels prods)))
     (and (is-grammar grammar)
          (no-unused-productions prods axiom)
	  (equal (card labs) 
		 (length prods))
          (member axiom labs)
          (equal (intersection  nonts terms) nil )
          (not (member (end-of-file) vocab))
          (not (member (dot) vocab))
          (subsetp (right-hand-sides prods) vocab)))))

#|
(r-loop)
;; The functions can be tested with the expression grammar.

(setq grammar-expr
 (mk-grammar
  '(e t f s)
  '(plus times open close a)
    (list (mk-prod 0 's '(e))
          (mk-prod 1 'e '(e plus t))
	  (mk-prod 2 'e '(t))
	  (mk-prod 3 't '(t times f))
	  (mk-prod 4 't '(f))
	  (mk-prod 5 'f '(open e close))
	  (mk-prod 6 'f '(a)))
  0 ))

(is-wf-grammar grammar)
|#

(deftheory grammar
 (IS-WF-GRAMMAR LABELS NO-UNUSED-PRODUCTIONS ALL-BUT-AXIOM
  RIGHT-HAND-SIDES LEFT-HAND-SIDES DOT END-OF-FILE PROD-NR find-label VOCAB
  MK-PROD MK-GRAMMAR))
(disable-theory grammar)
(disable-theory lists)
(disable-theory sets);; ---------------------------------------------------------------------------
;; ~/events/stack.events
;; ---------------------------------------------------------------------------

;; This file implements a generic data type stack.

(enable-theory lists)

;; I will use a shell for implementing the basic stack. The bottom element is
;; EmptyStack, stackp is the recognizer, push the constructor and 
;; top and pop the destructors.

(add-shell push EmptyStack is-stack
     ((top (none-of) zero)
      (pop (one-of is-stack) EmptyStack)))

;; The function to test for bottom element equality

(defn is-empty (s) 
  (if (is-stack s)
      (equal s (EmptyStack))
      F))

;; The functions for popping or pushing more than one element at a time.

(defn pop-n (n s)
 (if (not (is-stack s))
     s
     (if (zerop n)
	 s
	 (pop-n (sub1 n) (pop s)))))

(prove-lemma pop-n-emptystack (rewrite)
 (implies (numberp size)
	  (equal (pop-n size (emptystack))
		 (emptystack))))

;; The function top-n returns the top n elements of the stack in reverse order.

(defn top-n (n s)
 (if (or (not (is-stack s))
	 (equal s (emptystack)))
     nil
     (if (zerop n)
	 nil
         (append (top-n (sub1 n) (pop s))
		 (list (top s))))))

;; This function returns the number of elements on a stack.

(defn stack-length (s) 
  (if (or (not (is-stack s))
	  (is-empty s))
      0
      (add1 (stack-length (pop s)))))

;; This is a minor lemma to prove that a non-empty stack has non-zero length.

(prove-lemma not-empty-not-zero (rewrite)
 (implies (and (is-stack stack)
	       (not (is-empty stack)))
	  (lessp 0 (stack-length stack))))

;; Reading the stack from the bottom, i.e. the top element is last and 
;; the bottom element is first.  Note that (not (is-stack s)) was necessary 
;; for the proof of termination of this function. And I had to use append 
;; and put the second parameter in a list in order to obtain the function I
;; expected to have specified.

(defn from-bottom (s) 
   (if (or (is-empty s)
	   (not (is-stack s)))
       nil
       (append (from-bottom (pop s)) (list (top s)))))

;; One needs to know that pop is smaller than the original for a measure.

(prove-lemma lessp-pop-stack (rewrite)
  (implies (and (is-stack s)
		(not (is-empty s)))
	   (lessp (stack-length (pop s)) (stack-length s))))

;; This theorem is needed for the parser proof.

(prove-lemma append-from-bottom-pop-n (rewrite)
 (implies (is-stack s)
	  (equal (append (from-bottom (pop-n n s))
			 (top-n n s))
		 (from-bottom s))))

(prove-lemma plistp-from-bottom (rewrite)
 (implies (is-stack s)
	  (plistp (from-bottom s))))
       
(prove-lemma from-bottom-push (rewrite)
 (implies (is-stack b)
	  (equal (from-bottom (push a b))
		 (append (from-bottom b) (list a)))))

(deftheory stacks 
 (LESSP-POP-STACK FROM-BOTTOM NOT-EMPTY-NOT-ZERO STACK-LENGTH
  TOP-N POP-N pop-n-emptystack IS-EMPTY PUSH APPEND-FROM-BOTTOM-POP-N
  PLISTP-FROM-BOTTOM FROM-BOTTOM-PUSH))
(disable-theory stacks)
(disable-theory lists);; ---------------------------------------------------------------------------
;; ~/events/token.events
;; ---------------------------------------------------------------------------

;; This is the representation for a (pre-)token, which is what the scanner is
;; to deliver.

(add-shell mk-token nil tokenp
           ((token-name (none-of) zero)
            (token-value (none-of) zero)))

(defn token-listp (l)
  (if (nlistp l)
      (equal l nil) 
      (and (tokenp (car l))
           (token-listp (cdr l)))))

;; This function filters out the token names from a token list.

(defn pick-token-names (l)
 (if (nlistp l)
     nil
     (if (tokenp (car l))
	 (cons (token-name (car l)) (pick-token-names (cdr l)))
	 (cons (car l) (pick-token-names (cdr l))))))

(deftheory tokens (MK-TOKEN PICK-TOKEN-NAMES TOKEN-LISTP))
(disable-theory tokens)	;; ---------------------------------------------------------------------------
;; ~/events/tree.events
;; ---------------------------------------------------------------------------

;; These events construct trees and prove theorems about them

(enable-theory lists)
(enable-theory stacks)

;; A tree is a root and a sequence of branches.

(add-shell mk-Tree EmptyTree is-tree
  ((sel-Root     (none-of) Zero) 
   (sel-Branches (none-of) Zero)))

;; A tree is a leaf if the branches are empty.

(defn is-leaf (tree)
 (and (is-tree tree)
      (equal (sel-branches tree)
             Nil)))

(defn is-subtree (tag sub Tree)
 (if (equal tag 'tree)
     (if (or (equal (EmptyTree) Tree)
             (not (is-tree Tree)))
         F
         (if (equal sub Tree)
             T
             (is-subtree 'branches sub (sel-branches Tree))))
     ; list of branches
     (if (nlistp Tree)
         F
         (or (is-subtree 'tree sub (car Tree))
             (is-subtree 'branches sub (cdr Tree))))))

(prove-lemma subtree-reflexive (rewrite)
 (implies (and (is-tree tree)
               (not (equal tree (EmptyTree))))
          (is-subtree 'tree tree tree)))

(defn is-leaf-in (node tree)
  (and (is-leaf node)
       (is-subtree 'tree node tree)))

;; The function frontier collects the leaves of one tree into a list. 

(defn frontier (tag Item)
 (if (equal tag 'tree)
     (if (or (not (is-tree Item))
             (equal Item (Emptytree)))
         nil
       (if (is-leaf Item)
           (list (sel-root Item))
           (frontier 'branches  (sel-Branches Item))))
     ; Branches
     (if (nlistp Item)
         nil
         (append (frontier 'tree (car Item))
                 (frontier 'branches (cdr Item))))))

(prove-lemma plistp-frontier (rewrite)
 (plistp (frontier tag anything)))

(prove-lemma leaf-frontier (rewrite)
 (equal (frontier 'tree (mk-tree v nil))
        (list v)))

(prove-lemma member-append (rewrite)
 (equal (member x (append a b))
        (or (member x a)
            (member x b))))
                
;; This is the key lemma, which needs member-append.

(prove-lemma is-subtree-leaf-is-member-frontier (rewrite)
 (equal (is-subtree tag (mk-tree z nil) tree)
	(member z (frontier tag tree))))

;; This is theorem 1, all leaves in the tree are in the frontier.

(prove-lemma all-leaves-in-frontier (rewrite)
 (implies (and (is-leaf-in subtree tree)
               (is-tree tree))
          (member (sel-root subtree) (frontier 'tree tree))))

;; This is the nearest I come to demonstrating that only leaves
;; are in the frontier.

(prove-lemma only-leaves-in-frontier (rewrite)
 (implies (and (member x (frontier 'tree tree))
	       (is-tree tree))
          (is-leaf-in (mk-tree x nil) tree)))

;; I want to show that the leaves are kept in order.

;; I need to define an ordering on the nodes of the tree so that I can 
;; determine when a node (or leaf) preceeds another. I will print the 
;; entire collection of nodes in preorder (although postorder would do as 
;; well) and then prove that the frontier is a subsequence of the preorder. 
;; See below for the definition of subsequence.

(defn preorder-print (tag tree)
 (if (equal tag 'tree)
     (if (or (not (is-tree tree))
             (equal tree (Emptytree)))
         nil
       (append (list (sel-root tree))
               (preorder-print 'branches (sel-branches tree))))
   ; branches
   (if (nlistp tree)
       nil
       (append (preorder-print 'tree (car tree))
               (preorder-print 'branches  (cdr tree))))))

;; The theorem is; (subseq (frontier 'tree tree) (preorder-print 'tree tree))

;; x is a subsequence of y if I can remove some elements of y (not 
;; necessarily in order) and obtain x. That is, the elements of x are found 
;; in the same order in y.

(defn subseq (x y)
  (if (nlistp x)
      t
      (if (nlistp y)
          f
          (or (and (equal (car x) (car y))
                   (subseq (cdr x) (cdr y)))
              (and (not (equal (car x) (car y)))
                   (subseq x (cdr y)))))))

(prove-lemma subseq-cons-lemma (rewrite)
  (and (implies (subseq x y)
                (subseq (cdr x) y))
       (implies (subseq x (cdr y))
                (subseq x y))))

(prove-lemma subseq-cons-1 (rewrite)
  (implies (subseq (cons a x) y)
           (subseq x y)))

(prove-lemma subseq-cons-2 (rewrite)
  (implies (subseq x y)
           (subseq x (cons b y))))

(prove-lemma subseq-cons-append (rewrite)
            (implies (subseq (cons x z) u)
                     (subseq z (append v u))))

(prove-lemma subseq-append-append (rewrite)
        (implies (and (subseq b u) (subseq a y))
                 (subseq (append a b) (append y u))))

(prove-lemma subseq-frontier-preorder (rewrite) 
          (subseq (frontier tag tree)
                  (preorder-print tag tree)))

;; ---------------------------------------------------------------------------
;; Other functions using trees

;; The function roots collects up the roots of all the trees in a sequence,
;; It is often used on a collection of branches.

(defn roots (trees)
  (if (nlistp trees)
      nil
      (if (is-tree (car trees))
          (append (list (sel-Root (car trees)))
	          (roots (cdr trees)))
	(roots (cdr trees)))))

(prove-lemma plistp-roots (rewrite)
 (plistp (roots r)))

;; The function leaves collects up the leaves of a list of trees from the 
;; bottom. 

(defn leaves (Trees)
  (if (nlistp trees)
      NIL
      (append (frontier 'tree (car Trees))
              (leaves (cdr trees)))))

(prove-lemma plistp-leaves (rewrite)
  (plistp (leaves s))
 ((enable-theory lists)))

(deftheory trees 
 (ROOTS SUBSEQ-FRONTIER-PREORDER SUBSEQ-APPEND-APPEND SUBSEQ-CONS-APPEND
        SUBSEQ-CONS-2 SUBSEQ-CONS-1 SUBSEQ-CONS-LEMMA SUBSEQ PREORDER-PRINT
        ONLY-LEAVES-IN-FRONTIER ALL-LEAVES-IN-FRONTIER
        IS-SUBTREE-LEAF-IS-MEMBER-FRONTIER MEMBER-APPEND LEAF-FRONTIER FRONTIER
        IS-LEAF-IN SUBTREE-REFLEXIVE IS-SUBTREE IS-LEAF MK-TREE
        PLISTP-FRONTIER
        LEAVES PLISTP-LEAVES))
(disable-theory trees)
(disable-theory lists)
(disable-theory stacks)
;; ---------------------------------------------------------------------------
;; ~/events/configuration.events
;; ---------------------------------------------------------------------------

;; These events are the constructors and destructors for configurations.

(enable-theory stacks)
(enable-theory grammar)
(enable-theory lists)
(enable-theory trees)

(add-shell mk-configuration Undefined-Configuration is-configuration
  ((sel-input   (none-of) zero) 
   (sel-states  (none-of) zero)
   (sel-symbols (none-of) zero)
   (sel-Trees   (none-of) zero)
   (sel-Parse   (none-of) zero)   
   (sel-Deriv   (none-of) zero)
   (sel-Error   (none-of) Zero)))

(defn stack-of-trees (trs)
  (if (not (is-stack trs))
      F
      (if (equal (EmptyStack) trs)
	  T
	  (and (is-stack trs)
	       (is-tree (top trs))
	       (stack-of-trees (pop trs)))))
  ((lessp (stack-length trs))))

(defn stack-of-numbers (trs)
  (if (not (is-stack trs))
      F
      (if (equal (EmptyStack) trs)
	  T
	  (and (is-stack trs)
	       (numberp (top trs))
	       (stack-of-numbers (pop trs)))))
  ((lessp (stack-length trs))))

;; A well-formed configuration has as its states a stack of numbers, its
;; symbols a stack of litatoms, its trees a stack consisting of individual
;; trees, etc. Probably the derivation is a well-formed derivation and so on.
;; The input can only be a list of terminals so the terminal list is needed.

(defn is-wf-configuration (c terms)
  (and (stack-of-trees (sel-trees c))
        (not (equal (sel-trees c) (EmptyStack)))
	(is-string-in (sel-input c) terms)
	(stack-of-numbers (sel-states c))))

#| This lemma MUST fail to prove!
(prove-lemma sanity-check ()
 (equal (is-wf-configuration c terms)
	F))
|#

;; This function creates the set of productions used in a tree.

(defn get-prods (flag Param)
      (if (equal flag 'tree)
	  (if (or (is-leaf Param) ; only non-terminal nodes are collected
		  (not (is-tree Param))
		  (equal Param (EmptyTree)))
	      nil 
	    (union (mk-Prod nil (sel-Root Param) (roots (sel-branches Param)))
		   (get-prods 'branches (sel-branches Param))))
	(if (equal flag 'sequence)
	    (if (nlistp Param)
		nil
	        (union (get-prods 'tree (car Param))
		       (get-prods 'sequence (cdr Param))))
	  nil)))

;; This function collects the productions for a stack of trees.

(defn nodes (tree-stack terms)
  (if (or (is-empty tree-stack)
	  (not (is-stack tree-stack)))
      nil
      (union
        (get-prods 'tree (top tree-stack))
        (nodes (pop tree-stack) terms)))
  ((lessp (stack-length tree-stack))))

(deftheory configurations 
 (NODES GET-PRODS IS-WF-CONFIGURATION STACK-OF-NUMBERS STACK-OF-TREES
  MK-CONFIGURATION ))

(disable-theory configurations)
(disable-theory stacks)
(disable-theory grammar)
(disable-theory lists)
(disable-theory trees)




;; ---------------------------------------------------------------------------
;; ~/events/actions.events
;; ---------------------------------------------------------------------------

;; These events describe the parsing actions.
;; A parsing table consists of an action table and a goto table

(defn mk-Tables (Actiontab Gototab)
  (cons Actiontab Gototab))

(defn sel-Actiontab (tables)
  (car tables))

(defn sel-Gototab (tables)
  (cdr tables))

;; An action is a tag, which is either 'shift, 'reduce or 'error, the state to
;; shift to, the label of a reduction, the left hand side of a reduction and
;; the size of the reduction. It is a union type of the different components.

(add-shell mk-Action Empty-Action is-Action
	   ((sel-action-tag   (none-of)        zero)
	    (sel-state-shift  (one-of numberp) zero)
	    (sel-label-reduce (one-of numberp) zero)
	    (sel-lhs-reduce   (none-of)        zero)
	    (sel-size-reduce  (one-of numberp) zero)))

;; I construct actions with the following functions.

(defn mk-shift-action (state)
  (mk-action 'SHIFT state 0 0 0))

(defn mk-reduce-action (label lhs size)
  (mk-action 'REDUCE 0 label lhs size))

(defn mk-error-action ()
  (mk-action 'ERROR 0 0 0 0))

;; For look-up a selector is needed, which is a symbol and a state.

(defn mk-Selector (State Symbol)
  (list State Symbol))

(defn action-lookup (terminal state actiontab) 
  (let ((key (mk-selector state terminal)))
    (cdr (assoc key actiontab))))

(defn goto-lookup (lhs state gototab) 
  (let ((key (mk-selector state lhs)))
    (cdr (assoc key gototab))))

;; ---------------------------------------------------------------------------
;; ~/events/scanning.events
;; ---------------------------------------------------------------------------

;; The scanner will split a sequence of bytes into a sequence of tokens by
;; checking all prefixes with an automaton that recognizes tokens, 
;; and selecting the last one found, which is the longest such prefix. 

;; I use an automaton similar to the one in the fsa proof, but with 
;; (state, re) pairs in the set of finals instead of just states. This
;; enables me to determine which regular expression was responsible for
;; the acceptance of the prefix.

(enable-theory tokens)
(enable-theory sets)
(enable-theory lists)

(add-shell fsa* nil fsap*
  ((alphabet (none-of) zero)
   (states   (none-of) zero)
   (starts   (none-of) zero)
   (table    (none-of) zero)
   (finals   (none-of) zero)))

;; A "real" finite state automaton is an NQTHM-automaton with the following
;; properties. Note that finals is an association list. The domain is a
;; subset of the set of states. 

(defn fsap (auto)
  (let ((al (alphabet auto))
        (st (states auto))
        (s0 (starts auto))
        (tr (table auto))
        (fi (finals auto)))
    (and (fsap* auto)
         (listp al)
         (listp st)
         (listp s0)
         (alistp fi)
         (subsetp s0 st)
         (setp st)
         (setp fi)
         (subsetp (domain fi) st))))

(defn mk-transition (state input nexts)
  (cons (cons state input) nexts))

;; These are the selector functions for the transitions in the table.

(defn state (trans) (caar trans))
(defn input (trans) (cdar trans))
(defn nexts (trans) (cdr trans))

(defn transitionp (trans alphabet states)
 (and (member (input trans) alphabet)
      (member (state trans) states)
      (subsetp (nexts trans) states)
      (plistp (nexts trans))))

(defn wf-table (table alphabet states)
  (if (nlistp table)
      (equal table nil)
      (and (transitionp (car table) alphabet states)
           (wf-table (cdr table) alphabet states))))

(defn ndfsap (a)
  (and (fsap a)
       (wf-table (table a) (alphabet a) (states a))))

;; The automaton must be run against a tape.
;; (cons st a) is the state and symbol look-up element.

(defn next-states (table st a)
  (if (nlistp table)
      nil
      (if (equal (cons st a) (caar table))
          (nexts (car table))
          (next-states (cdr table) st a))))

(defn next-states-list (table states a)
  (if (nlistp states)
      nil
      (union
       (next-states table (car states) a)
       (next-states-list table (cdr states) a))))

(defn cc-name (char cc)
 (if (nlistp cc)
     'character-class-not-defined
     (if (member char (cadar cc))
         (caar cc)
         (cc-name char (cdr cc)))))

(defn all-regular-expressions-for-state (state finals)
 (if (nlistp finals)
     nil
     (if (equal state (caar finals))
         (append (list (cdar finals))
                 (all-regular-expressions-for-state state (cdr finals)))
         (all-regular-expressions-for-state state (cdr finals)))))

(defn all-regular-expressions (states finals)
 (if (nlistp states)
     nil
     (append (all-regular-expressions-for-state (car states) finals)
             (all-regular-expressions (cdr states) finals))))

;; The function accept1 returns a list of all regular expressions matching 
;; the states in finals. If there are no such expressions, nil is returned.

(defn accept1 (table states finals tape cc)
 (if (nlistp tape)
     (all-regular-expressions states finals)
     (accept1 table
              (next-states-list table states
                                (cc-name (car tape) cc))
              finals
              (cdr tape)
              cc)))

(defn accepting-regular-expressions (fsa cc tape)
 (accept1 (table fsa) (starts fsa) (finals fsa) tape cc))

(defn accept (fsa cc tape)
 (listp (accepting-regular-expressions fsa cc tape)))

;; ---------------------------------------------------------------------------
;; Proof
;; ---------------------------------------------------------------------------

;; I need the concept of "what does it mean to be a prefix?" prefixp 
;; returns T if a is a prefix of b. Note that nlisps are prefixes of anything.

(defn prefixp (a b)
    (if (nlistp a)
        T
        (if (listp b)
            (if (equal (car a) (car b))
                (prefixp (cdr a) (cdr b))
                F)
            F)))

;; prefixp is transitive.

(prove-lemma prefixp-transitive (rewrite)
               (implies (and (prefixp a b)
                             (prefixp b c))
                        (prefixp a c)))

;; The function consl conses x onto each element in l. I need this in
;; order to construct all the prefixes for a list.

(defn consl (x l)
   (if (listp l)
       (cons (cons x (car l))
             (consl x (cdr l)))
       (list (list x)))); changed this case

;; This is all prefixes without the nil prefix. They happen to be sorted 
;; longest first, but I will not use that fact.

(defn all-prefixes (tape)
  (if (nlistp tape)
      nil
      (consl (car tape) (all-prefixes (cdr tape)))))

;; When does a list l contain only prefixes of full?

(defn all-prefixp (l full)
  (if (nlistp l)
      T
      (and (prefixp (car l) full)
           (all-prefixp (cdr l) full))))

(prove-lemma all-prefixp-all-prefixes (rewrite)
 (all-prefixp (all-prefixes tape) tape))

;; When are all the elements of a list accepting tapes for the 
;; automaton nfsa/cc?

(defn all-accepting (prefixes nfsa cc)
  (if (nlistp prefixes)
      nil
      (if (accept nfsa cc (car prefixes))
          (cons (car prefixes) (all-accepting (cdr prefixes) nfsa cc))
          (all-accepting (cdr prefixes) nfsa cc))))

(prove-lemma all-prefixp-all-accepting (rewrite)
 (implies (all-prefixp x y)
          (all-prefixp (all-accepting x nfsa cc) y)))

;; This function expresses the concept of longest element of a list  -  the
;; longest-to-date is kept around until the entire list has been seen. If I
;; find something longer, that is then the longest-to-date.

(defn longest1 (rest longest-to-date)
 (if (nlistp rest)
     longest-to-date
     (if (lessp (length longest-to-date)
                (length (car rest)))
         (longest1 (cdr rest) (car rest))
         (longest1 (cdr rest) longest-to-date))))

(prove-lemma prefixp-longest1 (rewrite)
 (implies (and (all-prefixp rest tape)
               (prefixp longest-to-date tape))
          (prefixp (longest1 rest longest-to-date) tape)))

(defn longest (l)
 (if (nlistp l)
     nil
     (longest1 l (car l))))

(prove-lemma prefixp-longest (rewrite)
 (implies (all-prefixp l tape)
          (prefixp (longest l) tape)))

;; This function delivers the longest of all the accepting prefixes of tape.

(defn lop (nfsa cc tape)
 (longest (all-accepting (all-prefixes tape) nfsa cc )))

;; ---------------------------------------------------------------------------
;; Theorem 1: Prefixp longest accepting prefix
;; ---------------------------------------------------------------------------

(prove-lemma all-prefixp-all-accepting-all-prefixes (rewrite)
 (all-prefixp (all-accepting (all-prefixes tape) nfsa cc) tape))

(prove-lemma prefixp-lop (rewrite)
 (prefixp (lop nfsa cc tape) tape)
  ((use (prefixp-longest (l (all-accepting (all-prefixes tape) nfsa cc))
                          (tape tape)))))

;; ---------------------------------------------------------------------------
;; Theorem 2: longest accepting prefix really accepts
;; ---------------------------------------------------------------------------
        
(defn accept-all (l nfsa cc)
 (if (nlistp l)
     T
     (and (accept nfsa cc (car l))
          (accept-all (cdr l) nfsa cc))))
     
(prove-lemma member-accept-all-accepts (rewrite)
 (implies (and (accept-all l nfsa cc)
               (member p l))
          (accept nfsa cc p)))

(prove-lemma accept-all-all-accepting (rewrite)
 (accept-all (all-accepting x nfsa cc) nfsa cc))

(prove-lemma member-longest1 (rewrite)
      (implies (not (equal (longest1 x z) z))
               (member (longest1 x z) x)))

(prove-lemma member-longest (rewrite)
 (implies (listp l)
           (member (longest l) l)))

;; This lemma never seemed to prove on a SPARC, but on a Pentium-90 it
;; zipped through in less time than you need to drink a cup of coffee!

(prove-lemma helper (rewrite)
 (implies (and (accept-all l nfsa cc) 
               (listp l))
          (accept nfsa cc (longest l))))

;; The theorem should have as its hypothesis something like
;; (or (accepts-longest-prefix ...)
;;     (accepts-no-prefix ...)
;; So I restate this to be: if the longest prefix is not nil, then it
;; accepts. If the longest prefix IS nil (for epsilon productions) then we
;; have the problem of deciding their acceptance.

(prove-lemma accepts-lop ()
 (implies (and (listp tape)
               (not (equal (lop nfsa cc tape) nil)))
          (accept nfsa cc (lop nfsa cc tape)))
          ((use (helper (l (all-accepting (all-prefixes tape) nfsa cc))
               (tape tape))))))

;; ---------------------------------------------------------------------------
;; Theorem 3: longest accepting prefix is really the longest one
;; ---------------------------------------------------------------------------

;; The definition of longest is twofold, it has to be a member and there can
;; be none larger.

(defn none-larger (x l)
 (if (nlistp l)
     T
     (if (lessp (length x) (length (car l)))
         F
         (none-larger x (cdr l)))))

(defn longestp (x l)
  (and (member x l)
       (none-larger x l)))

(prove-lemma not-lessp-length-longest1-other (rewrite)
 (not (lessp (length (longest1 v z))
                      (length z))))

(prove-lemma none-larger-longest1 (rewrite)
 (none-larger (longest1 v z) v))

;; This gets accepted using generalization THREE times!

(prove-lemma accepting-prefix-is-longest ()
 (implies (and (listp tape)
               (not (equal (lop nfsa cc tape) nil)))
          (longestp (lop nfsa cc tape) 
                    (all-accepting (all-prefixes tape) nfsa cc))))

;; ---------------------------------------------------------------------------
;; Now we have to make something useful out of the prefix: a token
;; ---------------------------------------------------------------------------

(defn longest-prefix-token (nfsa cc prefix)
 (mk-token (car (accepting-regular-expressions nfsa cc prefix))
              prefix))

;; Once a token has been made out of the longest prefix, I have to continue.

(defn remove-common-prefix (a b)
  (if (nlistp a)
      b
      (if (nlistp b)
          nil
          (if (equal (car a) (car b))
              (remove-common-prefix (cdr a) (cdr b))
              nil))))

;; This lemma is needed for the termination argument in split.

(prove-lemma remove-common-prefix-lessp (rewrite)
 (implies (and (prefixp a b)
               (listp a)
               (listp b))
          (equal (lessp (length (remove-common-prefix a b)) (length b))
                 T)))
(disable lop)

;; Now one must split off the longest prefix token. Note that Ie 
;; have to exclude epsilon prefixes or I have no termination argument!

(defn split (nfsa cc tape)
 (if (nlistp tape)
     tape
     (let ((prefix (lop nfsa cc tape)))
       (if (equal (length prefix) 0)
           (cons (mk-token 'lexicographic-error tape) nil)
           (cons (longest-prefix-token nfsa cc prefix)
                 (split nfsa cc (remove-common-prefix prefix tape))))))
 ((lessp (length tape))))
        
;; And the theorem for split is that it splits the tape, i.e. collecting up
;; the token-values gives us the tape again.

(defn collect-values (toklist)
 (if (nlistp toklist)
     toklist
     (if (not (tokenp (car toklist)))
         'not-a-token-list
         (append (token-value (car toklist))
                 (collect-values (cdr toklist))))))

(prove-lemma plistp-remove-common-prefix (rewrite)
 (implies (plistp tape)
          (plistp (remove-common-prefix a tape))))

(prove-lemma collect-values-cons (rewrite)
 (implies (tokenp a)
          (equal (collect-values (cons a b))
                 (append (token-value a) (collect-values b)))))

(prove-lemma append-remove-common-prefix (rewrite)
 (implies (prefixp a b)
          (equal (append a (remove-common-prefix a b))
                 b)))

; The nasty induction structure must be spoon-fed to the prover.

(defn split-splits-hint (nfsa cc tape)
  (if (or (nlistp tape)
          (nlistp (lop nfsa cc tape)))
      T
      (cons (lop nfsa cc tape)
            (split-splits-hint 
             nfsa cc (remove-common-prefix (lop nfsa cc tape) tape))))
 ((lessp (length tape))))

(prove-lemma split-splits (rewrite)
 (implies (plistp tape)
          (equal (collect-values (split nfsa cc tape))
                 tape))
  ((do-not-generalize T)
   (induct (split-splits-hint nfsa cc tape ))))

(deftheory scanning-defs
 (SPLIT-SPLITS-HINT COLLECT-VALUES REMOVE-COMMON-PREFIX LONGEST-PREFIX-TOKEN
  SPLIT LONGESTP NONE-LARGER ACCEPT-ALL LOP LONGEST LONGEST1 ALL-ACCEPTING
  ALL-PREFIXP ALL-PREFIXES CONSL PREFIXP ACCEPT ACCEPTING-REGULAR-EXPRESSIONS
  ACCEPT1 ALL-REGULAR-EXPRESSIONS ALL-REGULAR-EXPRESSIONS-FOR-STATE CC-NAME
  NEXT-STATES-LIST NEXT-STATES NDFSAP WF-TABLE TRANSITIONP NEXTS INPUT STATE
  MK-TRANSITION FSAP FSA* ))

(disable-theory scanning-defs)

(deftheory scanning-proofs 
 (SPLIT-SPLITS APPEND-REMOVE-COMMON-PREFIX
  COLLECT-VALUES-CONS PLISTP-REMOVE-COMMON-PREFIX REMOVE-COMMON-PREFIX-LESSP
  ACCEPTING-PREFIX-IS-LONGEST NONE-LARGER-LONGEST1
  NOT-LESSP-LENGTH-LONGEST1-OTHER ACCEPTS-LOP HELPER MEMBER-LONGEST
  MEMBER-LONGEST1 ACCEPT-ALL-ALL-ACCEPTING MEMBER-ACCEPT-ALL-ACCEPTS
  PREFIXP-LOP ALL-PREFIXP-ALL-ACCEPTING-ALL-PREFIXES PREFIXP-LONGEST
  PREFIXP-LONGEST1 ALL-PREFIXP-ALL-ACCEPTING ALL-PREFIXP-ALL-PREFIXES
  PREFIXP-TRANSITIVE ))

(disable-theory scanning-proofs)
;; ---------------------------------------------------------------------------
;;     ~/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))
;; ---------------------------------------------------------------------------
;;   ~/events/toktrans-2.events
;; ---------------------------------------------------------------------------

;; This token transformation function looks through the token list for tokens 
;; that are in the domain of the replace alist, and replaces them with the 
;; range component. This is in contrast to toktrans-3, which has a default 
;; value to be used when the value is not found. Perhaps these two could be 
;; combined, with the default value being 'error!

(enable-theory tokens)
(enable-theory lists)

(defn make-replace (toks name dom replace-list)
  (if (nlistp toks)
      toks
      (if (and (equal (token-name (car toks)) name)
               (member (car (token-value (car toks))) dom))
          (cons (mk-token (value (car (token-value (car toks))) replace-list)
                          (token-value (car toks)))
                (make-replace (cdr toks) name dom replace-list))
          (cons (car toks)
                (make-replace (cdr toks) name dom replace-list)))))


;; I am using this as an optimization, selecting the domain once for the
;; whole token list instead of constructing it for every token.
;; This is the token transformation function toktrans-2.

(defn replace (toks name replace-list)
 (if (listp replace-list)
     (let ((dom (domain replace-list)))
       (make-replace toks name dom replace-list))
     toks))

;; I need a stepper that will demonstrate that everything else stays the
;; same and that the domain tokens get replaceed.

(defn replace-step (source target name replace-list)
 (if (nlistp source)
     (nlistp target)
      (if (and (equal (token-name (car source)) name)
               (member (car (token-value (car source))) (domain replace-list)))
         (and (equal (car target) 
                     (mk-token (value (car (token-value (car source))) 
                                      replace-list)
                          (token-value (car source))))
              (replace-step (cdr source) (cdr target) name replace-list))
         (and (equal (car source) (car target))
              (replace-step (cdr source) (cdr target) name replace-list)))))
              
;; When is replace correct?
;; When all tokens not in the domain of replace-list remain the same
;; and the tokens in the domain are replaced by the values from the alist.

(prove-lemma toktrans-2-main-theorem (rewrite)
 (implies (and (token-listp toks)
               (listp replace-list))
          (replace-step toks (replace toks name replace-list) 
                        name replace-list)))
;; ---------------------------------------------------------------------------
;;   ~/events/toktrans-3.events
;; ---------------------------------------------------------------------------

;; This token transformation function looks through the token list for 
;; tokens with  token-name equal to name. The value is looked up in a table, 
;; as in toktrans-2. If there is no entry in the table, a default value 
;; is substituted. 

(enable-theory tokens)

(defn make-key-words (toks name dom key-words-list default)
  (if (nlistp toks)
      toks
      (if (equal (token-name (car toks)) name)
	  (if (member (token-value (car toks)) dom)
	      (cons (mk-token (value (token-value (car toks)) 
				     key-words-list) 
			      (token-value (car toks)))
		    (make-key-words (cdr toks) 
				    name dom key-words-list default))
	      (cons (mk-token default 
                              (token-value (car toks)))
		    (make-key-words (cdr toks) 
				    name dom key-words-list default)))
	  (cons (car toks)
		(make-key-words (cdr toks) 
				name dom key-words-list default)))))

(defn determine-key-words (toks name key-words-list default)
 (if (listp key-words-list)
     (let ((dom (domain key-words-list)))
       (make-key-words toks name dom key-words-list default))
     toks))

(defn key-words-step (source target name key-words-list default)
 (if (nlistp source)
     (nlistp target)
      (if (equal (token-name (car source)) name)
	  (if (member (token-value (car source)) (domain key-words-list))
	      (and (equal (car target) 
                          (mk-token (value (token-value (car source)) 
					   key-words-list) 
                                    (token-value (car source))))
		   (key-words-step (cdr source) (cdr target) 
				   name key-words-list default))
	      (and (equal (car target) 
                          (mk-token default 
                                    (token-value (car target))))
		   (key-words-step (cdr source) (cdr target) 
				   name key-words-list default)))
	  (and (equal (car source) (car target))
	       (key-words-step (cdr source) (cdr target) 
			       name key-words-list default)))))

(prove-lemma toktrans-3-main-theorem (rewrite)
 (implies (and (token-listp toks)
	       (listp key-words-list))
	  (key-words-step 
	       toks 
               (determine-key-words toks name key-words-list default) 
               name key-words-list default)))
;; ---------------------------------------------------------------------------
;; ~/events/toktrans-4.events
;; ---------------------------------------------------------------------------

(enable-theory tokens)
(enable-theory lists)

;; This is a token transformation function for converting lists of digit 
;; characters which are contained in token values to decimal integers. The 
;; function is called integer-convert.
;; It only works on the INTEGER tokens, and leaves all other tokens intact.
;; It is modelled on Bill Bevier's positional number etude.
;; The digits must first be converted from ASCII values to digits.

(defn ascii-zero () 48)
(defn ascii-nine () 57)

(defn digit-zero () 0)
(defn digit-nine () 9)

(defn base () 10)

;; This is the predicate for finding the tokens that toktrans-4 will work on.

(defn is-integer-token (tok)
 (equal (token-name tok) 'INTEGER))

;; This function checks that the list consists of digits less than b.

(defn just-digits-less-than-b (l b) 
 (if (listp l)
     (and (numberp (car l))
          (lessp (car l) b) ; Each digit must be less than the base
          (just-digits-less-than-b (cdr l) b))
     (equal l nil)))

;; This is the Horner method for computing a natural number from
;; a positional number representation l and a base b.
;; This means the list l must be in the reverse digit form - but that 
;; saves worrying about exponents and such.

(defn pn-to-nat (l b)
  (if (listp l) 
      (plus (car l)
            (times (pn-to-nat (cdr l) b) b))
      (digit-zero)))  

;; This is the conversion function that returns the digit for an ASCII code.
;; This function coerces all non-digital digits to 0, 

(defn ascii-to-digit (ascii)
 (if (or (lessp ascii (ascii-zero))
         (lessp (ascii-nine) ascii))
     (digit-zero)
     (difference ascii (ascii-zero))))

(defn valid-ascii-digit-p (ascii)
 (and (numberp ascii)
      (not (or (lessp ascii (ascii-zero))
               (lessp (ascii-nine) ascii)))))

(defn ascii-to-digits (l)
 (if (nlistp l)
     l
     (cons (ascii-to-digit (car l))
           (ascii-to-digits (cdr l)))))

(prove-lemma plistp-ascii-to-digits (rewrite)
 (equal (plistp (ascii-to-digits w))
        (plistp w)))

;; This is the token transformation function toktrans-4.

(defn integer-convert (toks)
 (if (nlistp toks)
     toks
     (if (is-integer-token (car toks))
         (let ((value (ascii-to-digits (token-value (car toks)))))
           (if (just-digits-less-than-b value (base))
               (cons (mk-token (token-name (car toks))
                            (pn-to-nat (reverse value) (base)))
                     (integer-convert (cdr toks)))
               'token-error))
         (cons (car toks) (integer-convert (cdr toks))))))

;; This is the retrieve function for one number, it converts a natural 
;; number to a positional number with digits of base b.

(defn nat-to-pn (n b)   
 (if (lessp 1 b)
     (if (zerop n)
         nil
         (cons (remainder n b)
               (nat-to-pn (quotient n b) b )))
     nil))

;; There have to be inverse functions for ascii-to-digits as well.

(defn digit-to-ascii (digit)
 (plus digit (ascii-zero))))

(defn digits-to-ascii (digits)
 (if (nlistp digits)
     digits
     (cons (digit-to-ascii (car digits))
           (digits-to-ascii (cdr digits)))))

;; When does a list consist of valid ascii digits?

(defn valid-ascii-digits-p (l)  
 (if (nlistp l)
     T
     (and (valid-ascii-digit-p (car l))
          (valid-ascii-digits-p (cdr l)))))

(prove-lemma d-a-inverse-1 (rewrite)
 (implies (and (listp value)
               (valid-ascii-digits-p value))
          (equal (digits-to-ascii (ascii-to-digits value))
                 (cons (digit-to-ascii (ascii-to-digit (car value)))
                       (digits-to-ascii (ascii-to-digits (cdr value)))))))
                 
(prove-lemma d-a-inverse-2 (rewrite)
 (implies (and (listp value)
               (valid-ascii-digits-p value))
          (equal (digits-to-ascii (ascii-to-digits value))
                 value))
 ((induct (length value))))

;; This is the retrieve function for a list. Note that I have to reverse 
;; the result before constructing the token.

(defn convert-back (toks)
 (if (nlistp toks)
     toks
     (if (is-integer-token (car toks))
           (cons (mk-token 
                  (token-name (car toks)) 
                  (reverse (digits-to-ascii 
                            (nat-to-pn (token-value (car toks)) 
                                       (base)))))
                 (convert-back (cdr toks)))
         (cons (car toks) (convert-back (cdr toks))))))


;; This lemma is to show that this direction is an inverse.

(prove-lemma inverse1 (rewrite)
 (implies (and (lessp 1 b)
               (numberp n)
               (numberp b))
          (equal (pn-to-nat (nat-to-pn n b) b)
                 n)))

;; One has to know if the positional notation lists are well-formed. 
;; Leading zeros are not acceptable.

(defn lastdigit (l)
     (if (listp l) 
         (if (not (equal (cdr l) nil))
             (lastdigit (cdr l))
             (car l))
         F))

(defn no-leading-zeros (l)
     (not (equal (lastdigit l) (digit-zero))))

(defn well-formed-pn (l b)
     (and (lessp 1 b)
              (plistp l)
              (numberp b)
              (no-leading-zeros l)
              (just-digits-less-than-b l b)))

;; This is the interesting inverse function.

(prove-lemma inverse2 (rewrite)
 (implies (well-formed-pn l b)
          (equal (nat-to-pn (pn-to-nat l b) b)
                 l)))

;; These are the lemmata needed for the proof of the main theorem.

;; If x is a just-digits-less-than-b, reversing it preserves 
;; just-digits-less-than-b-ness

(prove-lemma toktrans-4-help1 (rewrite)
  (implies (just-digits-less-than-b x b)
          (just-digits-less-than-b (reverse x) b)))

(prove-lemma toktrans-4-help2 (Rewrite)
 (implies (and (plistp x)
               (just-digits-less-than-b (reverse x) b))
          (just-digits-less-than-b x b))
 ((use (toktrans-4-help1 (x (reverse x)) (b b)))))

;; I need to know that all the integer token values are well formed.

(defn integer-tokens-well-formed (toks)
 (if (nlistp toks)
     T
     (if (is-integer-token (car toks))
         (and (no-leading-zeros 
               (reverse (ascii-to-digits (token-value (car toks)))))
              (valid-ascii-digits-p (token-value (car toks)))         
              (just-digits-less-than-b 
               (reverse (ascii-to-digits (token-value (car toks)))) (base))
              (plistp (ascii-to-digits (token-value (car toks))))
              (integer-tokens-well-formed (cdr toks)))
         (integer-tokens-well-formed (cdr toks)))))

(prove-lemma toktrans-4-help3 (rewrite)
 (implies (and (not (just-digits-less-than-b 
                     (ascii-to-digits (token-value (car z))) (base)))
               (is-integer-token (car z))
               (listp z))
          (not (integer-tokens-well-formed z))))

(prove-lemma ascii-to-digits-append (rewrite)
 (equal (ascii-to-digits (append a b))
        (append (ascii-to-digits a) (ascii-to-digits b))))

(prove-lemma reverse-ascii-to-digits (rewrite)
 (implies (valid-ascii-digits-p l)
          (equal (reverse (ascii-to-digits l))
                 (ascii-to-digits (reverse l)))))

(prove-lemma valid-ascii-digits-p-append (rewrite)
 (equal (valid-ascii-digits-p (append a b))
        (and (valid-ascii-digits-p a) (valid-ascii-digits-p b))))
        
(prove-lemma valid-ascii-digits-p-reverse (rewrite)
 (equal (valid-ascii-digits-p (reverse w))
        (valid-ascii-digits-p w)))

(prove-lemma reverse-d-a-reverse (rewrite)
 (implies (and (not (equal (lastdigit (ascii-to-digits (reverse w))) 0))
                    (valid-ascii-digits-p w)
                    (just-digits-less-than-b (ascii-to-digits (reverse w))
                                             10)
                    (plistp w))
               (equal (reverse (digits-to-ascii (ascii-to-digits (reverse w))))
                      w))
 ((use (d-a-inverse-2 (value (reverse w)))
       (reverse-reverse (l w)))))

; -----------------------------------------------------
;      Main theorem for toktrans-4
; -----------------------------------------------------

(prove-lemma toktrans-4-main-theorem (rewrite)
 (implies (and (token-listp toks)
               (integer-tokens-well-formed toks)
               (listp toks))
          (equal (convert-back (integer-convert toks))
                 toks))
 ((do-not-generalize T)))
;; ---------------------------------------------------------------------------
;;   ~/events/toktrans-5.events
;; ---------------------------------------------------------------------------

(enable-theory tokens)

;; This token transformation function finds and removes continuations from a 
;; token list.
;; From the occam Reference Manual: 
;; "A long statement may be broken immediately after one of the following: 
;; an operator, a comma, a semi-colon, an assignment, or the keywords 
;; IS, FROM or FOR. A statement can be broken over several lines, providing the
;; continuation is indentated at least as much as the first line of the 
;; statement." In this token transformation function, I remove any 
;; indentation that immediately follows the elements from the list 
;; that are contained in PL0R.

(defn is-kw-indentation (x)   
  (equal (token-name x) 'indent))

(defn is-indentation (x)   
  (and (is-kw-indentation x)
       (numberp (token-value x))))

(prove-lemma tokenp-is-kw-indentation (rewrite)
 (implies (is-kw-indentation x)
          (tokenp x)))

;; Since empty lines disturb the proof as well, they are removed.

(defn remove-empty-lines (l)
  (if (nlistp l)
      l
      (if (and (is-kw-indentation (car l))
               (or (nlistp (cdr l))
                   (is-kw-indentation (cadr l))))
          (remove-empty-lines (cdr l))
          (cons (car l) (remove-empty-lines (cdr l))))))

(defn no-empty-lines (l)
 (if (nlistp l)
     t
     (if (and (is-kw-indentation (car l))
              (or (nlistp (cdr l))
                  (is-kw-indentation (cadr l))))
         f
         (no-empty-lines (cdr l)))))

(prove-lemma main-theorem-toktrans-5a (rewrite) 
  (no-empty-lines (remove-empty-lines l)))

(prove-lemma no-empty-lines-meaning (rewrite)
 (implies (and (no-empty-lines toks)
               (is-kw-indentation (car toks)))
          (not (is-kw-indentation (cadr toks)))))

;; This function removes the continuations.

(defn discontinue (toks continue-list)
 (if (nlistp toks)
     toks
     (if (member (token-name (car toks)) continue-list)
         (if (is-kw-indentation (cadr toks))
             (cons (car toks) (discontinue (cddr toks) continue-list))
             (cons (car toks) (discontinue (cdr toks) continue-list)))
         (cons (car toks) (discontinue (cdr toks) continue-list)))))

(defn no-continuations-p (toks continue-list)
  (if (nlistp toks)
      T
      (if (member (token-name (car toks)) continue-list)
          (if (is-kw-indentation (cadr toks))
              F
              (no-continuations-p (cdr toks) continue-list))
          (no-continuations-p (cdr toks) continue-list))))

(prove-lemma discontinue-car (rewrite)
 (implies (listp toks)
          (equal (car (discontinue toks list))
                 (car toks))))

;; The main theorem for toktrans-5b insists on no empty lines.

(prove-lemma main-theorem-toktrans-5b (rewrite)
 (implies (no-empty-lines toks)
          (no-continuations-p (discontinue toks continue-list) continue-list))
          ((disable is-kw-indentation)))

(defn toktrans-5 (toks continue-list)
 (remove-empty-lines 
   (discontinue toks continue-list)))
;; ---------------------------------------------------------------------------
;;     ~/events/toktrans-6.events
;; ---------------------------------------------------------------------------

(enable-theory tokens)
(enable-theory lists)

;; This token transformation function prepares for the indentation work to be 
;; done in toktrans-7. It looks for the indentation tokens and replaces the 
;; value, which is a carriage return followed by 0 or more blanks, by the
;; number of blanks found. 
;; The halving of the indentation (2 blanks = 1 level) is done here as well.
;; The function toktrans-6a removes the CR and puts in the number of blanks, 
;; the function toktrans-6b halves.

;; ------------ replace chars by length --------------
;;              toktrans 6a

(defn prepare-indentations (toks)
 (if (nlistp toks)
     toks
     (if (is-kw-indentation (car toks))
         (cons
          (mk-token
           (token-name (car toks))
           (sub1 (length (token-value (car toks)))))
          (prepare-indentations (cdr toks)))
         (cons (car toks) (prepare-indentations (cdr toks))))))

(defn ok-indentation-value (l1 l2)
 (if (nlistp l1)
     (nlistp l2)
     (and (if (is-kw-indentation (car l1))
              (and (equal (token-name (car l1))
                          (token-name (car l2)))
                   (equal (token-value (car l2))
                          (sub1 (length (token-value (car l1))))))
              (equal (car l1) (car l2)))
          (ok-indentation-value (cdr l1) (cdr l2)))))

(prove-lemma toktrans-6a-main-theorem (rewrite)
 (implies (and (token-listp toks)
               (listp toks))
          (ok-indentation-value toks (prepare-indentations toks))))

;; ------------ divide length by 2 --------------
;;              toktrans6b

;; The function half returns half of a number (rounded down).

(defn half (n) (quotient n 2))

;; The function halve is applied to a list, not a token!

(defn halve (l)
  (if (nlistp l)
      l
      (if (is-indentation (car l))
          (cons (mk-token (token-name (car l)) 
                          (half (token-value (car l))))
                (halve (cdr l)))
          (cons (car l)
                (halve (cdr l))))))

(defn indent-positions-preserved (l1 l2)
  (if (nlistp l1)
      (equal l1 l2) 
      (if (is-indentation (car l1))
          (and (is-indentation (car l2))
               (indent-positions-preserved (cdr l1) (cdr l2)))
          (and (equal (car l1) (car l2))
               (indent-positions-preserved (cdr l1) (cdr l2))))))

(prove-lemma indent-positions-preserved-halve (rewrite)
  (indent-positions-preserved l (halve l)))

(defn collect-indents (l)
  (if (nlistp l)
      nil 
      (if (is-indentation (car l))
          (cons (fix (token-value (car l)))
                (collect-indents (cdr l)))
          (collect-indents (cdr l)))))

(prove-lemma collect-indents-nlistp (rewrite)
 (implies (nlistp l)
          (equal (collect-indents l) nil)))

(defn halved-listp (l1 l2)
  (if (nlistp l1)
      (nlistp l2)
      (and (equal (car l2) (half (car l1)))
           (halved-listp (cdr l1) (cdr l2)))))

(prove-lemma indents-halved (rewrite)
  (halved-listp (collect-indents l)
                (collect-indents (halve l))))

;; ----- combine both passes -----

(defn toktrans-6 (toks)
 (halve (prepare-indentations toks)))

(defn ok-toktrans-6 (l1 l2)
 (if (nlistp l1)
     (nlistp l2)
     (and (if (is-kw-indentation (car l1))
              (and (equal (token-name (car l1))
                          (token-name (car l2)))
                   (equal (token-value (car l2))
                          (half (sub1 (length (token-value (car l1)))) )))
              (equal (car l1) (car l2)))
          (ok-toktrans-6 (cdr l1) (cdr l2)))))

(prove-lemma main-theorem-toktrans-6 (rewrite)
  (ok-toktrans-6 toks (toktrans-6 toks)))

(disable-theory tokens)
(disable-theory lists)
;; ---------------------------------------------------------------------------
;; ~/events/toktrans-7.events 
;; ---------------------------------------------------------------------------

(enable-theory tokens)                                  
(enable-theory lists)

;; These definitions and theorems are from an old lists library.

(defn firstn (n l)
  (if (not (listp l))
      nil
      (if (zerop n)
          nil
          (cons (car l) (firstn (sub1 n) (cdr l))))))

(defn nthcdr (n l)
  (if (not (listp l))
      l
      (if (zerop n)
          l
          (nthcdr (sub1 n) (cdr l)))))

(prove-lemma listp-append (rewrite)
  (equal (listp (append a b))
         (or (listp a)
             (listp b))))

(prove-lemma nthcdr-append (rewrite)
  (equal (nthcdr n (append a b))
         (if (leq n (length a))
             (append (nthcdr n a) b)
             (nthcdr (difference n (length a)) b))))

(prove-lemma append-firstn-nthcdr (rewrite)
  (equal (append (firstn i l) (nthcdr i l))
         l))

;; The specification function diff-cycle states the relationship between 
;; absolute and relative indentations using a proper difference function.

(defn pdiff (i j)
  (if (lessp (fix i) (fix j))
      (minus (difference j i))
      (if (equal (fix i) (fix j))
          0
          (difference i j))))

(defn diff-cycle1 (l orig prev)
  (if (nlistp l)
      (list (pdiff orig prev))
      (cons (pdiff (car l) prev)
            (diff-cycle1 (cdr l) orig (car l)))))

(prove-lemma diff-cycle1-nlistp (rewrite)
             (implies (nlistp l)
                      (equal (diff-cycle1 l orig prev)
                             (list (pdiff orig prev)))))

(prove-lemma diff-cycle1-listp (rewrite)
             (implies (listp l)
                      (equal (diff-cycle1 l orig prev)
                             (cons (pdiff (car l) prev)
                                   (diff-cycle1 (cdr l) orig (car l))))))

(defn diff-cycle (l old)
  (diff-cycle1 l old old))


; First determine the magnitude and sign of the indentation. Use a
; fresh token name, 'relative, for this kind of token.
; This means that the resulting list remains a token-listp, which will
; go easy on the induction proof.

(defn is-relative (tok)
  (and (tokenp tok)
       (equal (token-name tok) 'relative)
       (or (numberp (token-value tok))
           (and (negativep (token-value tok))
                (not (equal (negative-guts (token-value tok)) 0))))))

(defn emit-relative (i j)
  (if (lessp (fix i) (fix j))
      (mk-token 'relative (minus (difference j i)))
      (if (equal (fix i) (fix j))
          (mk-token 'relative 0)
          (mk-token 'relative (difference i j)))))

;; Unfortunately, emit1 has to watch out for indentations which are not.
;; well formed. I will ignore such indentations.

(defn emit1 (l orig prev)
  (if (nlistp l)
      (list (emit-relative orig prev))
      (if (is-kw-indentation (car l))
          (if (is-indentation (car l))
              (cons (emit-relative (token-value (car l)) prev)
                    (emit1 (cdr l) orig (token-value (car l))))
              ; should be an error
              (emit1 (cdr l) orig prev))
          (cons (car l) (emit1 (cdr l) orig prev)))))

(defn emit (l old)
  (emit1 l old old))

;; This is the meaning function for the relative indentations.

(defn relative-meaning (l)
  (if (nlistp l)
      nil
      (if (is-relative (car l))
          (cons (token-value (car l))
                (relative-meaning (cdr l)))
          (relative-meaning (cdr l)))))

;; There are no 'relative tokens left in the list.

(defn relative-free (l)  
  (if (nlistp l)
      T
      (if (tokenp (car l))
          (and (not (equal (token-name (car l)) 'relative))
               (relative-free (cdr l)))
          F)))

(prove-lemma diff-cycle1-not-numberp (rewrite)
             (implies  (not (numberp v))
                       (equal (diff-cycle1 z orig v)
                              (diff-cycle1 z orig 0))))

(prove-lemma emit1-theorem (rewrite)
             (implies (and (relative-free l)
                           (token-listp l))
                      (equal (relative-meaning (emit1 l orig prev))
                             (diff-cycle1 (collect-indents l) orig prev))))

(prove-lemma emit-theorem (rewrite)
             (implies (and (relative-free l)
                           (token-listp l))
                      (equal (relative-meaning (emit l old))
                             (diff-cycle (collect-indents l) old)))
             ((do-not-induct T)))

;; This makes a list which contains n copies of v.

(defn my-make-list (v n)
  (if (or (zerop n)
          (not (numberp n)))
      nil
      (cons v (my-make-list v (sub1 n)))))

(prove-lemma length-my-make-list (rewrite)
             (equal (length (my-make-list v n))
                    (fix n)))

(prove-lemma not-numberp-my-make-list (rewrite)
             (implies (not (numberp n))
                      (equal (my-make-list x n) nil)))

(prove-lemma listp-my-make-list (rewrite)
             (implies (lessp 0 (fix n))
                      (listp (my-make-list x n))))

(prove-lemma my-make-list-zero (rewrite)
             (implies (equal n 0)
                      (equal (my-make-list x n) nil)))

(prove-lemma plist-my-make-list (rewrite)
             (equal (plist (my-make-list v n))
                    (my-make-list v n)))

;; Now all I have to do is go through and expand the 'relative tokens
;; to the ni, si, and bi stuff the grammar needs.

(defn ni-si-bis (n)
  (if (equal n 0)
      (my-make-list (mk-token 'si nil) 1)
      (if (lessp 0 n)
          (my-make-list (mk-token 'ni nil) n)
          (my-make-list (mk-token 'bi nil) (negative-guts n)))))

(defn relative-to-ni-si-bi (toks)
  (if (nlistp toks)
      toks
      (if (is-relative (car toks))
          (append (ni-si-bis (token-value (car toks)))
                  (relative-to-ni-si-bi (cdr toks)))
          (cons (car toks) (relative-to-ni-si-bi (cdr toks))))))

;; The specification is more complex than that of the implementation. The 
;; function matches cdrs down the toks, seeing if it matches the 
;; relative value.

(defn matches (n toks)
  (if (nlistp toks)
      F
      (if (equal n 0)
          (equal (car toks) (mk-token 'si nil))
          (if (lessp 0 n)
              (equal (firstn n toks) (my-make-list (mk-token 'ni nil) n))
              (equal (firstn (negative-guts n) toks) 
                     (my-make-list (mk-token 'bi nil) (negative-guts n)))))))

(defn how-much (n)
  (if (equal n 0)
      1
      (if (lessp 0 n)
          (fix n)
          (negative-guts n))))

(defn relative-conversion-ok (pre post)
  (if (nlistp pre)
      ;; There should be just a number of bi tokens on the end.
      (if (nlistp post)
          T
          (and (equal (token-name (car post)) 'bi)
               (relative-conversion-ok pre (cdr post))))
      (if (is-relative (car pre))
          (and (matches (token-value (car pre)) post)
               (relative-conversion-ok 
                (cdr pre)
                (nthcdr (how-much (token-value (car pre))) post)))
          (and (equal (car pre) (car post))
               (relative-conversion-ok (cdr pre) (cdr post)))))
  ((ord-lessp (cons (add1 (length pre)) (length post)))))

;; If it has the name 'relative, it had better be well formed.

(defn all-relative-tokens-good (toks)
  (if (nlistp toks)
      T
      (if (equal (token-name (car toks)) 'relative)
          (and (is-relative (car toks))
               (all-relative-tokens-good (cdr toks)))
          (all-relative-tokens-good (cdr toks)))))

(prove-lemma firstn-my-make-list (rewrite)
 (implies (numberp x)
          (equal (firstn x (my-make-list l x))
                 (my-make-list l  x))))

(prove-lemma nthcdr-my-make-list (rewrite)
 (implies (numberp x)
          (equal (nthcdr x (my-make-list l x))
                 nil)))

(prove-lemma firstn-append-my-make-list (rewrite)
 (implies (numberp x)
          (equal (firstn x (append (my-make-list z x) foo))
                 (my-make-list z x))))
                         

(prove-lemma relative-theorem (rewrite)
 (implies (and (token-listp toks)
               (all-relative-tokens-good toks))
          (relative-conversion-ok toks
                                  (relative-to-ni-si-bi toks)))
 ((do-not-generalize t)))


;; Now I try proving some glue so I can feel good about combining the
;; passes. If toks is a token list and free of relative tokens, emit1 will
;; have the properties so that the relative conversion will go okay.

(prove-lemma glue1 (rewrite)
             (implies (and (token-listp toks)
                           (relative-free toks))
                      (all-relative-tokens-good (emit1 toks n m))))

(prove-lemma glue2 (rewrite)
 (implies (token-listp toks)
          (token-listp (emit1 toks n m))))

;; This is the indentator function.

(defn indentator (l)
 (relative-to-ni-si-bi (emit1 l 0 0)))

;; The result is free of indentation tokens

(defn indent-free (l)
 (if (nlistp l)
     (not (is-kw-indentation l))
     (if (is-kw-indentation (car l))
         F
         (indent-free (cdr l)))))

(prove-lemma indent-free-cons (rewrite)
 (implies (and (indent-free a)
               (not (is-kw-indentation b)))
          (indent-free (cons b a))))

(prove-lemma indent-free-append (rewrite)
 (implies (and (indent-free a)
               (indent-free b))
          (indent-free (append a b)))
 ((disable is-kw-indentation)))

(prove-lemma indent-free-my-make-list (rewrite)
 (implies (indent-free a) 
          (indent-free (my-make-list a n)))))

(prove-lemma indent-free-realtive-to-ni-si-bi (rewrite)
 (implies (and (token-listp x)
               (indent-free x))
          (indent-free (relative-to-ni-si-bi x))))


(prove-lemma non-wf-indentations-removed (rewrite)
 (implies (and (not (nlistp z))
               (is-kw-indentation (car z))
               (not (is-indentation (car z)))
               (numberp n))
         (equal (emit1 z m n)
                (emit1 (cdr z) m n))))

(prove-lemma indent-free-emit1 (rewrite)
 (implies (numberp n)
          (indent-free (emit1 z 0 n))))

(prove-lemma indent-free-indentator (rewrite)
 (implies (token-listp l)
          (indent-free (indentator l))))

(deftheory toktrans 
 (INDENT-FREE INDENTATOR ALL-RELATIVE-TOKENS-GOOD
  RELATIVE-CONVERSION-OK HOW-MUCH MATCHES RELATIVE-TO-NI-SI-BI NI-SI-BIS
  MY-MAKE-LIST RELATIVE-FREE RELATIVE-MEANING EMIT EMIT1 EMIT-RELATIVE
  IS-RELATIVE DIFF-CYCLE DIFF-CYCLE1 PDIFF NTHCDR FIRSTN OK-TOKTRANS-6
  TOKTRANS-6 HALVED-LISTP COLLECT-INDENTS INDENT-POSITIONS-PRESERVED HALVE
  HALF OK-INDENTATION-VALUE PREPARE-INDENTATIONS TOKTRANS-5 NO-CONTINUATIONS-P
  DISCONTINUE NO-EMPTY-LINES REMOVE-EMPTY-LINES IS-INDENTATION
  IS-KW-INDENTATION INTEGER-TOKENS-WELL-FORMED WELL-FORMED-PN NO-LEADING-ZEROS
  LASTDIGIT CONVERT-BACK VALID-ASCII-DIGITS-P DIGITS-TO-ASCII DIGIT-TO-ASCII
  NAT-TO-PN INTEGER-CONVERT ASCII-TO-DIGITS VALID-ASCII-DIGIT-P ASCII-TO-DIGIT
  PN-TO-NAT JUST-DIGITS-LESS-THAN-B IS-INTEGER-TOKEN BASE DIGIT-NINE
  DIGIT-ZERO ASCII-NINE ASCII-ZERO KEY-WORDS-STEP DETERMINE-KEY-WORDS
  MAKE-KEY-WORDS REPLACE-STEP REPLACE MAKE-REPLACE TOKEN-LISTP VALUE
  NO-DISCARDS-LEFT NON-DISCARDS-UNDISTURBED DISCARD ))

(disable-theory toktrans)

(deftheory toktrans-proofs
 (INDENT-FREE-INDENTATOR INDENT-FREE-EMIT1 NON-WF-INDENTATIONS-REMOVED
  INDENT-FREE-REALTIVE-TO-NI-SI-BI INDENT-FREE-MY-MAKE-LIST INDENT-FREE-APPEND
  INDENT-FREE-CONS 
  GLUE2 GLUE1 RELATIVE-THEOREM
  NTHCDR-MY-MAKE-LIST FIRSTN-MY-MAKE-LIST PLIST-MY-MAKE-LIST MY-MAKE-LIST-ZERO
  LISTP-MY-MAKE-LIST NOT-NUMBERP-MY-MAKE-LIST LENGTH-MY-MAKE-LIST EMIT-THEOREM
  EMIT1-THEOREM DIFF-CYCLE1-NOT-NUMBERP DIFF-CYCLE1-LISTP DIFF-CYCLE1-NLISTP
  APPEND-FIRSTN-NTHCDR NTHCDR-APPEND LISTP-APPEND 
  MAIN-THEOREM-TOKTRANS-6 INDENTS-HALVED COLLECT-INDENTS-NLISTP
  INDENT-POSITIONS-PRESERVED-HALVE TOKTRANS-6A-MAIN-THEOREM
  MAIN-THEOREM-TOKTRANS-5B DISCONTINUE-CAR NO-EMPTY-LINES-MEANING
  MAIN-THEOREM-TOKTRANS-5A TOKENP-IS-KW-INDENTATION TOKTRANS-4-MAIN-THEOREM
  VALID-ASCII-DIGITS-P-REVERSE VALID-ASCII-DIGITS-P-APPEND
  REVERSE-ASCII-TO-DIGITS ASCII-TO-DIGITS-APPEND TOKTRANS-4-HELP3
  TOKTRANS-4-HELP2 TOKTRANS-4-HELP1 INVERSE2 INVERSE1 D-A-INVERSE-2
  PLISTP-ASCII-TO-DIGITS REMAINDER-TIMES1-INSTANCE QUOTIENT-TIMES-INSTANCE
  QUOTIENT-PLUS REMAINDER-PLUS QUOTIENT-LESSP-ARG1 COMMUTATIVITY-OF-TIMES
  LESSP-QUOTIENT PLUS-REMAINDER-TIMES-QUOTIENT TIMES-ADD1 EQUAL-TIMES-0
  TIMES-ZERO PLUS-ZERO-ARG2 EQUAL-PLUS-0 COMMUTATIVITY-OF-PLUS
  FIRSTN-APPEND-MY-MAKE-LIST
  TOKTRANS-3-MAIN-THEOREM TOKTRANS-2-MAIN-THEOREM TOKTRANS-1-MAIN-THEOREM
  DISCARD-DOES-NOT-DISTURB-NON-DISCARDS ))

(disable-theory tokens)
(disable-theory lists)
;; ---------------------------------------------------------------------------
;;  ~/events/derivation.events
;; ---------------------------------------------------------------------------

;; These are the functions defining a derivation.

(enable-theory sets)
(enable-theory lists)
(enable-theory grammar)
(enable-theory tokens)

;; A Derivation is a list of Derivation Steps.
;; A Derivation Step consists of a left part, a prod and a right part.
;; A Derivation Rule is a list of Labels.

;; There will be some lists with tokens and nonterminals mixed. One needs to
;; pick the token-name out for the tokens and make a list.

(add-shell mk-Derivation-Step Undefined-DS is-derivation-step
  ((sel-left-Derivation-Step (none-of) zero)
   (sel-prod-Derivation-Step (none-of) zero) 
   (sel-right-Derivation-Step (none-of) zero)))

;; The lhs is an atom, so it must be put in a list, or append will ignore it!

(defn step-source (DS)
 (append (sel-left-Derivation-Step DS)
	 (append (list (sel-lhs (sel-prod-Derivation-Step DS)))
		 (sel-right-Derivation-Step DS))))

(defn step-target (DS)
 (append (sel-left-Derivation-Step DS)
	 (append (sel-rhs (sel-prod-Derivation-Step DS))
		 (sel-right-Derivation-Step DS))))

(defn source (Derivation)
 (if (nlistp Derivation)
     nil
     (step-source (car Derivation))))

(defn target (Derivation)
 (if (nlistp Derivation)
     nil
     (step-target (last Derivation))))

(defn deriv-rule (Derivation)
 (if (nlistp Derivation)
     nil
     (append
      (sel-label (sel-prod-Derivation-Step (car Derivation)))
      (deriv-rule (cdr Derivation)))))

(defn productions (Derivation)
 (if (nlistp Derivation)
     nil
     (union (list (sel-prod-Derivation-Step (car Derivation)))
	    (productions (cdr Derivation)))))

; This function would be a witness for a forall construct.

(defn lockstep (Derivation)
  (if (or (nlistp Derivation)
	  (nlistp (cdr Derivation)))
      T
      (and (equal (step-source (cadr Derivation))
		  (step-target (car Derivation)))
	   (lockstep (cdr Derivation)))))

;; This function, too, is for the forall. Since the lockstep checks that 
;; source and target are equal, it should suffice to test just the source here.

(defn all-in-vocab (Derivation v)
  (if (nlistp Derivation)
      T
      (and (is-string-in (step-source (car Derivation)) v)
	   (all-in-vocab (cdr Derivation) v))))

(defn is-Derivation-in (Derivation Grammar)
   (and (subsetp (productions Derivation) (sel-productions Grammar))
	(all-in-vocab Derivation (append (vocab Grammar) (list (end-of-file))))
	(lockstep Derivation)))

(defn all-rights-terminal (Derivation Terminals)
 (if (nlistp Derivation)
     T
     (and (is-string-in 
	   (sel-right-Derivation-Step (car Derivation)) Terminals)
	  (all-rights-terminal (cdr Derivation) Terminals))))

(defn all-lefts-terminal (Derivation Terminals)
 (if (nlistp Derivation)
     T
     (and (is-string-in (sel-left-Derivation-Step (car Derivation)) Terminals)
	  (all-rights-terminal (cdr Derivation) Terminals))))


(defn is-right-derivation-in (Derivation Grammar)
 (and (is-Derivation-in Derivation Grammar)
      (all-rights-terminal 
       Derivation 
       (append (sel-terminals Grammar) (list (end-of-file))))))

(defn is-left-derivation-in (Derivation Grammar)
 (and (is-Derivation-in Derivation Grammar)
      (all-lefts-terminal 
       Derivation 
       (append (sel-terminals Grammar) (list (end-of-file))))))
(deftheory derivations 
 (IS-LEFT-DERIVATION-IN IS-RIGHT-DERIVATION-IN
  ALL-LEFTS-TERMINAL ALL-RIGHTS-TERMINAL IS-DERIVATION-IN ALL-IN-VOCAB
  LOCKSTEP PRODUCTIONS DERIV-RULE TARGET SOURCE STEP-TARGET STEP-SOURCE
  MK-DERIVATION-STEP ))

(disable-theory derivations)
;; ---------------------------------------------------------------------------
;; ~/events/parser.events
;; ---------------------------------------------------------------------------
;;
;; This is the skeleton parser
;;

(enable-theory stacks)
(enable-theory lists)
(enable-theory grammar)
(enable-theory configurations)
(enable-theory derivations)

;; This is what happens to trees during reduction. It should keep the
;; frontier invariant.

(defn reduce-trees (lhs size trees)
 (if (or (lessp (stack-length trees) size)
         (not (is-stack trees))
         (zerop size))
     (emptystack)
     (push (mk-tree 
            lhs 
            (top-n size trees))
           (pop-n size trees))))

;; The list l matches s if l corresponds to s in stack order.

(defn matches-stack (l s)
 (if (not (is-stack s))
     F
     (if (is-empty s)
         (nlistp l)
         (if (nlistp l)
             T
             (and (equal (car l) (top s))
                  (matches-stack (cdr l) (pop s)))))))

;; This is the basic parsing step.

(defn parsing-step (conf tables grammar)
 (let ((input   (sel-input conf))
       (states  (sel-states conf))
       (symbols (sel-symbols conf))
       (trees   (sel-trees conf))
       (parse   (sel-parse conf))
       (deriv   (sel-deriv conf))
       (error   (sel-error conf))
       (prods   (sel-productions grammar)))

   (if (nlistp input)
       (mk-configuration
         input states symbols trees parse deriv T)
       (let ((act  (action-lookup (token-name (car input))
                                  (top states) 
                                  (sel-Actiontab tables))))
         (case (sel-action-tag act)
           (error
            ;; Set the error flag and terminate.
            (mk-configuration
             input states symbols trees parse deriv T))
           (shift
            (let ((s (sel-state-shift act)))
              (mk-configuration
               (cdr input)
               (push s states)
               ;; I only push the token-name, not the whole token.
               (push (token-name (car input)) symbols)
               (push (mk-tree (car input) nil) trees)
               parse
               deriv
               F)))
           (reduce
              (let ((label (sel-Label-Reduce act))
                    (lhs   (car (sel-Lhs-Reduce act)))
                    (size  (sel-Size-Reduce act)))
                (let ((rhs (sel-rhs (prod-nr label prods))))
                (if (or (lessp (stack-length trees) size)
                        (not (matches-stack (reverse rhs) symbols))
                        (zerop size))
                    ;; I cannot do a reduction if there are less than
                    ;; size things on the stack or if the rhs does not match,
                    ;; so terminate with error.
                    (mk-configuration
                     input states symbols trees parse deriv T)
                  (let ((goto (goto-lookup lhs
                                           (top (pop-n size states))
                                           (sel-Gototab tables))))
                    (mk-configuration
                     input
                     (push goto (pop-n size states))
                     (push lhs (pop-n size symbols))
                     (reduce-trees lhs size trees)
                     (append parse (list label))
                     (append (list (mk-Derivation-Step 
                                    (from-bottom (pop-n size symbols))
                                    (mk-prod label lhs (top-n size symbols))
                                    ;; I only use the token names.
                                    (pick-token-names input)))
                             deriv)
                     F))))))
           (otherwise
                (mk-configuration
                 input states symbols trees parse deriv T)))))))

;; I define an explicit acceptance predicate. This is the difference
;; to the standard method of parsing, which has an accept action which
;; is a special reduction. Special cases are not especially conductive
;; to proofs!

(defn accepting (conf axiom)
 (and (equal (car (sel-Input conf))
             (mk-token (end-of-file) nil))  ; input consumed
      (equal (last (sel-Parse conf))        ; Last reduction was the goal
             (list Axiom )))) 

(defn error (conf)
  (sel-Error conf))

;; This is the skeleton parser. I parse until either the clock runs out,
;; or a configuration is reached which is either in error or accepting.

(defn parse-it (conf tables grammar clock)
   (if (zerop clock) ; go buy some more time
       conf
     (if (or (error conf)
             (accepting conf (sel-axiom grammar)))
         conf
         (parse-it (parsing-step conf tables grammar) 
                   tables 
                   grammar 
                   (sub1 clock))))
 ((lessp (count clock))))

;; The input string needs an end-of-file on the end. 
;; I use the twice the length of the input (once for each read and once
;; for the maximum stack size) times the number of productions, which
;; is the same as the maximum reduction sequence possible without a cycle,
;; as an approximation for the length of the parsing process.

(defn parser (string tables grammar)
  (parse-it
   (mk-configuration
    (append string (list (mk-token (end-of-file) nil)))
    (push 0 (emptystack))
    (emptystack)
    (emptystack)
    nil
    nil
    F)
    tables
    grammar
    (times (times (length string) 2) 
           (length (sel-productions grammar))))) 

(disable-theory stacks)
(disable-theory lists)
(disable-theory grammar)
(disable-theory configurations)
(disable-theory derivations)

;; ---------------------------------------------------------------------------
;; ~/events/parsing-inv.events
;; ---------------------------------------------------------------------------

;; This is an attempt to prove the invariants of parsing correct.
;; A *massive* use of PC-NQTHM was necessary to "see" the proofs.

(enable-theory lists)
(enable-theory stacks)
(enable-theory trees)

;; ---------------------------------------------------------------------------
;;      Leaves invariant
;; ---------------------------------------------------------------------------

(prove-lemma leaves-base (rewrite)
 (equal (append (leaves (from-bottom (emptystack))) input)
        input))

(prove-lemma leaves-append (rewrite)
 (implies (listp b)
          (equal (leaves (append a b))
                 (append (leaves a) (leaves b))))
 ((enable-theory lists trees)))

(prove-lemma better-leaves (rewrite)
 (implies (listp l)
   (equal (leaves (list (mk-tree x l)))
          (leaves l)))
 ((enable-theory trees)))

(prove-lemma configuration-induction-step-shift (rewrite)
 (implies (and (token-listp input)
               (listp input)
               (is-stack trees)
               (equal next (mk-configuration
                            (cdr input)
                            (push s states)
                            (push (car input) symbols)
                            (push (mk-tree (car input) nil) trees)
                            parse
                            deriv
                            F)))
            (equal (append (leaves (from-bottom (sel-trees next))) 
                           (sel-input next))
                   (append (leaves (from-bottom trees)) input)))
 ((enable-theory stacks lists trees)))

(prove-lemma frontier-leaf-rewrite (rewrite)
 (equal (frontier 'tree (mk-tree a b))
        (if (is-leaf (mk-tree a b))
            (list a)
            (frontier 'branches b))))

(prove-lemma frontier-tree-is-leaves (rewrite)
 (implies (listp l)
          (equal (frontier 'tree (mk-tree x l))
                 (leaves l))))

(prove-lemma append-leaves (rewrite)
 (implies (listp b)
          (equal (append (leaves a) (leaves b))
                 (leaves (append a b)))))

;; The lemma needs the help of PC-NQTHM to prove, it is just a rewriting
;; proof. NQTHM alone cannot be coaxed to do the necessary rewriting.

(prove-lemma leaves-from-bottom-reduce-leaves (rewrite)
 (implies (and (is-stack trees)
               (not (zerop size))
               (not (lessp (stack-length trees) size)))
          (equal (leaves (from-bottom (reduce-trees lhs size trees)))
                 (leaves (from-bottom trees))))
           ((instructions promote
                          (dive 1 1 1)
                          x up
                          (rewrite from-bottom-push)
                          up
                          (rewrite leaves-append)
                          (dive 2)
                          (rewrite better-leaves)
                          up
                          (rewrite append-leaves)
                          (dive 1)
                          (rewrite append-from-bottom-pop-n)
                          top prove prove prove)))

;; Disable this lemma because it is an incredibly bad rewrite rule!

(disable append-leaves) 

(prove-lemma configuration-induction-step-reduce (rewrite)
 (implies (and (token-listp input)
               (listp input)
               (is-stack trees)
               (not (zerop size))
               (not (lessp (stack-length trees) size))
               (equal next (mk-configuration
                            input
                            (push s states)
                            (push (car input) symbols)
                            (reduce-trees lhs size trees)
                            parse
                            deriv
                            F)))
            (equal (append (leaves (from-bottom (sel-trees next))) 
                           (sel-input next))
                   (append (leaves (from-bottom trees)) input)))
 ((disable reduce-trees)))

(prove-lemma frontier-branches-is-leaves (rewrite)
 (equal (frontier 'branches q)
        (leaves q)))
        
(prove-lemma leaves-from-bottom-pop-n-trees (rewrite)
 (implies (and (is-stack trees)
               (not (zerop size))
               (not (lessp (stack-length trees) size)))
          (equal (append (leaves (from-bottom (pop-n size trees)))
                         (frontier 'branches
                                   (top-n size trees)))
                 (leaves (from-bottom trees))))
             ((instructions promote
                            (dive 1 2)
                            top
                            (dive 2)
                            top
                            (dive 1 2)
                            (rewrite frontier-branches-is-leaves)
                            up
                            (claim (listp (top-n size trees)))
                            (rewrite append-leaves)
                            (dive 1)
                            (rewrite append-from-bottom-pop-n)
                            top prove)))

(prove-lemma append-elimination (rewrite)
 (implies (equal (append x y) a)
          (equal (append x (append y z))
                 (append a z))))

(prove-lemma great-parsing-step-invariant (rewrite)
 (implies (equal next
                 (parsing-step (mk-configuration input states
                                                 symbols
                                                 trees parse
                                                 deriv f)
                               tables grammar))
          (equal (append (leaves (from-bottom (sel-trees next)))
                         (sel-input next))
                 (append (leaves (from-bottom trees))
                         input)))
             ((instructions promote
                            (dive 1 1 1 1 1)
                            = top bash prove promote
                            (dive 1)
                            (rewrite append-elimination
                                     (($a (leaves (from-bottom trees)))))
                            top prove
                            (dive 1)
                            (rewrite append-leaves)
                            (dive 1)
                            (rewrite append-from-bottom-pop-n)
                            top prove 
                            prove)))

;; ---------------------------------------------------------------------------
;;      Right Sentential form
;; ---------------------------------------------------------------------------

(enable-theory derivations)
(enable-theory grammar)
(disable sel-action-tag)
(disable action-lookup)

:; A problem with this invariant is that it is not valid until I have made 
;; a first reduction, as the derivation is empty at the beginning of parsing.
;; I cannot put a "dummy" derivation on, as there would be nothing to
;; put in the production component, and thus the derivation would not be
;; in lockstep.

(prove-lemma car-append-list (rewrite)
 (equal (car (append (list x) y)) x))

(prove-lemma inv-rt-sent-1-shift (rewrite)
  (implies (and (equal next
                       (mk-configuration
                        (cdr input)
                        (push s states)
                        (push (token-name (car input)) symbols)
                        (push (mk-tree (car input) nil) trees)
                        parse
                        deriv
                        f))
                (listp input)
                (token-listp input)
                (equal (append (from-bottom symbols) (pick-token-names input))
                       (step-source (car deriv))))
           (equal (append (from-bottom (sel-symbols next)) 
                           (pick-token-names (sel-input next)))
                  (step-source (car (sel-deriv next))))))

(prove-lemma append-from-bottom-push (rewrite)
      (implies (and (is-stack symbols)
                    (equal (append (from-bottom symbols)
                                   (pick-token-names input))
                           (append d (cons x w))))
               (equal (append (from-bottom (push lhs (pop-n size symbols)))
                              (pick-token-names input))
                      (append (from-bottom (pop-n size symbols))
                              (cons lhs (pick-token-names input))))))

(prove-lemma inv-rt-sent-1-reduce (rewrite)
  (implies (and (equal next
                       (mk-configuration
                        input
                        (push goto (pop-n size states))
                        (push lhs (pop-n size symbols))
                        (reduce-trees lhs size trees)
                        (append parse (list label))
                        (append (list (mk-derivation-step 
                                       (from-bottom (pop-n size symbols))
                                       (mk-prod label lhs (top-n size symbols))
                                       (pick-token-names input)))
                                deriv)
                        f))
                (is-stack symbols)
                (equal (append (from-bottom symbols) (pick-token-names input))
                       (step-source (car deriv))))
           (equal (append (from-bottom (sel-symbols next))
                           (pick-token-names (sel-input next)))
                   (step-source (car (sel-deriv next))))))

(prove-lemma inv-rt-sent-1 (rewrite)
  (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (is-stack symbols)
                (token-listp input)
                (listp input)
                (equal (append (from-bottom symbols) 
                               (pick-token-names input))
                       (step-source (car deriv))))
           (equal (append (from-bottom (sel-symbols next)) 
                          (pick-token-names (sel-input next)))
                   (step-source (car (sel-deriv next))))))

;; ---------------------------------------------------------------------------
;;      Stack size
;; ---------------------------------------------------------------------------

(prove-lemma inv-stack-size-shift (rewrite)
 (implies (and (equal next (mk-configuration
                             (cdr input)
                             (push s states)
                             (push (token-name (car input)) symbols)
                             (push (mk-tree (car input) nil) trees)
                             parse
                             deriv
                             f))
                (is-stack symbols)
                (is-stack states)
                (is-stack trees)
                (and (equal (stack-length trees)
                            (stack-length symbols))
                     (equal (add1 (stack-length symbols))
                            (stack-length states))))
           (and (equal (stack-length (sel-trees next))
                       (stack-length (sel-symbols next)))
                (equal (add1 (stack-length (sel-symbols next)))
                       (stack-length (sel-states next))))))

(prove-lemma stack-length-push (rewrite)
 (equal (stack-length (push a b))
        (add1 (stack-length b))))

(prove-lemma stack-length-pop-n (rewrite)
 (implies (not (lessp (stack-length a) size))
          (equal (stack-length (pop-n size a))
                 (difference (stack-length a) size))))

(prove-lemma inv-stack-size-reduce (rewrite)
 (implies (and (equal next 
                      (mk-configuration
                       input
                       (push goto (pop-n size states))
                       (push lhs (pop-n size symbols))
                       (reduce-trees lhs size trees)
                       (append parse (list label))
                       (append (list (mk-derivation-step 
                                      (from-bottom (pop-n size symbols))
                                      (mk-prod label lhs (top-n size symbols))
                                      (pick-token-names input)))
                               deriv)
                       f))
                (is-stack symbols)
                (is-stack states)
                (is-stack trees)
                (not (zerop size))
                (not (lessp (stack-length trees) size))
                (and (equal (stack-length trees)
                            (stack-length symbols))
                     (equal (add1 (stack-length symbols))
                            (stack-length states))))
           (and (equal (stack-length (sel-trees next))
                       (stack-length (sel-symbols next)))
                (equal (add1 (stack-length (sel-symbols next)))
                       (stack-length (sel-states next))))))

(prove-lemma inv-stack-size (rewrite)
 (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (is-stack symbols)
                (is-stack states)
                (is-stack trees)
                (and (equal (stack-length trees)
                            (stack-length symbols))
                     (equal (add1 (stack-length symbols))
                            (stack-length states))))
           (and (equal (stack-length (sel-trees next))
                       (stack-length (sel-symbols next)))
                (equal (add1 (stack-length (sel-symbols next)))
                       (stack-length (sel-states next))))))

;; ---------------------------------------------------------------------------
;;      Number of reductions
;; ---------------------------------------------------------------------------

;; I only count the inner nodes.

(defn node-count (tag tree)
  (if (equal tag 'tree)
      (if (or (not (is-tree tree))
              (equal tree (emptytree))
              (is-leaf tree))
          0
          (add1 (node-count 'branches (sel-branches tree))))
      (if (nlistp tree)
          0
          (plus (node-count 'tree (car tree))
                (node-count 'branches (cdr tree))))))
                   
(prove-lemma length-append (rewrite)
 (equal (length (append a b))
        (plus (length a)
              (length b))))

(prove-lemma node-count-append (rewrite)
 (equal (node-count 'branches (append a b))
        (plus (node-count 'branches a)
              (node-count 'branches b))))
        
(prove-lemma node-count-top-n-pop-n (rewrite)
 (equal (plus (node-count 'branches (top-n size trees))
              (node-count 'branches (from-bottom (pop-n size trees))))
        (node-count 'branches (from-bottom trees))))

(prove-lemma inv-reductions-shift (rewrite)
 (implies (and (equal next (mk-configuration
                             (cdr input)
                             (push s states)
                             (push (token-name (car input)) symbols)
                             (push (mk-tree (car input) nil) trees)
                             parse
                             deriv
                             f))
               (equal (node-count 'branches (from-bottom trees)) 
                      (length parse)))
           (equal (node-count 'branches (from-bottom (sel-trees next)))
                  (length (sel-parse next)))))

;; I need to know that trees is not empty, as the node-count
;; of an empty tree is 0, as is the node-count of a leaf.

(prove-lemma node-count-reduce-trees (rewrite)
 (implies (and (not (zerop size))
               (not (lessp (stack-length trees) size))
               (not (equal trees (emptystack))))
          (equal (node-count 'branches 
                             (from-bottom (reduce-trees lhs size trees)))
                 (add1 (node-count 'branches (from-bottom trees)))))
 ((enable-theory trees)))

(prove-lemma inv-reductions-reduce (rewrite)
 (implies (and (equal next 
                      (mk-configuration
                       input
                       (push goto (pop-n size states))
                       (push lhs (pop-n size symbols))
                       (reduce-trees lhs size trees)
                       (append parse (list label))
                       (append (list (mk-Derivation-Step 
                                      (from-bottom (pop-n size symbols))
                                      (mk-prod label lhs (top-n size symbols))
                                      (pick-token-names input)))
                               deriv)
                       f))
               (not (zerop size))
               (not (lessp (stack-length trees) size))
               (equal (node-count 'branches (from-bottom trees)) 
                      (length parse))
                      )
           (equal (node-count 'branches (from-bottom (sel-trees next)))
                  (length (sel-parse next))))
 ((disable reduce-trees)))

(prove-lemma inv-reductions (rewrite)
  (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (not  (equal trees (emptytree)))
                (equal (node-count 'branches (from-bottom trees)) 
                       (length parse)))
           (equal (node-count 'branches (from-bottom (sel-trees next)))
                  (length (sel-parse next))))
 ((disable reduce-trees )
  (induct (stack-length trees))))

;; ---------------------------------------------------------------------------
;;      Roots
;; ---------------------------------------------------------------------------

(prove-lemma roots-mk-tree (rewrite)
 (equal (roots (list (mk-tree a b))) (list a)))

(prove-lemma roots-append (rewrite)
 (implies (listp b)
          (equal (roots (append a b))
                 (append (roots a) (roots b)))))

(prove-lemma pick-token-names-append (rewrite)
 (equal (pick-token-names (append a b))
        (append (pick-token-names a) (pick-token-names b))))

(prove-lemma pick-token-names-list (rewrite)
 (implies (tokenp a)
          (equal (pick-token-names (list a))
                 (list (token-name a)))))

(prove-lemma inv-roots-shift (rewrite)
  (implies (and (equal next (mk-configuration
                             (cdr input)
                             (push s states)
                             (push (token-name (car input)) symbols)
                             (push (mk-tree (car input) nil) trees)
                             parse
                             deriv
                             f))
                (is-stack symbols)
                (token-listp input)
                (listp input)
                (is-stack trees)
                (equal (pick-token-names (roots (from-bottom trees)))
                       (from-bottom symbols)))
           (equal (pick-token-names (roots (from-bottom (sel-trees next))))
                  (from-bottom (sel-symbols next)))))

#|
;; ---------------------------------------------------------------------------
;; This is the statement of the roots reduction theorem
;; ---------------------------------------------------------------------------

;; The problem is: Sometimes the nodes are tokens (when they are leaves)
;; and sometimes they are just the names of the lhs. 
;; Even when I ensure that trees is a stack of trees - what if
;; a left hand side happens to be a token? Then it is not valid!
;; Proof abandonded at this point, as I would need to go back to the
;; definition of grammar and introduce an explicit shell for left hand
;; sides so that I can know that a left hand side can never be a token.

(prove-lemma inv-roots-reduce (rewrite)
  (implies (and (equal next 
                       (mk-configuration
                        input
                        (push goto (pop-n size states))
                        (push lhs (pop-n size symbols))
                        (reduce-trees lhs size trees)
                        (append parse (list label))
                        (append (list (mk-derivation-step 
                                       (from-bottom (pop-n size symbols))
                                       (mk-prod label lhs (top-n size symbols))
                                       (pick-token-names input)))
                                deriv)
                        f))
                (is-stack symbols)
                (token-listp input)
                (not (lessp (stack-length trees) size))
                (not (zerop size))
                (listp input)
                (is-stack trees)
                (stack-of-trees trees)
                (equal (pick-token-names (roots (from-bottom trees)))
                       (from-bottom symbols)))
           (equal (pick-token-names (roots (from-bottom (sel-trees next))))
                  (from-bottom (sel-symbols next)))))

(prove-lemma inv-roots (rewrite)
  (implies (and (equal next
                      (parsing-step (mk-configuration input states
                                                      symbols
                                                      trees parse
                                                      deriv f)
                                    tables grammar))
                (is-stack symbols)
                (token-listp input)
                (listp input)
                (is-stack trees)
                (equal (pick-token-names (roots (from-bottom trees)))
                       (from-bottom symbols)))
           (equal (pick-token-names (roots (from-bottom (sel-trees next))))
                  (from-bottom (sel-symbols next)))))
|#