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

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