blob: 9495676f4d0c4190d3f71255a7048a4800dc41e3 (
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
|
(in-package "ACL2")
(defun cons-all (e x)
(declare (xargs :guard (true-listp x)))
(if (endp x)
nil
(cons (cons e (car x))
(cons-all e (cdr x)))))
(defun combinations (x n)
(declare (xargs :guard (and (true-listp x)
(natp n))))
(cond
((zp n) (list nil))
((endp x) nil)
(t
(append (cons-all (car x)
(combinations (cdr x) (- n 1)))
(combinations (cdr x) n)))))
(defun comb (n k)
(cond
((zp k) 1)
((zp n) 0)
(t (+ (comb (- n 1) k)
(comb (- n 1) (- k 1))))))
(defthm len-combinations
(equal (len (combinations x n))
(comb (len x) n)))
(defun factorial (n)
(if (zp n)
1
(* n (factorial (- n 1)))))
(include-book "arithmetic/top" :dir :system)
(defthm comb-zero
(implies (and (natp n)
(natp k)
(< n k))
(equal (comb n k) 0)))
(defthm comb-1
(implies (natp n)
(equal (comb n 1) n)))
(defthm comb-factorial-lemma
(implies (natp n)
(equal (* n (+ -1 n) x)
(+ (* (+ -1 n) x)
(* (+ -1 n) (+ -1 n) x))))
:rule-classes nil)
(defthm comb-factorial
(implies (natp n)
(equal (comb n k)
(cond ((zp k) 1)
((< n k) 0)
(t (/ (factorial n)
(* (factorial (- n k))
(factorial k)))))))
:hints (("Subgoal *1/4.2'" :use (:instance comb-factorial-lemma
(x (factorial (+ -2 n)))))))
(defthm len-combination-factorial
(equal (len (combinations x k))
(cond ((zp k) 1)
((< (len x) k) 0)
(t (/ (factorial (len x))
(* (factorial (- (len x) k))
(factorial k)))))))
|
