wip62

2 files changed, 202 insertions, 527 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 5f7b16d..d1da85b 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -1,5 +1,5 @@
 ;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
 ;;;
 ;;; This file is part of Vikalpa.
 ;;;
@@ -28,8 +28,9 @@
             define-system
             define-proof
             define-core-function
+            define-core-function/guard
             define-function
-            define-trivial-total-function
+            define-function/guard
             define-syntax-rules
             define-axiom
             define-theorem)
@@ -77,7 +78,7 @@
 (define-class <axiom> (<theorem*>))
 
 (define-class <function*> (<definition>)
-  (conditions #:getter get-conditions #:init-keyword #:conditions))
+  (guards #:getter get-guards #:init-keyword #:guards))
 (define-class <core-function> (<function*>)
   (procedure #:getter get-procedure #:init-keyword #:procedure))
 (define-class <expandable-function> (<function*>)
@@ -85,7 +86,6 @@
   (code #:getter get-code #:init-keyword #:code))
 (define-class <function> (<expandable-function> <provable>))
 (define-class <total-function> (<expandable-function> <proved>))
-(define-class <trivial-total-function> (<expandable-function>))
 
 (define-class <macro> (<definition>)
   (mrules #:getter macro-mrules #:init-keyword #:mrules)
@@ -118,8 +118,6 @@
   (write-definition 'function d port))
 (define-method (write (d <core-function>) port)
   (write-definition 'core-function d port))
-(define-method (write (d <trivial-total-function>) port)
-  (write-definition 'trivial-total-function d port))
 (define-method (write (d <total-function>) port)
   (write-definition 'total-function d port))
 
@@ -791,11 +789,11 @@
 
 (define (function->rules x)
   (list (rule (get-variables x)
-              (get-conditions x)
+              (list)
               (defined-function-app-form x)
               (get-expression x))
         (rule (get-variables x)
-              (get-conditions x)
+              (list)
               (get-expression x)
               (defined-function-app-form x))))
 
@@ -972,53 +970,65 @@
        (validate t)
        t))))
 
-(define-syntax define-core-function
-  (syntax-rules ()
-    ((_ name (var ...) proc)
+(define-syntax define-core-function/guard
+  (syntax-rules (and)
+    ((_ name (var ...) (and guard ...) proc)
      (let ((f (make <core-function>
                 #:name 'name
                 #:variables '(var ...)
-                #:conditions '()
+                #:guards (map convert-to-expression (list 'guard ...))
                 #:procedure proc)))
        (current-system (add-definition f (current-system)))
        (validate f)
-       f))))
+       f))
+    ((_ name (var ...) guard proc)
+     (define-core-function/guard name (var ...) (and guard) proc))))
 
-(define-syntax define-function
+(define-syntax define-core-function
   (syntax-rules ()
-    ((_ name (var ...) expr)
-     (let ((f (let ((expression (convert-to-expression '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 '())))))
+    ((_ name (var ...) proc)
+     (define-core-function/guard name (var ...) (and) proc))))
+
+(define (recursive? f)
+  (member (get-name f) (expression-functions (get-expression f))))
+
+(define (has-guard-claim? f sys)
+  (let ((claim (make-guard-claim (get-expression f) sys)))
+    (not (equal? ''#t claim))))
+
+(define-syntax define-function/guard
+  (syntax-rules (and)
+    ((_ name (var ...) (and guard ...) expr)
+     (let* ((expression (convert-to-expression 'expr))
+            (guard-expressions (map convert-to-expression
+                                    (list 'guard ...)))
+            (f (make <function>
+                 #:name 'name
+                 #:variables '(var ...)
+                 #:guards guard-expressions
+                 #:expression expression
+                 #:code (code 'expr))))
        (current-system (add-definition f (current-system)))
        (validate f)
-       f))))
+       (when (and (not (recursive? f))
+                  (not (has-guard-claim? f (current-system))))
+         (let ((g (make <total-function>
+                    #:name (get-name f)
+                    #:variables (get-variables f)
+                    #:guards (get-guards f)
+                    #:expression (get-expression f)
+                    #:code (get-code f)
+                    #:claim ''#t
+                    #:proof '())))
+           (current-system (update-definition g (current-system)))
+           (validate g)))))
+    ((_ name (var ...) guard expr)
+     (define-function/guard name (var ...) (and guard) expr))))
 
-(define-syntax define-trivial-total-function
+(define-syntax define-function
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (let ((f (make <trivial-total-function>
-                #:name 'name
-                #:variables '(var ...)
-                #:conditions '()
-                #:expression (convert-to-expression 'expr)
-                #:code (code 'expr))))
-       (current-system (add-definition f (current-system)))
-       (validate f)
-       f))))
+     (define-function/guard name (var ...) (and) expr))))
 
 (define-syntax define-syntax-rules
   (syntax-rules ()
@@ -1032,6 +1042,10 @@
 
 (define* (core-system #:optional (parent (make <system>)))
   (parameterize ((current-system parent))
+    (define-syntax-rules and ()
+      ((and) '#t)
+      ((and x) x)
+      ((and x . xs) (if x (and . xs) #f)))
     (define-core-function not (x) not)
     (define-core-function equal? (x y) equal?)
     (current-system)))
@@ -1159,34 +1173,34 @@
                       (let f ((args (app-form-args expr)))
                         (cond ((null? args) ''#t)
                               ((single? args) (loop (car args)))
-                              (else (and/if (loop (car args))
-                                            (f (cdr args))))))))
+                                  (else (and/if (loop (car args))
+                                                (f (cdr args))))))))
                  (if (eq? name (app-form-name expr))
                      (and/if `(,(get-measure-less-than sys)
                                ,(convert expr)
-                               ,m-expr)
-                             rest)
+                                   ,m-expr)
+                                 rest)
                      rest)))
               (else (error "(vikalpa) make-totality-claim: error"
                            (get-name f)
                            m-expr))))
            ''#f)))
 
-(define (make-condition-claim expr sys)
+(define (make-guard-claim expr sys)
   (define (find-preconds expr)
     (cond
      ((app-form? expr)
       (let ((rest (append-map find-preconds (cdr expr))))
         (append (cond ((lookup (car expr) sys) =>
                        (lambda (f)
-                         (let ((preconds (get-conditions f)))
+                         (let ((preconds (get-guards f)))
                            (map (lambda (precond)
                                   (substitute (map cons
                                                    (get-variables f)
                                                    (cdr expr))
                                               precond))
                                 preconds))))
-                      (else (error "make-condition-claim: error")))
+                      (else (error "make-guard-claim: error" (car expr))))
                 rest)))
      ((if-form? expr)
       (find-preconds (if-form-test expr)))
@@ -1274,27 +1288,39 @@
             seq))
 
 (define (add-proof/function sys f seed seq)
+  (define (update-claim claim)
+    (update-definition (make <total-function>
+                         #:name (get-name f)
+                         #:variables (get-variables f)
+                         #:guards (get-guards f)
+                         #:expression (get-expression f)
+                         #:code (get-code f)
+                         #:claim claim
+                         #:proof seq)
+                       sys))
   (validate-sequence sys f seq)
-  (if seed
-      (begin
-        (validate-expression sys
-                             `(defien-proof ,(get-name f))
-                             (get-variables f)
-                             seed)
-        (update-definition (make <total-function>
-                             #:name (get-name f)
-                             #:variables (get-variables f)
-                             #:conditions (get-conditions f)
-                             #:expression (get-expression f)
-                             #:code (get-code f)
-                             #:claim (make-totality-claim* sys seed f)
-                             #:proof seq)
-                           sys))
-      (raise-exception
-       (make-exception
-        (make-exception-with-origin 'define-proof)
-        (make-exception-with-message "need seed")
-        (make-exception-with-irritants (get-expression f))))))
+  (if (recursive? f)
+      (if seed
+          (begin
+            (validate-expression sys
+                                 `(defien-proof ,(get-name f))
+                                 (get-variables f)
+                                 seed)
+            (update-claim
+             (fold implies/if
+                   (and/if (make-totality-claim* sys seed f)
+                            (make-guard-claim (get-expression f)
+                                              sys))
+                   (get-guards f))))
+          (raise-exception
+           (make-exception
+            (make-exception-with-origin 'define-proof)
+            (make-exception-with-message "need measure expression")
+            (make-exception-with-irritants (get-expression f)))))
+      (update-claim
+       (fold implies/if
+             (make-guard-claim (get-expression f) sys)
+             (get-guards f)))))
 
 (define (add-proof/theorem sys t seed seq)
   (validate-sequence sys t seq)
@@ -1451,7 +1477,6 @@
 (define-method (get-type (s <core-function>)) 'core-function)
 (define-method (get-type (s <function>)) 'function)
 (define-method (get-type (s <total-function>)) 'total-function)
-(define-method (get-type (s <trivial-total-function>)) 'trivial-total-function)
 (define-method (get-type (s <macro>)) 'macro)
 
 (define-method (show (d <macro>))
@@ -1484,27 +1509,6 @@
                     #f))
               (get-definitions sys)))
 
-(define (system-code/definition d)
-  (and (is-a? d <expandable-function>)
-       (get-code d)
-       `(define (,(get-name d) ,@(get-variables d))
-          ,(code-expr (get-code d)))))
-
-(define/guard (system-code/name (sys system?) (name symbol?))
-  (cond
-   ((lookup name sys) => system-code/definition)
-   (else #f)))
-
-(define/guard (system-code/all (sys system?))
-  `(begin
-     ,@(filter-map system-code/definition
-                   (reverse (get-definitions sys)))))
-
-(define* (system-code sys #:optional (name #f))
-  (if name
-      (system-code/name sys name)
-      (system-code/all sys)))
-
 (define (system-check sys)
   (let loop ((sys sys)
              (fails '()))
@@ -1544,14 +1548,5 @@
    ((lookup name sys) => show)
    (else #f)))
 
-(define/guard (system-load/name (sys system?) (name symbol?))
-  (primitive-eval (system-code sys name)))
-
-(define/guard (system-load/all (sys system?))
-  (primitive-eval (system-code sys)))
-
-(define/guard (system-load (sys system?))
-  (primitive-eval (system-code sys)))
-
 (define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?))
   (rewrite sys (convert-to-expression expr) seq))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 66d2b73..176983c 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -1,5 +1,5 @@
 ;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
 ;;;
 ;;; This file is part of Vikalpa.
 ;;;
@@ -48,25 +48,23 @@
     ((_ x y) (if x y #t))
     ((_ x y z ...) (if x (implies y z ...) #t))))
 
-(define-system prelude/macros ()
-  (define-syntax-rules and ()
-    ((and) '#t)
-    ((and x) x)
-    ((and x . xs) (if x (and . xs) #f)))
-  (define-syntax-rules or ()
-    ((or) '#f)
-    ((or x) x)
-    ((or x . xs) (if x x (or . xs))))
+(define-system prelude/macro ()
   (define-syntax-rules cond (else)
     ((cond (else e)) e)
     ((cond (test then) . rest)
      (if test then (cond . rest))))
+  (define-syntax-rules or ()
+    ((or) '#f)
+    ((or x) x)
+    ((or x . xs) (if x x (or . xs))))
   (define-syntax-rules implies ()
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
-     (if x (implies y z . rest) #t))))
+     (if x (implies y z . rest) #t)))
+  (define-syntax-rules is-a ()
+    ((is-a x y) (implies x (equal? y #t)))))
 
-(define-system prelude/equal (prelude/macros)
+(define-system prelude/axiom/equal (prelude/macro)
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
   (define-axiom equal-swap (x y)
@@ -76,7 +74,7 @@
   (define-axiom equal-if-false (x y)
     (if x #t (equal? x #f))))
 
-(define-system prelude/if (prelude/equal)
+(define-system prelude/axiom/if (prelude/axiom/equal)
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
@@ -91,426 +89,108 @@
     (equal? (if (not x) y z)
             (if x z y))))
 
-(define-system prelude/integer (prelude/if)
-  (define-core-function integer? (x) exact-integer?)
-  (define-core-function positive-integer? (x) exact-positive-integer?)
-  (define-function zero? (x)
-    (equal? x 0))
+(define-system prelude/number (prelude/axiom/if)
+  (define-core-function number? (x) number?)
+  (define-axiom number-predicate (x)
+    (is-a (number? x) (number? x)))
+
+  (define-core-function real? (x) real?)
+  (define-axiom real-predicate (x)
+    (implies (real? x) (equal? (real? x) #t)))
+  (define-axiom real-is-a-numbers (x)
+    (implies (real? x) (equal? (number? x) #t)))
+
+  (define-core-function integer? (x) integer?)
+  (define-axiom integer-predicate (x)
+    (implies (integer? x) (equal? (integer? x) #t)))
+  (define-axiom integer-is-a-real (x)
+    (implies (integer? x) (equal? (number? x) #t)))
+
+  (define-core-function/guard exact? (x) (number? x) exact?)
+  (define-axiom exact-predicate (x)
+    (implies (exact? x) (equal? (exact? x) #t)))
+
+  (define-function/guard inexact? (x)
+    (number? x)
+    (not (exact? x)))
+  (define-theorem inexact-predicate (x)
+    (implies (inexact? x) (equal? (inexact? x) #t)))
+
+  (define-core-function exact-integer? (x) exact-integer?)
+  (define-axiom exact-integer-predicate (x)
+    (implies (exact-integer? x) (equal? (exact-integer? x) #t)))
+  (define-axiom exact-integer-is-a-integer (x)
+    (implies (exact-integer? x) (equal? (integer? x) #t)))
+  (define-axiom exact-integer-is-a-exact (x)
+    (implies (exact-integer? x) (equal? (exact? x) #t)))
+
+  (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
+  (define-axiom less-than-predicate (x y)
+    (implies (< x y) (equal? (< x y) #t)))
+
+  (define-function/guard positive? (x)
+    (real? x)
+    (< 0 x))
+  (define-theorem positive-predicate (x)
+    (implies (positive? x) (equal? (positive? x) #t)))
+  (define-function/guard negative? (x)
+    (real? x)
+    (< x 0))
+  (define-theorem negative-predicate (x)
+    (implies (negative? x) (equal? (negative? x) #t)))
+
+  (define-function exact-positive-integer? (x)
+    (and (exact-integer? x)
+         (positive? x)))
+  (define-theorem exact-positive-integer-predicate (x)
+    (implies (exact-positive-integer? x)
+             (equal? (exact-positive-integer? x) #t)))
+
+  (define-function exact-zero? (x) (equal? x 0))
+  (define-theorem exact-zero-predicate (x)
+    (implies (exact-zero? x) (equal? (exact-zero? x) #t)))
+
   (define-function natural? (x)
-    (if (zero? x)
+    (if (exact-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)
-            (< (pred x) (pred y))
-            #f)
-        (if (positive-integer? y)
-            #t
-            (if (negative-integer? x)
-                (if (negative-integer? y)
-                    (< (succ x) (succ y))
-                    #t)
-                #f))))
-  (set-measure-predicate natural?)
-  (set-measure-less-than <)
-  (define-axiom integer?/true (x)
-    (implies (integer? x)
-             (equal? (integer? x) #t)))
-  (define-axiom integer/pred (x)
-    (implies (integer? x)
-             (equal? (integer? (pred x)) #t)))
-  (define-axiom integer/succ (x)
-    (implies (integer? x)
-             (equal? (integer? (pred x)) #t)))
-  (define-axiom positive-integer?-is-predicate (x)
-    (implies (positive-integer? x)
-             (equal? (positive-integer? x) #t)))
-  (define-axiom negative-integer?-is-predicate (x)
-    (implies (negative-integer? x)
-             (equal? (negative-integer? x) #t)))
-  (define-axiom natural/pred (x)
-    (implies (positive-integer? x)
-             (equal? (natural? (pred x)) #t)))
-  (define-axiom positive-integer/pred (x)
-    (implies (natural? x)
-             (equal? (positive-integer? (pred x)) #t)))
-  (define-axiom positive-integer-is-integer (x)
-    (implies (positive-integer? x)
-             (equal? (integer? x) #t)))
-  (define-axiom negative-integer-is-integer (x)
-    (implies (negative-integer? x)
-             (equal? (integer? x) #t)))
-  (define-axiom axiom-zero (x)
-    (if (integer? x)
-        (if (positive-integer? x)
-            (equal? (zero? x) #f)
-            (if (negative-integer? x)
-                (equal? (zero? x) #f)
-                (equal? (zero? x) #t)))
-        (equal? (zero? x) #f)))
-  (define-axiom axiom-positive-integer (x)
-    (if (integer? x)
-        (if (negative-integer? x)
-            (equal? (positive-integer? x) #f)
-            (if (zero? x)
-                (equal? (positive-integer? x) #f)
-                (equal? (positive-integer? x) #t)))
-        (equal? (positive-integer? x) #f)))
-  (define-axiom axiom-negative-integer (x)
-    (if (integer? x)
-        (if (positive-integer? x)
-            (equal? (negative-integer? x) #f)
-            (if (zero? x)
-                (equal? (negative-integer? x) #f)
-                (equal? (negative-integer? x) #t)))
-        (equal? (negative-integer? x) #f)))
-  (define-axiom integer/negate (x)
-    (implies (integer? x)
-             (equal? (integer? (negate x)) #t)))
-  (define-axiom positive-integer/negate (x)
-    (if (negative-integer? x)
-        (equal? (positive-integer? (negate x)) #t)
-        (implies (integer? x)
-                 (equal? (positive-integer? (negate x)) #f))))
-  (define-axiom negative-integer/negate (x)
-    (if (positive-integer? x)
-        (equal? (negative-integer? (negate x)) #t)
-        (implies (integer? x)
-                 (equal? (negative-integer? (negate x)) #f))))
-  (define-axiom zero/negate (x)
-    (implies (zero? x)
-             (equal? (zero? (negate x)) #t)))
-  (define-function abs (x)
-    (if (integer? x)
-        (if (negative-integer? x)
-            (negate x)
-            x)
-        0))
-  (define-theorem natural-is-integer (x)
-    (implies (natural? x) (equal? (integer? x) #t)))
-  (define-theorem natural/abs (x)
-    (equal? (natural? (abs x)) #t))
-  (define-theorem zero-is-0 (x)
-    (implies (zero? x)
-             (equal? x 0)))
-  (define-theorem not-natural-implies-not-positive-integer (x)
-    (implies (not (natural? x))
-             (equal? (positive-integer? x) #f)))
-  (define-theorem natural-and-not-zero-implies-positive-integer (x)
-    (implies (natural? x)
-             (not (zero? x))
-             (equal? (positive-integer? x) #t)))
-  (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)
-    (implies (positive-integer? x)
-             (not (positive-integer? (pred x)))
-             (equal? x 1)))
-  (define-theorem %%abs/pred-1 (x)
-    (implies (positive-integer? x)
-             (positive-integer? (pred x))
-             (equal? (< (pred x) x) #t)))
-  (define-theorem abs/pred (x)
-    (if (positive-integer? x)
-        (equal? (< (abs (pred x)) (abs x)) #t)
-        #t))
-  (define-theorem abs/succ (x)
-    (if (negative-integer? x)
-        (equal? (< (abs (succ x)) (abs x)) #t)
-        #t))
-  (define-function natural-induction (x)
-    (if (natural? x)
-        (if (zero? x)
-            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))
-        (if (negative-integer? x)
-            (pred (+ (succ x) y))
-            y))))
-
-(define-system prelude/pair (prelude/integer)
-  (define-core-function pair? (x) pair?)
-  (define-core-function cons (x y) cons)
-  (define-core-function car (x)
-    (lambda (x) (if (pair? x) (car x) '())))
-  (define-core-function cdr (x)
-    (lambda (x) (if (pair? x) (cdr x) '()))))
-
-(define-system prelude/tree (prelude/pair)
-  (define-trivial-total-function size (x)
-    (if (pair? x)
-        (+ 1
-           (+ (size (car x))
-              (size (cdr x))))
-        0))
-  (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-function tree-induction (x)
-    (if (not (pair? x))
-        x
-        (cons (tree-induction (car x))
-              (tree-induction (cdr x))))))
-
-(define-system prelude/proofs (prelude/tree)
-  (define-proof natural/abs
-    (((1) natural?)
-     ((1 1 1) abs)
-     ((1 1) if-same (set x (integer? x)))
-     ((1 1 3 1) if-nest)
-     ((1 1 3) integer?)
-     ((1 1 2 1) if-nest)
-     ((1 1 2) if-same (set x (negative-integer? x)))
-     ((1 1 2 2 1) if-nest)
-     ((1 1 2 2) integer/negate)
-     ((1 1 2 3 1) if-nest)
-     ((1) if-same (set x (integer? x)))
-     ((1 3 1) if-nest)
-     ((1 3) if-true)
-     ((1 3 1 1) abs)
-     ((1 3 1 1) if-nest)
-     ((1 3 1) negative-integer?)
-     ((1 3) not)
-     ((1 2 1) if-nest)
-     ((1 2 1 3) integer?-is-predicate)
-     ((1 2 1) if-same)
-     ((1 2) if-true)
-     ((1 2 1 1) abs)
-     ((1 2 1 1) if-nest)
-     ((1 2) if-same (set x (negative-integer? x)))
-     ((1 2 2 1 1) if-nest)
-     ((1 2 3 1 1) if-nest)
-     ((1 2 3 1) equal-if-false)
-     ((1 2 3) not)
-     ((1 2 2) if-same (set x (positive-integer? x)))
-     ((1 2 2 2 1) negative-integer/negate)
-     ((1 2 2 2) not)
-     ((1 2 2 3 1) negative-integer/negate)
-     ((1 2 2 3) not)
-     ((1 2 2 1) axiom-positive-integer)
-     ((1 2 2) if-false)
-     ((1 2) if-same)
-     ((1) if-same)
-     (() equal?)))
-
-  (define-proof abs/pred
-    (((2 1 1) abs)
-     ((2 1) if-same (set x (positive-integer? (pred x))))
-     ((2 1 2 1 2 1) axiom-negative-integer)
-     ((2 1 2 1 2) if-false)
-     ((2 1 2 1 1) positive-integer-is-integer)
-     ((2 1 2 1) if-true)
-     ((2 1 2 2) abs)
-     ((2 1 2 2 1) positive-integer-is-integer)
-     ((2 1 2 2) if-true)
-     ((2 1 2 2) if-same (set x (integer? x)))
-     ((2 1 2 2 2 1) axiom-negative-integer)
-     ((2 1 2 2 2) if-false)
-     ((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 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) (eval))
-     ((2 1) if-same)
-     ((2) equal-same)
-     (() if-same)))
-
-  (define-proof %%abs/pred-1
-    (natural-induction x)
-    (((2 2 1 1) zero-is-0)
-     ((2 2 1) positive-integer?)
-     ((2 2) if-false)
-     ((2 3) if-same (set x (positive-integer? (pred x))))
-     ((2 3 2 1) if-nest)
-     ((2 3 3 1) if-nest)
-     ((2 3 3) if-true)
-     ((2 3 2 2 2) if-nest)
-     ((2 3 2 2 1) natural-and-not-zero-implies-positive-integer)
-     ((2 3 2 2) if-true)
-     ((2 3 2) if-same (set x (positive-integer? (pred (pred x)))))
-     ((2 3 2 2 1) if-nest)
-     ((2 3 2 3 1) if-nest)
-     ((2 3 2 3) if-true)
-     ((2 3 2 2 2 1) <)
-     ((2 3 2 2 2 1) if-nest)
-     ((2 3 2 2 2 1 1) natural-and-not-zero-implies-positive-integer)
-     ((2 3 2 2 2 1) if-true)
-     ((2 3 2 2 2 1) equal-if)
-     ((2 3 2 2 2) equal?)
-     ((2 3 2 2) if-same)
-     ((2 3 2 3 1) <)
-     ((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) (eval))
-     ((2 3 2) if-same)
-     ((2 3 3 2) if-nest)
-     ((2 3 3) if-same)
-     ((2 3) if-same)
-     ((2) if-same)
-     ((3 1) not-natural-implies-not-positive-integer)
-     ((3) if-false)
-     (() if-same)))
-
-  (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)
-     ((2 2 2 2 1 1) zero-is-0)
-     ((2 2 2 2) (eval))
-     ((2 2 2 1) positive-integer-is-integer)
-     ((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) if-true)
-     ((2 2 2 1) natural-is-integer)
-     ((2 2 2) if-true)
-     ((2 2 1) natural/pred)
-     ((2 2) if-true)
-     ((2) if-same)
-     (() if-same)))
-
-  (define-proof %%abs/pred--zero/pred
-    (((2 2 1) natural?)
-     ((2 2 1) if-nest)
-     ((2 2 2) if-same (set x (zero? x)))
-     ((2 2 2 2 1 1) zero-is-0)
-     ((2 2 2 2) (eval))
-     ((2 2 2 1) axiom-zero)
-     ((2 2 2) if-true)
-     ((2 2) if-same)
-     ((2) if-same)
-     (() if-same)))
+        (exact-positive-integer? x)))
+  (define-theorem (predicate natural?) (x)
+    (implies (natural? x) (equal? (natural? x) #t))))
 
-  (define-proof natural-is-integer
-    (((1) natural?)
-     (() if-same (set x (integer? x)))
-     ((2 2 1) integer?-is-predicate)
-     ((2 2) equal-same)
-     ((2) if-same)
-     ((3 1) if-nest)
-     ((3) if-false)
-     (() if-same)))
+(define-system prelude/measure/natural (prelude/number)
+  (set-measure-predicate natural?)
+  (set-measure-predicate <))
 
-  (define-proof zero-is-0
-    (((1) zero?)
-     ((2 1) equal-if)
-     ((2) equal?)
+(define-system prelude (prelude/measure/natural)
+  (define-proof inexact?
+    (((2) if-nest)
      (() if-same)))
-  
-  (define-proof not-natural-implies-not-positive-integer
-    (((1 1) natural?)
-     (() if-same (set x (integer? x)))
-     ((2 1 1) if-nest)
-     ((2) if-not)
-     ((2) if-not)
-     ((2 2) if-same (set x (positive-integer? x)))
-     ((2 2 3 1) equal-if-false)
-     ((2 2 3) equal?)
-     ((2 2 1) axiom-positive-integer)
-     ((2 2) if-false)
-     ((2) if-same)
-     ((3 1 1) if-nest)
-     ((3 1) not)
-     ((3) if-true)
-     ((3 1) axiom-positive-integer)
-     ((3) equal?)
+  (define-proof inexact-predicate
+    (((1) inexact?)
+     (() if-not)
+     ((3 1) inexact?)
+     ((3 1 1) equal-if-false)
+     ((3) (eval))
      (() if-same)))
-
-  (define-proof natural-and-not-zero-implies-positive-integer
-    (((1) natural?)
-     (() if-same (set x (integer? x)))
-     ((2 1) if-nest)
-     ((2 2 2 1) axiom-positive-integer)
-     ((2 2 2) equal?)
-     ((2 2) if-same)
-     ((2) if-same)
-     ((3 1) if-nest)
-     ((3) if-false)
+  (define-proof positive?
+    (((2 1 1) (eval))
+     ((2 1) if-true)
+     ((2) if-nest)
      (() if-same)))
-  
-  (define-proof natural-induction
-    (abs x)
-    (((1) natural/abs)
-     (() if-true)
-     ((2 3) if-same (set x (positive-integer? x)))
-     ((2 3 2) abs/pred)
-     ((2 3 1) natural-and-not-zero-implies-positive-integer)
-     ((2 3) if-true)
-     ((2) if-same)
+  (define-proof positive-predicate
+    (((1) positive?)
+     ((2 1) positive?)
+     ((2 1) less-than-predicate)
+     ((2) (eval))
      (() if-same)))
-
-  (define-proof integer-induction
-    (abs x)
-    (((1) natural/abs)
-     (() if-true)
-     ((2) abs/pred)
-     ((3 2) abs/succ)
-     ((3) if-same)
+  (define-proof negative?
+    (((2 1) if-nest)
+     ((2 1) (eval))
+     ((2) if-true)
      (() if-same)))
-  
-  (define-proof +
-    (abs x)
-    (((1) natural/abs)
-     (() if-true)
-     ((2) abs/pred)
-     ((3 2) abs/succ)
-     ((3) if-same)
-     (() if-same)))
-  
-  (define-proof tree-induction
-    (size x)
-    (((2 3 1) size/car)
-     ((2 3 2) size/cdr)
-     ((2 3) if-true)
-     ((2) if-same)
-     ((1) natural/size)
-     (() if-true))))
-
-
-(define-system prelude (prelude/proofs))
+  (define-proof negative-predicate
+    (((1) negative?)
+     ((2 1) negative?)
+     ((2 1) less-than-predicate)
+     ((2) (eval))
+     (() if-same))))