diff options
Diffstat (limited to 'vikalpa/prelude.scm')
| -rw-r--r-- | vikalpa/prelude.scm | 90 |
1 files changed, 52 insertions, 38 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 9fb7571..66d2b73 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -17,12 +17,7 @@ ;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. (define-module (vikalpa prelude) - #:export (exact-positive-integer? - exact-negative-integer? - succ pred - implies - negate - prelude) + #:export (prelude) #:use-module (vikalpa)) (define (exact-positive-integer? x) @@ -96,22 +91,28 @@ (equal? (if (not x) y z) (if x z y)))) -(define-system prelude/number (prelude/if) +(define-system prelude/integer (prelude/if) (define-core-function integer? (x) exact-integer?) (define-core-function positive-integer? (x) exact-positive-integer?) - (define-core-function negative-integer? (x) exact-negative-integer?) - (define-core-function negate (x) negate) - (define-function natural? (x) - (if (integer? x) - (not (negative-integer? x)) - #f)) (define-function zero? (x) (equal? x 0)) - (define-core-function succ (x) succ) - (define-core-function pred (x) pred) + (define-function natural? (x) + (if (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) @@ -126,7 +127,7 @@ #f)))) (set-measure-predicate natural?) (set-measure-less-than <) - (define-axiom integer?-is-predicate (x) + (define-axiom integer?/true (x) (implies (integer? x) (equal? (integer? x) #t))) (define-axiom integer/pred (x) @@ -144,7 +145,7 @@ (define-axiom natural/pred (x) (implies (positive-integer? x) (equal? (natural? (pred x)) #t))) - (define-axiom positive-integer/succ (x) + (define-axiom positive-integer/pred (x) (implies (natural? x) (equal? (positive-integer? (pred x)) #t))) (define-axiom positive-integer-is-integer (x) @@ -200,9 +201,7 @@ x) 0)) (define-theorem natural-is-integer (x) - (if (natural? x) - (equal? (integer? x) #t) - #t)) + (implies (natural? x) (equal? (integer? x) #t))) (define-theorem natural/abs (x) (equal? (natural? (abs x)) #t)) (define-theorem zero-is-0 (x) @@ -215,16 +214,16 @@ (implies (natural? x) (not (zero? x)) (equal? (positive-integer? x) #t))) - (define-theorem %abs/pred--zero/pred (x) + (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) + (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) + (define-theorem %%abs/pred-1 (x) (implies (positive-integer? x) (positive-integer? (pred x)) (equal? (< (pred x) x) #t))) @@ -242,6 +241,12 @@ 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)) @@ -249,7 +254,7 @@ (pred (+ (succ x) y)) y)))) -(define-system prelude/pair (prelude/number) +(define-system prelude/pair (prelude/integer) (define-core-function pair? (x) pair?) (define-core-function cons (x y) cons) (define-core-function car (x) @@ -333,26 +338,26 @@ ((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 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 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 + (define-proof %%abs/pred-1 (natural-induction x) (((2 2 1 1) zero-is-0) ((2 2 1) positive-integer?) @@ -379,8 +384,8 @@ ((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 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) @@ -391,7 +396,7 @@ ((3) if-false) (() if-same))) - (define-proof %abs/pred--x-is-1 + (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) @@ -401,7 +406,7 @@ ((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 1) %%abs/pred--zero/pred) ((2 2 2 2) if-true) ((2 2 2 1) natural-is-integer) ((2 2 2) if-true) @@ -410,7 +415,7 @@ ((2) if-same) (() if-same))) - (define-proof %abs/pred--zero/pred + (define-proof %%abs/pred--zero/pred (((2 2 1) natural?) ((2 2 1) if-nest) ((2 2 2) if-same (set x (zero? x))) @@ -480,6 +485,15 @@ ((2) if-same) (() if-same))) + (define-proof integer-induction + (abs x) + (((1) natural/abs) + (() if-true) + ((2) abs/pred) + ((3 2) abs/succ) + ((3) if-same) + (() if-same))) + (define-proof + (abs x) (((1) natural/abs) |