blob: 670c372902d60aaa83e2b5ef57f108f9e3c1453a (
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
|
; Copyright (C) 2014, Regents of the University of Texas
; Original author: Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
; See book-thms.lisp. This is an example that tests the utilities contained in
; that book.
(include-book "book-thms")
; Example:
(logic)
(local (encapsulate-then-new-info
my-name
(defthm foo
(equal (car (cons x y)) x))
(defun f1 (x y) (<= x y))
(defthm bar
(< (acl2-count x) (acl2-count (cons x y))))
(defun-sk exists-x-f1 (y)
(exists x (f1 x y)))
(encapsulate ((f (x) t)
(h (x) t))
(local (defun f (x) x))
(defun g (x) (f x))
(local (defun h (x) x))
(defthm my-thm
(equal (f x) (h (g x)))))
(defchoose my-ch (x) (y)
(f1 x (cons 0 y)))
))
(local
(assert-event
(equal (my-name)
'((FOO :THEOREM (EQUAL (CAR (CONS X Y)) X))
(F1 :DEF (EQUAL (F1 X Y) (<= X Y)))
(BAR :THEOREM (< (ACL2-COUNT X)
(ACL2-COUNT (CONS X Y))))
(EXISTS-X-F1-SUFF :THEOREM (IMPLIES (F1 X Y) (EXISTS-X-F1 Y)))
((EXISTS-X-F1 EXISTS-X-F1-WITNESS)
:CONSTRAINT
(AND (EQUAL (EXISTS-X-F1 Y)
(LET ((X (EXISTS-X-F1-WITNESS Y)))
(F1 X Y)))
(IMPLIES (F1 X Y) (EXISTS-X-F1 Y))))
(MY-THM :THEOREM (EQUAL (F X) (H (G X))))
((G F H)
:CONSTRAINT
(AND (EQUAL (G X) (F X))
(EQUAL (F X) (H (G X)))))
(MY-CH :DEFCHOOSE (IMPLIES (F1 X (CONS 0 Y))
(LET ((X (MY-CH Y)))
(F1 X (CONS 0 Y)))))))))
|
