← 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/greve1.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/greve1.lisp
 
1
; A double-rewrite example based on events from Dave Greve.
 
2
 
 
3
(in-package "ACL2")
 
4
 
 
5
(defun equiv (x y)
 
6
  (equal x y))
 
7
 
 
8
(defequiv equiv)
 
9
 
 
10
(encapsulate
 
11
 ((foo (x) t)
 
12
  (pred (x) t)
 
13
  (goo (x) t)
 
14
  (hoo (x) t))
 
15
 
 
16
 (set-ignore-ok t)
 
17
 (set-irrelevant-formals-ok t)
 
18
 (local (defun foo (x) t))
 
19
 (local (defun pred (x) t))
 
20
 (local (defun goo (x) t))
 
21
 (local (defun hoo (x) t))
 
22
 
 
23
 (defthm pred-hoo
 
24
   (pred (hoo x)))
 
25
 (defthm goo-to-hoo
 
26
   (equiv (goo x) (hoo x)))
 
27
 (defcong equiv iff (pred x) 1)
 
28
 (defthm pred-implies-foo
 
29
   (implies
 
30
    (pred (double-rewrite x)) ; warning eliminated by double-rewrite call
 
31
    (foo x))))
 
32
 
 
33
(defthm foo-of-goo-equiv-enabled
 
34
  (foo (goo x))
 
35
  :rule-classes nil)
 
36
 
 
37
; Let's keep equiv in the mix for experiments below.
 
38
(in-theory (disable equiv))
 
39
 
 
40
(defthm foo-of-goo
 
41
  (foo (goo x))
 
42
  :rule-classes nil)
 
43
 
 
44
(defthm foo-of-goo-again
 
45
  (foo (goo x))
 
46
  :rule-classes nil)
 
47
 
 
48
(defthm pred-implies-foo-again
 
49
  (implies
 
50
   (and (equiv y (double-rewrite x))
 
51
        (pred y))
 
52
   (foo x)))
 
53
 
 
54
(in-theory (disable pred-implies-foo))
 
55
 
 
56
(defthm foo-of-goo-yet-again
 
57
  (foo (goo x))
 
58
  :rule-classes nil)
 
59
 
 
60
; The following modification of pred-implies-foo-again (above) generates a
 
61
; double-rewrite warning, because without the double-rewrite call, the equiv
 
62
; hypothesis does not bind y.
 
63
(defthm pred-implies-foo-again-with-warning
 
64
  (implies (and (equiv y x)
 
65
                (pred y))
 
66
           (foo x)))
 
67
 
 
68
; Fails, as the above-mentioned warning suggests could happen:
 
69
; (thm (foo (goo x))
 
70
;      :hints (("Goal" :in-theory (disable pred-implies-foo-again))))