← 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/rhs2.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/rhs2.lisp
 
1
; Here is another example of a double-rewrite warning from the right-hand side
 
2
; of a rewrite rule (see also rhs1.lisp).
 
3
 
 
4
(in-package "ACL2")
 
5
 
 
6
; The following explanation is given in a bit more detail in the associated
 
7
; paper.
 
8
 
 
9
; The problem illustrated below is that when we are relieving hyps, we have
 
10
; just one rewrite to make everything work.  So we cannot rely on the second
 
11
; pass.
 
12
 
 
13
; In more detail, we need to relieve (h (e (f a))).  H admits equiv1 as a
 
14
; congruence.  We use rule1 to rewrite (h (e (f a))) to (h (f a)).  Then we'd
 
15
; like to use rule2 to rewrite (h (f a)) to (h (g a)) so we can finish by
 
16
; appealing to rule4.  But without a double-rewrite on the right-hand side of
 
17
; rule1 it won't work.
 
18
 
 
19
; The above is not absolutely correct.  There is a way to make it work without
 
20
; putting a double-rewrite on the right-hand side of rule1.  The way is to put
 
21
; TWO double-rewrites in rule3, i.e., turn it into
 
22
 
 
23
; (defthm rule3 (implies (h (double-rewrite (double-rewrite x))) (c x)))
 
24
 
 
25
; But we don't like that because you can't predict how many nested
 
26
; double-rewrites you'll need.  The "fault" lies with rule1.
 
27
 
 
28
(skip-proofs
 
29
 (progn
 
30
   (defstub equiv1 (x y) t)
 
31
   (defequiv equiv1)
 
32
 
 
33
   (defstub c (x) t)
 
34
   (defstub e (x) t)
 
35
   (defstub f (x) t)
 
36
   (defstub g (x) t)
 
37
   (defstub h (x) t)
 
38
   (defstub i (x) t)
 
39
   (defthm rule1 (equiv1 (e x) x)) ; Double-rewrite warning for x on rhs
 
40
   (defthm rule2 (equiv1 (f x) (g x)))
 
41
   (defcong equiv1 equal (h x) 1)
 
42
   (defthm rule3 (implies (h (double-rewrite (double-rewrite x))) (c x)))
 
43
   (defthm rule4 (h (g a)))))
 
44
 
 
45
(defthm test
 
46
  (c (e (f a))))