← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/arithmetic/unary-divide.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/unary-divide.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(local (include-book "predicate"))
 
4
(local (include-book "fp2"))
 
5
(local (include-book "inverted-factor"))
 
6
 
 
7
(defthm unary-divide-less-than-zero
 
8
  (implies (case-split (not (complex-rationalp x))) ;drop?
 
9
           (equal (< (/ x) 0)
 
10
                  (< x 0))))
 
11
 
 
12
#|
 
13
;try
 
14
(defthm unary-divide-less-than-zero
 
15
  (implies t;(case-split (not (complex-rationalp x))) ;drop?
 
16
           (equal (< (/ x) 0)
 
17
                  (< x 0))))
 
18
|#
 
19
 
 
20
;perhaps we don't need these, if we have rules like
 
21
;less-than-multiply-through-by-inverted-factor-from-left-hand-side ?
 
22
(defthm unary-divide-greater-than-zero
 
23
  (implies (case-split (not (complex-rationalp x))) ;drop?
 
24
           (equal (< 0 (/ x))
 
25
                  (< 0 x))))
 
26
 
 
27
(defthm unary-divide-equal-0
 
28
  (implies (case-split (acl2-numberp x))
 
29
           (equal (equal 0 (/ x))
 
30
                  (equal 0 x))))
 
31
 
 
32
;BOZO Why do we require the constant to be non-zero?
 
33
(defthm unary-divide-equal-non-zero-constant
 
34
  (implies (and (syntaxp (and (quotep k)
 
35
                              ;(not (equal 0 (cadr k)))
 
36
                              ))  ;drop?
 
37
                ;(case-split (not (equal 0 k)))
 
38
                (case-split (acl2-numberp x))
 
39
                (case-split (acl2-numberp k))
 
40
                )
 
41
           (equal (equal k (/ x))
 
42
                  (equal (/ k) x))))
 
43
 
 
44
;make a negative case?
 
45
(defthm unary-divide-less-than-non-zero-constant
 
46
  (implies (and (syntaxp (and (quotep k) (not (equal 0 (cadr k)))))  ;drop?
 
47
                (<= 0 k)
 
48
                (case-split (<= 0 x))
 
49
                (case-split (not (equal 0 k)))
 
50
                (case-split (not (equal 0 x)))
 
51
                (case-split (rationalp x))
 
52
                (case-split (rationalp k))
 
53
                )
 
54
           (equal (< (/ x) k)
 
55
                  (< (/ k) x))))
 
56
 
 
57
 
 
58
;once with this msg failed:
 
59
;1x (:REWRITE UNARY-DIVIDE-GREATER-THAN-NON-ZERO-CONSTANT) failed because it permutes a big term forward.
 
60
;so I changed the conclusion to not use unary-/
 
61
(defthm unary-divide-greater-than-non-zero-constant
 
62
  (implies (and (syntaxp (and (quotep k) (not (equal 0 (cadr k)))))  ;drop?
 
63
                (<= 0 k)
 
64
                (case-split (<= 0 x))
 
65
                (case-split (not (equal 0 k)))
 
66
                (case-split (not (equal 0 x)))
 
67
                (case-split (rationalp x))
 
68
                (case-split (rationalp k))
 
69
                )
 
70
           (equal (< k (/ x))
 
71
                  (< x (/ 1 k)))))
 
 
b'\\ No newline at end of file'