derivatives [ T : TYPE FROM real ] : THEORY BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) not_one_element : ASSUMPTION FORALL (x : T) : EXISTS (y : T) : x /= y ENDASSUMING IMPORTING limit_of_functions, continuous_functions f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] x : VAR T u : VAR nzreal b : VAR real l, l1, l2 : VAR real %------------------- % Newton Quotient %------------------- A(x) : setof[nzreal] = { u | T_pred(x + u) } NQ(f, x)(h : (A(x))) : real = (f(x + h) - f(x)) / h deriv_TCC : LEMMA FORALL x : adh[(A(x))](fullset[real])(0) %---------------------------- % Differentiable functions %---------------------------- derivable(f, x) : bool = convergent(NQ(f, x), 0) derivable(f) : bool = FORALL x : derivable(f, x) %-------------------------------------- % Derivable functions are continuous %-------------------------------------- continuous_lim : LEMMA convergence(LAMBDA (h : (A(x))) : f(x + h), 0, f(x)) IFF continuous(f, x) deriv_continuous : LEMMA convergence(NQ(f, x), 0, l) IMPLIES continuous(f, x) derivable_continuous : PROPOSITION derivable(f, x) IMPLIES continuous(f, x) derivable_continuous2 : PROPOSITION derivable(f) IMPLIES continuous(f) %--------------------- % Properties of NQ %--------------------- sum_NQ : LEMMA NQ(f1 + f2, x) = NQ(f1, x) + NQ(f2, x) opposite_NQ : LEMMA NQ(- f, x) = - NQ(f, x) diff_NQ : LEMMA NQ(f1 - f2, x) = NQ(f1, x) - NQ(f2, x) scal_NQ : LEMMA NQ(b * f, x) = b * NQ(f, x) const_NQ : LEMMA NQ(b, x) = 0 identity_NQ : LEMMA NQ(I[T], x) = 1 prod_NQ : LEMMA FORALL (h : (A(x))): NQ(f1 * f2, x)(h) = NQ(f1, x)(h) * f2(x) + NQ(f2, x)(h) * f1(x + h) limit_prod_NQ : LEMMA convergence(NQ(f1, x), 0, l1) AND convergence(NQ(f2, x), 0, l2) IMPLIES convergence(NQ(f1 * f2, x), 0, f2(x) * l1 + f1(x) * l2) inv_NQ : LEMMA FORALL (h : (A(x))) : NQ(1/g, x)(h) = - NQ(g, x)(h) / (g(x) * g(x + h)) limit_inv_NQ : LEMMA convergence(NQ(g, x), 0, l1) IMPLIES convergence(NQ(1/g, x), 0, - l1 / (g(x) * g(x))) %--------------------------------------- % Operations preserving derivability %--------------------------------------- sum_derivable : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES derivable(f1 + f2, x) opposite_derivable : LEMMA derivable(f, x) IMPLIES derivable(- f, x) diff_derivable : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES derivable(f1 - f2, x) prod_derivable : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES derivable(f1 * f2, x) scal_derivable : LEMMA derivable(f, x) IMPLIES derivable(b * f, x) const_derivable : LEMMA derivable(b, x) inv_derivable : LEMMA derivable(g, x) IMPLIES derivable(1/g, x) div_derivable : LEMMA derivable(f, x) AND derivable(g, x) IMPLIES derivable(f / g, x) identity_derivable : LEMMA derivable(I, x) sum_derivable2 : LEMMA derivable(f1) AND derivable(f2) IMPLIES derivable(f1 + f2) opposite_derivable2 : LEMMA derivable(f) IMPLIES derivable(- f) diff_derivable2 : LEMMA derivable(f1) AND derivable(f2) IMPLIES derivable(f1 - f2) prod_derivable2 : LEMMA derivable(f1) AND derivable(f2) IMPLIES derivable(f1 * f2) scal_derivable2 : LEMMA derivable(f) IMPLIES derivable(b * f) const_derivable2 : LEMMA derivable(b) inv_derivable2 : LEMMA derivable(g) IMPLIES derivable(1/g) div_derivable2 : LEMMA derivable(f) AND derivable(g) IMPLIES derivable(f / g) identity_derivable2 : LEMMA derivable(I) %-------------- % Derivative %-------------- deriv(f, (x0 : { x | derivable(f, x) })) : real = lim(NQ(f, x0), 0) deriv_sum : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES deriv(f1 + f2, x) = deriv(f1, x) + deriv(f2, x) deriv_opposite : LEMMA derivable(f, x) IMPLIES deriv(- f, x) = - deriv(f, x) deriv_diff : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES deriv(f1 - f2, x) = deriv(f1, x) - deriv(f2, x) deriv_prod : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES deriv(f1 * f2, x) = deriv(f1, x) * f2(x) + deriv(f2, x) * f1(x) deriv_const : LEMMA deriv(b, x) = 0 deriv_scal : LEMMA derivable(f, x) IMPLIES deriv(b * f, x) = b * deriv(f, x) deriv_inv : LEMMA derivable(g, x) IMPLIES deriv(1/g, x) = - deriv(g, x) / (g(x) * g(x)) deriv_div : LEMMA derivable(f, x) AND derivable(g, x) IMPLIES deriv(f / g, x) = (deriv(f, x) * g(x) - deriv(g, x) * f(x)) / (g(x) * g(x)) deriv_identity : LEMMA deriv(I[T], x) = 1 %----------------------------------- % Type of derivable functions %----------------------------------- deriv_fun : TYPE = { f | derivable(f) } nz_deriv_fun : TYPE = { g | derivable(g) } ff, ff1, ff2 : VAR deriv_fun gg : VAR nz_deriv_fun derivable_cont: JUDGEMENT deriv_fun SUBTYPE_OF continuous_fun[T] nz_derivable_cont: JUDGEMENT nz_deriv_fun SUBTYPE_OF nz_continuous_fun[T] derivable_sum: JUDGEMENT +(ff1, ff2) HAS_TYPE deriv_fun derivable_diff: JUDGEMENT -(ff1, ff2) HAS_TYPE deriv_fun derivable_prod: JUDGEMENT *(ff1, ff2) HAS_TYPE deriv_fun derivable_scal: JUDGEMENT *(b, ff) HAS_TYPE deriv_fun derivable_opp: JUDGEMENT -(ff) HAS_TYPE deriv_fun derivable_div: JUDGEMENT /(ff, gg) HAS_TYPE deriv_fun derivable_inv: JUDGEMENT /(b, gg) HAS_TYPE deriv_fun derivable_const: JUDGEMENT K_conversion(b) HAS_TYPE deriv_fun derivable_id: JUDGEMENT I[T] HAS_TYPE deriv_fun %------------------------ % Derivative function %------------------------ deriv(ff) : [T -> real] = LAMBDA x : deriv(ff, x) deriv_sum_fun : LEMMA deriv(ff1 + ff2) = deriv(ff1) + deriv(ff2) deriv_opp_fun : LEMMA deriv(- ff) = - deriv(ff) deriv_diff_fun : LEMMA deriv(ff1 - ff2) = deriv(ff1) - deriv(ff2) deriv_prod_fun : LEMMA deriv(ff1 * ff2) = deriv(ff1) * ff2 + deriv(ff2) * ff1 deriv_scal_fun : LEMMA deriv(b * ff) = b * deriv(ff) deriv_inv_fun : LEMMA deriv(1 / gg) = - deriv(gg) / (gg * gg) deriv_scaldiv_fun : LEMMA deriv(b / gg) = - (b * deriv(gg)) / (gg * gg) deriv_div_fun : LEMMA deriv(ff / gg) = (deriv(ff) * gg - deriv(gg) * ff) / (gg * gg) deriv_const_fun : LEMMA deriv(b) = K_conversion(0) deriv_id_fun : LEMMA deriv(I) = K_conversion(1) % ------------------ following added by Rick Butler --------------------- n: VAR nat ^(f,n): [T -> real] = (LAMBDA (t:T): f(t)^n) deriv_exp_fun: LEMMA derivable(f) AND n > 0 IMPLIES derivable(f^n) AND deriv(f^n) = n*f^(n-1)*deriv(f) END derivatives