Filtering...

msort

books/acl2s/sorting/msort
other
(in-package "ACL2S")
other
(include-book "acl2s/definec" :dir :system :ttags :all)
other
(definec <<=
  (x y :all)
  :bool (lexorder x y))
other
(definec orderedp
  (x :tl)
  :bool (match x
    ((:or nil (&)) t)
    ((a b . &) (^ (<<= a b)
        (orderedp (cdr x))))))
other
(definec del
  (e :all x :tl)
  :tl (match x
    (nil nil)
    ((!e . r) r)
    ((f . r) (cons f (del e r)))))
other
(definec permp
  (x y :tl)
  :bool (match x
    (nil (endp y))
    ((f . r) (^ (in f y)
        (permp r (del f y))))))
other
(definec insert
  (a :all x :tl)
  :tl (match x
    (nil (list a))
    ((f . r) (if (<<= a f)
        (cons a x)
        (cons f (insert a r))))))
other
(definec isort
  (x :tl)
  :tl (match x
    (nil nil)
    ((f . r) (insert f (isort r)))))
other
(property orderedp-insert
  (x :all l :tl)
  :hyps (orderedp l)
  (orderedp (insert x l))
  :hints (("goal" :induct (insert x l))))
other
(property isort-ordered
  (x :tl)
  (orderedp (isort x))
  :hints (("goal" :induct (isort x))))
other
(property permp-cons
  (e :all x y :tl)
  :h (permp x y)
  :b (permp (insert e x)
    (cons e y))
  :hints (("goal" :induct (permp x y))))
other
(property isort-permp
  (x :tl)
  (permp (isort x) x)
  :hints (("goal" :induct (isort x))))
other
(property ordered-isort
  (x :tl)
  :h (orderedp x)
  :b (== (isort x) x)
  :hints (("goal" :induct (tlp x))))
other
(property isort-idempotent
  (x :tl)
  (== (isort (isort x))
    (isort x)))
other
(definec mrge
  (x y :tl)
  :tl (match (list x y)
    ((nil &) y)
    ((& nil) x)
    (((fx . rx) (fy . ry)) (if (<<= fx fy)
        (cons fx (mrge rx y))
        (cons fy (mrge x ry))))))
other
(definec even-els
  (l :tl)
  :tl (match l
    (nil nil)
    ((f . &) (cons f (even-els (cddr l))))))
other
(property even-els-size
  (l :tl)
  (<= (acl2s-size (even-els l))
    (acl2s-size l))
  :hints (("goal" :induct (even-els l)))
  :rule-classes :linear)
other
(definec odd-els
  (l :tl)
  :tl (even-els (cdr l)))
other
(set-induction-depth-limit 1)
other
(definec mrge-sort
  (x :tl)
  :tl (match x
    ((:or nil (&)) x)
    (& (mrge (mrge-sort (even-els x))
        (mrge-sort (odd-els x))))))
other
(set-induction-depth-limit 0)
other
(property mrge-ordered
  (x y :tl)
  :h (^ (orderedp x)
    (orderedp y))
  :b (orderedp (mrge x y))
  :hints (("goal" :induct (mrge x y))))
other
(property mrge-sort-ordered
  (x :tl)
  (orderedp (mrge-sort x))
  :hints (("goal" :induct (mrge-sort x))))
other
(property mrge-insert-list
  (e :all x :tl)
  (== (mrge (list e) x)
    (insert e x))
  :hints (("goal" :induct (tlp x))))
other
(property mrge-insert
  (e :all x y :tl)
  (== (mrge (insert e x) y)
    (insert e (mrge x y)))
  :hints (("goal" :induct (mrge x y))))
other
(property mrge-isort
  (x y :tl)
  (== (mrge (isort x)
      (isort y))
    (isort (app x y)))
  :hints (("goal" :induct (tlp x))))
other
(property insert-insert
  (a b :all x :tl)
  (== (insert a (insert b x))
    (insert b (insert a x)))
  :hints (("goal" :induct (tlp x))))
other
(property isort-ap
  (x y :tl e :all)
  (== (isort (app x (cons e y)))
    (insert e
      (isort (app x y))))
  :hints (("goal" :induct (tlp x))))
other
(property isort-ap-even
  (x :tl)
  (== (isort (app (even-els x)
        (even-els (cdr x))))
    (isort x))
  :hints (("goal" :induct (even-els x))))
other
(property mrge-sort=isort
  (x :tl)
  (== (mrge-sort x)
    (isort x))
  :hints (("goal" :induct (mrge-sort x))))
other
(property mrge-sort-perm
  (x :tl)
  (permp (mrge-sort x) x))