wip61

2 files changed, 78 insertions, 51 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 1c29e7e..5f7b16d 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -988,14 +988,21 @@
   (syntax-rules ()
     ((_ name (var ...) expr)
      (let ((f (let ((expression (convert-to-expression 'expr)))
-                (make (if (member 'name (expression-functions expression))
-                          <function>
-                          <trivial-total-function>)
-                  #:name 'name
-                  #:variables '(var ...)
-                  #:conditions '()
-                  #:expression expression
-                  #:code (code 'expr)))))
+                (if (member 'name (expression-functions expression))
+                    (make <function>
+                        #:name 'name
+                        #:variables '(var ...)
+                        #:conditions '()
+                        #:expression expression
+                        #:code (code 'expr))
+                    (make <total-function>
+                      #:name 'name
+                      #:variables '(var ...)
+                      #:conditions '()
+                      #:expression expression
+                      #:code (code 'expr)
+                      #:claim ''#t
+                      #:proof '())))))
        (current-system (add-definition f (current-system)))
        (validate f)
        f))))
@@ -1461,12 +1468,18 @@
         (get-variables d)
         (get-expression d)))
 
-(define/guard (system-apropos (sys system?) (str string?))
+(define* (system-apropos sys
+                         str
+                         #:key all?)
   (filter-map (lambda (d)
-                (if (string-match (string-append ".*"
-                                                 (regexp-quote str)
-                                                 ".*")
-                                  (symbol->string (get-name d)))
+                (if (and (or all?
+                             (not (string-match "^%"
+                                                (symbol->string
+                                                 (get-name d)))))
+                         (string-match (string-append ".*"
+                                                      (regexp-quote str)
+                                                      ".*")
+                                       (symbol->string (get-name d))))
                     (list (get-name d) (show d))
                     #f))
               (get-definitions sys)))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 9fb7571..66d2b73 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,12 +17,7 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (exact-positive-integer?
-            exact-negative-integer?
-            succ pred
-            implies
-            negate
-            prelude)
+  #:export (prelude)
   #:use-module (vikalpa))
 
 (define (exact-positive-integer? x)
@@ -96,22 +91,28 @@
     (equal? (if (not x) y z)
             (if x z y))))
 
-(define-system prelude/number (prelude/if)
+(define-system prelude/integer (prelude/if)
   (define-core-function integer? (x) exact-integer?)
   (define-core-function positive-integer? (x) exact-positive-integer?)
-  (define-core-function negative-integer? (x) exact-negative-integer?)
-  (define-core-function negate (x) negate)
-  (define-function natural? (x)
-    (if (integer? x)
-        (not (negative-integer? x))
-        #f))
   (define-function zero? (x)
     (equal? x 0))
-  (define-core-function succ (x) succ)
-  (define-core-function pred (x) pred)
+  (define-function natural? (x)
+    (if (zero? x)
+        #t
+        (positive-integer? x)))
+  (define-core-function + (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (+ x y)
+              x)
+          (if (number? y)
+              y
+              0))))
   (define-axiom succ/pred (x)
     (implies (integer? x)
              (equal? (succ (pred x)) x)))
+  
   (define-trivial-total-function < (x y)
     (if (positive-integer? x)
         (if (positive-integer? y)
@@ -126,7 +127,7 @@
                 #f))))
   (set-measure-predicate natural?)
   (set-measure-less-than <)
-  (define-axiom integer?-is-predicate (x)
+  (define-axiom integer?/true (x)
     (implies (integer? x)
              (equal? (integer? x) #t)))
   (define-axiom integer/pred (x)
@@ -144,7 +145,7 @@
   (define-axiom natural/pred (x)
     (implies (positive-integer? x)
              (equal? (natural? (pred x)) #t)))
-  (define-axiom positive-integer/succ (x)
+  (define-axiom positive-integer/pred (x)
     (implies (natural? x)
              (equal? (positive-integer? (pred x)) #t)))
   (define-axiom positive-integer-is-integer (x)
@@ -200,9 +201,7 @@
             x)
         0))
   (define-theorem natural-is-integer (x)
-    (if (natural? x)
-        (equal? (integer? x) #t)
-        #t))
+    (implies (natural? x) (equal? (integer? x) #t)))
   (define-theorem natural/abs (x)
     (equal? (natural? (abs x)) #t))
   (define-theorem zero-is-0 (x)
@@ -215,16 +214,16 @@
     (implies (natural? x)
              (not (zero? x))
              (equal? (positive-integer? x) #t)))
-  (define-theorem %abs/pred--zero/pred (x)
+  (define-theorem %%abs/pred--zero/pred (x)
     (implies (integer? x)
              (not (positive-integer? x))
              (natural? x)
              (equal? (zero? x) #t)))
-  (define-theorem %abs/pred--x-is-1 (x)
+  (define-theorem %%abs/pred--x-is-1 (x)
     (implies (positive-integer? x)
              (not (positive-integer? (pred x)))
              (equal? x 1)))
-  (define-theorem %abs/pred-1 (x)
+  (define-theorem %%abs/pred-1 (x)
     (implies (positive-integer? x)
              (positive-integer? (pred x))
              (equal? (< (pred x) x) #t)))
@@ -242,6 +241,12 @@
             0
             (succ (natural-induction (pred x))))
         0))
+  (define-function integer-induction (x)
+    (if (positive-integer? x)
+        (succ (integer-induction (pred x)))
+        (if (negative-integer? x)
+            (pred (integer-induction (succ x)))
+            0)))
   (define-function + (x y)
     (if (positive-integer? x)
         (succ (+ (pred x) y))
@@ -249,7 +254,7 @@
             (pred (+ (succ x) y))
             y))))
 
-(define-system prelude/pair (prelude/number)
+(define-system prelude/pair (prelude/integer)
   (define-core-function pair? (x) pair?)
   (define-core-function cons (x y) cons)
   (define-core-function car (x)
@@ -333,26 +338,26 @@
      ((2 1 2 2 3 1) axiom-negative-integer)
      ((2 1 2 2 3) if-false)
      ((2 1 2 2) if-same)
-     ((2 1 2) %abs/pred-1)
+     ((2 1 2) %%abs/pred-1)
      ((2 1 3) if-same (set x (integer? (pred x))))
      ((2 1 3 2 1) if-nest)
      ((2 1 3 3 1) if-nest)
      ((2 1 3 2) if-same (set x (negative-integer? (pred x))))
      ((2 1 3 2 2 1) if-nest)
      ((2 1 3 2 3 1) if-nest)
-     ((2 1 3 1 1 1) %abs/pred--x-is-1)
-     ((2 1 3 2 1 1 1) %abs/pred--x-is-1)
-     ((2 1 3 2 2 1 1 1) %abs/pred--x-is-1)
-     ((2 1 3 2 2 2 1) %abs/pred--x-is-1)
-     ((2 1 3 2 3 1 1) %abs/pred--x-is-1)
-     ((2 1 3 2 3 2 1) %abs/pred--x-is-1)
-     ((2 1 3 3 2 1) %abs/pred--x-is-1)
+     ((2 1 3 1 1 1) %%abs/pred--x-is-1)
+     ((2 1 3 2 1 1 1) %%abs/pred--x-is-1)
+     ((2 1 3 2 2 1 1 1) %%abs/pred--x-is-1)
+     ((2 1 3 2 2 2 1) %%abs/pred--x-is-1)
+     ((2 1 3 2 3 1 1) %%abs/pred--x-is-1)
+     ((2 1 3 2 3 2 1) %%abs/pred--x-is-1)
+     ((2 1 3 3 2 1) %%abs/pred--x-is-1)
      ((2 1 3) (eval))
      ((2 1) if-same)
      ((2) equal-same)
      (() if-same)))
 
-  (define-proof %abs/pred-1
+  (define-proof %%abs/pred-1
     (natural-induction x)
     (((2 2 1 1) zero-is-0)
      ((2 2 1) positive-integer?)
@@ -379,8 +384,8 @@
      ((2 3 2 3 1) if-nest)
      ((2 3 2 3 1 1) natural-and-not-zero-implies-positive-integer)
      ((2 3 2 3 1) if-true)
-     ((2 3 2 3 1 1 1) %abs/pred--x-is-1)
-     ((2 3 2 3 1 2) %abs/pred--x-is-1)
+     ((2 3 2 3 1 1 1) %%abs/pred--x-is-1)
+     ((2 3 2 3 1 2) %%abs/pred--x-is-1)
      ((2 3 2 3) (eval))
      ((2 3 2) if-same)
      ((2 3 3 2) if-nest)
@@ -391,7 +396,7 @@
      ((3) if-false)
      (() if-same)))
 
-  (define-proof %abs/pred--x-is-1
+  (define-proof %%abs/pred--x-is-1
     (((2 2) if-same (set x (zero? (pred x))))
      ((2 2 2) if-same (set x (integer? x)))
      ((2 2 2 2 1) succ/pred)
@@ -401,7 +406,7 @@
      ((2 2 2) if-true)
      ((2 2) if-same (set x (natural? (pred x))))
      ((2 2 2) if-same (set x (integer? (pred x))))
-     ((2 2 2 2 1) %abs/pred--zero/pred)
+     ((2 2 2 2 1) %%abs/pred--zero/pred)
      ((2 2 2 2) if-true)
      ((2 2 2 1) natural-is-integer)
      ((2 2 2) if-true)
@@ -410,7 +415,7 @@
      ((2) if-same)
      (() if-same)))
 
-  (define-proof %abs/pred--zero/pred
+  (define-proof %%abs/pred--zero/pred
     (((2 2 1) natural?)
      ((2 2 1) if-nest)
      ((2 2 2) if-same (set x (zero? x)))
@@ -480,6 +485,15 @@
      ((2) if-same)
      (() if-same)))
 
+  (define-proof integer-induction
+    (abs x)
+    (((1) natural/abs)
+     (() if-true)
+     ((2) abs/pred)
+     ((3 2) abs/succ)
+     ((3) if-same)
+     (() if-same)))
+  
   (define-proof +
     (abs x)
     (((1) natural/abs)