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
|
(in-package "ACL2")
;This book contains basic arith stuff which i'm pretty sure won't hurt anything.
(local (include-book "arith2"))
;This is a meta rule to cancel identical terms from both sides of an equality of sums.
(include-book "meta/meta-plus-equal" :dir :system)
;This is a meta rule to cancel identical terms from both sides of a < of sums.
(include-book "meta/meta-plus-lessp" :dir :system)
;This is a meta rule to cancel identical terms from both sides of an equality of products (I think).
(include-book "meta/meta-times-equal" :dir :system)
;Note! There is not meta-times-lessp, which would be really nice to have. I now have a bind-free rule to do that...
(defthm collect-constants-in-equal-of-sums
(implies (and (syntaxp (and (quotep c1) (quotep c2)))
(case-split (acl2-numberp c1))
)
(and (equal (equal (+ c2 x) c1)
(equal (fix x) (- c1 c2)))
(equal (equal c1 (+ c2 x))
(equal (fix x) (- c1 c2))))))
(defthm collect-constants-in-equal-of-sums-2
(implies (syntaxp (and (quotep c1) (quotep c2)))
(and (equal (equal (+ c2 x) (+ c1 y))
(equal (fix x) (+ (- c1 c2) y))))))
(defthm collect-constants-in-<-of-sums
(implies (syntaxp (and (quotep c1) (quotep c2)))
(and (equal (< (+ c2 x) c1)
(< x (- c1 c2)))
(equal (< c1 (+ c2 x))
(< (- c1 c2) x)))))
(defthm collect-constants-in-<-of-sums-2
(implies (syntaxp (and (quotep c1) (quotep c2)))
(equal (< (+ c2 x) (+ c1 y))
(< x (+ (- c1 c2) y)))))
;I put this in because it seems to help rewrite stupid hyps quickly.
(defthm dumb
(equal (< x x)
nil))
|
