consecutive-fibonacci-numbers-are-coprime: Gcd$ is common-divisor.

1 files changed, 23 insertions, 0 deletions

diff --git a/consecutive-fibonacci-numbers-are-coprime.lisp b/consecutive-fibonacci-numbers-are-coprime.lisp
index 1700e8e..5b807a4 100644
--- a/consecutive-fibonacci-numbers-are-coprime.lisp
+++ b/consecutive-fibonacci-numbers-are-coprime.lisp
@@ -31,6 +31,29 @@
                 (posp n))
            (posp (gcd$ m n))))
 
+;; c が n と m の公約数であるかを調べる述語
+(defmacro common-divisor-p (c n m)
+  `(and (integerp (* ,n (/ ,c)))
+        (integerp (* ,m (/ ,c)))))
+
+;; gcd-is-common-divisor の補助定理
+(defthm gcd-is-common-divisor-lemma-1
+  (implies (common-divisor-p c (+ (- a) b) a)
+           (integerp (* b (/ c))))
+  :rule-classes ((:rewrite :match-free :all)))
+
+;; gcd-is-common-divisor の補助定理
+(defthm gcd-is-common-divisor-lemma-2
+  (implies (common-divisor-p c (+ a (- b)) b)
+           (integerp (* a (/ c))))
+  :rule-classes ((:rewrite :match-free :all)))
+
+;; (gcd$ n m) は n と m の公約数である
+(defthm gcd-is-common-divisor
+  (implies (and (natp n)
+                (natp m))
+           (common-divisor-p (gcd$ m n) n m)))
+
 ;; n と m が互いに素かどうかを調べる述語
 (defmacro coprimep (n m)
   `(equal (gcd$ ,n ,m) 1))