		Search-engine friendly clone of the ACL2 documentation.

Implementation

Rotations

Left and right tree rotations.

Rotations preserve the binary search tree property while rotating up the head of one or the other subtrees.

Definitions and Theorems

Function: rotate-left$inline

(defun rotate-left$inline (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (declare (xargs :guard (not (tree-emptyp (tree-right tree)))))
  (if (mbt (not (tree-emptyp (tree-right tree))))
      (tree-node (tree-head (tree-right tree))
                 (tree-node (tree-head tree)
                            (tree-left tree)
                            (tree-left (tree-right tree)))
                 (tree-right (tree-right tree)))
    (tree-fix tree)))

Theorem: binary-tree-p-of-rotate-left

(defthm binary-tree-p-of-rotate-left
  (b* ((tree$ (rotate-left$inline tree)))
    (binary-tree-p tree$))
  :rule-classes :rewrite)

Function: rotate-right$inline

(defun rotate-right$inline (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (declare (xargs :guard (not (tree-emptyp (tree-left tree)))))
  (if (mbt (not (tree-emptyp (tree-left tree))))
      (tree-node (tree-head (tree-left tree))
                 (tree-left (tree-left tree))
                 (tree-node (tree-head tree)
                            (tree-right (tree-left tree))
                            (tree-right tree)))
    (tree-fix tree)))

Theorem: binary-tree-p-of-rotate-right

(defthm binary-tree-p-of-rotate-right
  (b* ((tree$ (rotate-right$inline tree)))
    (binary-tree-p tree$))
  :rule-classes :rewrite)

Subtopics

Rotate-right: Perform a right tree rotation.
Rotate-left: Perform a left tree rotation.