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
|
(in-package "ACL2")
(defund fl (x)
(declare (xargs :guard (real/rationalp x)))
(floor x 1))
(include-book "ground-zero")
(local (include-book "../arithmetic/top"))
(defthm lognot-of-non-integer
(implies (not (integerp i))
(equal (lognot i)
-1))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-lognot
(implies (case-split (integerp i))
(equal (lognot (lognot i))
i))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-integerp
(integerp (lognot i))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-equal-minus-one
(implies (case-split (integerp i))
(equal (EQUAL (LOGNOT i) -1)
(equal i 0)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-equal-0
(implies (case-split (integerp i))
(equal (EQUAL (LOGNOT i) 0)
(equal i -1)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-<-0
(implies (case-split (integerp i))
(equal (< (lognot i) 0)
(<= 0 i)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot->-0
(implies (case-split (integerp i))
(equal (< 0 (lognot i))
(< i -1)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-even
(implies (case-split (integerp i))
(equal (integerp (* 1/2 (lognot i)))
(not (integerp (* 1/2 i)))))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-of-double
(implies (case-split (integerp i))
(EQUAL (LOGNOT (* 2 i))
(+ 1 (* 2 (LOGNOT i)))))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-of-double-minus-1
(implies (case-split (integerp i))
(EQUAL (LOGNOT (1- (* 2 i)))
(* 2 (LOGNOT (1- i)))))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-simp
(implies (case-split (integerp i))
(equal (LOGNOT (+ 1 (* 2 i)))
(* 2 (LOGNOT i))))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-bound-1
(implies (case-split (integerp i))
(equal (< (LOGNOT I) -1)
(< 0 i)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-bound-2
(implies (case-split (integerp i))
(equal (< -1 (LOGNOT I))
(< i 0)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-bound-gen
(implies (and (case-split (integerp i))
(case-split (rationalp k)))
(equal (< (LOGNOT I) k)
(< (1- (- k)) i)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm lognot-bound-gen-2
(implies (and (case-split (integerp i))
(case-split (rationalp k)))
(equal (< k (LOGNOT I))
(< i (1- (- k)))))
:hints (("Goal" :in-theory (enable lognot))))
;from ihs
(defthm cancel-equal-lognot
(equal (equal (lognot i) (lognot j))
(equal (ifix i) (ifix j)))
:hints (("Goal" :in-theory (enable lognot))))
(defthm fl-lognot
(implies (case-split (integerp i))
(= (fl (* 1/2 (lognot i)))
(lognot (fl (* 1/2 i)))))
:hints (("Goal" :in-theory (enable lognot))))
(defthm floor-lognot
(implies (case-split (integerp i))
(equal (floor (lognot i) 2)
(lognot (floor i 2)))))
(defthm mod-lognot-by-2
(implies (case-split (integerp i))
(equal (mod (lognot i) 2)
(+ 2 (lognot (mod i 2)))))
:hints (("Goal" :in-theory (enable lognot mod-mult-of-n mod-by-2-rewrite-to-even)))
)
|
