%% natural numbers in unary notation, and some operations
natural_number(0).
natural_number(s(X)) :- natural_number(X).

le(0,X) :- natural_number(X).
le(s(X),s(Y)) :- le(X,Y).

lt(0,s(X)) :- natural_number(X).
lt(s(X),s(Y)) :- lt(X,Y).

ge(X,Y) :- le(Y,X).
gt(X,Y) :- lt(Y,X).

plus(0,X,X) :- natural_number(X).
plus(s(X),Y,s(Z)) :- plus(X,Y,Z).

diff(X,Y,Z) :- plus(Z,Y,X).

times(0,X,0) :- natural_number(X).
times(s(X),Y,Z) :- times(X,Y,W), plus(W,Y,Z).

to_int(0,0).
to_int(s(M),Np1) :- to_int(M,N), Np1 is N + 1.

to_natural(N,M) :- to_int(M,N).


% A list is either [], or of the form [Head|Tail], where Tail is a list
list([]).
list([Head|Tail]) :- list(Tail).

% X is a member of a list of the form [Y|Zs] either if Y = X
% or if X is a member of Zs.  The cases are handled by unification.
% Note that the failure of member(X, []) is handled by Prolog's closed world
% assumption.
member(X, [X|Xs]).
member(X, [Y|Ys]) :- member(X,Ys).
% an alternative translation would be...
member2(X, [Y|Zs]) :- X = Y.
member2(X, [Y|Zs]) :- not(X = Y), member2(X,Zs).

% The append of lists Xs and Ys is defined by induction on the structure of Xs:
% basis: if Xs is null, the result is Ys
append([],Ys,Ys).
% induction: if Xs has the form [X|Xs'], then the result is [X|Zs],
% where Zs is append(Xs',Ys,Zs).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

% Using append, we can do member solely using Prolog's backtracking.
% The idea is that X is a member of a list L if L can be written as
% L1 concatenated with [X] concatenated with L2.  This may seem tricky,
% but it's just based on that definition.
member3(X,L) :- append(L1,[X|L2],L).

% Prolog's built-in notation for lists isn't special...
lisp_list(nil).
lisp_list(cons(Head,Tail)) :- lisp_list(Tail).

% Here's another inductive definition
to_list(nil,[]).
to_list(cons(Head,Tail),[Head|PL]) :- to_list(Tail,PL).

% The reverse of a list L is defined by induction on the structure of L:
% basis: reverse of [] is []
reverse([],[]).
% induction: if L has the form [H|T], its reverse is the reverse of T
% concatenated with [H].
reverse([Head|Tail], L) :- reverse(Tail,M), append(M,[Head],L).


% association lists are mappings from keys to values
alist([]).
alist([[Key,Value]|Tail]) :- alist(Tail).

% lookup is like LISP assoc; it returns the value, if any, for a key in
% an alist.  There is a value if the key is a member of some Key-Value pair
% in the alist.
lookup(Key,Alist,Value) :- member([Key,Value],Alist).

% using a fact as a "global variable"
capitols([[chile, santiago],
	  [peru, lima]]).
% ?- capitols(C), lookup(peru,C,Capitol).


% A difference list is a term of the form L-Z, where L is a list whose last
% element is the logical variable Z.
difference_list(X - X).
difference_list([X|Y] - Z) :- difference_list(Y - Z).

% There is nothing special about the minus sign (-), Prolog doesn't understand
% it either...  We could define difference lists as follows.
diff_list(diff(X,X)).
diff_list(diff([X|Y],Z)) :- diff_list(diff(Y,Z)).

% The following funciton transforms a difference list into a regular list,
% and vice versa.  It is defined by induction on the structure of each.
% (You can't use this to solve the difference list problems on your homework.)
simplify(X - X, []).
simplify([X|Y] - Z, [X|W]) :- simplify(Y - Z, W).


% Appending difference lists works is adding in arithmetic:
%	(X-Y) + (Y-Z) = X-Z
% This makes sense when you think about what a difference list "means"
diffappend(X-Y, Y-Z, X-Z).