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
|
(in-package "HANOI")
(acl2::set-verify-guards-eagerness 2)
(defund new-stack ()
nil)
(defund stackp (stk)
(true-listp stk))
(defund has-morep (stk)
(declare (xargs :guard (stackp stk)))
(consp stk))
(defund push (v stk)
(declare (xargs :guard (stackp stk)))
(cons v stk))
(local (in-theory (enable stackp has-morep)))
(defund pop (stk)
(declare (xargs :guard (and (stackp stk)
(has-morep stk))))
(cdr stk))
(defund top (stk)
(declare (xargs :guard (and (stackp stk)
(has-morep stk))))
(car stk))
;----------------------------------------------------------------------
(defthm push-stackp
(implies (stackp stk)
(stackp (push v stk)))
:hints (("Goal" :in-theory (enable stackp push))))
(defthm pop-stackp
(implies (and (stackp stk)
(has-morep stk))
(stackp (pop stk)))
:hints (("Goal" :in-theory (enable stackp pop))))
(defthm new-stack-stackp
(stackp (new-stack))
:hints (("Goal" :in-theory (enable stackp new-stack))))
(defthm new-stack-empty
(not (has-morep (new-stack)))
:hints (("Goal" :in-theory (enable stackp has-morep new-stack))))
|
