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