diff options
| -rw-r--r-- | vikalpa.scm | 84 | ||||
| -rw-r--r-- | vikalpa/prelude.scm | 14 |
2 files changed, 62 insertions, 36 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 98a7d97..a2b4dd2 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -1040,7 +1040,8 @@ (syntax-rules () ((_ name (var ...) expr) (let ((t (axiom 'name '(var ...) - (convert-to-expression 'expr)))) + (make-theorem-claim (convert-to-expression 'expr) + (current-system))))) (add-definition t) (validate-definition t) t)))) @@ -1049,7 +1050,8 @@ (syntax-rules () ((_ name (var ...) expr) (let ((t (theorem 'name '(var ...) - (convert-to-expression 'expr)))) + (make-theorem-claim (convert-to-expression 'expr) + (current-system))))) (add-definition t) (validate-definition t) t)))) @@ -1170,14 +1172,15 @@ (fail 'cdr extracted-expr)))) ((integer?) (match extracted-expr - (('integer? `(quote ,x)) - (expr-quote (integer? x))) + (('natural? `(quote ,x)) + (expr-quote (natural? x))) (else - (fail 'integer? extracted-expr)))) + (fail 'natural? extracted-expr)))) ((succ) (match extracted-expr (('succ `(quote ,x)) - (if (integer? x) + (if (and (natural? x) + (< 0 x)) (expr-quote (succ x)) ''undefined)) (else @@ -1185,7 +1188,7 @@ ((pred) (match extracted-expr (('pred `(quote ,x)) - (if (integer? x) + (if (natural? x) (expr-quote (pred x)) ''undefined)) (else @@ -1193,7 +1196,7 @@ ((<) (match extracted-expr (('< `(quote ,x) `(quote ,y)) - (if (and (integer? x) (integer? y)) + (if (and (natural? x) (natural? y)) (expr-quote (< x y)) ''undefined)) (else @@ -1206,20 +1209,12 @@ (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 integer? (x)) - (define-core-function < (x y) - ;;(integer? x) (integer? y) - ) - (define-core-function succ (x) ;;(integer? x) - ) - (define-core-function pred (x) ;;(integer? x) - ) + (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 @@ -1371,6 +1366,51 @@ '#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?)) diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index c7ab89e..c61e459 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -102,11 +102,6 @@ (define-function zero? (x) (equal? 0 x)) - (define-function natural? (x) - (and (integer? x) - (or (zero? x) - (< 0 x)))) - (define-axiom pred/succ (x) (implies (natural? x) (equal? (pred (succ x)) x))) @@ -122,8 +117,6 @@ (equal? (< (pred x) x) #t))) (define-totality-claim natural? natural? <) - - (define-function + (x y) (natural? x) (natural? y) @@ -131,13 +124,6 @@ y (succ (+ (pred x) y)))) - (define-proof zero? - () - ()) - - (define-proof natural? - () - ()) (define-proof + (natural? x) ()) |