← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/arithmetic/power2p.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/arithmetic/power2p.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;The rule power2p-rewrite has proven quite helpful.
 
4
 
 
5
(defund fl (x)
 
6
  (declare (xargs :guard (real/rationalp x)))
 
7
  (floor x 1))
 
8
 
 
9
(local (include-book "fl")) ;or could use floor?
 
10
(local (include-book "fp2"))
 
11
(local (include-book "predicate"))
 
12
(local (include-book "unary-divide"))
 
13
 
 
14
;old version
 
15
;(defun power2p (x)
 
16
 ; (equal x (expt 2 (expo x))))
 
17
 
 
18
(include-book "../../../ordinals/e0-ordinal")
 
19
(set-well-founded-relation e0-ord-<)
 
20
 
 
21
(defund power2p-measure (x)
 
22
  (declare (xargs :guard (and (rationalp x) (not (equal x 0)))))
 
23
  (cond ((or (not (rationalp x))
 
24
             (<= x 0)) 0)
 
25
        ((< x 1) (cons 1 (fl (/ x))))
 
26
        (t (fl x))))
 
27
 
 
28
(defund power2p (x)
 
29
  (declare (xargs :guard t
 
30
                  :measure (power2p-measure x)
 
31
                  :hints (("goal" :in-theory (enable power2p-measure)))))
 
32
  (cond ((or (not (rationalp x))
 
33
             (<= x 0))
 
34
         nil)
 
35
        ((< x 1) (power2p (* 2 x)))
 
36
        ((<= 2 x) (power2p (* 1/2 x)))
 
37
        ((equal x 1) t)
 
38
        (t nil) ;got a number in the doubly-open interval (1,2)
 
39
        ))
 
40
 
 
41
#| A term fits the "power of 2" pattern iff it is a tree built using * and /  (actually, binary-* and unary-/)
 
42
in which each leaf is either a rational constant which is a power of 2 or a term of the form (EXPT 2 I).
 
43
|#
 
44
 
 
45
(defund power2-syntaxp (term)
 
46
  (if (not (consp term))
 
47
      nil
 
48
    (case (car term)
 
49
      (quote (and (rationalp (cadr term)) 
 
50
                  (power2p (cadr term))))
 
51
      (expt (equal (cadr term) '(quote 2))) ;allow the base to be any power of 2?  (constants only? or (expt 2 n)??
 
52
      (binary-* (and (power2-syntaxp (cadr term))
 
53
                     (power2-syntaxp (caddr term))))
 
54
      (unary-/ (power2-syntaxp (cadr term)))
 
55
      (otherwise nil))))
 
56
 
 
57
#|
 
58
 
 
59
Notes:
 
60
 
 
61
(power2-syntaxp ''2)
 
62
(power2-syntaxp '(expt 2 i))
 
63
(power2-syntaxp '(unary-/ (expt 2 i)))
 
64
(power2-syntaxp '(binary-/ (expt 2 i) (expt 2 j)))
 
65
(power2-syntaxp '(binary-* (expt 2 i) (expt 2 j)))
 
66
(power2-syntaxp '(binary-* '2 (binary-* (expt '2 j) (expt '2 k))))
 
67
(power2-syntaxp '(binary-* '2 (binary-* (expt '2 j) (expt '2 (binary-+ k (binary-* '-1 j))))))
 
68
 
 
69
|#
 
70
 
 
71
 
 
72
;induction?
 
73
(defthmd power2p-with-arg-between-one-and-two
 
74
  (implies (and (< 1/2 x)
 
75
                (< x 1)
 
76
                )
 
77
           (not (power2p x)))
 
78
  :hints (("goal" :in-theory  (enable power2p)))
 
79
  )
 
80
 
 
81
(defthm power2p-of-non-rational
 
82
  (implies (not (rationalp x))
 
83
           (equal (power2p x)
 
84
                  nil))
 
85
  :hints (("goal" :in-theory (enable power2p))))
 
86
 
 
87
(defthm power2p-of-non-positive
 
88
  (implies (not (< 0 x))
 
89
           (equal (power2p x)
 
90
                  nil))
 
91
  :hints (("goal" :in-theory (enable power2p))))
 
92
 
 
93
;induction
 
94
(defthm power2p-inverse
 
95
  (and (equal (power2p (/ x))
 
96
              (power2p x))
 
97
       (equal (power2p (/ 1 x)) ;do we need this?
 
98
              (power2p x)))
 
99
  :otf-flg t
 
100
  :hints (("goal" :in-theory (enable power2p
 
101
                                     power2p-with-arg-between-one-and-two))))
 
102
 
 
103
;what about (/ -1 x) ? (/ 1 (- x)) ?
 
104
;in general, what if x is negative, and we have something like (power2p (- x)) ?
 
105
 
 
106
;power2p-double and power2p-half helped clean up the proof of power2p-prod
 
107
(defthmd power2p-double
 
108
  (equal (power2p (* 2 x))
 
109
         (power2p x))
 
110
  :hints (("goal" :in-theory (enable power2p
 
111
                                     power2p-with-arg-between-one-and-two))))
 
112
 
 
113
(defthmd power2p-half
 
114
  (equal (power2p (* 1/2 x))
 
115
         (power2p x))
 
116
  :hints (("goal" :in-theory (enable power2p
 
117
                                     power2p-with-arg-between-one-and-two))))
 
118
;consider enabling?
 
119
(defthmd power2p-prod
 
120
  (implies (and (power2p x)
 
121
                (power2p y))
 
122
           (power2p (* x y)))
 
123
  :hints (("goal" :in-theory (enable power2p power2p-double power2p-half
 
124
                                     power2p-with-arg-between-one-and-two))))
 
125
 
 
126
;robustify with power2p-quotient?
 
127
 
 
128
;reorder hyps?  make conclusion into an equality?
 
129
(defthmd power2p-prod-not
 
130
  (implies (and (not (power2p x))
 
131
                (power2p y)
 
132
                )
 
133
           (not (power2p (* x y))))
 
134
   :hints (("goal" :in-theory (disable power2p-prod)
 
135
            :use (:instance power2p-prod (x (* x y)) (y (/ y))))))
 
136
 
 
137
(defthm power2p-shift
 
138
  (implies (and (syntaxp (power2-syntaxp x))
 
139
                (force (power2p x)) ;this should be true if the syntaxp hyp is satisfied
 
140
                )
 
141
           (equal (power2p (* x y))
 
142
                  (power2p y)))
 
143
  :hints (("goal"
 
144
           :use ((:instance power2p-prod-not (y x) (x y))
 
145
                 (:instance power2p-prod (y x) (x y))))))
 
146
 
 
147
(defthm power2p-shift-2
 
148
  (implies (and (syntaxp (power2-syntaxp y))
 
149
                (force (power2p y)) ;this should be true if the syntaxp hyp is satisfied
 
150
                )
 
151
           (equal (power2p (* x y))
 
152
                  (power2p x)))
 
153
  :hints (("goal" :in-theory (disable power2p)
 
154
           :use ( power2p-prod-not power2p-prod))))
 
155
 
 
156
 
 
157
;make rules for quotient of powers of 2
 
158
 
 
159
 
 
160
(defthm power2p-means-positive-rationalp
 
161
  (implies (power2p x)
 
162
           (and (< 0 x)
 
163
                (rationalp x)))
 
164
  :rule-classes ((:forward-chaining :trigger-terms ((POWER2P X)))))
 
165
 
 
166