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 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
|
(in-package "ACL2")
(local (include-book "../file-system-lemmas"))
(include-book "bounded-nat-listp")
(defun set-indices (v index-list value-list)
(declare (xargs :guard (and (true-listp v)
(nat-listp index-list)
(true-listp value-list)
(equal (len index-list) (len value-list)))))
(if (atom index-list)
v
(set-indices (update-nth (car index-list) (car value-list) v)
(cdr index-list)
(cdr value-list))))
(defthm set-indices-correctness-1
(implies (and (natp n)
(nat-listp index-list)
(not (member-equal n index-list)))
(equal (nth n (set-indices v index-list value-list))
(nth n v))))
(defthm set-indices-correctness-2
(implies (and (true-listp v)
(nat-listp index-list)
(true-listp value-list)
(equal (len index-list)
(len value-list))
(no-duplicatesp-equal index-list)
(natp m)
(< m (len index-list)))
(equal (nth (nth m index-list)
(set-indices v index-list value-list))
(nth m value-list))))
(defthm set-indices-correctness-3
(implies (bounded-nat-listp index-list (len v))
(equal (len (set-indices v index-list value-list))
(len v))))
(defthm set-indices-correctness-4
(implies (and (boolean-listp v)
(nat-listp index-list)
(boolean-listp value-list)
(equal (len index-list)
(len value-list)))
(boolean-listp (set-indices v index-list value-list))))
(defund set-indices-in-alv (alv index-list value)
(declare (xargs :guard (and (boolean-listp alv)
(nat-listp index-list)
(booleanp value))))
(set-indices alv index-list (make-list (len index-list) :initial-element value)))
(defthm
set-indices-in-alv-correctness-1
(implies
(and (boolean-listp alv)
(booleanp value))
(boolean-listp (set-indices-in-alv alv index-list value)))
:rule-classes (:type-prescription :rewrite)
:hints (("Goal" :in-theory (enable set-indices-in-alv))))
(defthm
set-indices-in-alv-correctness-2
(implies
(and (boolean-listp alv)
(booleanp value)
(bounded-nat-listp index-list (len alv)))
(equal (len (set-indices-in-alv alv index-list value))
(len alv)))
:hints (("Goal" :in-theory (enable set-indices-in-alv))))
(defthm
set-indices-in-alv-correctness-3
(implies
(and (boolean-listp alv)
(nat-listp index-list)
(booleanp value)
(member-equal n index-list)
(< n (len alv)))
(equal (nth n
(set-indices-in-alv alv index-list value))
value))
:hints (("Goal" :in-theory (enable set-indices-in-alv))))
(defthm
set-indices-in-alv-correctness-4
(implies
(and (boolean-listp alv)
(nat-listp index-list)
(booleanp value)
(natp n)
(not (member-equal n index-list))
(< n (len alv)))
(equal (nth n
(set-indices-in-alv alv index-list value))
(nth n alv)))
:hints (("Goal" :in-theory (enable set-indices-in-alv))))
|