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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
; Arithmetic-5 Library
; Written by Robert Krug
; Copyright/License:
; See the LICENSE file at the top level of the arithmetic-5 library.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; types.lisp
;;;
;;; The neccesity for these theorems does not arise very often,
;;; but it can be very irritating when they do.
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(local
(include-book "../../support/top"))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(local
(defthm one-a
(implies (and (< 0 x)
(< x 1))
(not (integerp x)))))
(local
(defthm one-b
(implies (and (< x 0)
(< -1 x))
(not (integerp x)))))
(local
(defthm two-a
(implies (and (real/rationalp x)
(< 1 x))
(and (< 0 (/ x))
(< (/ x) 1)))
:hints (("Goal" :in-theory (enable NORMALIZE-<-/-TO-*-2)))))
(local
(defthm two-b
(implies (and (real/rationalp x)
(< x -1))
(and (< (/ x) 0)
(< -1 (/ x))))
:hints (("Goal" :in-theory (enable NORMALIZE-<-/-TO-*-1)))))
(local
(defthm three
(implies (complex/complex-rationalp x)
(not (integerp (/ x))))))
(defthm not-integerp-/-1
(implies (< 1 x)
(not (integerp (/ x))))
:hints (("Goal" :cases ((real/rationalp x)
(complex/complex-rationalp x)))))
(defthm not-integerp-/-2
(implies (< x -1)
(not (integerp (/ x))))
:hints (("Goal" :cases ((real/rationalp x)
(complex/complex-rationalp x)))))
(defthm integerp-/-helper
(implies (integerp x)
(equal (integerp (/ x))
(or (equal x -1)
(equal x 0)
(equal x 1))))
:hints (("Goal" :use ((:instance not-integerp-/-1)
(:instance not-integerp-/-2))
:in-theory (disable not-integerp-/-1
not-integerp-/-2))))
|
