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