1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
(in-package "ACL2")
(local (include-book "ground-zero"))
(local (include-book "fp2"))
;denom of non-rat?
(defthm denominator-positive-integer-type-prescription
(and (< 0 (denominator x))
(integerp (denominator x)))
:rule-classes (:type-prescription))
(defthm denominator-positive
(< 0 (denominator x))
:rule-classes (:rewrite :linear))
(defthm denominator-integerp
(integerp (denominator x)))
(defthm denominator-one-means-integer
(implies (case-split (rationalp x))
(equal (equal (denominator x) 1)
(integerp x)))
:hints (("goal" :in-theory (disable rational-implies2)
:use (rational-implies2
(:instance lowest-terms
(n (denominator x))
(r x)
(q 1))))))
(defthm denominator-of-integer-is-one
(implies (integerp x)
(equal (denominator x)
1)))
;linear?
(encapsulate
()
(local (include-book "arithmetic/mod-gcd" :dir :system))
(defthm denominator-lower-bound
(implies (and (< 0 q)
(integerp p)
(integerp q)
)
(<= (denominator (* p (/ q))) q))
:hints (("goal" :use (:instance least-numerator-denominator-<= (n p) (d q))))
))
|
