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
|
(in-package "ACL2")
; cert_param: (non-acl2r)
(local (include-book "predicate"))
(defthm complex-rationalp-+-when-second-term-is-rational
(implies (rationalp y)
(equal (complex-rationalp (+ x y))
(complex-rationalp x))))
(defthm complex-rationalp-+-when-second-term-is-not-complex
(implies (not (complex-rationalp y))
(equal (complex-rationalp (+ x y))
(complex-rationalp x))))
(defthm complex-rationalp-+-when-first-term-is-rational
(implies (rationalp x)
(equal (complex-rationalp (+ x y))
(complex-rationalp y))))
(defthm complex-rationalp-+-when-first-term-is-not-complex
(implies (not (complex-rationalp x))
(equal (complex-rationalp (+ x y))
(complex-rationalp y))))
;add more cases
(defthm complex-rationalp-*-drop-first-term-if-rational
(implies (and (case-split (not (equal y 0)))
(rationalp y))
(equal (complex-rationalp (* y x))
(complex-rationalp x))))
#|
(defthm complex-rationalp-*-drop-first-term-if-not-complex
(implies (and (case-split (not (equal y 0)))
(not (complex-rationalp y))
)
(equal (complex-rationalp (* y x))
(complex-rationalp x))))
|#
|
