1(in-package "ACL2")
2
3#|
4
5  apply-total-order.lisp
6  ~~~~~~~~~~~~~~~~~~~~~~
7
8In this book, we describe some simple functions like insert and drop
9on a totally ordered list, and provide rules to manipulate them. The
10functions that we introduce are insert, drop, memberp, orderedp, and
11uniquep. Then we prove some theorems that we wish to export from this
12book.
13
14|#
15
16(include-book "total-order")
17
18(defun memberp (a x)
19  (and (consp x)
20       (or (equal a (first x))
21           (memberp a (rest x)))))
22
23(defun drop (a x)
24  (cond ((endp x) ())
25        ((equal a (first x))
26         (drop a (rest x)))
27        (t (cons (first x)
28                 (drop a (rest x))))))
29
30(defun insert (a x)
31  (cond ((endp x) (list a))
32        ((equal a (first x)) x)
33        ((<< a (first x)) (cons a x))
34        (t (cons (first x)
35                 (insert a (rest x))))))
36
37(defun orderedp (x)
38  (or (endp (rest x))
39      (and (<< (first x) (second x))
40           (orderedp (rest x)))))
41
42(defun uniquep (x)
43  (or (endp x)
44      (and (not (memberp (first x) (rest x)))
45           (uniquep (rest x)))))
46
47;;;; some simple properties about insert, drop, and member
48
49(defthm memberp-insert-same
50  (equal (memberp a (insert a x)) T))
51
52(defthm memberp-insert-diff
53  (implies (not (equal a b))
54           (equal (memberp a (insert b x))
55                  (memberp a x))))
56
57(defthm memberp-drop-same
58  (equal (memberp a (drop a x)) nil))
59
60(defthm memberp-drop-diff
61  (implies (not (equal a b))
62           (equal (memberp a (drop b x))
63                  (memberp a x))))
64
65(defthm ordered-implies-unique
66  (implies (orderedp x)
67           (uniquep x))
68  :rule-classes (:forward-chaining
69                 :rewrite))
70
71(defthm memberp-yes-reduce-insert
72  (implies (and (orderedp x)
73                (memberp a x))
74           (equal (insert a x) x)))
75
76(defthm memberp-no-reduce-drop
77  (implies (and (true-listp x)
78                (not (memberp a x)))
79           (equal (drop a x) x)))
80
81(local
82(defthm drop-is-monotonic
83  (implies (and (orderedp x)
84                (<< y (first x))
85                (consp (drop a x)))
86           (<< y (first (drop a x)))))
87)
88
89(defthm drop-preserves-orderedp
90  (implies (orderedp x)
91           (orderedp (drop a x))))
92
93(defthm insert-preserves-orderedp
94  (implies (orderedp x)
95           (orderedp (insert a x))))
96
97(defthm drop-of-insert-is-same
98  (implies (and (true-listp x)
99                (not (memberp a x)))
100           (equal (drop a (insert a x)) x)))
101
102(defthm insert-of-drop-is-same
103  (implies (and (orderedp x)
104                (true-listp x)
105                (memberp a x))
106           (equal (insert a (drop a x)) x)))
107
108(defthm insert-returns-true-lists
109  (implies (true-listp x)
110           (true-listp (insert a x)))
111  :rule-classes :type-prescription)
112