blob: 57c8d8940156ec9da17877b72da41e1e813e9e16 (
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 "isort")
(in-package "ACL2")
(include-book "perm")
(include-book "ordered-perms")
(include-book "convert-perm-to-how-many")
(defun insert (e x)
(if (endp x)
(cons e x)
(if (lexorder e (car x))
(cons e x)
(cons (car x)
(insert e (cdr x))))))
(defun isort (x)
(if (endp x)
nil
(insert (car x)
(isort (cdr x)))))
(defthm orderedp-isort
(orderedp (isort x)))
(defthm true-listp-isort
(true-listp (isort x)))
(defthm how-many-isort
(equal (how-many e (isort x))
(how-many e x)))
; (defthm perm-isort
; (perm (isort x) x))
|
