unif_cont_fun [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%
%  Additions made by Ricky W. Butler    NASA Langley
%
%----------------------------------------------------------------------------
BEGIN

   ASSUMING
     IMPORTING deriv_domain_def

     connected_domain : ASSUMPTION connected?[T]

     not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING


  IMPORTING continuous_functions[T], convergence_sequences


  f, f1, f2 : VAR [T -> real]
  g : VAR [T -> nzreal]
  u : VAR real
  x, x0 : VAR T
  epsi, delta : VAR posreal

%%%  E : VAR { S : setof[real] | subset?(S, T_pred) }

  E : VAR setof[T] 

  uniformly_continuous?(f, E) : bool =
        FORALL (epsi: posreal): EXISTS (delta: posreal):
    FORALL (x,y: (E)): abs(x-y) < delta IMPLIES
                                   abs(f(x) - f(y)) < epsi

  P3: VAR [real,real,posnat -> bool]

  getem_scaf4: LEMMA (FORALL (n: posnat): EXISTS (x,y: real): P3(x,y,n))
           IMPLIES (EXISTS (XX,YY: [posnat -> real]): 
                    FORALL (k: posnat):  P3(XX(k),YY(k),k))

  a,b,c: VAR T
  unif_cont_interval: LEMMA a < b IMPLIES   
                        LET D = {xx:T | a <= xx AND xx <= b} IN
                           continuous_on?(f,D) IMPLIES
                              uniformly_continuous?(f,D)

END unif_cont_fun