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
|
(in-package "ACL2")
(defund fl (x)
(declare (xargs :guard (real/rationalp x)))
(floor x 1))
(include-book "ground-zero")
(local (include-book "logior"))
(local (include-book "../arithmetic/fl"))
(local (include-book "lognot"))
(defthm floor-logorc1-by-2
(implies (and (case-split (integerp i))
(case-split (integerp j))
)
(equal (floor (logorc1 i j) 2)
(logorc1 (floor i 2) (floor j 2))))
:hints (("Goal" :in-theory (enable logorc1))))
(defthm fl-logorc1-by-2
(implies (and (case-split (integerp i))
(case-split (integerp j))
)
(equal (fl (* 1/2 (logorc1 i j)))
(logorc1 (fl (* 1/2 i)) (fl (* 1/2 j)))))
:hints (("Goal" :in-theory (enable logorc1))))
#| not true
(defthm mod-LOGORC1
(implies (and (case-split (integerp i))
(case-split (integerp j))
)
(equal (mod (logorc1 i j) 2)
(logorc1 (mod i 2) (mod j 2))))
:hints (("Goal" :in-theory (enable logorc1))))
|#
#|
(local
(defthm logorc1-mod-1
(implies (and (integerp i) (integerp j))
(iff (= (mod (logorc1 i j) 2) 0)
(and (= (mod (lognot i) 2) 0)
(= (mod j 2) 0))))
:rule-classes ()
:hints (("Goal" :in-theory (disable logior lognot)
:use ((:instance mod-logior-10 (i (lognot i))))))))
(local(defthm logorc1-mod
(implies (and (integerp i) (>= i 0)
(integerp j))
(iff (= (mod (logorc1 i j) 2) 0)
(and (= (mod i 2) 1)
(= (mod j 2) 0))))
:rule-classes ()
:hints (("Goal" :in-theory (disable logior lognot)
:use ((:instance mod-logior-9)
(:instance logorc1-mod-1)
(:instance mod012 (x i)))))))
|#
(defthm logorc1-type
(implies (and (<= 0 i)
(<= 0 j))
(< (logorc1 i j) 0))
:rule-classes (:rewrite :type-prescription)
:hints (("Goal" :in-theory (enable logorc1 lognot))))
|
