1 files changed, 79 insertions, 35 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index f37bdd0..17d1db8 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -21,23 +21,38 @@
   #:use-module (vikalpa))
 
 (define-system prelude ()
-  (define-function natural? (x)
-    (if (integer? x)
-        (< 0 x)
-        #f))
-
-  (define-syntax-rules + ()
-    ((+ x . xs) (binary-+ x (+ . xs)))
-    ((+ x) x)
-    ((+) '0))
-
-  (define-syntax-rules - ()
-    ((- x . xs) (binary-+ x (- . xs)))
-    ((- x) (unary-- x)))
-  
-  (define-syntax-rules list ()
-    ((list) '())
-    ((list x . y) (cons x (list . y))))
+  (define-core-function natural? (x) (lambda (x)
+                                       (and (integer? x)
+                                            (< 0 x))))
+  (define-core-function < (x y) (natural? x) (natural? y) <)
+  (define-core-function pair? (x) pair?)
+  (define-core-function cons (x y) cons)
+  (define-core-function car (x) (pair? x)
+    (lambda (x) (if (pair? x) (car x) '())))
+  (define-core-function cdr (x) (pair? x)
+    (lambda (x) (if (pair? x) (cdr x) '())))
+  (define-core-function + (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (+ x y)
+              x)
+          (if (number? y)
+              y
+              0))))
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+  (define-trivial-total-function list-induction (x)
+    (if (not (pair? x))
+        x
+        (cons (car x)
+              (list-induction (cdr x)))))
+  (define-trivial-total-function size (x)
+    (if (not (pair? x))
+        0
+        (+ 1
+           (+ (size (car x))
+              (size (cdr x))))))
 
   (define-syntax-rules and ()
     ((and) '#t)
@@ -58,16 +73,7 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
-
-  (define-axiom equal-same (x)
-    (equal? (equal? x x) '#t))
-
-  (define-axiom equal-swap (x y)
-    (equal? (equal? x y) (equal? y x)))
-
-  (define-axiom equal-if (x y)
-    (implies (equal? x y) (equal? x y)))
-
+  
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
@@ -86,6 +92,15 @@
     (equal? (if (not x) y z)
             (if x z y)))
 
+  (define-axiom equal-same (x)
+    (equal? (equal? x x) '#t))
+
+  (define-axiom equal-swap (x y)
+    (equal? (equal? x y) (equal? y x)))
+
+  (define-axiom equal-if (x y)
+    (implies (equal? x y) (equal? x y)))
+  
   (define-axiom pair/cons (x y)
     (equal? (pair? (cons x y)) '#t))
 
@@ -99,16 +114,45 @@
   (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
 
+  (define-axiom natural/size (x)
+    (equal? (natural? (size x)) #t))
+
+  (define-axiom size/car (x)
+    (equal? (< (size (car x)) (size x)) #t))
+
+  (define-axiom size/cdr (x)
+    (equal? (< (size (cdr x)) (size x)) #t))
+
   (define-axiom equal-car (x1 y1 x2 y2)
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? x1 x2)))
 
-  (define-axiom equal-cdr (x1 y1 x2 y2)
-    (implies (equal? (cons x1 y1) (cons x2 y2))
-             (equal? y1 y2)))
-
-  (define-function zero? (x)
-    (equal? 0 x))
+  (define-theorem caar-cons2 (x y z)
+    (equal? (car (car (cons (cons x y) z))) x))
+  
+  (define-function app (x y)
+    (if (not (pair? x))
+        y
+        (cons (car x)
+              (app (cdr x) y))))
+  
+  (define-theorem assoc-app (x y z)
+    (equal? (app x (app y z))
+            (app (app x y) z)))
+
+  (define-proof caar-cons2
+    (((1 1)  car/cons)
+     ((1) car/cons)
+     (() equal-same)))
+
+  (define-proof app
+    (size x)
+    (((2 3) size/cdr)
+     ((2) if-same)
+     ((1) natural/size)
+     (() if-true)))
+
+  (define-proof assoc-app
+    (list-induction x)
+    ()))
 
-  (define-totality-claim natural? natural? <)
-  )