% -*- prolog -*-

%%% Integers

%%% non-negative integers: {\cal N}

%%% use terms to represent elements of N, the "natural numbers."
%%% z for zero, s(X) for the successor of X, ie X+1.

%%% so the number five is: s(s(s(s(s(z)))))

%%% sum(X, Y, Z), means sum of X and Y is Z.

sum(z, X, X).				% (x+1)+y=z+1 <- x+y=z
sum(s(X), Y, s(Z)) :- sum(X, Y, Z).	% or x+y=z -> (x+1)+y=z+1

%%% prod(X, Y, Z) means X*Y=Z

%prod(_, z, z).
prod(z, _, z).

%prod(X, s(Y), ZpX) :- sum(Z, X, ZpX), prod(X, Y, Z).
prod(s(X), Y, ZpY) :- sum(Z, Y, ZpY), prod(X, Y, Z).

%%% x*y=z -> (x+1)*y=z+y
%%% x*y=z -> (x+1)*(y+1)=z+x+y+1

sum4(A, B, C, D, ABCD) :- sum(ABC, D, ABCD), sum(AB, C, ABC), sum(A, B, AB).

%%% sumlist(Xs, Y) means Xs is a list, the sum of whose elements is Y.

sumlist([], z).
sumlist([X|Xs], XpXs) :- sumlist(Xs, Xs_sum), sum(X, Xs_sum, XpXs).

prod(s(X), s(Y), ZZ) :- sum4(Z, X, Y, s(z), ZZ), prod(X, Y, Z).

%%% geq(X, Y) means X is greater than or equal to Y.

geq(X, X).
geq(s(X), Y) :- geq(X, Y).



%%% GOAL: define PRIME NUMBERS

%%% plus_one_is(X,Y) means Y is equal to X+1.

% plus_one_is(X,s(X)).
%% alternative definition:
% plus_one_is(X, Y) :- sum(X, s(z), Y).

%%% even(X) means X is even
%%% odd(X) means X is odd

even(z).
even(s(X)) :- odd(X).
odd(s(X)) :- even(X).

% geq(X, X).
% geq(X, z).
% %%% geq(X, Y) :- sum(Xm, s(z), X), sum(Ym, s(z), Y), geq(Xm, Ym).
% geq(s(X), s(Y)) :- geq(X, Y).

%%% What facts about numbers BIGGER than x,y,z are implied by x*y=z ?
%%% x*y=z implies x*(y+1)=z+x.
% prod(X, s(z), X).
% prod(X, s(s(z)), Y) :- sum(X, X, Y).