File: set-indices.lisp

package info (click to toggle)
acl2 8.5dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 991,452 kB
  • sloc: lisp: 15,567,759; javascript: 22,820; cpp: 13,929; ansic: 12,092; perl: 7,150; java: 4,405; xml: 3,884; makefile: 3,507; sh: 3,187; ruby: 2,633; ml: 763; python: 746; yacc: 723; awk: 295; csh: 186; php: 171; lex: 154; tcl: 49; asm: 23; haskell: 17
file content (100 lines) | stat: -rw-r--r-- 3,429 bytes parent folder | download | duplicates (3)
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))))