		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-insert

Insert a value into the tree.

Signature
(tree-insert x tree) → tree$
Arguments: tree — Guard (binary-tree-p tree).
Returns: tree$ — Type (binary-tree-p tree$).

The element is inserted with respect to the binary search tree ordering and then rebalanced with respect to the heapp property.

Definitions and Theorems

Function: tree-insert

(defun tree-insert (x tree)
 (declare (xargs :guard (binary-tree-p tree)))
 (let ((__function__ 'tree-insert))
   (declare (ignorable __function__))
   (b* (((when (tree-emptyp tree))
         (tree-node x nil nil))
        ((when (equal x (tree-head tree)))
         (tree-fix tree))
        (lt (bst< x (tree-head tree))))
     (if lt (b* ((left$ (tree-insert x (tree-left tree)))
                 (tree$ (tree-node-with-hint (tree-head tree)
                                             left$ (tree-right tree)
                                             tree)))
              (if (heap< (tree-head tree)
                         (tree-head left$))
                  (rotate-right tree$)
                tree$))
       (b* ((right$ (tree-insert x (tree-right tree)))
            (tree$ (tree-node-with-hint (tree-head tree)
                                        (tree-left tree)
                                        right$ tree)))
         (if (heap< (tree-head tree)
                    (tree-head right$))
             (rotate-left tree$)
           tree$))))))

Theorem: binary-tree-p-of-tree-insert

(defthm binary-tree-p-of-tree-insert
  (b* ((tree$ (tree-insert x tree)))
    (binary-tree-p tree$))
  :rule-classes :rewrite)

Theorem: tree-emptyp-of-tree-insert

(defthm tree-emptyp-of-tree-insert
  (not (tree-emptyp (tree-insert x tree))))