		Search-engine friendly clone of the ACL2 documentation.

Trees

Treep

Recognize XDOC trees.

These are the trees produced by the XDOC constructors.

These trees have strings at the leaves. A non-leaf node consists of one of the following:

A single keyword. This represents either (i) a preprocessor directive or (ii) a concatenation of subtrees without a surrounding XML tag or preprocessor directive. Examples of (i) are :@def and :@{}. The keyword :&& is used for (ii). The latter is useful to treat sequences of trees as single trees.
A cons pair whose car is a keyword and whose cdr is an alist from keywords to subtrees. This represents an XML tag, identified by the keyword at the car, with the attributes represented by the alist at the cdr. Examples are (:p) and (:img (:src ...)). The alist may often be nil. The values of the attributes are recursively represented as subtrees, but there may often be a single string subtree per attribute.

In some sense, the semantics of XDOC trees is defined by their conversion to flat strings. See tree-to-string.

Definitions and Theorems

Function: treep

(defun treep (x)
  (or (stringp x)
      (and (true-listp x)
           (consp x)
           (or (keywordp (car x))
               (tree-tagp (car x)))
           (tree-listp (cdr x)))))

Function: tree-listp

(defun tree-listp (x)
  (cond ((atom x) (eq x nil))
        (t (and (treep (car x))
                (tree-listp (cdr x))))))

Function: tree-tagp

(defun tree-tagp (x)
  (and (consp x)
       (keywordp (car x))
       (keyword-tree-alistp (cdr x))))

Function: keyword-tree-alistp

(defun keyword-tree-alistp (x)
  (cond ((atom x) (eq x nil))
        (t (and (consp (car x))
                (keywordp (car (car x)))
                (treep (cdr (car x)))
                (keyword-tree-alistp (cdr x))))))

Theorem: treep-when-stringp

(defthm treep-when-stringp
  (implies (stringp x) (treep x)))

Theorem: tree-listp-when-string-listp

(defthm tree-listp-when-string-listp
  (implies (string-listp x)
           (tree-listp x)))

Theorem: true-listp-when-tree-listp

(defthm true-listp-when-tree-listp
  (implies (tree-listp x) (true-listp x))
  :rule-classes :forward-chaining)

Theorem: treep-of-cons

(defthm treep-of-cons
  (equal (treep (cons x y))
         (and (or (keywordp x) (tree-tagp x))
              (tree-listp y))))

Theorem: tree-listp-of-cons

(defthm tree-listp-of-cons
  (equal (tree-listp (cons x y))
         (and (treep x) (tree-listp y))))

Theorem: tagp-of-cons

(defthm tagp-of-cons
  (equal (tree-tagp (cons x y))
         (and (keywordp x)
              (keyword-tree-alistp y))))

Theorem: keyword-tree-alistp-of-cons

(defthm keyword-tree-alistp-of-cons
  (equal (keyword-tree-alistp (cons x y))
         (and (consp x)
              (keywordp (car x))
              (treep (cdr x))
              (keyword-tree-alistp y))))