blob: 04accb63f81bbf68fbef0d8b3cd7f1004da92141 (
plain)
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
101
102
103
104
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; misc.lisp
;;;
;;; A collection of things that don't easily fit elsewhere.
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "bytes-and-words")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defthm eqlable-alistp-alistp
(implies (eqlable-alistp l)
(alistp l)))
(defund nat-to-boolean (x)
(not (= x 0)))
; Lists and Association Lists of Natural Numbers
(defund n08p-listp (xlst)
(if (atom xlst)
(null xlst)
(and (n08p (car xlst))
(n08p-listp (cdr xlst)))))
(defund n16p-listp (xlst)
(if (atom xlst)
(null xlst)
(and (n16p (car xlst))
(n16p-listp (cdr xlst)))))
(defund n32p-listp (xlst)
(if (atom xlst)
(null xlst)
(and (n32p (car xlst))
(n32p-listp (cdr xlst)))))
(defund n01p-alistp (alst)
(if (atom alst)
(symbolp alst)
(and (consp (car alst))
(n01p (cdar alst))
(n01p-alistp (cdr alst)))))
(defund n08p-alistp (alst)
(if (atom alst)
(symbolp alst)
(and (consp (car alst))
(n08p (cdar alst))
(n08p-alistp (cdr alst)))))
(defund n16p-alistp (alst)
(if (atom alst)
(symbolp alst)
(and (consp (car alst))
(n16p (cdar alst))
(n16p-alistp (cdr alst)))))
(defund n32p-alistp (alst)
(if (atom alst)
(symbolp alst)
(and (consp (car alst))
(n32p (cdar alst))
(n32p-alistp (cdr alst)))))
(defund symbolp-n32-alistp (alst)
(if (atom alst)
(symbolp alst)
(and (consp (car alst))
(symbolp (caar alst))
(n32p (cdar alst))
(n32p-alistp (cdr alst)))))
(defthmd natp-+
(implies (and (natp a)
(natp b))
(natp (+ a b))))
;;; from alist-thms:
(defthm n08p-alistp-put-assoc-equal
(implies (and (n08p-alistp al)
(n08p val))
(n08p-alistp (put-assoc-equal tag val al)))
:hints (("Goal" :in-theory (enable n08p-alistp))))
(defthm n32p-alistp-put-assoc-equal
(implies (and (n32p-alistp al)
(n32p val))
(n32p-alistp (put-assoc-equal tag val al)))
:hints (("Goal" :in-theory (enable n32p-alistp))))
;; May not be necessary
(defthm assoc-put-assoc-equal
(implies (alistp al)
(equal (assoc tag (put-assoc-equal tag val al))
(cons tag val))))
|
