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
|
;; Copyright (C) 2017, Regents of the University of Texas
;; Written by Cuong Chau (derived from the FM9001 work of Brock and Hunt)
;; License: A 3-clause BSD license. See the LICENSE file distributed with
;; ACL2.
;; The ACL2 source code for the FM9001 work is available at
;; https://github.com/acl2/acl2/tree/master/books/projects/fm9001.
;; Cuong Chau <ckcuong@cs.utexas.edu>
;; January 2019
;; For doing proofs of recursive module generators, it is often necessary to
;; know that a signal name is "unbound", i.e., does not appear further in the
;; generated body. By a "body" we mean an occurrence body, and by "bound" we
;; mean assigned a value in the ALIST created by SE-OCC. This concept is
;; eloquently summed up in the final two lemmas of this file.
(in-package "ADE")
(include-book "de")
;; ======================================================================
;; UNBOUND-IN-BODY
(defun unbound-in-body (name body)
(if (atom body)
t
(let ((occurrence (car body)))
(let ((outputs (occ-outs occurrence)))
(and (not (member name outputs))
(unbound-in-body name (cdr body)))))))
(defthm unbound-in-body-atom
(implies (atom body)
(unbound-in-body name body)))
(defthm unbound-in-body-listp
(equal (unbound-in-body name (cons occurrence rest))
(let ((outputs (occ-outs occurrence)))
(and (not (member name outputs))
(unbound-in-body name rest)))))
(in-theory (disable unbound-in-body))
;; ALL-UNBOUND-IN-BODY
(defun all-unbound-in-body (names body)
(if (atom body)
t
(let ((occurrence (car body)))
(let ((outputs (occ-outs occurrence)))
(and (disjoint names outputs)
(all-unbound-in-body names (cdr body)))))))
(defthm all-unbound-in-body-atom
(implies (atom body)
(all-unbound-in-body names body)))
(defthm all-unbound-in-body-listp
(equal (all-unbound-in-body names (cons occurrence rest))
(let ((outputs (occ-outs occurrence)))
(and (disjoint names outputs)
(all-unbound-in-body names rest)))))
(defthm all-unbound-in-body-append
(equal (all-unbound-in-body (append names1 names2) body)
(and (all-unbound-in-body names1 body)
(all-unbound-in-body names2 body))))
(defthm all-unbound-in-body-cons
(equal (all-unbound-in-body (cons name names) body)
(and (unbound-in-body name body)
(all-unbound-in-body names body))))
(defthm all-unbound-in-body-atom-names
(implies (atom names)
(all-unbound-in-body names body)))
(in-theory (disable all-unbound-in-body))
;; Lemmas
(defthm unbound-in-body-se-occ
(implies (unbound-in-body name body)
(equal (assoc-eq-value name
(se-occ body
bindings
state-bindings
netlist))
(assoc-eq-value name bindings)))
:hints (("Goal"
:induct (se-occ-induct body bindings state-bindings netlist))))
(defthm all-unbound-in-body-se-occ
(implies (all-unbound-in-body names body)
(equal (assoc-eq-values
names
(se-occ body bindings state-bindings netlist))
(assoc-eq-values names bindings)))
:hints (("Goal"
:induct (se-occ-induct body bindings state-bindings netlist))))
|
