blob: 20d2793a32248b62f6e4808dabb3b2ba2b1d0e87 (
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
103
104
105
106
107
108
109
110
111
112
|
;;; divisor-list.lisp: 約数に関する証明
(in-package "ACL2")
;; e が x の約数であるかどうかを調べる述語
(defmacro divisorp (e x)
`(integerp (/ ,x ,e)))
;; n の約数のリストを作る
(defun divisors-1 (n i)
(cond
((zp i) nil)
((divisorp i n)
(cons i (divisors-1 n (1- i))))
(t
(divisors-1 n (1- i)))))
(defmacro divisors (n)
`(divisors-1 ,n ,n))
;; x が n の約数のリストかどうかを調べる述語
(defun divisor-listp (x n)
(cond
((endp x) (null x))
(t (and (divisorp (car x) n)
(divisor-listp (cdr x) n)))))
;; 約数リストは真リストであることを示す定理
(defthm divisor-listp-to-true-listp
(implies (divisor-listp x n)
(true-listp x))
:rule-classes :forward-chaining)
;; divisors の結果は約数リストである
(defthm divisor-listp-divisors-1
(implies (and (natp n)
(posp m))
(divisor-listp (divisors-1 n m) n)))
(defthm divisor-listp-divisors
(implies (posp n)
(divisor-listp (divisors n) n)))
;; 正数 x について x - 1 が正数でないとき x は 1
(defthm posp-and-not-posp-n-1
(implies (posp n)
(iff (not (posp (+ -1 n)))
(equal n 1))))
;; divisorp-implies-member-divisors-1 の補助定理
(defthm divisorp-implies-member-divisors-1-lemma
(implies (and (natp n)
(posp m)
(not (posp (+ -1 m))))
(integerp (* (/ m) n)))
:hints (("Goal" :in-theory (disable posp-and-not-posp-n-1)
:use (:instance posp-and-not-posp-n-1
(n m)))))
;; e (e <= n) が n の約数のとき (divisors n) に
;; e が含まれている
(defthm divisorp-implies-member-divisors-1
(implies (and (natp n)
(posp m)
(posp e)
(<= e m))
(implies (divisorp e n)
(member e (divisors-1 n m))))
:hints (("Goal" :in-theory (disable posp-and-not-posp-n-1)
:use (:instance posp-and-not-posp-n-1
(n m)))))
(defthm divisorp-implies-member-divisors
(implies (and (posp n)
(posp e)
(<= e n))
(implies (divisorp e n)
(member e (divisors n)))))
;; (divisors n) に e が含まれているとき、
;; e は n の約数
(defthm member-divisors-1-implies-divisorp
(implies (and (natp n)
(posp m)
(posp e)
(member e (divisors-1 n m)))
(divisorp e n)))
(defthm member-divisors-implies-divisorp
(implies (and (posp n)
(posp e))
(implies (member e (divisors n))
(divisorp e n)))
:hints (("Goal" :in-theory (disable
member-divisors-1-implies-divisorp)
:use ((:instance member-divisors-1-implies-divisorp
(n n)
(m n)
(e e))))))
;; (divisors n) に e (<= n) が含まれていることは
;; e が n の約数であることの
;; 必要十分条件である
(defthm member-divisors-iff-divisorp
(implies (and (posp n)
(posp e)
(<= e n))
(iff (member e (divisors n))
(divisorp e n)))
:hints (("Goal" :in-theory (disable member-divisors-implies-divisorp)
:use ((:instance member-divisors-implies-divisorp
(n n)
(e e))))))
|
