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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
; 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")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(include-book "building-blocks")
(local
(include-book "types-helper"))
(local
(defthm equal-to-iff-1
(equal (equal (rationalp x) (rationalp y))
(iff (rationalp x) (rationalp y)))))
(local
(defthm equal-to-iff-1-real-case
(equal (equal (real/rationalp x) (real/rationalp y))
(iff (real/rationalp x) (real/rationalp y)))))
(local
(defthm equal-to-iff-2
(equal (equal (integerp x) (integerp y))
(iff (integerp x) (integerp y)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; These next two are subsumed by meta-integerp-correct or
;;; meta-rationalp-correct.
;;;(defthm rationalp-+
;;; (implies (and (rationalp x)
;;; (rationalp y))
;;; (rationalp (+ x y)))
;;; :rule-classes ((:rewrite :backchain-limit-lst 2)))
;;;(defthm integerp-+
;;; (implies (and (integerp x)
;;; (integerp y))
;;; (integerp (+ x y)))
;;; :rule-classes ((:rewrite :backchain-limit-lst 2)))
(defthm |(rationalp (- x))|
(implies (acl2-numberp x)
(equal (rationalp (- x))
(rationalp x))))
#+non-standard-analysis
(defthm |(real/rationalp (- x))|
(implies (acl2-numberp x)
(equal (real/rationalp (- x))
(real/rationalp x))))
(defthm |(integerp (- x))|
(implies (acl2-numberp x)
(equal (integerp (- x))
(integerp x))))
;;; These next two are subsumed by meta-integerp-correct or
;;; meta-rationalp-correct.
;;;(defthm rationalp-*
;;; (implies (and (rationalp x)
;;; (rationalp y))
;;; (rationalp (* x y)))
;;; :rule-classes ((:rewrite :backchain-limit-lst 2)))
;;;(defthm integerp-*
;;; (implies (and (integerp x)
;;; (integerp y))
;;; (integerp (* x y)))
;;; :rule-classes ((:rewrite :backchain-limit-lst 2)))
(defthm rationalp-/
(implies (acl2-numberp x)
(equal (rationalp (/ x))
(rationalp x))))
#+non-standard-analysis
(defthm real/rationalp-/
(implies (acl2-numberp x)
(equal (real/rationalp (/ x))
(real/rationalp x))))
(defthm not-integerp-/-1
(implies (< 1 x)
(not (integerp (/ x)))))
(defthm not-integerp-/-2
(implies (< x -1)
(not (integerp (/ x)))))
;;; We do not introduce the case-split unless we are rewriting a goal
;;; literal.
(defthm integerp-/
(implies (and (syntaxp (rewriting-goal-literal x mfc state))
(integerp x))
(equal (integerp (/ x))
(or (equal x -1)
(equal x 0)
(equal x 1)))))
(defthm rationalp-x
(implies (integerp x)
(rationalp x))
:rule-classes ((:rewrite :backchain-limit-lst 2)))
#+non-standard-analysis
(defthm real/rationalp-x
(implies (integerp x)
(real/rationalp x))
:rule-classes ((:rewrite :backchain-limit-lst 3)))
(defthm acl2-numberp-x
(implies (rationalp x)
(acl2-numberp x))
:rule-classes ((:rewrite :backchain-limit-lst 3)))
#+non-standard-analysis
(defthm acl2-number-if-real/rationalp-x
(implies (real/rationalp x)
(acl2-numberp x))
:rule-classes ((:rewrite :backchain-limit-lst 3)))
|
