		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-split

Split a tree into two disjoint subtrees.

Signature
(tree-split x tree) → (mv in left right)
Arguments: tree — Guard (binary-tree-p tree).
Returns: in — Type (booleanp in).; left — Type (binary-tree-p left).; right — Type (binary-tree-p right).

When tree is a set, (tree-split x tree) yields (mv in left right) where:

in is a boolean representing (tree-in x tree).
left is a set containing all elements of tree less than x (with respect to bst<).
right is a set containing all elements of tree greater than x (with respect to bst<).

The implementation is comparable to tree-insert if we were to pretend x is maximal with respect to heap<.

Definitions and Theorems

Function: tree-split

(defun tree-split (x tree)
 (declare (xargs :guard (binary-tree-p tree)))
 (let ((__function__ 'tree-split))
  (declare (ignorable __function__))
  (b* (((when (tree-emptyp tree))
        (mv nil nil nil))
       ((when (equal x (tree-head tree)))
        (mv t (tree-left tree)
            (tree-right tree))))
   (if
    (bst< x (tree-head tree))
    (b* (((mv in left$ right$)
          (tree-split x (tree-left tree))))
     (mbe
       :logic
       (let
         ((tree$ (rotate-right (tree-node (tree-head tree)
                                          (tree-node x left$ right$)
                                          (tree-right tree)))))
         (mv in (tree-left tree$)
             (tree-right tree$)))
       :exec (mv in left$
                 (tree-node (tree-head tree)
                            right$ (tree-right tree)))))
    (b* (((mv in left$ right$)
          (tree-split x (tree-right tree))))
     (mbe
       :logic
       (let
        ((tree$
              (rotate-left (tree-node (tree-head tree)
                                      (tree-left tree)
                                      (tree-node x left$ right$)))))
        (mv in (tree-left tree$)
            (tree-right tree$)))
       :exec (mv in
                 (tree-node (tree-head tree)
                            (tree-left tree)
                            left$)
                 right$)))))))

Theorem: booleanp-of-tree-split.in

(defthm booleanp-of-tree-split.in
  (b* (((mv ?in ?left ?right)
        (tree-split x tree)))
    (booleanp in))
  :rule-classes :type-prescription)

Theorem: binary-tree-p-of-tree-split.left

(defthm binary-tree-p-of-tree-split.left
  (b* (((mv ?in ?left ?right)
        (tree-split x tree)))
    (binary-tree-p left))
  :rule-classes :rewrite)

Theorem: binary-tree-p-of-tree-split.right

(defthm binary-tree-p-of-tree-split.right
  (b* (((mv ?in ?left ?right)
        (tree-split x tree)))
    (binary-tree-p right))
  :rule-classes :rewrite)