← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/arithmetic/fl-expt.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/fl-expt.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;don't need everything in this book!
 
4
(local (include-book "numerator"))
 
5
(local (include-book "denominator"))
 
6
(local (include-book "nniq"))
 
7
(local (include-book "arith2"))
 
8
;(local (include-book "type"))
 
9
(local (include-book "ground-zero"))
 
10
(local (include-book "floor"))
 
11
(local (include-book "integerp"))
 
12
(local (include-book "rationalp"))
 
13
(local (include-book "unary-divide"))
 
14
(local (include-book "expt"))
 
15
(local (include-book "expo"))
 
16
(local (include-book "power2p"))
 
17
(local (include-book "fl"))
 
18
 
 
19
(local (in-theory (enable expt-minus)))
 
20
 
 
21
(defun fl (x)
 
22
  (declare (xargs :guard (real/rationalp x)))
 
23
  (floor x 1))
 
24
 
 
25
;more general vesions of this below.  kill this one?
 
26
(defthm fl-simp
 
27
  (implies (case-split (rationalp x))
 
28
           (equal (FL (* 1/2 (FL (* X (/ (EXPT 2 N))))))
 
29
                  (FL (* 1/2 X (/ (EXPT 2 N))))))
 
30
  :hints (("Goal" :in-theory (disable fl-def-linear)
 
31
           :use 
 
32
           ((:instance fl-unique 
 
33
                       (x (* 1/2 (FL (* X (/ (EXPT 2 N))))))
 
34
                       (n (FL (* 1/2 X (/ (EXPT 2 N))))))
 
35
            (:instance fl-def-linear (x (* 1/2 X (/ (EXPT 2 N)))))))))
 
36
 
 
37
 
 
38
 
 
39
(encapsulate
 
40
 ()
 
41
 (local (defthm fl-shift-fl-case-1
 
42
          (implies (<= 0 m)
 
43
                   (equal (FL (* (FL X) (/ (expt 2 m))))
 
44
                          (FL (* X (/ (EXPT 2 m))))))
 
45
          :hints (("Goal" :cases ((rationalp x))))
 
46
          ))
 
47
 
 
48
 (local (defthm fl-shift-fl-case-2
 
49
          (implies (AND (< m 0)
 
50
                        (case-split (INTEGERP M))
 
51
                        )
 
52
                   (equal (FL (* (FL X) (/ (expt 2 m))))
 
53
                          (* (FL x) (/ (expt 2 m)))))
 
54
          :hints  (("Goal" :in-theory (disable fl-int)
 
55
                    :use (:instance fl-int (x (* (/ (expt 2 m)) (FL X))))))))
 
56
 
 
57
 
 
58
 
 
59
;can this be extended to let the out fl be of a sum?
 
60
;leave the case-1 event enabled too (not integerp hyp)?
 
61
 (defthm fl-shift-fl
 
62
   (implies (case-split (INTEGERP M))
 
63
            (equal (FL (* (/ (expt 2 m)) (FL X)))
 
64
                   (if (<= 0 m)
 
65
                       (FL (* (/ (EXPT 2 m)) X))
 
66
                     (* (/ (expt 2 m)) (FL x)))))
 
67
   :hints (("Goal" :cases ((< m 0))))
 
68
   )
 
69
 )
 
70
 
 
71
 
 
72
#|
 
73
(defthm fl-shift-fl-case-1-gen
 
74
  (implies (and (rationalp x)
 
75
                (rationalp y)
 
76
                (integerp m)
 
77
                (<= 0 m)
 
78
                )
 
79
           (equal (fl (* (/ (expt 2 m)) (+ y (* 2 (fl (* 1/2 x))))))
 
80
                  (fl (* (/ (expt 2 m)) (+ y x)))))
 
81
  :otf-flg t
 
82
 :hints (("Goal" :in-theory (disable  FL-DEF-LINEAR-PART-1
 
83
                                       FL-DEF-LINEAR-PART-2
 
84
                                       FL-WEAK-MONOTONE
 
85
;                                        LESS-THAN-MULTIPLY-THROUGH-BY-inverted-factor-FROM-LEFT-HAND-SIDE
 
86
                                       )
 
87
          :use (
 
88
          (:instance FL-DEF-LINEAR-part-1  
 
89
                     (x (+ (* X (/ (EXPT 2 M)))
 
90
                           (* Y (/ (EXPT 2 M))))))
 
91
          (:instance FL-DEF-LINEAR-part-1  
 
92
                     (x x))
 
93
          (:instance FL-DEF-LINEAR-part-2  
 
94
                     (x (+ (* X (/ (EXPT 2 M)))
 
95
                           (* Y (/ (EXPT 2 M))))))
 
96
          (:instance FL-DEF-LINEAR-part-2  
 
97
                     (x x))
 
98
 
 
99
          (:instance fl-unique 
 
100
                     (x (* (/ (expt 2 m)) (+ y (* 2 (FL (* 1/2 X))))))
 
101
                     (n (FL (* (/ (EXPT 2 m)) (+ y X)))))))))
 
102
|#
 
103
 
 
104
(defthm fl-shift-fl-2-factors
 
105
  (implies (AND ;(case-split (rationalp x))
 
106
                (case-split (INTEGERP M))
 
107
                (case-split (INTEGERP n))
 
108
                )
 
109
           (equal (FL (* (/ (expt 2 m)) (expt 2 n) (FL X)))
 
110
                  (if (<= 0 (- m n))
 
111
                      (FL (* (/ (EXPT 2 (- m n))) X))
 
112
                    (* (/ (expt 2 (- m n))) (FL x)))))
 
113
  :hints (("Goal" :in-theory (set-difference-theories
 
114
                              (enable expt-split)
 
115
                              '( fl-shift-fl  ;EXPO-COMPARISON-REWRITE-TO-BOUND
 
116
                                              ))
 
117
           :use (:instance fl-shift-fl (m (- m n))))))
 
118
 
 
119
(defthm fl-shift-fl-2-factors-2
 
120
  (implies (AND ;(case-split (rationalp x))
 
121
                (case-split (INTEGERP M))
 
122
                (case-split (INTEGERP n))
 
123
                )
 
124
           (equal (FL (* (expt 2 n) (/ (expt 2 m)) (FL X)))
 
125
                  (if (<= 0 (- m n))
 
126
                      (fl (* (/ (EXPT 2 (- m n))) X))
 
127
                    (* (/ (expt 2 (- m n))) (FL x)))))
 
128
  :hints (("Goal" :in-theory (set-difference-theories
 
129
                              (enable expt-split)
 
130
                              '( fl-shift-fl EXPO-COMPARISON-REWRITE-TO-BOUND))
 
131
           :use (:instance fl-shift-fl (m (- m n))))))
 
132
 
 
133
 
 
134
 
 
135
;(FL (* 2 (/ (EXPT 2 K)) (FL (* 1/2 X))))
 
136
 
 
137
 
 
138
(defthm fl-shift-fl-by-1
 
139
  (EQUAL (FL (* 1/2 (FL X)))
 
140
         (FL (* 1/2 X)))
 
141
  :hints (("Goal" :use (:instance fl-shift-fl (m 1)))))
 
142
 
 
143
 
 
144