Filtering...

sorting

books/acl2s/sorting/sorting
other
(in-package "ACL2S")
other
(include-book "acl2s/definec" :dir :system :ttags :all)
other
(include-book "sorting/msort" :dir :system)
other
(set-termination-method :ccg)
other
(set-ccg-time-limit 300)
other
(definec merge2
  (x :integer-list y :integer-list)
  :integer-list (cond ((endp x) y)
    ((endp y) x)
    ((< (car x) (car y)) (cons (car x)
        (merge2 (cdr x) y)))
    (t (cons (car y)
        (merge2 x (cdr y))))))
other
(sig evens
  ((listof :a))
  =>
  (listof :a))
other
(sig odds
  ((listof :a))
  =>
  (listof :a))
other
(definec msort
  (x :integer-list)
  :integer-list (cond ((endp x) x)
    ((endp (cdr x)) x)
    (t (merge2 (msort (evens x))
        (msort (odds x))))))
other
(definec merge2-no-dups
  (x :integer-list y :integer-list)
  :integer-list (cond ((endp x) y)
    ((endp y) x)
    ((< (car x) (car y)) (cons (car x)
        (merge2-no-dups (cdr x) y)))
    ((= (car x) (car y)) (cons (car x)
        (merge2-no-dups (cdr x) (cdr y))))
    (t (cons (car y)
        (merge2-no-dups x (cdr y))))))
other
(definec msort-no-dups
  (x :integer-list)
  :integer-list (cond ((endp x) x)
    ((endp (cdr x)) x)
    (t (merge2-no-dups (msort-no-dups (evens x))
        (msort-no-dups (odds x))))))
other
(defthm merge2-len
  (implies (and (integer-listp x)
      (integer-listp y))
    (equal (len (merge2 x y))
      (+ (len x) (len y)))))
other
(defthm expand-evens
  (implies (true-listp l)
    (equal (evens (cons a l))
      (cons a (evens (cdr l))))))
other
(defthm evens-len
  (implies (true-listp x)
    (equal (+ (len (evens x))
        (len (evens (cdr x))))
      (len x)))
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((evens x)))))
other
(defthm msort-len
  (implies (integer-listp x)
    (= (len (msort x))
      (len x))))
other
(defthm merge2-no-dups-len
  (implies (and (integer-listp x)
      (integer-listp y))
    (<= (len (merge2-no-dups x y))
      (+ (len x) (len y))))
  :rule-classes ((:linear) (:rewrite)))
other
(defthm msort-no-dups-len
  (implies (integer-listp x)
    (<= (len (msort-no-dups x))
      (len x)))
  :rule-classes ((:linear) (:rewrite)))
other
(definec insert
  (e :int l :integer-list)
  :integer-list (cond ((endp l) (list e))
    ((<= e (car l)) (cons e l))
    (t (cons (car l)
        (insert e (cdr l))))))
other
(definec insert-no-dups
  (e :int l :integer-list)
  :integer-list (cond ((endp l) (list e))
    ((< e (car l)) (cons e l))
    ((= e (car l)) l)
    (t (cons (car l)
        (insert-no-dups e (cdr l))))))
other
(definec isort
  (x :integer-list)
  :integer-list (if (endp x)
    nil
    (insert (car x) (isort (cdr x)))))
other
(definec isort-no-dups
  (x :integer-list)
  :integer-list (if (endp x)
    nil
    (insert-no-dups (car x)
      (isort-no-dups (cdr x)))))
other
(defthm insert-len
  (implies (and (integerp e) (integer-listp l))
    (= (len (insert e l))
      (1+ (len l)))))
other
(defthm isort-len
  (implies (integer-listp x)
    (= (len (isort x))
      (len x))))
other
(defthm insert-no-dups-len
  (implies (and (integerp e) (integer-listp l))
    (<= (len (insert-no-dups e l))
      (1+ (len l))))
  :rule-classes ((:linear) (:rewrite)))
other
(defthm isort-no-dups-len
  (implies (integer-listp x)
    (<= (len (isort-no-dups x))
      (len x)))
  :rule-classes ((:linear) (:rewrite)))
other
(definec rem-dups-sorted
  (x :integer-list)
  :integer-list (cond ((endp x) x)
    ((endp (rest x)) x)
    ((equal (car x) (cadr x)) (rem-dups-sorted (cdr x)))
    (t (cons (car x)
        (rem-dups-sorted (cdr x))))))
other
(definec fill-in-list
  (l :integer-list last :int cnt :nat)
  :integer-list (declare (xargs :consider-only-ccms ((+ (len l) cnt))))
  (cond ((= cnt 0) l)
    ((endp l) (cons (1+ last)
        (fill-in-list l (1+ last) (1- cnt))))
    ((< (1+ last) (car l)) (cons (1+ last)
        (fill-in-list l (1+ last) (1- cnt))))
    (t (cons (car l)
        (fill-in-list (cdr l)
          (car l)
          cnt)))))
other
(definec make-unique-ordered
  (l :integer-list min :int)
  :integer-list (let* ((len (len l)) (sort (msort-no-dups l))
      (lens (len sort)))
    (fill-in-list sort
      (1- min)
      (- len lens))))
other
(definec make-nondec
  (l :integer-list)
  :integer-list (msort l))
other
(definec make-unique-decreasing
  (l :integer-list min :int)
  :integer-list (rev (make-unique-ordered l min)))
other
(definec make-noninc
  (l :integer-list)
  :integer-list (rev (msort l)))