/*======================================================================
  File			:  mar_farmer.P
  Author(s)		:  Mauricio Ayala Rincon
  Modified by		:  
  Last modification	:  Oct. 08 1997
========================================================================*/

/************************************************************************/
% This program specifies verification of polynomials and derivation 
/************************************************************************/

natural_number(0).
natural_number(s(X)) :- natural_number(X).

constant(X) :- atomic(X).

pol(X,X).
pol(T,X) :- constant(T).
pol(T+S,X) :- pol(T,X), pol(S,X).
pol(T-S,X) :- pol(T,X), pol(S,X).
pol(T*S,X) :- pol(T,X), pol(S,X).
pol(T/S,X) :- pol(T,X), pol(S,X).
pol(T^N,X) :- pol(T,X), natural_number(N).


% simple derivation:

der(T,X,0) :- constant(T).
der(X,X,s(0)).
der(sin(X),X,cos(X)).
der(cos(X),X,-sin(X)).
der(X^s(N),X,s(N)*X^N).
der(e^X,X,e^X).
der(log(X),X,1/X).
der(F+G,X,DF+DG) :- der(F,X,DF), der(G,X,DG).
der(F-G,X,DF-DG) :- der(F,X,DF), der(G,X,DG).
der(F*G,X,F*DG+G*DF) :- der(F,X,DF), der(G,X,DG).
der(1/F,X,-DF/(F*F)) :- der(F,X,DF).
der(G/F,X,(F*DG-G*DF)/(F*F)) :- der(F,X,DF), der(G,X,DG).

% chain rule for composition of functions:

der(sin(U),X,cos(U)*DU) :- der(U,X,DU).
der(cos(U),X,-sin(U)*DU) :- der(U,X,DU).
der(U^s(N),X,s(N)*U^N*DU) :- der(U,X,DU).
der(e^U,X,e^U*DU) :- der(U,X,DU).
der(log(U),X,1/U*DU) :- der(U,X,DU).