integral_cont_scaf[T: TYPE FROM real]: THEORY
%----------------------------------------------------------------------------
% scaffolding: not intended for users
%----------------------------------------------------------------------------
BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING


   IMPORTING integral_prep[T], integral_step[T], interval_minmax[T],
             unif_cont_fun, continuity_interval

   f: VAR [T -> real]
   x,y,a,b: VAR T

   adh_lem: LEMMA a <= x AND x <= b
                     IMPLIES  adh[closed_interval(a, b)](fullset[real])(x)


   fun_cont_on(a:T,b:{x:T|a<x}): TYPE = {f | 
          (FORALL (x: closed_interval(a,b)):  
                   continuous?(restrict[T,closed_interval(a,b),real](f),x))}

   cont_restrict: LEMMA FORALL (x: closed_interval(a, b) ): 
                               continuous?(f, x)
                         IMPLIES
                    continuous?(restrict[T, closed_interval(a, b), real](f), x)
   
   cont_interv: LEMMA (FORALL (P: partition(a,b), xx: [below(length(P)) -> T]):
                       continuous?(restrict[T, closed_interval(a, b), real](f)) 
                         AND xx = seq(P) IMPLIES
                    (FORALL (ii : below(length(P)-1)): 
                       continuous?[closed_interval(xx(ii), xx(1 + ii))]
                  (restrict[T, closed_interval(xx(ii), xx(1 + ii)), real](f))))

%    The following is now in interval_minmax
%
%    min_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
%             {mx: T |  a <= mx AND mx <= b AND 
%                       (FORALL (x: T): a <= x AND x <= b IMPLIES
%                                       f(mx) <= f(x))}
%
%
%    max_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
%             {mx: T |  a <= mx AND mx <= b AND 
%                       (FORALL (x: T): a <= x AND x <= b IMPLIES
%                                       f(mx) >= f(x))}

   fmin_nonempty: LEMMA FORALL (P: partition(a,b), f: fun_cont_on(a,b)): 
                           nonempty?({fv: real |
                              FORALL (ii: below(length(P) - 1)):
                        (seq(P)(ii) < x AND x < seq(P)(1 + ii) IMPLIES
                        fv = f(min_x(seq(P)(ii), seq(P)(1 + ii), f)))
                        AND
                         ((seq(P)(ii) = x OR x = seq(P)(1 + ii)) IMPLIES
                            fv = f(x))})

   fmax_nonempty: LEMMA FORALL (P: partition(a,b), f: fun_cont_on(a,b)): 
                           nonempty?({fv: real |
                              FORALL (ii: below(length(P) - 1)):
                        (seq(P)(ii) < x AND x < seq(P)(1 + ii) IMPLIES
                        fv = f(max_x(seq(P)(ii), seq(P)(1 + ii), f)))
                        AND
                         ((seq(P)(ii) = x OR x = seq(P)(1 + ii)) IMPLIES
                            fv = f(x))})

   fmin(a:T,b:{x:T|a<x},P: partition(a,b), f: fun_cont_on(a,b)): 
         {ff: [T -> real] | LET xx = seq(P) IN
                  FORALL (ii : below(length(P)-1)): 
             FORALL (x: T):  (xx(ii) < x AND x < xx(ii+1) IMPLIES
                                ff(x) = f(min_x(xx(ii),xx(ii+1),f))) AND
                             ((xx(ii) = x OR x = xx(ii+1)) IMPLIES
                                ff(x) = f(x))} 

   fmax(a:T,b:{x:T|a<x},P: partition(a,b), f: fun_cont_on(a,b)): 
         {ff: [T -> real] | LET xx = seq(P) IN
                  FORALL (ii : below(length(P)-1)): 
               FORALL (x: T): (xx(ii) < x AND x < xx(ii+1) IMPLIES
                                 ff(x) = f(max_x(xx(ii),xx(ii+1),f))) AND
                              ((xx(ii) = x OR x = xx(ii+1)) IMPLIES
                                 ff(x) = f(x))} 



  fmax_step: LEMMA FORALL (PP: partition(a,b), f: fun_cont_on(a,b)): 
                      a < b IMPLIES step_function?(a, b, fmax(a, b, PP, f))

  fmin_step: LEMMA FORALL (PP: partition(a,b), f: fun_cont_on(a,b)): 
                      a < b IMPLIES step_function?(a, b, fmin(a, b, PP, f))

  fmax_ge  : LEMMA FORALL (PP: partition(a,b), f: fun_cont_on(a,b),
                           x: closed_interval(a,b)):
                          a < b IMPLIES 
                             fmax(a, b, PP, f)(x) - fmin(a, b, PP, f)(x) >= 0

END integral_cont_scaf