← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2006/kaufmann-moore/support/austel.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2006/kaufmann-moore/support/austel.lisp
 
1
; This example is essentially due to Vernon Austel.
 
2
 
 
3
(in-package "ACL2")
 
4
 
 
5
(defun eqv (x y)
 
6
  (equal x y))
 
7
 
 
8
(defequiv eqv)
 
9
 
 
10
(in-theory (disable eqv))
 
11
 
 
12
(encapsulate
 
13
 (((prop * *) => *)
 
14
  ((fn1 *) => *))
 
15
 
 
16
 (set-ignore-ok t)
 
17
 (set-irrelevant-formals-ok t)
 
18
 
 
19
 (local (defun prop (x y) t))
 
20
 (local (defun fn1 (x) x))
 
21
 
 
22
 (defthm booleanp-prop
 
23
   (booleanp (prop x y))
 
24
   :rule-classes (:rewrite :type-prescription))
 
25
 
 
26
 (defthm eqv-fn-prop
 
27
   (eqv (fn1 x) x)) ; Double-rewrite warning for x on rhs
 
28
 
 
29
 (defthm prop-thm
 
30
   (implies (eqv (double-rewrite x) y) ; Double-rewrite warning for y
 
31
            (prop x y)))
 
32
 )
 
33
 
 
34
(defthm prop-fn1
 
35
  (prop (fn1 x) x))
 
36
 
 
37
; Theorem prop-fn1-fails below is the same as prop-fn1 just above, but fails
 
38
; because the double-rewrite call is missing on x in prop-thm-bad.
 
39
 
 
40
(defthm prop-thm-bad
 
41
   (implies (eqv x y) ; Double-rewrite warning for x and y
 
42
            (prop x y)))
 
43
 
 
44
(in-theory (disable prop-fn1 prop-thm))
 
45
 
 
46
; See comment above.
 
47
; (defthm prop-fn1-fails
 
48
;   (prop (fn1 x) x))
 
49
 
 
50
; The following eliminates all warnings for the rule.
 
51
 
 
52
(defthm prop-thm-overkill
 
53
   (implies (eqv (double-rewrite x) (double-rewrite y))
 
54
            (prop x y)))