		Search-engine friendly clone of the ACL2 documentation.

Semantics

Tree->string

String at the leaves of trees.

Signature
(tree->string tree) → string
Arguments: tree — Guard (treep tree).
Returns: string — Type (stringp string).

This collects all the leaves of a tree, left to right, and assembles them into a string.

Function: tree->string

(defun tree->string (tree)
  (declare (xargs :guard (treep tree)))
  (tree-case tree
             :leafterm tree.get
             :leafrule (list tree.get)
             :nonleaf (tree-list-list->string tree.branches)))

Function: tree-list->string

(defun tree-list->string (trees)
  (declare (xargs :guard (tree-listp trees)))
  (cond ((endp trees) nil)
        (t (append (tree->string (car trees))
                   (tree-list->string (cdr trees))))))

Function: tree-list-list->string

(defun tree-list-list->string (treess)
  (declare (xargs :guard (tree-list-listp treess)))
  (cond ((endp treess) nil)
        (t (append (tree-list->string (car treess))
                   (tree-list-list->string (cdr treess))))))

Theorem: return-type-of-tree->string.string

(defthm return-type-of-tree->string.string
  (b* ((?string (tree->string tree)))
    (stringp string))
  :rule-classes :rewrite)

Theorem: return-type-of-tree-list->string.string

(defthm return-type-of-tree-list->string.string
  (b* ((?string (tree-list->string trees)))
    (stringp string))
  :rule-classes :rewrite)

Theorem: return-type-of-tree-list-list->string.string

(defthm return-type-of-tree-list-list->string.string
  (b* ((?string (tree-list-list->string treess)))
    (stringp string))
  :rule-classes :rewrite)

Theorem: tree->string-of-tree-fix-tree

(defthm tree->string-of-tree-fix-tree
  (equal (tree->string (tree-fix tree))
         (tree->string tree)))

Theorem: tree-list->string-of-tree-list-fix-trees

(defthm tree-list->string-of-tree-list-fix-trees
  (equal (tree-list->string (tree-list-fix trees))
         (tree-list->string trees)))

Theorem: tree-list-list->string-of-tree-list-list-fix-treess

(defthm tree-list-list->string-of-tree-list-list-fix-treess
  (equal (tree-list-list->string (tree-list-list-fix treess))
         (tree-list-list->string treess)))

Theorem: tree->string-tree-equiv-congruence-on-tree

(defthm tree->string-tree-equiv-congruence-on-tree
  (implies (tree-equiv tree tree-equiv)
           (equal (tree->string tree)
                  (tree->string tree-equiv)))
  :rule-classes :congruence)

Theorem: tree-list->string-tree-list-equiv-congruence-on-trees

(defthm tree-list->string-tree-list-equiv-congruence-on-trees
  (implies (tree-list-equiv trees trees-equiv)
           (equal (tree-list->string trees)
                  (tree-list->string trees-equiv)))
  :rule-classes :congruence)

Theorem: tree-list-list->string-tree-list-list-equiv-congruence-on-treess

(defthm
   tree-list-list->string-tree-list-list-equiv-congruence-on-treess
  (implies (tree-list-list-equiv treess treess-equiv)
           (equal (tree-list-list->string treess)
                  (tree-list-list->string treess-equiv)))
  :rule-classes :congruence)

Theorem: tree-list->string-when-atom

(defthm tree-list->string-when-atom
  (implies (atom trees)
           (equal (tree-list->string trees) nil)))

Theorem: tree-list->string-of-cons

(defthm tree-list->string-of-cons
  (equal (tree-list->string (cons tree trees))
         (append (tree->string tree)
                 (tree-list->string trees))))

Theorem: tree-list->string-of-append

(defthm tree-list->string-of-append
  (equal (tree-list->string (append trees1 trees2))
         (append (tree-list->string trees1)
                 (tree-list->string trees2))))

Theorem: tree-list-list->string-when-atom

(defthm tree-list-list->string-when-atom
  (implies (atom treess)
           (equal (tree-list-list->string treess)
                  nil)))

Theorem: tree-list-list->string-of-cons

(defthm tree-list-list->string-of-cons
  (equal (tree-list-list->string (cons trees treess))
         (append (tree-list->string trees)
                 (tree-list-list->string treess))))

Theorem: tree-list-list->string-of-append

(defthm tree-list-list->string-of-append
  (equal (tree-list-list->string (append treess1 treess2))
         (append (tree-list-list->string treess1)
                 (tree-list-list->string treess2))))

Subtopics

Tree-list->string
Tree-list-list->string