cont_if_fun[ T : TYPE FROM real] : THEORY
%------------------------------------------------------------------------------------
%
%    Continuity of a function defined using an IF-THEN-ELSE
%
%    G = IF <expr> THEN f1 ELSE f2 ENDIF
%
%    is continuous if f1 and f2 are continuous and they are equal at all of the
%    place where the <expr> is discontinuous.
%
%    Author: Rick Butler                     NASA Langley
%            Jan 22, 2009
%--------------------------------------------------------------------------------------
BEGIN

  ASSUMING

     connected_domain : ASSUMPTION
 FORALL (x, y : T), (z : real) :
     x <= z AND z <= y IMPLIES T_pred(z)

  ENDASSUMING

  IMPORTING continuous_functions[T]

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

  P : VAR [T -> bool]

  a, b, c, d, x : VAR T

  discont_pts(P): set[T] = {x:T | NOT continuous_at?(P,x)}

  discont_pts_lem: LEMMA NOT discont_pts(P)(a) IMPLIES
                            EXISTS (delta: posreal): 
                               (FORALL (x:T): abs(x-a) < delta IMPLIES P(x) = true) OR
                               (FORALL (x:T): abs(x-a) < delta IMPLIES P(x) = false)

  if_fun(P: [T-> bool], f1:[T -> real], f2:[T -> real]): [T -> real] = 
       (LAMBDA (x:T): IF P(x) THEN f1(x) ELSE f2(x) ENDIF)

  if_fun_cont: LEMMA continuous?(f1) AND continuous?(f2) AND
                     (FORALL (x:T): discont_pts(P)(x) IMPLIES f1(x) = f2(x))
                    IMPLIES
                     continuous?(if_fun(P,f1,f2))

  discont_pts_simple: LEMMA continuous?(f1) AND continuous?(f2) AND
    P = (LAMBDA (t: T): f1(t) > 0 AND f2(t) > 0) AND
    discont_pts(P)(x) 
    IMPLIES f1(x) = 0 OR f2(x) = 0

  prod_fun_lem: LEMMA continuous?(f1) AND continuous?(f2) AND
    P = (LAMBDA (t: T): f1(t) > 0 AND f2(t) > 0) AND
    discont_pts(P)(x)
    IMPLIES
       f1(x)*f2(x) = -abs(f1(x)*f2(x))
    


END cont_if_fun