step_fun_props[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Theory and proofs taken from Introduction to Analysis (Maxwell Rosenlicht)
%
%  Author:  Rick Butler               NASA Langley
%------------------------------------------------------------------------------
BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

%   AUTO_REWRITE+ not_one_element


%   <=(x,y:T): bool = x <= y   %% hide ugly restrictions

%   AUTO_REWRITE+ <=

   IMPORTING step_fun_def[T],  % integral_step, 
             reals@sigma_below, 
             structures@sort_seq_lems[T,<=],
             step_fun_scaf[T]

   a,b,c,d,x,y,z,xl,xh: VAR T

   f,f1,f2,g: VAR [T -> real]

   eps, delta: VAR posreal

   xv,yv,cc: VAR real



   is_step: LEMMA a < b AND
                  (EXISTS (P: partition[T](a,b)):     %% PROVED %%
                    Let N = length(P), xx = seq(P) IN
                    (FORALL (ii: below(N-1)): (EXISTS (fv: real):
                           (FORALL x: xx(ii) < x AND x < xx(ii+1) IMPLIES
                                      f(x) = fv))))
              IMPLIES
                step_function?(a,b,f) 


   UUPart(a:T, b:{x:T|a<x}, c: {x:T|b<x}, P1: partition[T](a,b), 
             P2: partition[T](b, c)):  partition[T](a,c) =
               LET  N1 = length(P1), 
                    NUU = length(P1) + length(P2) - 1 IN
               (# length := NUU,
                  seq :=  (LAMBDA (kk: below(NUU)):
                            IF kk < N1 THEN P1`seq(kk)
                            ELSE P2`seq(kk-N1+1) 
                            ENDIF)
               #)

   split_step_is_step: LEMMA a < b AND b < c AND       %% PROVED %%
                            step_function?(a, b, f) AND
                            step_function?(b, c, g)
                         IMPLIES
                           step_function?(a, c,
                             (LAMBDA (x: T):
                                IF x < a OR x > c THEN 0
                                ELSIF x <= b THEN f(x)
                                ELSE g(x)
                                ENDIF))

%    UnionPart(a:T,b:{x:T|a<x},P1,P2: partition[T](a,b)): partition[T](a,b) =
%             set2part(union(part2set(a, b, P1), part2set(a, b, P2)))



   ssis_prep: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b),
                            nn: below(length(UnionPart(a,b,P1,P2))-1), x,y: T):
                     (in_sect?(a,b,UnionPart(a,b,P1,P2),nn,x) AND
                      in_sect?(a,b,UnionPart(a,b,P1,P2),nn,y)     )
                        IMPLIES
      (EXISTS (ii: below(length(P1)-1)): in_sect?(a,b,P1,ii,x) AND 
                                         in_sect?(a,b,P1,ii,y))
  AND (EXISTS (jj: below(length(P2)-1)): in_sect?(a,b,P2,jj,x) AND 
                                         in_sect?(a,b,P2,jj,y))


   sum_step_is_step: LEMMA a < b AND                   %% PROVED %%
                           step_function?(a, b, f) AND
                           step_function?(a, b, g)
                         IMPLIES
                           step_function?(a, b, f + g)


   diff_step_is_step: LEMMA a < b AND
                            step_function?(a, b, f) AND    %% PROVED %%
                            step_function?(a, b, g)
                         IMPLIES
                           step_function?(a, b, f - g)


   step_function_subrng: LEMMA a <= b AND b < c AND c <= d AND 
                               step_function?(a, d, f)
                               IMPLIES step_function?(b, c, f)


END step_fun_props