% -*- 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(+,+,-) OR prod(-,-,+),     ...maybe even.. prod(-,-,-)
%%% working: prod(+,+,-), prod(+,-,+), prod(-,+,+): one solution then ...

prod(z, _, z).
prod(s(X), Y, ZpY) :- prod(X, Y, Z), sum(Z, Y, ZpY).

%composite(Z) :- prod(X, Y, Z), geq(X, s(s(z))), geq(Y, s(s(z))).

%composite(Z) :-
%	geq(Z, s(s(s(X)))),
%	geq(Z, s(s(s(Y)))),
%	prod(s(s(X)), s(s(Y)), Z).

composite(Z) :- factors(_,_,Z).

factors(s(s(X)), s(s(Y)), Z) :-
	geq(Z, s(s(s(X)))),
	geq(Z, s(s(s(Y)))),
	prod(s(s(X)), s(s(Y)), Z).

%%% def: Signature of a Prolog relation
%%%  foo(+,+,-) means foo/3 is a relation between three things, the
%%% 		first two of which are "grounded", ie not uninstantiated
%%% 		variables.
%%% These queries would be okay:
%%%  ?- foo(3, 14, X).
%%%  ?- foo( bar(3,s(s(s(91,g)))), 14, X).
%%%  ?- foo( bar(3,s(s(s(91,g)))), 14, blaz(zonk,zonk,bork)).
%%%  ?- foo( bar(3,s(s(s(91,g)))), 14, blaz(_, zonk, _, X)).
%%% These queries would be ***NOT*** okay:
%%%  ?- foo(3, X, X).
%%%  ?- foo(3, _, 'icky bleck string').
%%%  ?- foo(3, bar(s(17,X)), 'icky bleck string').

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

%%% 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(z,_,z).
%prod(_,z,z).
%prod(s(X), s(Y), ZZ) :- sumlist([Z, X, Y, s(z)], ZZ), prod(X, Y, Z).

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

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).
