blob: de31670c7c359e3ea1b29bde09ff5b145c3dbbda (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
; (certify-book "sorts-equivalent2")
(in-package "ACL2")
(include-book "equisort2")
(include-book "isort")
(include-book "msort")
(include-book "qsort")
(include-book "bsort")
(defthm msort-is-isort
(equal (msort x) (isort x))
:hints (("Goal" :use (:functional-instance sortfn1-is-sortfn2
(sorthyp (lambda (x) t))
(sortfn1 msort)
(sortfn2 isort)))))
(defthm qsort-is-isort
(equal (qsort x) (isort x))
:hints (("Goal" :use (:functional-instance sortfn1-is-sortfn2
(sorthyp (lambda (x) t))
(sortfn1 qsort)
(sortfn2 isort)))))
(defthm bsort-is-isort
(implies (true-listp x)
(equal (bsort x) (isort x)))
:hints (("Goal" :use (:functional-instance sortfn1-is-sortfn2
(sorthyp true-listp)
(sortfn1 bsort)
(sortfn2 isort)))))
|
