wip43

2 files changed, 746 insertions, 1201 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index a2b4dd2..1b3c158 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -17,40 +17,104 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa)
-  #:export (rewrite
-            show
-            check
-            system->scheme
-            load-system
-            system-primitives
-            system-functions
-            system-macros
-            system-theorems
-            system-axioms
-            system-totality-claims
-            define-system
-            define-axiom
-            define-theorem
-            define-primitive-function
-            define-function
-            define-scheme-function
-            define-proof
-            define-totality-claim
-            define-syntax-rules
-            system-eval
-            natural?
-            succ
-            pred)
+  #:export () ;; (rewrite
+           ;;  show
+           ;;  check
+           ;;  system->scheme
+           ;;  load-system
+           ;;  system-primitives
+           ;;  system-functions
+           ;;  system-macros
+           ;;  system-theorems
+           ;;  system-axioms
+           ;;  system-totality-claims
+           ;;  define-system
+           ;;  define-axiom
+           ;;  define-theorem
+           ;;  define-primitive-function
+           ;;  define-function
+           ;;  define-scheme-function
+           ;;  define-proof
+           ;;  define-totality-claim
+           ;;  define-syntax-rules
+           ;;  system-eval)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
+  #:use-module (ice-9 exceptions)
   #:use-module ((srfi srfi-1)
                 #:select (every any member lset-union fold append-map
                                 find))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-11)
   #:use-module (srfi srfi-26)
-  #:use-module (ice-9 pretty-print))
+  #:use-module (ice-9 pretty-print)
+  #:use-module (oop goops))
+
+(define-class <system> ()
+  (definitions #:getter system-definitions #:init-keyword #:definitions)
+  (total-cliam-method #:getter system-total-claim-method
+                      #:init-keyword #:total-cliam-method))
+
+(define-class <definition> ()
+  (name #:getter definition-name #:init-keyword #:name))
+
+(define-class <condition> ()
+  (expressions #:getter condition-expressions #:init-keyword #:expressions))
+
+(define-class <function> (<definition>)
+  (variables #:getter function-variables #:init-keyword #:variables)
+  (condition #:getter function-condition #:init-keyword #:condition))
+
+(define-class <total-function> ())
+
+(define-class <core-function> (<function>)
+  (procedure #:getter core-function-procedure #:init-keyword #:procedure))
+
+(define-class <defined-function> (<function>)
+  (expression #:getter defined-function-expression #:init-keyword #:expression)
+  (code #:getter defined-function-code #:init-keyword #:code))
+
+(define-class <total-function> (<defined-function>)
+  (proof #:getter theorem-proof #:init-keyword #:proof))
+
+(define-class <primitive-function> (<defined-function>))
+
+(define-generic total-function?)
+(define-method (total-function? x)
+  (or (is-a? x <core-function>)
+      (is-a? x <primitive-function>)
+      (is-a? x <total-function>)))
+
+(define-class <proposition> (<definition>)
+  (variables #:getter proposition-variables #:init-keyword #:variables)
+  (expression #:getter proposition-expression #:init-keyword #:expression))
+
+(define-class <conjecture> (<proposition>))
+(define-class <theorem> (<proposition>)
+  (proof #:getter theorem-proof #:init-keyword #:proof))
+(define-class <axiom> (<theorem>))
+
+(define (theorem? x)
+  (or (is-a? x <theorem>)
+      (is-a? x <axiom>)))
+
+(define-generic lookup)
+(define-method (lookup (name <symbol>) (s <system>))
+  (find (lambda (x) (eq? name (definition-name x)))
+        (system-definitions s)))
+
+(define-generic add-definition)
+(define-method (add-definition (d <definition>) (s <system>))
+  (if (lookup (definition-name d) s)
+      (raise-exception
+       (make-exception
+        (make-exception-with-message
+         "(vikalpa) add-definition: duplicated definition")
+        (make-exception-with-irritants (definition-name s))))
+      (make <system>
+        #:definitions (cons d (system-definitions s))
+        #:total-cliam-method (system-total-claim-method s))))
 
 (define (debug f . args)
   (if #f
@@ -73,13 +137,13 @@
     ((_ name
         constractor
         (m p?)
-        (n t? getter-name getter) ...)
+        (n t? getter-var getter) ...)
      (begin
        (define len (+ 1 (length (list n ...))))
-       (define (constractor getter-name ...)
+       (define (constractor getter-var ...)
          (let ((data (make-list len)))
            (list-set! data m 'name)
-           (list-set! data n getter-name)
+           (list-set! data n getter-var)
            ...
            data))
        (define (p? x)
@@ -128,6 +192,9 @@
        (not (eq? (car expr) 'quote))
        (not (eq? (car expr) 'if))))
 
+(define (app-form name args)
+  (cons name args))
+
 (define (app-form-name expr)
   (car expr))
 
@@ -204,39 +271,25 @@
 (define (variable=? v1 v2)
   (eq? v1 v2))
 
-;; (rule? x) -> boolean?
-(define (rule? x)
-  (and (list? x)
-       (= 5 (length x))
-       (eq? (car x) 'rule)
-       (let ((vars (list-ref x 1)))
-         (and (list? vars)
-              (every variable? vars)))
-       (let ((preconds (list-ref x 2)))
-         (and (list? preconds)
-              (every expression? preconds)))
-       (expression? (list-ref x 3))
-       (expression? (list-ref x 4))))
-
-;; (rule (list-of variable?) expression? expression?) -> rule?
-(define (rule vars preconds lhs rhs)
-  (list 'rule vars preconds lhs rhs))
-
-;; (rule-vars rule?) -> (list-of variable?)
-(define (rule-vars r)
-  (list-ref r 1))
-
-;; (rule-preconds rule?) -> expression?
-(define (rule-preconds r)
-  (list-ref r 2))
-
-;; (rule-lhs rule?) -> expression?
-(define (rule-lhs r)
-  (list-ref r 3))
-
-;; (rule-rhs rule?) -> expression?
-(define (rule-rhs r)
-  (list-ref r 4))
+(define-type rule
+  rule
+  (0 rule?)
+  (1 (lambda (vars)
+       (and (list? vars)
+            (every variable? vars)))
+     vars
+     rule-vars)
+  (2 (lambda (ps)
+       (and (list? ps)
+            (every expression? ps)))
+     ps
+     rule-preconds)
+  (3 expression?
+     lhs
+     rule-lhs)
+  (4 expression?
+     rhs
+     rule-rhs))
 
 (define (binding? x)
   (and (pair? x)
@@ -357,142 +410,18 @@
     => (cut substitute <> (rule-rhs rl)))
    (else #f)))
 
-(define (system? x)
-  (and (list? x)
-       (= 4 (length x))
-       (eq? 'system (list-ref x 0))
-       (system-definitions? (system-definitions x))
-       (system-proofs? (system-proofs x))
-       ((const #t) (system-totality-claim-list x))))
-
-(define (make-system defs prfs totality-claims)
-  (list 'system defs prfs totality-claims))
-
-(define (system-definitions sys)
-  (list-ref sys 1))
-
-(define (system-proofs sys)
-  (list-ref sys 2))
-
-(define (system-totality-claim-list sys)
-  (list-ref sys 3))
-
-(define (totality-claim id nat? less-than)
-  (list id nat? less-than))
-
-(define (totality-claim-id x)
-  (list-ref x 0))
-
-(define (totality-claim-natural x)
-  (list-ref x 1))
-
-(define (totality-claim-less-than x)
-  (list-ref x 2))
-
-(define (lookup x sys)
-  (assoc x (system-definitions sys)))
-
-(define (find-proof x sys)
-  (assoc x (system-proofs sys)))
-
-;; (system-definitions? x) -> boolean?
-(define (system-definitions? x)
-  (cond ((null? x) #t)
-        ((pair? x)
-         (and (pair? (car x))
-              (or (theorem*? (car x))
-                  (primitive-function? (car x))
-                  (macro? (car x))
-                  (function? (car x)))
-              (system-definitions? (cdr x))))
-        (else #f)))
-
-;; (system-proofs? x) -> boolean?
-(define (system-proofs? x)
-  (cond ((null? x) #t)
-        ((pair? x)
-         (and (pair? (car x))
-              (proof? (car x))
-              (system-proofs? (cdr x))))
-        (else #f)))
-
-(define (primitive-function? x)
-  (and (list? x)
-       (= 6 (length x))
-       (variable? (function-name x))
-       (eq? 'primitive-function (list-ref x 1))
-       (vars? (function-vars x))
-       ((option expression?) (function-expression x))
-       ((option code?) (function-code x))
-       ((list-of expression?) (function-preconds x))))
-
-;; (primitive-function variable? vars?) -> primitive-function?
-(define (primitive-function name vs expr preconds code)
-  (list name 'primitive-function vs expr preconds code))
-
-(define (function? x)
-  (and (list? x)
-       (= 6 (length x))
-       (variable? (function-name x))
-       (eq? 'function (list-ref x 1))
-       (vars? (function-vars x))
-       (expression? (function-expression x))
-       ((option code?) (function-code x))
-       ((list-of expression?) (function-preconds x))))
-
-(define (code? x)
-  (and (list? x)
-       (= 2 (length x))
-       (eq? 'code (list-ref x 0))
-       ((const #t) (code-expr x))))
-
-(define (code x)
-  (list 'code x))
-
-(define (code-expr x)
-  (cadr x))
-
-;; (function variable? vars? expression?) -> function?
-(define/guard (function (name variable?)
-                        (vars vars?)
-                        (expr expression?)
-                        (preconds (list-of expression?))
-                        (code (option code?)))
-  (list name 'function vars expr preconds code))
-
-(define (function-name f)
-  (list-ref f 0))
-
-(define (function-vars f)
-  (list-ref f 2))
-
-(define (function-expression f)
-  (list-ref f 3))
-
-(define (function-preconds f)
-  (list-ref f 4))
+(define-type code
+  code
+  (0 code?)
+  (1 (const #t)
+     expr
+     code-expr))
 
-(define (function-code f)
-  (list-ref f 5))
-
-(define (definition-name d)
-  (list-ref d 0))
-
-(define (definition-vars d)
-  (list-ref d 2))
-
-(define (definition-expression d)
-  (list-ref d 3))
-
-(define (mrule? x)
-  (and (list? x)
-       (= 3 (length x))
-       (eq? 'mrule (list-ref x 0))
-       ((const #t) (mrule-lhs x))
-       ((const #t) (mrule-rhs x))))
-
-(define (mrule lhs rhs)
-  (list 'mrule lhs rhs))
+(define-type mrule
+  mrule
+  (0 mrule?)
+  (1 (const #t) lhs mrule-lhs)
+  (2 (const #t) rhs mrule-rhs))
 
 (define (mrule-vars mrl)
   (define (all-vars x)
@@ -504,33 +433,18 @@
           (else '())))
   (all-vars (mrule-lhs mrl)))
 
-(define (mrule-lhs mrl)
-  (list-ref mrl 1))
-
-(define (mrule-rhs mrl)
-  (list-ref mrl 2))
-
-(define (macro? x)
-  (and (list? x)
-       (= 4 (length x))
-       (eq? 'macro (list-ref x 1))
-       (variable? (macro-name x))
-       (let ((mrls (macro-mrules x)))
-         (and (list? mrls)
-              (every mrule? mrls)))
-       ((list-of symbol?) (macro-literals x))))
-
-(define (macro-name m)
-  (list-ref m 0))
-
-(define (macro-mrules m)
-  (list-ref m 2))
-
-(define (macro-literals m)
-  (list-ref m 3))
-
-(define (macro name rules ls)
-  (list name 'macro rules ls))
+(define-type macro
+  macro
+  (1 macro?)
+  (0 variable? name macro-name)
+  (2 (lambda (mrls)
+       (and (list? mrls)
+            (every mrule? mrls)))
+     mruls
+     macro-mrules)
+  (3 (list-of symbol?)
+     literals
+     macro-literals))
 
 (define (apply-mrule rl ls expr)
   (define (literal? x)
@@ -669,90 +583,23 @@
           (expand-let (cdr x))))
    (else x)))
 
-(define (succ x)
-  (+ x 1))
-
-(define (pred x)
-  (- x 1))
-
-(define (natural->expr n)
-  (if (<= n 0)
-      ''0
-      `(succ ,(natural->expr (pred n)))))
-
-(define (pair->expr x)
-  (if (pair? x)
-      `(cons ,(pair->expr (car x))
-             ,(pair->expr (cdr x)))
-      (expr-quote x)))
-
 (define (convert-to-expression x)
   (quote-all
    (expand* (filter macro? (system-definitions (current-system)))
             (expand-let x))))
 
-;; (axiom variable? vars? expression?) -> axiom?
-;; axiom? is theorem*
-(define/guard (axiom (name variable?) (vars vars?) (expr expression?))
-  (list name 'axiom vars expr))
-
 (define (vars? x)
   (and (list? x)
        (every variable? x)))
 
-;; (axiom? x) -> boolean?
-(define (axiom? x)
-  (and (list? x)
-       (= 4 (length x))
-       (variable?  (list-ref x 0))
-       (eq? 'axiom (list-ref x 1))
-       (vars? (list-ref x 2))
-       (expression? (list-ref x 3))))
-
-;; (theorem name vars? expression?) -> theorem?
-(define/guard (theorem (name variable?) (vars vars?) (expr expression?))
-  (list name 'theorem vars expr))
-
-;; (theorem? x) -> boolean?
-;; theorem? is theorem*
-(define (theorem? x)
-  (and (list? x)
-       (= 4 (length x))
-       (variable? (list-ref x 0))
-       (eq? 'theorem (list-ref x 1))
-       (vars? (list-ref x 2))
-       (expression? (list-ref x 3))))
-
-(define (theorem-name x)
-  (list-ref x 0))
-
-;; (theorem*? x) -> boolean?
-(define (theorem*? x)
-  (or (axiom? x)
-      (theorem? x)))
-
-(define (theorem-name x)
-  (list-ref x 0))
-
-(define (theorem-vars x)
-  (list-ref x 2))
-
-(define (theorem-expression x)
-  (list-ref x 3))
-
 (define (theorem-rules x)
-  (expression->rules (theorem-vars x)
+  (expression->rules (theorem-variables x)
                      '()
                      (theorem-expression x)))
 
-(define (error? x)
-  (and (pair? x)
-       (eq? 'error (car x))))
-
 (define (rewrite/eval expr sys)
   (let eval ((expr expr))
     (cond
-     ((error? expr) expr)
      ((expr-quoted? expr) expr)
      ((app-form? expr)
       (let ((args (map eval (app-form-args expr)))
@@ -773,11 +620,6 @@
      (else
       `(error eval invalid-expression ,expr)))))
 
-(define/guard (system-eval (expr (const #t)) (sys system?))
-  (rewrite/eval (parameterize ((current-system sys))
-                  (convert-to-expression expr))
-                sys))
-
 ;; (rewriter path? command?) -> rewriter?
 (define (rewriter p c)
   (cons p c))
@@ -831,6 +673,11 @@
 (define (command-options x)
   (cdr x))
 
+;; (define/guard (system-eval (expr (const #t)) (sys system?))
+;;   (rewrite/eval (parameterize ((current-system sys))
+;;                   (convert-to-expression expr))
+;;                 sys))
+
 ;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?)
 (define (extract path expr fail)
   (if (null? path)
@@ -865,22 +712,22 @@
           (fail 'invalid-path path))))))
 
 (define (function->rules x)
-  (list (rule (function-vars x)
-              (function-preconds x)
+  (list (rule (function-variables x)
+              (condition-expressions (function-condition x))
               (function-app-form x)
-              (definition-expression x))
-        (rule (function-vars x)
-              (function-preconds x)
-              (definition-expression x)
+              (defined-function-expression x))
+        (rule (function-variables x)
+              (condition-expressions (function-condition x))
+              (defined-function-expression x)
               (function-app-form x))))
 
 (define (apply-function f args)
   (apply-rule '()
-              (rule (function-vars f)
+              (rule (function-variables f)
                     '()
-                    (function-app-form f)
-                    (function-expression f))
-              (cons (function-name f) args)
+                    (defined-function-app-form f)
+                    (defined-function-expression f))
+              (app-form (definition-name f) args)
               '()))
 
 (define (parse-options/theorem ops fail)
@@ -905,6 +752,12 @@
      (else
       (fail 'apply-theorem cmd expr)))))
 
+(define (rewrite/induction sys fname vars expr fail)
+  (cond
+   ((lookup fname sys)
+    (cut make-induction-claim <> vars expr))
+   (else (fail 'induction 'not-found fname))))
+
 (define (rewrite1 sys expr fail r)
   (let* ((cmd (rewriter-command r))
          (cmd/name (command-name cmd)))
@@ -913,20 +766,23 @@
         (extract (rewriter-path r) expr fail)
       (builder
        (cond
-        ((core-function-name? cmd/name)
-         (rewrite/core cmd/name extracted-expr fail))
         ((equal? '(eval) cmd/name)
          (rewrite/eval extracted-expr sys))
+        ((match cmd/name
+           (`(induction ,(f . vars))
+            (rewrite/induction sys f vars extracted-expr fail))
+           (`(induction . ,x)
+            (fail 'induction x))
+           (else #f)) => identity)
         ((eq? 'error cmd/name) (fail extracted-expr))
         ((and (symbol? cmd/name)
               (lookup cmd/name sys))
          => (lambda (x)
               (cond
-               ((theorem*? x)
+               ((is-a? x <proposition>)
                 (rewrite/theorem cmd sys x preconds extracted-expr fail))
-               ((or (function? x)
-                    (and (primitive-function? x)
-                         (function-expression x)))
+               ((and (total-function? x)
+                     (is-a? x <defined-function>))
                 (cond
                  ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
@@ -936,6 +792,7 @@
                 (fail 'invalid-command cmd extracted-expr)))))
         (else (fail 'command-not-found cmd extracted-expr)))))))
 
+#;
 (define/guard (rewrite (sys system?) (expr (const #t)) (seq sequence?))
   (let ((expr (convert-to-expression expr)))
     (let loop ((expr expr)
@@ -999,250 +856,226 @@
           '())))
 
 (define (theorem->rules def)
-  (expression->rules (theorem-vars def)
+  (expression->rules (theorem-variables def)
                      '()
                      (theorem-expression def)))
 
-(define current-system (make-parameter (make-system '() '() '())))
-
-(define (add-definition x)
-  (let ((sys (current-system)))
-    (current-system
-     (cond ((lookup (definition-name x) sys)
-            => (lambda (d)
-                 (if (equal? x d)
-                     sys
-                     (error "(vikalpa) add-definition: duplicated"
-                            (definition-name d)))))
-           (else (make-system (cons x (system-definitions sys))
-                              (system-proofs sys)
-                              (system-totality-claim-list sys)))))
-    x))
-
-(define (add-proof x)
-  (let ((sys (current-system)))
-    (current-system
-     (cond ((find-proof (proof-name x) sys)
-            => (lambda (prf)
-                 (if (equal? x prf)
-                     sys
-                     (error "add-proof: duplicated"))))
-           (else (make-system (system-definitions sys)
-                              (cons x (system-proofs sys))
-                              (system-totality-claim-list sys)))))
-    x))
-
-(define reserved-symbols '(quote let if error))
-(define (reserved? x)
-  (member x reserved-symbols))
-
-(define-syntax define-axiom
-  (syntax-rules ()
-    ((_ name (var ...) expr)
-     (let ((t (axiom 'name '(var ...)
-                     (make-theorem-claim (convert-to-expression 'expr)
-                                         (current-system)))))
-       (add-definition t)
-       (validate-definition t)
-       t))))
-
-(define-syntax define-theorem
-  (syntax-rules ()
-    ((_ name (var ...) expr)
-     (let ((t (theorem 'name '(var ...)
-                       (make-theorem-claim (convert-to-expression 'expr)
-                                           (current-system)))))
-       (add-definition t)
-       (validate-definition t)
-       t))))
-
-(define-syntax define-function
-  (syntax-rules ()
-    ((_ name (var ...) precond ... expr)
-     (let ((f (function 'name '(var ...)
-                        (convert-to-expression 'expr)
-                        '(precond ...)
-                        (code 'expr))))
-       (add-definition f)
-       (validate-definition f)
-       f))))
-
-(define-syntax define-primitive-function
-  (syntax-rules ()
-    ((_ name (var ...) precond ... expr)
-     (let ((f (primitive-function 'name '(var ...)
-                                  (convert-to-expression 'expr)
-                                  '(precond ...)
-                                  (code 'expr))))
-       (add-definition f)
-       (validate-definition f)
-       f))))
-
-(define-syntax define-core-function
-  (syntax-rules ()
-    ((_ name (var ...) precond ...)
-     (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f)))
-       (add-definition f)
-       f))))
-
-(define-syntax define-syntax-rules
-  (syntax-rules ()
-    ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
-     (let ((m (macro 'name
-                (list (mrule '(lhs1 . lhs2) 'rhs)
-                      ...)
-                '(l ...))))
-       (add-definition m)
-       m))))
-
-(define (find-totality-claim name sys)
-  (assoc name (system-totality-claim-list sys)))
-
-(define (add-totality-claim tc)
-  (let ((sys (current-system)))
-    (cond ((find-totality-claim (totality-claim-id tc) sys)
-           => (lambda (tc2)
-                (unless (equal? tc tc2)
-                  (error "(vikalpa) define-totality-claim: duplicated"
-                         tc)))))
-    (unless (and (symbol? (totality-claim-id tc))
-                 (cond ((lookup (totality-claim-natural tc) sys)
-                        => function*?)
-                       (else #f))
-                 (cond ((lookup (totality-claim-less-than tc) sys)
-                        => function*?)
-                       (else #f)))
-      (error "(vikalpa) define-totality-claim: invalid totality-claim"
-             tc))
-    (current-system
-     (make-system (system-definitions sys)
-                  (system-proofs sys)
-                  (cons tc (system-totality-claim-list sys))))))
-
-(define-syntax-rule (define-totality-claim name nat? <)
-  (add-totality-claim (totality-claim 'name 'nat? '<)))
-
-(define core-function-names
-  '(not equal? pair? cons car cdr integer? < succ pred))
-
-(define (core-function-name? x)
-  (member x core-function-names))
-
-(define (rewrite/core name extracted-expr fail)
-  (case name
-    ((not)
-     (match extracted-expr
-       (('not `(quote ,x))
-        (expr-quote (not x)))
-       (else
-        (fail 'not extracted-expr))))
-    ((equal?)
-     (match extracted-expr
-       (('equal? `(quote ,x) `(quote ,y))
-        (expr-quote (equal? x y)))
-       (else
-        (fail 'equal? extracted-expr))))
-    ((pair?)
-     (match extracted-expr
-       (('pair? `(quote ,x))
-        (expr-quote (pair? x)))
-       (else
-        (fail 'pair? extracted-expr))))
-    ((cons)
-     (match extracted-expr
-       (('cons `(quote ,x) `(quote ,y))
-        (expr-quote (cons x y)))
-       (else
-        (fail 'cons extracted-expr))))
-    ((car)
-     (match extracted-expr
-       (('car `(quote ,x))
-        (if (pair? x)
-            (expr-quote (car x))
-            ''undefined))
-       (else
-        (fail 'car extracted-expr))))
-    ((cdr)
-     (match extracted-expr
-       (('cdr `(quote ,x))
-        (if (pair? x)
-            (expr-quote (cdr x))
-            ''undefined))
-       (else
-        (fail 'cdr extracted-expr))))
-    ((integer?)
-     (match extracted-expr
-       (('natural? `(quote ,x))
-        (expr-quote (natural? x)))
-       (else
-        (fail 'natural? extracted-expr))))
-    ((succ)
-     (match extracted-expr
-       (('succ `(quote ,x))
-        (if (and (natural? x)
-                 (< 0 x))
-            (expr-quote (succ x))
-            ''undefined))
-       (else
-        (fail 'succ extracted-expr))))
-    ((pred)
-     (match extracted-expr
-       (('pred `(quote ,x))
-        (if (natural? x)
-            (expr-quote (pred x))
-            ''undefined))
-       (else
-        (fail 'pred extracted-expr))))
-    ((<)
-     (match extracted-expr
-       (('< `(quote ,x) `(quote ,y))
-        (if (and (natural? x) (natural? y))
-            (expr-quote (< x y))
-            ''undefined))
-       (else
-        (fail 'pred extracted-expr))))
-    (else (fail 'rewrite/core 'invalid))))
-
-(define* (core-system #:optional (parent (make-system '() '() '())))
-  (parameterize ((current-system parent))
-    (define-core-function not (x))
-    (define-core-function equal? (x y))
-    (define-core-function pair? (x y))
-    (define-core-function cons (x y))
-    (define-core-function car (x) (pair? x))
-    (define-core-function cdr (x) (pair? x))
-    (define-core-function natural? (x))
-    (define-core-function < (x y) (natural? x) (natural? y))
-    (define-core-function succ (x) (natural? x))
-    (define-core-function pred (x) (natural? x))
-    (current-system)))
-
-(define-syntax define-system
-  (syntax-rules ()
-    ((_ name (systems ...) expr ...)
-     (define* (name #:optional (parent (make-system '() '() '())))
-       (parameterize ((current-system
-                       ((compose systems ... core-system) parent)))
-         expr
-         ...
-         (unless (system? (current-system))
-           (error "define-system: invalid system"))
-         (current-system))))))
-
-(define (measure? x)
-  (and (pair? x)
-       (variable? (car x))
-       (list? (cdr x))
-       (<= 1 (length (cdr x)))))
-
-(define (measure-function-name m)
-  (car m))
-
-(define (measure-function-vars m)
-  (cdr m))
-
-(define (function-app-form f)
-  (cons (function-name f) (function-vars f)))
+;; (define current-system (make-parameter (make-system '() '() '())))
+
+
+;; (define (add-definition x)
+;;   (let ((sys (current-system)))
+;;     (current-system
+;;      (cond ((lookup (definition-name x) sys)
+;;             => (lambda (d)
+;;                  (if (equal? x d)
+;;                      sys
+;;                      (error "(vikalpa) add-definition: duplicated"
+;;                             (definition-name d)))))
+;;            (else (make-system (cons x (system-definitions sys))
+;;                               (system-proofs sys)
+;;                               (system-totality-claim-list sys)))))
+;;     x))
+
+;; (define (add-proof x)
+;;   (let ((sys (current-system)))
+;;     (current-system
+;;      (cond ((find-proof (proof-name x) sys)
+;;             => (lambda (prf)
+;;                  (if (equal? x prf)
+;;                      sys
+;;                      (error "add-proof: duplicated"))))
+;;            (else (make-system (system-definitions sys)
+;;                               (cons x (system-proofs sys))
+;;                               (system-totality-claim-list sys)))))
+;;     x))
+
+;; (define reserved-symbols '(quote let if error))
+;; (define (reserved? x)
+;;   (member x reserved-symbols))
+
+;; (define-syntax define-axiom
+;;   (syntax-rules ()
+;;     ((_ name (var ...) expr)
+;;      (let ((t (axiom 'name '(var ...)
+;;                      (convert-to-expression 'expr))))
+;;        (add-definition t)
+;;        (validate-definition t)
+;;        t))))
+
+;; (define-syntax define-theorem
+;;   (syntax-rules ()
+;;     ((_ name (var ...) expr)
+;;      (let ((t (theorem 'name '(var ...)
+;;                        (convert-to-expression 'expr))))
+;;        (add-definition t)
+;;        (validate-definition t)
+;;        t))))
+
+;; (define-syntax define-function
+;;   (syntax-rules ()
+;;     ((_ name (var ...) precond ... expr)
+;;      (let ((f (function 'name '(var ...)
+;;                         (convert-to-expression 'expr)
+;;                         '(precond ...)
+;;                         (code 'expr))))
+;;        (add-definition f)
+;;        (validate-definition f)
+;;        f))))
+
+;; (define-syntax define-primitive-function
+;;   (syntax-rules ()
+;;     ((_ name (var ...) precond ... expr)
+;;      (let ((f (primitive-function 'name '(var ...)
+;;                                   (convert-to-expression 'expr)
+;;                                   '(precond ...)
+;;                                   (code 'expr))))
+;;        (add-definition f)
+;;        (validate-definition f)
+;;        f))))
+
+;; (define-syntax define-core-function
+;;   (syntax-rules ()
+;;     ((_ name (var ...) precond ...)
+;;      (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f)))
+;;        (add-definition f)
+;;        f))))
+
+;; (define-syntax define-syntax-rules
+;;   (syntax-rules ()
+;;     ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
+;;      (let ((m (macro 'name
+;;                 (list (mrule '(lhs1 . lhs2) 'rhs)
+;;                       ...)
+;;                 '(l ...))))
+;;        (add-definition m)
+;;        m))))
+
+;; (define (find-totality-claim name sys)
+;;   (assoc name (system-totality-claim-list sys)))
+
+;; (define (add-totality-claim tc)
+;;   (let ((sys (current-system)))
+;;     (cond ((find-totality-claim (totality-claim-id tc) sys)
+;;            => (lambda (tc2)
+;;                 (unless (equal? tc tc2)
+;;                   (error "(vikalpa) define-totality-claim: duplicated"
+;;                          tc)))))
+;;     (unless (and (symbol? (totality-claim-id tc))
+;;                  (cond ((lookup (totality-claim-natural tc) sys)
+;;                         => function*?)
+;;                        (else #f))
+;;                  (cond ((lookup (totality-claim-less-than tc) sys)
+;;                         => function*?)
+;;                        (else #f)))
+;;       (error "(vikalpa) define-totality-claim: invalid totality-claim"
+;;              tc))
+;;     (current-system
+;;      (make-system (system-definitions sys)
+;;                   (system-proofs sys)
+;;                   (cons tc (system-totality-claim-list sys))))))
+
+;; (define-syntax-rule (define-totality-claim name nat? <)
+;;   (add-totality-claim (totality-claim 'name 'nat? '<)))
+
+;; (define core-function-names
+;;   '(not equal? pair? cons car cdr integer? < binary-+ unary--))
+
+;; (define (core-function-name? x)
+;;   (member x core-function-names))
+
+;; (define (rewrite/core name extracted-expr fail)
+;;   (case name
+;;     ((not)
+;;      (match extracted-expr
+;;        (('not `(quote ,x))
+;;         (expr-quote (not x)))
+;;        (else
+;;         (fail 'not extracted-expr))))
+;;     ((equal?)
+;;      (match extracted-expr
+;;        (('equal? `(quote ,x) `(quote ,y))
+;;         (expr-quote (equal? x y)))
+;;        (else
+;;         (fail 'equal? extracted-expr))))
+;;     ((pair?)
+;;      (match extracted-expr
+;;        (('pair? `(quote ,x))
+;;         (expr-quote (pair? x)))
+;;        (else
+;;         (fail 'pair? extracted-expr))))
+;;     ((cons)
+;;      (match extracted-expr
+;;        (('cons `(quote ,x) `(quote ,y))
+;;         (expr-quote (cons x y)))
+;;        (else
+;;         (fail 'cons extracted-expr))))
+;;     ((car)
+;;      (match extracted-expr
+;;        (('car `(quote ,x))
+;;         (if (pair? x)
+;;             (expr-quote (car x))
+;;             ''()))
+;;        (else
+;;         (fail 'car extracted-expr))))
+;;     ((cdr)
+;;      (match extracted-expr
+;;        (('cdr `(quote ,x))
+;;         (if (pair? x)
+;;             (expr-quote (cdr x))
+;;             ''()))
+;;        (else
+;;         (fail 'cdr extracted-expr))))
+;;     ((integer?)
+;;      (match extracted-expr
+;;        (('integer? `(quote ,x))
+;;         (expr-quote (integer? x)))
+;;        (else
+;;         (fail 'integer? extracted-expr))))
+;;     ((<)
+;;      (match extracted-expr
+;;        (('< `(quote ,x) `(quote ,y))
+;;         (let ((x (if (integer? x) x 0))
+;;               (y (if (integer? y) y 0)))
+;;           (expr-quote (< x y))))
+;;        (else
+;;         (fail '< extracted-expr))))
+;;     ((succ)
+;;      (match extracted-expr
+;;        (('binary-+ `(quote ,x) `(quote ,y))
+;;         (if (integer? x)
+;;             (if (integer? y)
+;;                 (expr-quote (+ x y))
+;;                 (expr-quote x))
+;;             (if (integer? y)
+;;                 (expr-quote y)
+;;                 (expr-quote 0))))
+;;        (else
+;;         (fail 'binary-+ extracted-expr))))
+;;     ((unary--)
+;;      (match extracted-expr
+;;        (('unary-- `(quote ,x))
+;;         (if (integer? x)
+;;             (expr-quote (- x))
+;;             (expr-quote 0)))
+;;        (else
+;;         (fail 'unary-- extracted-expr))))
+;;     (else (fail 'rewrite/core 'invalid))))
+
+;; (define-syntax define-system
+;;   (syntax-rules ()
+;;     ((_ name (systems ...) expr ...)
+;;      (define* (name #:optional (parent (make-system '() '() '())))
+;;        (parameterize ((current-system
+;;                        ((compose systems ... core-system) parent)))
+;;          expr
+;;          ...
+;;          (unless (system? (current-system))
+;;            (error "define-system: invalid system"))
+;;          (current-system))))))
+
+(define (defined-function-app-form f)
+  (cons (definition-name f) (function-variables f)))
 
 (define (single? x)
   (and (pair? x)
@@ -1274,435 +1107,360 @@
    (else
     (if/if x y ''#t))))
 
-(define (make-totality-claim tc m-expr f)
-  (let* ((name (function-name f)))
-    (define (convert app-form)
-      (cond
-       ((apply-rule '()
-                    (rule (function-vars f)
-                          '()
-                          (function-app-form f)
-                          m-expr)
-                    app-form
-                    '())
-        => identity)
-       (else (error "make-totality-claim: convert error"
-                    (function-name f)
-                    m-expr
-                    app-form))))
-    (if/if `(,(totality-claim-natural tc) ,m-expr)
-           (let loop ((expr (function-expression f)))
-             (cond
-              ((expr-quoted? expr) ''#t)
-              ((variable? expr) ''#t)
-              ((if-form? expr)
-               (let ((test/result (loop (if-form-test expr)))
-                     (then/result (loop (if-form-then expr)))
-                     (else/result (loop (if-form-else expr))))
-                 (and/if test/result
-                         (if/if (if-form-test expr)
-                                then/result
-                                else/result))))
-              ((app-form? expr)
-               (let ((rest
-                      (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))))))))
-                 (if (eq? name (app-form-name expr))
-                     (and/if `(,(totality-claim-less-than tc)
-                               ,(convert expr)
-                               ,m-expr)
-                             rest)
-                     rest)))
-              (else (error "(vikalpa) make-totality-claim: error"
-                           (function-name f)
-                           m-expr))))
-           ''#f)))
-
-(define (make-totality-claim/preconds 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 (function-preconds f)))
-                           (map (lambda (precond)
-                                  (substitute (map cons
-                                                   (function-vars f)
-                                                   (cdr expr))
-                                              precond))
-                                preconds))))
-                      (else (error "make-totality-claim/preconds: error")))
-                rest)))
-     ((if-form? expr)
-      (find-preconds (if-form-test expr)))
-     (else '())))
-  (define (build/find-if expr)
-    (cond
-     ((if-form? expr)
-      (if/if (build/find-if (if-form-test expr))
-             (build (if-form-then expr))
-             (build (if-form-else expr))))
-     ((app-form? expr)
-      (apply and/if (map build/find-if (app-form-args expr))))
-     (else ''#t)))
-  (define (build expr)
-    (cond
-     ((if-form? expr)
-      (apply and/if
-             (append (find-preconds (if-form-test expr))
-                     (list (if/if (if-form-test expr)
-                                  (build (if-form-then expr))
-                                  (build (if-form-else expr)))))))
-     ((app-form? expr)
-      (apply and/if
-             (append (find-preconds expr)
-                     (list (build/find-if expr)))))
-     (else ''#t)))
-  (if/if (build expr)
-         '#t
-         '#f))
-
-(define (make-theorem-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 (function-preconds f)))
-                           (map (lambda (precond)
-                                  (substitute (map cons
-                                                   (function-vars f)
-                                                   (cdr expr))
-                                              precond))
-                                preconds))))
-                      (else (error "make-theorem-claim/preconds: error")))
-                rest)))
-     ((if-form? expr)
-      (find-preconds (if-form-test expr)))
-     (else '())))
-  (define (build/find-if expr)
-    (cond
-     ((if-form? expr)
-      (if/if (build/find-if (if-form-test expr))
-             (build (if-form-then expr))
-             (build (if-form-else expr))))
-     ((app-form? expr)
-      (fold implies/if
-            expr
-            (map build/find-if (app-form-args expr))))
-     (else expr)))
-  (define (build expr)
-    (cond
-     ((if-form? expr)
-      (fold implies/if
-            (if/if (if-form-test expr)
-                   (build (if-form-then expr))
-                   (build (if-form-else expr)))
-            (find-preconds (if-form-test expr))))
-     ((app-form? expr)
-      (fold implies/if
-            (build/find-if expr)
-            (find-preconds expr)))
-     (else expr)))
-  (build expr))
-
-(define/guard (make-induction-claim (f function*?)
-                                    (vars (list-of variable?))
-                                    (t theorem?))
+;; (define (make-totality-claim tc m-expr f)
+;;   (let* ((name (function-name f)))
+;;     (define (convert app-form)
+;;       (cond
+;;        ((apply-rule '()
+;;                     (rule (function-vars f)
+;;                           '()
+;;                           (function-app-form f)
+;;                           m-expr)
+;;                     app-form
+;;                     '())
+;;         => identity)
+;;        (else (error "make-totality-claim: convert error"
+;;                     (function-name f)
+;;                     m-expr
+;;                     app-form))))
+;;     (if/if `(,(totality-claim-natural tc) ,m-expr)
+;;            (let loop ((expr (function-expression f)))
+;;              (cond
+;;               ((expr-quoted? expr) ''#t)
+;;               ((variable? expr) ''#t)
+;;               ((if-form? expr)
+;;                (let ((test/result (loop (if-form-test expr)))
+;;                      (then/result (loop (if-form-then expr)))
+;;                      (else/result (loop (if-form-else expr))))
+;;                  (and/if test/result
+;;                          (if/if (if-form-test expr)
+;;                                 then/result
+;;                                 else/result))))
+;;               ((app-form? expr)
+;;                (let ((rest
+;;                       (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))))))))
+;;                  (if (eq? name (app-form-name expr))
+;;                      (and/if `(,(totality-claim-less-than tc)
+;;                                ,(convert expr)
+;;                                ,m-expr)
+;;                              rest)
+;;                      rest)))
+;;               (else (error "(vikalpa) make-totality-claim: error"
+;;                            (function-name f)
+;;                            m-expr))))
+;;            ''#f)))
+
+;; (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 (function-guard f)))
+;;                            (map (lambda (precond)
+;;                                   (substitute (map cons
+;;                                                    (function-vars f)
+;;                                                    (cdr expr))
+;;                                               precond))
+;;                                 preconds))))
+;;                       (else (error "make-guard-claim: error")))
+;;                 rest)))
+;;      ((if-form? expr)
+;;       (find-preconds (if-form-test expr)))
+;;      (else '())))
+;;   (define (build/find-if expr)
+;;     (cond
+;;      ((if-form? expr)
+;;       (if/if (build/find-if (if-form-test expr))
+;;              (build (if-form-then expr))
+;;              (build (if-form-else expr))))
+;;      ((app-form? expr)
+;;       (apply and/if (map build/find-if (app-form-args expr))))
+;;      (else ''#t)))
+;;   (define (build expr)
+;;     (cond
+;;      ((if-form? expr)
+;;       (apply and/if
+;;              (append (find-preconds (if-form-test expr))
+;;                      (list (if/if (if-form-test expr)
+;;                                   (build (if-form-then expr))
+;;                                   (build (if-form-else expr)))))))
+;;      ((app-form? expr)
+;;       (apply and/if
+;;              (append (find-preconds expr)
+;;                      (list (build/find-if expr)))))
+;;      (else ''#t)))
+;;   (if/if (build expr)
+;;          ''#t
+;;          ''#f))
+
+(define (make-induction-claim f vars c)
   (define (find-app-forms expr)
     (cond
      ((app-form? expr)
       (let ((rest (append-map find-app-forms (cdr expr))))
-        (if (eq? (function-name f) (app-form-name expr))
+        (if (eq? (definition-name f) (app-form-name expr))
             (cons expr rest)
             rest)))
      ((if-form? expr)
       (error "make-induction-claim(find-app-forms): not supported"
              expr))
      (else '())))
-  (let ((c (theorem-expression t)))
-    (define (prop app-form)
-      (cond
-       ((apply-rule '()
-                    (rule vars
-                          '()
-                          (cons (function-name f) vars)
-                          c)
-                    app-form
-                    '())
-        => identity)
-       (else
-        (error "make-induction-claim: fail" app-form))))
+  (define (prop app-form)
     (cond
-     ((apply-function f vars)
-      => (lambda (expr)
-           (let build ((expr expr))
-             (cond
-              ((if-form? expr)
-               (let ((app-forms (find-app-forms (if-form-test expr))))
-                 (implies/if (if (null? app-forms)
-                                 ''#t
-                                 (fold implies/if c (map prop app-forms)))
-                             (if/if (if-form-test expr)
-                                    (build (if-form-then expr))
-                                    (build (if-form-else expr))))))
-              (else
-               (let ((app-forms (find-app-forms expr)))
-                 (fold implies/if c (map prop app-forms))))))))
-     (else (error "make-induction-claim: invalid"
-                  f vars t)))))
-
-(define (proof? x)
-  (and (list? x)
-       (= 4 (length x))
-       (symbol? (proof-name x))
-       (eq? 'proof (list-ref x 1))
-       (seed? (proof-seed x))
-       (sequence? (proof-sequence x))))
-
-(define (proof name seed sequence)
-  (list name 'proof seed sequence))
-
-(define (proof-name x)
-  (list-ref x 0))
-
-(define (proof-seed x)
-  (list-ref x 2))
-
-(define (proof-sequence x)
-  (list-ref x 3))
-
-(define seed? (const #t))
-
-(define-syntax define-proof
-  (syntax-rules ()
-    ((_ name
-        (seed ...)
-        (((n ...) cmd ...) ...))
-     (add-proof (proof 'name
-                       '(seed ...)
-                       '(((n ...) cmd ...) ...))))))
-
-(define (function*? x)
-  (or (function? x)
-      (primitive-function? x)))
-
-(define (validate-expression sys name vars expr)
-  (let* ((expr-fnames (expression-functions expr))
-         (expr-vars (expression-vars expr)))
-    (when (reserved? name)
-      (error (format #f "(vikalpa) ~a: reserved name" name)))
-    (for-each (lambda (x)
-                (when (member x expr-fnames)
-                  (error (format #f "(vikalpa) ~a: invalid variable name" name)
-                         x)))
-              vars)
-    (for-each (lambda (x)
-                (unless (cond ((lookup x sys) => function*?)
-                              (else #f))
-                  (error (format #f "(vikalpa) ~a: undefined function" name)
-                         x)))
-              expr-fnames)
-    (for-each (lambda (x)
-                (unless (member x vars)
-                  (error (format #f "(vikalpa) ~a: undefined variable" name)
-                         x)))
-              expr-vars)))
-
-(define (validate-definition d)
-  (let* ((vars (definition-vars d))
-         (name (definition-name d))
-         (expr (definition-expression d)))
-    (validate-expression (current-system) name vars expr)))
-
-(define (trivial-total? f)
-  (not (member (function-name f)
-               (expression-functions (function-expression f)))))
-
-(define (prove sys def pf)
-  (cond
-   ((theorem? def)
-    (prove/theorem sys def pf))
-   ((function? def)
-    (prove/function sys def pf))
-   (else (error "prove" def pf))))
-
-(define (prove/theorem sys t pf)
-  (let ((sys-without-self
-         (make-system (filter (lambda (d) (not (equal? t d)))
-                              (system-definitions sys))
-                      (system-proofs sys)
-                      (system-totality-claim-list sys))))
-    (match (proof-seed pf)
-      ((f . vars)
-       (cond
-        ((lookup f sys-without-self)
-         => (lambda (seed)
-              (let ((claim (make-induction-claim seed vars t)))
-                (validate-expression sys
-                                     `(claim-of ,(proof-name pf))
-                                     (theorem-vars t)
-                                     claim)
-                (rewrite sys-without-self
-                         claim
-                         (proof-sequence pf)))))
-        (else (error "(vikalpa) define-proof: induction function is not found."
-                     (proof-name pf)
-                     (cons f vars)))))
-      (()
-       (rewrite sys-without-self
-                (theorem-expression t)
-                (proof-sequence pf)))
-      (else
-       (error "prove/theorem: fail")))))
-
-(define (prove/function sys f pf)
-  (match (proof-seed pf)
-    (()
-     (unless (trivial-total? f)
-       (error "prove/function"))
-     (rewrite sys
-              (fold implies/if
-                    (make-totality-claim/preconds
-                     (function-expression f)
-                     sys)
-                    (function-preconds f))
-              (proof-sequence pf)))
-    ((id m-expr)
-     (cond
-      ((find-totality-claim id sys)
-       => (lambda (tc)
-            (let ((claim (make-totality-claim tc m-expr f)))
-              (validate-expression sys
-                                   `(claim-of ,(function-name f))
-                                   (function-vars f)
-                                   claim)
-              (rewrite sys
-                       (fold implies/if
-                             (and/if
-                              (make-totality-claim/preconds
-                               (function-expression f)
-                               sys)
-                              claim)
-                             (function-preconds f))
-                       (proof-sequence pf)))))
-      (else
-       (error "(vikalpa) define-proof: totality-claim is not found:"
-              (proof-name pf)
-              (proof-seed pf)))))
-    (else
-     (error "define-proof: fail"
-            (proof-name pf) (proof-seed pf)))))
-
-(define (system->scheme sys)
-  `(begin
-     ,@(map (lambda (f)
-              `(define (,(function-name f) ,@(function-vars f))
-                 ,(code-expr (function-code f))))
-            (reverse (filter (lambda (x)
-                               (and (function*? x)
-                                    (function-code x)))
-                             (system-definitions sys))))))
-
-(define/guard (check (sys system?))
-  (let loop ((sys sys)
-             (fails '()))
-    (let ((defs (system-definitions sys)))
-      (define* (next #:optional fail)
-        (loop (make-system (cdr defs)
-                           (system-proofs sys)
-                           (system-totality-claim-list sys))
-              (if fail
-                  (cons fail fails)
-                  fails)))
-      (cond
-       ((null? defs) fails)
-       ((or (theorem? (car defs))
-            (function? (car defs)))
-        (cond
-         #;
-         ((and (function? (car defs))
-               (trivial-total? (car defs)))
-          (next))
-         (else
-          (cond
-           ((find-proof (definition-name (car defs)) sys)
-            => (lambda (pf)
-                 (let ((result (prove sys (car defs) pf)))
-                   (cond
-                    ((equal? result ''#t)
-                     (next))
-                    (else
-                     (next (list (definition-name (car defs))
-                                 result)))))))
-           (else
-            (next (list (definition-name (car defs)))))))))
-       (else
-        (next))))))
-
-(define (pp x)
-  (pretty-print x
-                #:width 79
-                #:max-expr-width 50))
-
-(define/guard (show (sys system?) (name symbol?))
+     ((apply-rule '()
+                  (rule vars
+                        '()
+                        (app-form (definition-name f) vars)
+                        c)
+                  app-form
+                  '())
+      => identity)
+     (else
+      (error "make-induction-claim: fail" app-form))))
   (cond
-   ((lookup name sys)
-    => (lambda (def)
-         (cond
-          ((function? def)
-           `(define-function ,(function-name def) ,(function-vars def)
-              ,(function-expression def)))
-          ((theorem? def)
-           `(define-theorem ,(theorem-name def) ,(theorem-vars def)
-              ,(theorem-expression def)))
-          ((axiom? def)
-           `(define-axiom ,(theorem-name def) ,(theorem-vars def)
-              ,(theorem-expression def)))
-          ((primitive-function? def)
-           `(define-primitive-function
-              ,(function-name def)
-              ,(function-vars def)))
-          ((macro? def)
-           `(define-syntax-rules ,(macro-name def)))
-          (else
-           `(error 'fatal-error ,name)))))
-   (else
-    `(error 'not-found ,name))))
-
-(define/guard (load-system (sys system?))
-  (primitive-eval (system->scheme sys)))
-
-(define/guard (system-primitives (sys system?))
-  (append reserved-symbols
-          (map function-name
-               (filter primitive-function?
-                       (system-definitions sys)))))
-
-(define/guard (system-functions (sys system?))
-  (map function-name
-       (filter function?
-               (system-definitions sys))))
-
-(define/guard (system-theorems (sys system?))
-  (map theorem-name
-       (filter theorem?
-               (system-definitions sys))))
-
-(define/guard (system-axioms (sys system?))
-  (map theorem-name
-       (filter axiom?
-               (system-definitions sys))))
-
-(define/guard (system-macros (sys system?))
-  (map macro-name
-       (filter macro?
-               (system-definitions sys))))
-
-(define/guard (system-totality-claims (sys system?))
-  (system-totality-claim-list sys))
+   ((apply-function f vars)
+    => (lambda (expr)
+         (let build ((expr expr))
+           (cond
+            ((if-form? expr)
+             (let ((app-forms (find-app-forms (if-form-test expr))))
+               (implies/if (if (null? app-forms)
+                               ''#t
+                               (fold implies/if c (map prop app-forms)))
+                           (if/if (if-form-test expr)
+                                  (build (if-form-then expr))
+                                  (build (if-form-else expr))))))
+            (else
+             (let ((app-forms (find-app-forms expr)))
+               (fold implies/if c (map prop app-forms))))))))
+   (else (error "make-induction-claim: invalid"
+                f vars c))))
+
+;; (define (proof? x)
+;;   (and (list? x)
+;;        (= 4 (length x))
+;;        (symbol? (proof-name x))
+;;        (eq? 'proof (list-ref x 1))
+;;        (seed? (proof-seed x))
+;;        (sequence? (proof-sequence x))))
+
+;; (define (proof name seed sequence)
+;;   (list name 'proof seed sequence))
+
+;; (define (proof-name x)
+;;   (list-ref x 0))
+
+;; (define (proof-seed x)
+;;   (list-ref x 2))
+
+;; (define (proof-sequence x)
+;;   (list-ref x 3))
+
+;; (define seed? (const #t))
+
+;; (define-syntax define-proof
+;;   (syntax-rules ()
+;;     ((_ name
+;;         (((n ...) cmd ...) ...))
+;;      (add-proof (proof 'name
+;;                        '()
+;;                        '(((n ...) cmd ...) ...))))
+;;     ((_ name
+;;         (seed ...)
+;;         (((n ...) cmd ...) ...))
+;;      (add-proof (proof 'name
+;;                        '(seed ...)
+;;                        '(((n ...) cmd ...) ...))))))
+
+;; (define (function*? x)
+;;   (or (function? x)
+;;       (primitive-function? x)))
+
+;; (define (validate-expression sys name vars expr)
+;;   (let* ((expr-fnames (expression-functions expr))
+;;          (expr-vars (expression-vars expr)))
+;;     (when (reserved? name)
+;;       (error (format #f "(vikalpa) ~a: reserved name" name)))
+;;     (for-each (lambda (x)
+;;                 (when (member x expr-fnames)
+;;                   (error (format #f "(vikalpa) ~a: invalid variable name" name)
+;;                          x)))
+;;               vars)
+;;     (for-each (lambda (x)
+;;                 (unless (cond ((lookup x sys) => function*?)
+;;                               (else #f))
+;;                   (error (format #f "(vikalpa) ~a: undefined function" name)
+;;                          x)))
+;;               expr-fnames)
+;;     (for-each (lambda (x)
+;;                 (unless (member x vars)
+;;                   (error (format #f "(vikalpa) ~a: undefined variable" name)
+;;                          x)))
+;;               expr-vars)))
+
+;; (define (validate-definition d)
+;;   (let* ((vars (definition-vars d))
+;;          (name (definition-name d))
+;;          (expr (definition-expression d)))
+;;     (validate-expression (current-system) name vars expr)))
+
+;; (define (recur? f)
+;;   (member (function-name f)
+;;           (expression-functions (function-expression f))))
+
+;; (define (p x)
+;;   (format #t "p:~%~y" x)
+;;   x)
+
+;; (define (trivial-total? f sys)
+;;   (and (not (recur? f))))
+
+;; (define (prove sys def pf)
+;;   (cond
+;;    ((theorem? def)
+;;     (prove/theorem sys def pf))
+;;    ((function? def)
+;;     (prove/function sys def pf))
+;;    (else (error "prove" def pf))))
+
+;; (define (prove/theorem sys t pf)
+;;   (let ((sys-without-self
+;;          (make-system (filter (lambda (d) (not (equal? t d)))
+;;                               (system-definitions sys))
+;;                       (system-proofs sys)
+;;                       (system-totality-claim-list sys))))
+;;     (rewrite sys-without-self
+;;              (theorem-expression t)
+;;              (proof-sequence pf))))
+
+;; (define (prove/function sys f pf)
+;;   (match (proof-seed pf)
+;;     (()
+;;      (error "prove/function error"))
+;;     ((id m-expr)
+;;      (cond
+;;       ((find-totality-claim id sys)
+;;        => (lambda (tc)
+;;             (let ((claim (make-totality-claim tc m-expr f)))
+;;               (validate-expression sys
+;;                                    `(claim-of ,(function-name f))
+;;                                    (function-vars f)
+;;                                    claim)
+;;               (rewrite sys
+;;                        claim
+;;                        (proof-sequence pf)))))
+;;       (else
+;;        (error "(vikalpa) define-proof: totality-claim is not found:"
+;;               (proof-name pf)
+;;               (proof-seed pf)))))
+;;     (else
+;;      (error "define-proof: fail"
+;;             (proof-name pf) (proof-seed pf)))))
+
+;; (define (system->scheme sys)
+;;   `(begin
+;;      ,@(map (lambda (f)
+;;               `(define (,(function-name f) ,@(function-vars f))
+;;                  ,(code-expr (function-code f))))
+;;             (reverse (filter (lambda (x)
+;;                                (and (function*? x)
+;;                                     (function-code x)))
+;;                              (system-definitions sys))))))
+
+;; (define/guard (check (sys system?))
+;;   (let loop ((sys sys)
+;;              (fails '()))
+;;     (let ((defs (system-definitions sys)))
+;;       (define* (next #:optional fail)
+;;         (loop (make-system (cdr defs)
+;;                            (system-proofs sys)
+;;                            (system-totality-claim-list sys))
+;;               (if fail
+;;                   (cons fail fails)
+;;                   fails)))
+;;       (cond
+;;        ((null? defs) fails)
+;;        ((or (theorem? (car defs))
+;;             (function? (car defs)))
+;;         (cond
+;;          ((and (function? (car defs))
+;;                (trivial-total? (car defs) sys))
+;;           (next))
+;;          (else
+;;           (cond
+;;            ((find-proof (definition-name (car defs)) sys)
+;;             => (lambda (pf)
+;;                  (let ((result (prove sys (car defs) pf)))
+;;                    (cond
+;;                     ((equal? result ''#t)
+;;                      (next))
+;;                     (else
+;;                      (next (list (definition-name (car defs))
+;;                                  result)))))))
+;;            (else
+;;             (next (list (definition-name (car defs)))))))))
+;;        (else
+;;         (next))))))
+
+;; (define/guard (show (sys system?) (name symbol?))
+;;   (cond
+;;    ((lookup name sys)
+;;     => (lambda (def)
+;;          (cond
+;;           ((function? def)
+;;            `(define-function ,(function-name def) ,(function-vars def)
+;;               ,(function-expression def)))
+;;           ((theorem? def)
+;;            `(define-theorem ,(theorem-name def) ,(theorem-vars def)
+;;               ,(theorem-expression def)))
+;;           ((axiom? def)
+;;            `(define-axiom ,(theorem-name def) ,(theorem-vars def)
+;;               ,(theorem-expression def)))
+;;           ((primitive-function? def)
+;;            `(define-primitive-function
+;;               ,(function-name def)
+;;               ,(function-vars def)))
+;;           ((macro? def)
+;;            `(define-syntax-rules ,(macro-name def)))
+;;           (else
+;;            `(error 'fatal-error ,name)))))
+;;    (else
+;;     `(error 'not-found ,name))))
+
+;; (define/guard (load-system (sys system?))
+;;   (primitive-eval (system->scheme sys)))
+
+;; (define/guard (system-primitives (sys system?))
+;;   (append reserved-symbols
+;;           (map function-name
+;;                (filter primitive-function?
+;;                        (system-definitions sys)))))
+
+;; (define/guard (system-functions (sys system?))
+;;   (map function-name
+;;        (filter function?
+;;                (system-definitions sys))))
+
+;; (define/guard (system-theorems (sys system?))
+;;   (map theorem-name
+;;        (filter theorem?
+;;                (system-definitions sys))))
+
+;; (define/guard (system-axioms (sys system?))
+;;   (map theorem-name
+;;        (filter axiom?
+;;                (system-definitions sys))))
+
+;; (define/guard (system-macros (sys system?))
+;;   (map macro-name
+;;        (filter macro?
+;;                (system-definitions sys))))
+
+;; (define/guard (system-totality-claims (sys system?))
+;;   (system-totality-claim-list sys))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index c61e459..f37bdd0 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,16 +17,24 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (natural? size implies prelude)
+  #:export (prelude)
   #:use-module (vikalpa))
 
-(define-syntax implies
-  (syntax-rules ()
-    ((_ x y) (if x y #t))
-    ((_ x y z rest ...)
-     (if x (implies y z rest ...) #t))))
-
 (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))))
@@ -102,226 +110,5 @@
   (define-function zero? (x)
     (equal? 0 x))
 
-  (define-axiom pred/succ (x)
-    (implies (natural? x)
-             (equal? (pred (succ x)) x)))
-
-
-  (define-axiom succ/pred (x)
-    (implies (natural? x)
-             (not (zero? x))
-             (equal? (succ (pred x)) x)))
-
-  (define-axiom less/pred (x)
-    (implies (natural? x)
-             (equal? (< (pred x) x) #t)))
-  
   (define-totality-claim natural? natural? <)
-  (define-function + (x y)
-    (natural? x)
-    (natural? y)
-    (if (zero? x)
-        y
-        (succ (+ (pred x) y))))
-
-  (define-proof +
-    (natural? x)
-    ())
-  
-  #;
-  (define-proof natural?
-    ()
-    (((1 2 3 1) (eval))
-     ((1 2 3) if-true)
-     (() if-same (set x (zero? x)))
-     ((2 1 2) if-nest)
-     ((2 1) if-same)
-     ((2) if-true)
-     ((3 1 2) if-nest)
-     ((3) if-same (set x (integer? x)))
-     ((3 2 1) if-nest)
-     ((3 2) if-nest)
-     ((3 3 1) if-nest)
-     ((3 3) if-true)
-     ((3) if-same)
-     (() if-same)))
-
-  #;
-  (define-proof +
-    (natural? x)
-    ()
-    #;
-    (((2) if-nest)
-     ((2 3) less/pred)
-     ((2) if-same)
-     (() if-same)))
-  
-  ;; (define-proof if-implies
-  ;;   ()
-  ;;   (((1) if-same (set x x))
-  ;;    ((1 2 1) if-nest)
-  ;;    ((1 3 1) if-nest)
-  ;;    ((1 3) if-true)
-
-  ;; (define-proof less-than/pred
-  ;;   (natural-induction x)
-  ;;   (((2 2) if-nest)
-  ;;    ((2 2) if-not)
-  ;;    ((2 2) if-nest)
-  ;;    ((2 3 2) if-nest)
-  ;;    ((2 3 2) if-nest)
-  ;;    ((2 3) if-implies)
-  ;;    ((2 3 2) if-implies)
-     
-  ;;    (() error)
-  ;;    (() error)))
-
-  ;; (define-proof less-than/pred-1
-  ;;   ()
-  ;;   (((2 2) if-same (set x (natural? (pred x))))
-  ;;    ((2 2 2) if-same (set x (not (zero? (pred x)))))
-  ;;    ((2 2 2) if-same (set x (not (zero? (pred x)))))
-  ;;    ;; ((2 2 3 1 1) zero?)
-  ;;    ;; ((2 2 3 1 1) if-nest)
-  ;;    ;; ((2 2 3 1) if-false)
-  ;;    ;; ((2 2 3 1) if-false)
-  ;;    ))
-  
-
-
-  ;; (define-theorem natural/add1 (x)
-  ;;     (implies (natural? x)
-  ;;              (equal? (natural? (add1 x)) #t)))
-
-  #;
-  (define-axiom natural/sub1 (x)
-  (if (natural? x)
-  (if (< '0 x)
-  (equal? (natural? (sub1 x)) '#t)
-  '#t)
-  '#t))
-
-  #;
-  (define-theorem less-than/sub1 (x)
-  (implies (natural? x)
-  (< '0 x)
-  (equal? (< (sub1 x) x) '#t)))
-
-  #;
-  (define-axiom add1/sub1 (x)
-  (if (natural? x)
-  (if (equal? '0 x)
-  '#t
-  (equal? (add1 (sub1 x)) x))
-  '#t))
-
-  #;
-  (define-built-in-function + (x y)
-  (if (natural? x)
-  (if (equal? '0 x)
-  y
-  (add1 (+ (sub1 x) y)))
-  'undefined))
-
-  #;
-  (define-axiom natural/size (x)
-  (equal? (natural? (size x))
-  '#t))
-
-  #;
-  (define-axiom size/car (x)
-  (if (pair? x)
-  (equal? (< (size (car x)) (size x))
-  '#t)
-  '#t))
-
-  #;
-  (define-axiom size/cdr (x)
-  (if (pair? x)
-  (equal? (< (size (cdr x)) (size x))
-  '#t)
-  '#t))
-  
-  #;
-  (define-proof +
-  (total/natural? x)
-  (((2) if-nest)
-  ((2 3) </sub1)
-  ((2) if-same)
-  (() if-same)))
-
-  #;
-  (define-theorem thm-1+1=2 ()
-  (equal? (+ 1 1) 2))
-
-  #;
-  (define-function natural-induction (n)
-  (if (natural? n)
-  (if (equal? '0 n)
-  '0
-  (add1 (natural-induction (sub1 n))))
-  'undefined))
-
-  #;
-  (define-proof natural-induction
-  (total/natural? n)
-  (((2) if-nest)
-  ((2 3) </sub1)
-  ((2) if-same)
-  (() if-same)))
-
-  #;
-  (define-theorem equal?/add1 (n)
-  (if (natural? n)
-  (equal? (equal? n (add1 n)) #f)
-  #t))
-
-  #;
-  (define-proof equal?/add1
-  (induction (natural-induction n))
-  (((2 2 2 1 1) equal-if)
-  ((2 2 2 1 2 1) equal-if)
-  ((2 2 2 1) equal?/01)
-  ((2 2 2) equal-same)
-  ((2 2) if-same)
-  ((2 3 1 1) natural?/sub1)
-  ((2 3 1) if-true)
-  ((2 3 2 2 1 1) add1/sub1)
-  ((2 3 2 2 1 2 1) add1/sub1)
-  ((2 3 2 2) if-same (set x (natural? (add1 (sub1 n)))))
-  ((2 3 2 2) if-same (set x (natural? (sub1 n))))
-  ((2 3 2 2 2 2 1) common-add1
-  ;; ルール探索のアルゴリズムにバグがある
-  (set x (sub1 n))
-  (set y (add1 (sub1 n))))
-  ((2 3 2 2 2 2 1) equal-if)
-  ((2 3 2 2 2 2) equal-same)
-  ((2 3 2 2 2 1) natural?/add1)
-  ((2 3 2 2 2) if-true)
-  ((2 3 2 2 1) natural?/sub1)
-  ((2 3 2 2) if-true)
-  ((2 3 2) if-same)
-  ((2 3) if-same)
-  ((2) if-same)
-  ((3) if-nest)
-  (() if-same)))
-
-  #;
-  (define-proof thm-1+1=2
-  ()
-  ((() if-same (set x (natural? '0)))
-  ((2 1) +)
-  ((2 1 2 2 1) equal-if)
-  ((2 1 2 3 1 1) sub1/add1)
-  ((2 1 2 3 1) +)
-  ((2 1 2 3 1 2 1) equal-same)
-  ((2 1 2 3 1 2) if-true)
-  ((2 1 2 3 1 1) natural?/0)
-  ((2 1 2 3 1) if-true)
-  ((2 1 2) if-same)
-  ((2 1 1) natural?/add1)
-  ((2 1) if-true)
-  ((2) equal-same)
-  ((1) natural?/0)
-  (() if-true)))
   )