blob: 791e04edd0bfec2fa07db329ea9765f1e9a68f3a (
plain)
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
|
(defmacro zero? (x)
`(equal ,x nil))
(defmacro z? (x)
`(atom ,x))
(defmacro succ (x)
`(cons nil ,x))
(defmacro pred (x)
`(cdr ,x))
(defun nat? (x)
(if (z? x)
(null x)
(and (equal (car x) nil)
(nat? (pred x)))))
(defthm zero-is-nat
(implies (zero? x)
(nat? x)))
(defun nat= (x y)
(cond
((and (z? x) (z? y)) t)
((or (z? x) (z? y)) nil)
(t (nat= (pred x) (pred y)))))
(defthm nat-reflexive
(implies (nat? x)
(nat= x x)))
(defthm nat-symmetric
(implies (and (nat? x)
(nat? y))
(equal (nat= x y)
(nat= y x))))
(defthm nat-transitive
(implies (and (nat? x)
(nat? y)
(nat? z)
(nat= x y)
(nat= y z))
(nat= x z)))
(defthm nat=-to-equal
(implies (and (nat? x)
(nat? y))
(equal (nat= x y)
(equal x y))))
(defun nat+ (x y)
(if (z? y)
x
(succ (nat+ x (pred y)))))
(defthm nat+-commutative
(implies (and (nat? x)
(nat? y))
(equal (nat+ x y)
(nat+ y x))))
(defthm nat+-zero
(implies (nat? x)
(equal (nat+ nil x)
x)))
(defthm nat+-cancellative-1-1-1
(implies (and (consp x)
(nat? x)
(nat? k))
(not (equal (nat+ x k)
k))))
(defthm nat+-cancellative-1-1
(implies (and (consp x)
(nat? x)
(nat? k))
(not (equal (nat+ k x)
k)))
:hints (("Goal" :in-theory (disable nat+-commutative)
:use ((:instance nat+-commutative
(x x)
(y k))))))
(defthm nat+-cancellative-1
(implies (and (consp x)
(nat? x)
(nat? k))
(not (equal (nat+ k x)
k))))
(defthm nat+-cancellative
(implies (and (nat? x)
(nat? y)
(nat? k))
(equal (equal (nat+ k x) (nat+ k y))
(equal x y)))
:hints (("Goal" :induct (nat= x y))))
|
