From 42f3851f4f6b80acdc416ff0f95bee52ef369b9a Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Tue, 5 Jan 2021 10:25:26 +0900
Subject: wip69

---
 vikalpa/prelude.scm | 47 +++++++++++++++++++++++++++++------------------
 1 file changed, 29 insertions(+), 18 deletions(-)

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index e24d32d..74cbe98 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -43,6 +43,21 @@
       (- x)
       0))
 
+(define-syntax-rule (define-axiom/is p1 p2)
+  (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x))))
+
+(define-syntax-rule (define-theorem/is p1 p2)
+  (define-theorem (is p1 p2) (x) (is (p1 x) (p2 x))))
+
+(define-syntax-rule (define-proof/is p1 p2 pc)
+  (define-proof (is p1 p2)
+    ((rewrite (2) if-same (set x (pc x)))
+     (rewrite (2 2 1) (is pc p2))
+     (eval (2 2))
+     (rewrite (2 1) (is p1 pc))
+     (rewrite (2) if-true)
+     (rewrite () if-same))))
+
 (define-syntax implies
   (syntax-rules ()
     ((_ x y) (if x y #t))
@@ -97,15 +112,16 @@
 
   (define-core-function real? (x) real?)
   (define-axiom (predicate real?) (x) (predicate (real? x)))
-  (define-axiom (is real? number?) (x) (is (real? x) (number? x)))
+  (define-axiom/is real? number?)
 
   (define-core-function integer? (x) integer?)
   (define-axiom (predicate integer?) (x) (predicate (integer? x)))
-  (define-axiom (is integer? real?) (x) (is (integer? x) (real? x)))
+  (define-axiom/is integer? real?)
+  (define-theorem/is integer? number?)
+  (define-proof/is integer? number? real?)
 
   (define-core-function/guard exact? (x) (number? x) exact?)
   (define-axiom (predicate exact?) (x) (predicate (exact? x)))
-
   (define-function/guard inexact? (x)
     (number? x)
     (not (exact? x)))
@@ -113,13 +129,12 @@
 
   (define-core-function exact-integer? (x) exact-integer?)
   (define-axiom (predicate exact-integer?) (x) (predicate (exact-integer? x)))
-  (define-axiom (is exact-integer? integer?) (x)
-    (is (exact-integer? x)
-        (integer? x)))
-  (define-axiom (is exact-integer? exact?) (x) (is (exact-integer? x)
-                                                   (exact? x)))
-  (define-theorem (is exact-integer? real?) (x)
-    (is (exact-integer? x) (real? x)))
+  (define-axiom/is exact-integer? integer?)
+  (define-axiom/is exact-integer? exact?)
+  (define-theorem/is exact-integer? real?)
+  (define-proof/is exact-integer? real? integer?)
+  (define-theorem/is exact-integer? number?)
+  (define-proof/is exact-integer? number? real?)
   (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
   (define-axiom (predicate <) (x y) (predicate (< x y)))
 
@@ -137,17 +152,20 @@
          (positive? x)))
   (define-theorem (predicate exact-positive-integer?) (x)
     (predicate (exact-positive-integer? x)))
+  (define-theorem/is exact-positive-integer? exact-integer?)
 
   (define-function exact-zero? (x) (equal? x 0))
   (define-theorem (predicate exact-zero?) (x)
     (predicate (exact-zero? x)))
+  (define-theorem/is exact-zero? exact-integer?)
 
   (define-function natural? (x)
     (if (exact-zero? x)
         #t
         (exact-positive-integer? x)))
   (define-theorem (predicate natural?) (x)
-    (predicate (natural? x))))
+    (predicate (natural? x)))
+  (define-theorem/is natural? exact-integer?))
 
 (define-system prelude/measure/natural (prelude/number)
   (set-measure-predicate natural?)
@@ -192,13 +210,6 @@
      (rewrite (2 1) (predicate <))
      (eval (2))
      (rewrite () if-same)))
-  (define-proof (is exact-integer? real?)
-    ((rewrite (2) if-same (set x (integer? x)))
-     (rewrite (2 2 1) (is integer? real?))
-     (eval (2 2))
-     (rewrite (2 1) (is exact-integer? integer?))
-     (rewrite (2) if-true)
-     (rewrite () if-same)))
   (define-proof exact-positive-integer?
     ((rewrite (1 2) (is exact-integer? real?))
      (rewrite (1) if-same)
-- 
cgit v1.2.3