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