; This exercise is a minor re-working of the distributed book:
; books/sorting/isort.lisp
(in-package "ACL2")
(include-book "sorting/perm" :dir :system)
(include-book "convert-perm-to-how-many")
(include-book "ordered-perms")
(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 how-many-isort
(equal (how-many e (isort x))
(how-many e x)))
; Follows now from convert-perm-to-how-many:
(defthm isort-perm
(perm (isort x) x))