blob: 3eef0820443bb3bab5979171a764d687fcc7d4ec (
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
|
;; Julien Schmaltz
;; File: octagon-nodeset.lisp
;; August 15th
;; definition and validation of the nodes of the Octagon
(in-package "ACL2")
;; we import the book containing the generic definition of NodeSet
(include-book "../../generic-modules/GeNoC-nodeset")
;; 1. OctagonNodeSetGenerator
;; -------------------------
(defun naturals (bound)
;; define the naturals up to bound
;; they are the nodes of the Octagon
(if (zp bound)
(list 0)
(cons bound (naturals (1- bound)))))
(defun OctagonNodeSetGenerator (bound)
;; more precisely we choose the bound to be the
;; number of nodes in one quarter of the Octagon
(naturals (+ -1 (* 4 bound))))
(defun OctagonValidParamsp (x)
;; the parameter is a positive integer and not zero
(and (integerp x) (< 0 x)))
;; 2. OctagonNodeSetp
;; -----------------
(defun OctagonValidNodep (x)
;; a valid node is simply a natural
(natp x))
(defun OctagonNodeSetp (x)
;; corresponds to the predicate NodeSetp
(if (endp x)
t
(and (OctagonValidNodep (car x))
(OctagonNodeSetp (cdr x)))))
;; 3. Validation of the nodes of the Octagon
;; -----------------------------------------
;; we need to prove
(defthm octagon-subsets-are-valid
(implies (and (OctagonNodeSetp x)
(subsetp y x))
(OctagonNodeSetp y)))
(defthm OctagonNodeSetp-naturals
;; lemma needed for the next theorem
(implies (and (integerp bound) (< 0 bound))
(OctagonNodeSetp (naturals bound))))
(defthm check-compliance-octagon-nodeset
t
:rule-classes nil
:hints (("GOAL"
:use (:functional-instance
nodeset-generates-valid-nodes
(ValidParamsp OctagonValidParamsp)
(NodeSetp OctagonNodeSetp)
(Nodesetgenerator OctagonNodeSetGenerator))
:in-theory (disable nodeset-generates-valid-nodes))))
|
