diff options
Diffstat (limited to 'vikalpa/prelude.scm')
| -rw-r--r-- | vikalpa/prelude.scm | 65 |
1 files changed, 49 insertions, 16 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 5b70a72..c7ab89e 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -51,16 +51,6 @@ ((implies x y z . rest) (if x (implies y z . rest) #t))) - (define-function zero? (x) - (equal? 0 x)) - - (define-function natural? (x) - (and (integer? x) - (or (zero? x) - (< 0 x)))) - - (define-totality-claim natural? natural? <) - (define-axiom equal-same (x) (equal? (equal? x x) '#t)) @@ -109,10 +99,19 @@ (implies (equal? (cons x1 y1) (cons x2 y2)) (equal? y1 y2))) + (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))) + (define-axiom succ/pred (x) (implies (natural? x) (not (zero? x)) @@ -121,16 +120,51 @@ (define-axiom less/pred (x) (implies (natural? x) (equal? (< (pred x) x) #t))) + + (define-totality-claim natural? natural? <) + (define-function + (x y) - (if (natural? x) - (if (zero? x) - y - (succ (+ (pred x) y))) - 'undeifned<+>)) + (natural? x) + (natural? y) + (if (zero? x) + y + (succ (+ (pred x) y)))) + + (define-proof zero? + () + ()) + + (define-proof natural? + () + ()) + (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) @@ -142,7 +176,6 @@ ;; ((1 2 1) if-nest) ;; ((1 3 1) if-nest) ;; ((1 3) if-true) - ;; (() equal-same))) ;; (define-proof less-than/pred ;; (natural-induction x) |