← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/arithmetic/even-odd.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/even-odd.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(local (include-book "integerp"))
 
4
(local (include-book "predicate"))
 
5
(local (include-book "fp2"))
 
6
 
 
7
;a funny little rule:
 
8
;can be expensive!
 
9
;perhaps should export disabled
 
10
;make a forward-chaining rule?
 
11
(defthmd even-int-implies-int
 
12
  (implies (and (integerp (* 1/2 x))
 
13
                (rationalp x) ;gen?
 
14
                )
 
15
           (integerp x))
 
16
  :rule-classes ((:rewrite :backchain-limit-lst (1 nil)))
 
17
  :hints (("Goal" :in-theory (disable integerp-prod)
 
18
           :use (:instance integerp-prod (x (* 1/2 x)) (y 2)))))
 
19
 
 
20
;this book is currently a mess.
 
21
 
 
22
;normal forms: leave evenp and oddp enabled
 
23
 
 
24
;from basic
 
25
(defun INDUCT-NAT (x)
 
26
  (if (and (integerp x)
 
27
           (> x 0))
 
28
      (induct-nat (1- x))
 
29
    ()))
 
30
 
 
31
 
 
32
(local
 
33
 (defthm x-or-x/2-4
 
34
   (implies (and (integerp x) (>= x 0))
 
35
            (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
 
36
   :rule-classes ()
 
37
   :hints (("Goal" :induct (induct-nat x)))))
 
38
 
 
39
;is this sort of thing elsewhere? integerp.lisp?
 
40
(defthm integerp-+
 
41
  (implies (and (integerp x)
 
42
                (integerp y))
 
43
           (integerp (+ x y))))
 
44
 
 
45
(defthm x-or-x/2
 
46
  (implies (integerp x) 
 
47
           (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
 
48
  :rule-classes ()
 
49
  :hints (("Goal" :in-theory (disable integerp-+)
 
50
           :use ((:instance integerp-+ (x (+ 1/2 (* -1/2 X))) (y x))
 
51
                 (:instance x-or-x/2-4)
 
52
                 (:instance x-or-x/2-4 (x (- x)))))))
 
53
 
 
54
 
 
55
 
 
56
;end stuff from basic
 
57
 
 
58
(encapsulate
 
59
 ()
 
60
 (local (defthm hack-int
 
61
          (implies (and (integerp x)
 
62
                        (integerp y))
 
63
                   (integerp (+ x y)))))
 
64
 
 
65
 (defthm integerp-sum-of-odds-over-2
 
66
   (implies (and (rationalp x)
 
67
                 (rationalp y)
 
68
                 (integerp (* 2 x)) ;these two hyps say x is of the form (odd)/2
 
69
                 (not (integerp x)) ;
 
70
                 )
 
71
            (equal (integerp (+ x y))
 
72
                   (and (integerp (* 2 y))
 
73
                        (not (integerp y)) ; (oddp (* 2 y)) ;rephrase the oddp hyps?
 
74
                        )))
 
75
   :hints (("Goal" :in-theory (disable even-int-implies-int)
 
76
            :use ( (:instance even-int-implies-int (x (+ (* 2 x) (* 2 y))))
 
77
                   (:instance hack-int (x (+ 1/2 X)) (y (+ 1/2 y)))
 
78
                   (:instance x-or-x/2 (x (* 2 x)))
 
79
                   (:instance x-or-x/2 (x (* 2 y)))))))
 
80
 )
 
81
 
 
82
;derive the results below from the above (or eliminate them)
 
83
 
 
84
(in-theory (disable integerp-sum-of-odds-over-2))
 
85
 
 
86
;make this a rewrite?
 
87
;special case
 
88
(defthm integerp-sum-of-odds-over-2-leading-constant
 
89
  (implies (and (syntaxp (and (quotep x)
 
90
                              (integerp (* 2 x)) ;;these two hyps say x is of the form (odd)/2
 
91
                              (not (integerp x)) ;; 
 
92
                              ))
 
93
                (rationalp x)
 
94
                (rationalp y)
 
95
                (integerp (* 2 x)) ;;these two hyps say x is of the form (odd)/2
 
96
                (not (integerp x)) ;;
 
97
                (integerp (* 2 y))
 
98
                (not (integerp y)) ; (oddp (* 2 y)) ;rephrase the oddp hyps?
 
99
                )
 
100
           (integerp (+ x y)))
 
101
  :hints (("Goal" :use integerp-sum-of-odds-over-2)))
 
102
 
 
103
;do we need all this stuff?
 
104
 
 
105
;(defthm even-or-odd
 
106
 ; (implies (integerp x)
 
107
  ;         (or (evenp x) (oddp x)))
 
108
  ;:rule-classes nil)
 
109
 
 
110
;should be a rewrite? - general rewrites for evenp/oddp of sum/diff?
 
111
;(defthm odd-+-1
 
112
 ; (implies (and (integerp x)
 
113
  ;              (oddp x))
 
114
   ;        (evenp (+ 1 x)))
 
115
  ;:hints (("Goal" :use (:instance x-or-x/2 ))))
 
116
 
 
117
;(defthm odd/2-plus-1/2
 
118
 ; (implies (and (integerp x)
 
119
  ;              (oddp x))
 
120
   ;        (integerp (+ 1/2 (/ x 2))))
 
121
  ;:hints (("Goal" :use (:instance odd-+-1))))
 
122
 
 
123
;hack, don't leave enabled ;rewrite?
 
124
;(defthm integerp-next
 
125
 ; (implies (and (rationalp x)
 
126
  ;              (integerp (+ x 1)))
 
127
   ;        (integerp x)))
 
128
 
 
129
;(defthm odd/2-minus-1/2
 
130
 ; (implies (and (integerp x)
 
131
  ;              (oddp x))
 
132
   ;        (integerp (+ -1/2 (/ x 2))))
 
133
  ;:hints (("Goal" :use (:instance odd/2-plus-1/2))))
 
134
 
 
135
;(in-theory (disable integerp-next))
 
136
 
 
137
;(defthm odd/2-minus-1/2-alt
 
138
 ; (implies (and (integerp x)
 
139
  ;              (oddp x))
 
140
   ;        (integerp (+ -1/2 (* 1/2 x))))
 
141
 ; :hints (("Goal" :in-theory (disable  odd/2-minus-1/2)
 
142
  ;         :use (:instance  odd/2-minus-1/2))))
 
143
 
 
144
;floor of odd/2 is odd/2 -1/2
 
145
 
 
146
 
 
147
 ;; :hints (("Goal" :use ( (:instance  fl-unique 
 
148
   ;                                  (x (* 1/2 x))
 
149
    ;                                 (n (- (* 1/2 x) 1/2)))))))
 
150
 
 
151
 
 
152
;needed?
 
153
 
 
154
(defthm even-and-odd-alternate-eric
 
155
  (implies (and (rationalp x)
 
156
                (integerp (* 2 x)))
 
157
           (equal (integerp (+ 1/2 x))
 
158
                  (not (integerp x)))))
 
159
 
 
160
 
 
161
;should this go in type.lisp?
 
162
;needed? ;lets change any leading constant of -1/2 to 1/2 and elim this rule
 
163
(defthm even-and-odd-alternate-3
 
164
  (implies (and (integerp x))
 
165
           (equal (integerp (+ -1/2 (* -1/2 x)))
 
166
                  (not (integerp (* 1/2 x)))))
 
167
  :hints (("Goal" :in-theory (disable integerp-minus)
 
168
           :use (:instance integerp-minus (x (+ -1/2 (* -1/2 x)))))))
 
169
 
 
170
#| never finished this
 
171
(defthm integerp-+-odd-over-2-reduce
 
172
  (implies (and (rationalp x)
 
173
                (integerp (* 2 x)) ;these two hyps say x is of the form (odd)/2
 
174
                (not (integerp x))
 
175
                (rationalp y))
 
176
           (implies (integerp (+ x y))
 
177
                    (and (integerp (* 2 y)) ;these two hyps say x is of the form (odd)/2
 
178
                         (not (integerp y))))) ;
 
179
  :otf-flg t
 
180
  :hints (("Goal" :use  integerp-sum-of-odds-over-2)))
 
181
|#
 
182
 
 
183
 
 
184
 
 
185
 
 
186
(defthm even-and-odd-alternate-eric-2-bk
 
187
  (implies (rationalp x)
 
188
           (implies (and (integerp (* 2 x))
 
189
                         (not (integerp x)))
 
190
                    (integerp (+ 1/2 x)))))
 
191
 
 
192
;if s is even, then s-1 is odd
 
193
(defthm even-odd-5
 
194
  (implies (and (rationalp x)
 
195
                (integerp (* 1/2 x)))
 
196
           (and (integerp (- x 1))
 
197
                (not (integerp (* 1/2 (- x 1))))))
 
198
  :hints (("Goal" :in-theory (enable even-int-implies-int)))
 
199
)
 
200
 
 
201
 
 
202
(defthm even-and-odd-alternate-eric-2-fw
 
203
  (implies (rationalp x)
 
204
           (implies (integerp (+ 1/2 x))
 
205
                  (and (integerp (* 2 x))
 
206
                       (not (integerp x)))))
 
207
  :hints (("Goal"
 
208
           :in-theory (disable even-odd-5)
 
209
           :use (:instance even-odd-5 (x (+ 1 (* 2 x)))))))
 
210
 
 
211
 
 
212
;replace the 1/2 rules above and similarly generalize the rules at the top to be equal rules
 
213
(defthm even-and-odd-alternate-eric-2
 
214
  (implies (rationalp x)
 
215
           (equal (integerp (+ 1/2 x))
 
216
                  (and (integerp (* 2 x))
 
217
                       (not (integerp x))))))
 
218
 
 
219
(in-theory (disable  even-and-odd-alternate-eric-2-fw even-and-odd-alternate-eric-2-bk))
 
220
 
 
221