blob: 8c7f7d3e2b84b6d8a9edb47d885a62627f1e279c (
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
|
(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
(nat= x x))
(defthm nat=-symmetric
(equal (nat= x y)
(nat= y x)))
(defthm nat=-transitive
(implies (and (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+-right-cancellative
(equal (equal (nat+ x k) (nat+ y k))
(equal x y)))
(defthm nat+-left-cancellative
(implies (and (nat? x)
(nat? y)
(nat? k))
(equal (equal (nat+ k x) (nat+ k y))
(equal x y)))
:hints (("Goal" :in-theory (disable nat+-commutative)
:use ((:instance nat+-commutative
(x x)
(y k))
(:instance nat+-commutative
(x y)
(y k))))))
(defthm associativity-of-nat+
(equal (nat+ x (nat+ y z))
(nat+ (nat+ x y) z)))
|
