SSL step_fun_def.pvs   Sprache: PVS

step_fun_def[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Integration over Step Functions: 
%
%  Author: Rick Butler   NASA Langley Research Center
%
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]

      not_one_element  : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   a,b,x,y,z,xx: VAR T
   c:      VAR real
   f,g:    VAR [T -> real]
   xl,xh:     VAR T

   IMPORTING integral_def[T]


   step_function_on?(a:T,b:{x:T|a<x},f:[T->real], P: partition[T](a,b)): bool =
                            Let N = length(P), xx = seq(P) IN
                    (FORALL (ii: below(N-1)): (EXISTS (fv: real):
                           (FORALL (x: open_interval[T](xx(ii),xx(ii+1))):
                                      f(x) = fv)))


%   step_function?(a:T,b:{x:T|a<x},f:[T -> real]): bool 
%                   = (EXISTS (P: partition(a,b)):
%                    Let N = length(P), xx = seq(P) IN
%                    (FORALL (ii: below(N-1)): (EXISTS (fv: real):
%                           (FORALL (x: open_interval(xx(ii),xx(ii+1))):
%                                      f(x) = fv))))


   step_function?(a:T,b:{x:T|a<x},f:[T -> real]): bool 
                   = (EXISTS (P: partition(a,b)): step_function_on?(a,b,f,P))

%  ALternate formulation without "fv":

   step_fun?(a:T,b:{x:T|a<x},f:[T -> real]): bool =
                    (EXISTS (P: partition(a,b)):
                    Let N = length(P), xx = seq(P) IN
                    (FORALL (ii: below(N-1)): 
                           (FORALL (x,y: open_interval(xx(ii),xx(ii+1))):
                                      f(x) = f(y))))


   step_fun?_lem: LEMMA a < b IMPLIES
                          (step_function?(a,b,f) IFF step_fun?(a,b,f))  




END step_fun_def