msort

other

(in-package "ACL2")

include-book

(include-book "perm")

include-book

(include-book "ordered-perms")

include-book

(include-book "convert-perm-to-how-many")

merge2function

(defun merge2
  (x y)
  (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
  (if (endp x)
    y
    (if (endp y)
      x
      (if (lexorder (car x) (car y))
        (cons (car x) (merge2 (cdr x) y))
        (cons (car y) (merge2 x (cdr y)))))))

acl2-count-evens-strongtheorem

(defthm acl2-count-evens-strong
  (implies (and (consp x) (consp (cdr x)))
    (< (acl2-count (evens x)) (acl2-count x)))
  :rule-classes :linear)

acl2-count-evens-weaktheorem

(defthm acl2-count-evens-weak
  (<= (acl2-count (evens x)) (acl2-count x))
  :hints (("Goal" :induct (evens x)))
  :rule-classes :linear)

msortfunction

(defun msort
  (x)
  (if (endp x)
    nil
    (if (endp (cdr x))
      (list (car x))
      (merge2 (msort (evens x)) (msort (odds x))))))

orderedp-msorttheorem

(defthm orderedp-msort (orderedp (msort x)))

true-listp-msorttheorem

(defthm true-listp-msort (true-listp (msort x)))

how-many-merge2theorem

(defthm how-many-merge2
  (equal (how-many e (merge2 x y))
    (+ (how-many e x) (how-many e y))))

how-many-evens-and-oddstheorem

(defthm how-many-evens-and-odds
  (implies (consp x)
    (equal (+ (how-many e (evens x)) (how-many e (evens (cdr x))))
      (how-many e x))))

how-many-msorttheorem

(defthm how-many-msort
  (equal (how-many e (msort x)) (how-many e x)))

Included Books