piecewise_continuous[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Piecewise Continuity
%
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING fundamental_theorem[T],%continuity_interval,
         indefinite_integral[T],
      reals@sigma_nat

   a,b,c,x: VAR T
   f,F,G: VAR [T -> real]
   N: VAR posnat

   % continuous on a closed interval

   piecewise_continuous?(N,(P:[upto(N)->T]),H:[below(N)->[T->real]]): bool =
     strict_increasing?(P) AND
     FORALL (i:below(N)): continuous_on?(H(i),closed_intv(P(i),P(i+1)))

   piecewise_continuous?(f,a,b,N,(P:[upto(N)->T]),
                               H:[below(N)->[T->real]]): bool =
       piecewise_continuous?(N,P,H) AND
       P(0)=a AND P(N)=b AND
       FORALL (i:below(N)): FORALL (x):
         P(i)<x AND x<P(i+1) IMPLIES f(x)=H(i)(x)

   piecewise_continuous?(f,a,b): bool =
     EXISTS (N,(P:[upto(N)->T]),H:[below(N)->[T->real]]):
       piecewise_continuous?(f,a,b,N,P,H)

   % Integration

   continuous_on_integrable: AXIOM a < b AND 
     continuous_on?(f,closed_intv(a,b))
                            IMPLIES Integrable?(a,b,f)

   piecewise_continuous_integrable: AXIOM
     a<b AND
     piecewise_continuous?(f,a,b) IMPLIES
     Integrable?(a,b,f)

   piecewise_continuous_integral: AXIOM
     FORALL (N,(P:[upto(N)->T]),H:[below(N)->[T->real]],i:nat):
       i<N AND
       a<b AND piecewise_continuous?(f,a,b,N,P,H) AND
       P(i)<=x AND x<=P(i+1)
       IMPLIES
       Integrable?(a,x,f) AND
       Integral(a,x,f) = sigma(0,i-1,LAMBDA (k:nat): IF k<N THEN Integral(P(k),P(k+1),H(k)) ELSE 0 ENDIF) +
                Integral(P(i),x,H(i))
       


   % fundamental3_piecewise: THEOREM 
   %   FORALL (N,(P:[upto(N)->T]),H:[below(N)->[T->real]]):
   %     a<b AND piecewise_continuous?(F,a,b,N,H) AND
   %     (FORALL (i:upto(N),x:closed_interval(P(i),P(i+1))): 
   %     derivable?(H(i),x) AND (P(i)<x AND x<P(i+1) 
   %       IMPLIES deriv(H(i),x)=f(x)))
      

END piecewise_continuous