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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
; (certify-book "msort")
(in-package "ACL2")
(include-book "perm")
(include-book "ordered-perms")
(include-book "convert-perm-to-how-many")
(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)))))))
(defthm acl2-count-evens-strong
(implies (and (consp x)
(consp (cdr x)))
(< (acl2-count (evens x)) (acl2-count x)))
:rule-classes :linear)
(defthm acl2-count-evens-weak
(<= (acl2-count (evens x)) (acl2-count x))
:hints (("Goal" :induct (evens x)))
:rule-classes :linear)
(defun msort (x)
(if (endp x)
nil
(if (endp (cdr x))
(list (car x))
(merge2 (msort (evens x))
(msort (odds x))))))
(defthm orderedp-msort
(orderedp (msort x)))
(defthm true-listp-msort
(true-listp (msort x)))
(defthm how-many-merge2
(equal (how-many e (merge2 x y))
(+ (how-many e x) (how-many e y))))
(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))))
(defthm how-many-msort
(equal (how-many e (msort x))
(how-many e x)))
; (defthm perm-msort
; (perm (msort x) x))
|
