%%% The natural numbers in unary notation, and some operations
%%% These allow backtracking (except for to_int and to_nat).
%%% AUTHOR: Gary T. Leavens

module unary.







%%% ``le N1 N2'' succeeds if N1 is less than or equal to N2.
le z X.
le (s X) (s Y) :- le X Y.

%%% ``lt N1 N2'' succeeds if N1 is strictly less than N2.
lt z (s X).
lt (s X) (s Y) :- lt X Y.

%%% ``ge N1 N2'' succeeds if N1 is greater than or equal to N2.
ge X Y :- le Y X.
%%% ``gt N1 N2'' succeeds if N1 is strictly greater than N2.
gt X Y :- lt Y X.

%%% ``plus X Y Z'' succeeds when Z is the sum of X and Y.
plus z X X.
plus(s X) Y (s Z) :- plus X Y Z.

%%% ``diff X Y Z'' succeeds when Z is X - Y.
diff X Y Z :- plus Z Y X.

%%% ``times X Y Z'' succeeds when Z is the product of X and Y.
times z X z.
times (s X) Y Z :- (times X Y W), (plus W Y Z).

%%% ``to_int N I'' succeeds if N represents the integer I.
to_int z 0 :- !.
to_int (s M) Np1 :- (to_int M N),  (Np1 is N + 1).

%%% ``to_nat I N'' succeeds if N represents the integer I.
to_nat 0 z :- !.
to_nat M (s N) :- (Mm1 is M - 1), (to_nat Mm1 N).