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
|
; These events were initially contributed by Robert Krug and incorporated
; after ACL2 Version 3.2.1. See the "Essay on Type-set Deductions for
; Integerp" in the ACL2 sources for a discussion of a change to ACL2 that
; allowed for the proofs of the theorems below, where they had previously
; failed.
(in-package "ACL2")
(encapsulate
((foo (x) t))
(local (defun foo (x) x))
(defthm foo-thm
(implies x
(foo x))))
; Make sure we use only type-reasoning to relieve foo-thm's
; hypothesis.
(set-backchain-limit 0)
(defthm lemma-1
(implies (and (rationalp x)
(integerp (* 1/2 x)))
(foo (integerp x)))
:rule-classes nil)
(defthm lemma-2
(implies (and (rationalp x)
(integerp (* 2 x)))
(foo (integerp (* 4 x))))
:rule-classes nil)
(defthm lemma-3
(implies (and (rationalp x)
(integerp (* 2 x)))
(foo (integerp (+ -1 (* 4 x)))))
:rule-classes nil)
(defthm lemma-4
(implies (and (rationalp x)
(integerp (+ 1 x)))
(foo (integerp (+ 2 x))))
:rule-classes nil)
(defthm lemma-5
(implies (and (rationalp x)
(integerp (+ 1 x)))
(foo (integerp x)))
:rule-classes nil)
(defthm lemma-6
(implies (and (rationalp x)
(integerp (+ -1/2 x)))
(foo (integerp (+ 1/2 x))))
:rule-classes nil)
(defthm lemma-7
(implies (and (rationalp x)
(integerp (* 2 x)))
(foo (not (integerp (+ 1/2 (* 4 x))))))
:rule-classes nil)
(defun not-integerp (x)
(not (integerp x)))
(defthm not-integerp-implies-not-integerp
(implies (not (integerp x))
(not-integerp x)))
(in-theory (disable not-integerp))
(defthm lemma-8
(implies (and (rationalp x)
(integerp (+ 1/2 x)))
(foo (not-integerp x)))
:rule-classes nil)
|
