		Search-engine friendly clone of the ACL2 documentation.

Insertion-sort

A generic insert sort based on ACL2's total order of values.

Signature
(insertion-sort list) → sorted-list
Arguments: list — Guard (true-listp list).
Returns: sorted-list — Type (true-listp sorted-list), given the guard.

This should be moved to a more general library.

Definitions and Theorems

Function: insertion-sort-insert

(defun insertion-sort-insert (elem list)
  (declare (xargs :guard (true-listp list)))
  (let ((__function__ 'insertion-sort-insert))
    (declare (ignorable __function__))
    (cond ((endp list) (list elem))
          ((<< elem (car list)) (cons elem list))
          (t (cons (car list)
                   (insertion-sort-insert elem (cdr list)))))))

Theorem: true-listp-of-insertion-sort-insert

(defthm true-listp-of-insertion-sort-insert
  (implies (and (true-listp list))
           (b* ((list-with-elem (insertion-sort-insert elem list)))
             (true-listp list-with-elem)))
  :rule-classes (:rewrite :type-prescription))

Function: insertion-sort

(defun insertion-sort (list)
  (declare (xargs :guard (true-listp list)))
  (let ((__function__ 'insertion-sort))
    (declare (ignorable __function__))
    (cond ((endp list) nil)
          (t (insertion-sort-insert (car list)
                                    (insertion-sort (cdr list)))))))

Theorem: true-listp-of-insertion-sort

(defthm true-listp-of-insertion-sort
  (implies (and (true-listp list))
           (b* ((sorted-list (insertion-sort list)))
             (true-listp sorted-list)))
  :rule-classes (:rewrite :type-prescription))

Subtopics

Insertion-sort-of-integers-from-to: Applying insertion sort to an ordered list of integers in a range yields the same list.