1; formerly (approximately) examples/acl2/examples/encap/example.lisp
2
3(in-package "ACL2")
4
5; This one is trivial, in the sense that its first argument is the empty list
6; of signatures.  The encapsulate should simply be removed.
7(encapsulate
8 ()
9 (defthm car-cons-1
10   (equal (car (cons x y))
11          x)))
12
13; This one is trivial, just as the one above, but has a local event, which
14; (like all local events inside an encapsulate) should be ignored.
15(encapsulate
16 ()
17 (local (defthm a-local-theorem
18          (equal (cdr (cons x y)) y)))
19 (defthm car-cons-2
20   (equal (car (cons x y))
21          x)))
22
23; This one is like the one just above except that it has three non-local
24; events.  This time, two of them are function definitions.
25(encapsulate
26 ()
27 (local (defthm a-local-theorem
28          (equal (cdr (cons x y)) y)))
29 (defun f1 (x)
30   x)
31 (defthm car-cons-3
32   (equal (car (cons x y))
33          x))
34 (defun f2 (x)
35   x))
36
37; Next we have an encapsulate whose signature is non-empty, thus introducing a
38; new function.  In this example, that function is axiomatized to return an
39; integer.  The translation could be a definition, along with a corresponding
40; theorem (presumably proved by showing the existence of the g1 guaranteed by
41; "some g1" below).
42; Definition.  g1 = some g1 . forall x . (integerp (g1 x))
43; |- forall x . |= (integerp (g1 x))
44(encapsulate
45 ((g1 (x) t))
46 (local (defun g1 (x)
47          (declare (ignore x))
48          0))
49 (defthm integerp-g1
50   (integerp (g1 x))))
51
52; The next one is similar to the one just above, except that the function
53; returns two values -- well, every function returns one value actually, so we
54; needn't explain the "two values" idea here, and maybe we won't have to deal
55; with it until we do a round trip.
56; Definition.  g2 = some g2 . (integerp (mv-nth 0 (g2 x)))
57; |- forall x . |= (integerp (mv-nth 0 (g2 x)))
58(encapsulate
59 ((g2 (x) (mv t t)))
60 (local (defun g2 (x)
61          (declare (ignore x))
62          (mv 0 0)))
63 (defthm integerp-first-g2
64   (integerp (mv-nth 0 (g2 x)))))
65
66; The next encapsulate is like the preceding one, except that it introduces two
67; functions.  We also use alternate syntax for encapsulate.  Presumably the
68; corresponding HOL might look sort of as follows.
69; Definition.  temp = some pair . let h1 = first(pair), h2 = second(pair) .
70;                                 forall x . forall y .
71;                                 (implies (integerp x) (integerp (h1 x)))
72;                              /\ (implies (integerp y)
73;                                          (integerp (mv-nth 0 (h2 x y))))
74; Definition.  h1 = first(temp)
75; Definition.  h2 = second(temp)
76; |- forall x . |= (implies (integerp x) (integerp (h1 x)))
77; |- forall x . forall y . |= (implies (integerp y)
78;                                      (integerp (mv-nth 0 (h2 x y))))
79(encapsulate
80 (((h1 *)   => *)
81  ((h2 * *) => (mv * *)))
82 (local (defun h1 (x) x))
83 (local (defun h2 (x y) (mv y x)))
84 (defthm h1-prop
85   (implies (integerp x)
86            (integerp (h1 x))))
87 (defthm h2-prop
88   (implies (integerp y)
89            (integerp (mv-nth 0 (h2 x y))))))
90
91; The next encapsulate is like the preceding one, except that it introduces
92; more axioms and a function not in the signature.  The idea is to treat h5 as
93; though it were being introduced too, because that is indeed the case.
94(encapsulate
95 (((h3 *)   => *)
96  ((h4 * *) => (mv * *)))
97 (local (defun h3 (x) x))
98 (local (defun h4 (x y) (mv y x)))
99 (defthm h3-prop
100   (implies (integerp x)
101            (integerp (h3 x))))
102 (defun h5 (x) (h3 x))
103 (defthm h4-h5-prop
104   (implies (integerp y)
105            (integerp (h5 (mv-nth 0 (h4 x y)))))))
106