%% interval_lnexp.pvs

interval_lnexp : THEORY
BEGIN
  IMPORTING lnexp_fnd@exp_approx,
            lnexp_fnd@ln_approx,
            interval

  X,Y : VAR Interval
  x   : VAR real
  n   : VAR nat

  Exp(n)(X) : (Pos?) =
   [|exp_lb(lb(X),n),exp_ub(ub(X),n)|]

  Exp_fundamental: LEMMA
   X << Y IMPLIES
   Exp(n)(X) << Exp(n)(Y)

  Ln(n)(X) : Interval = 
    if lb(X) > 0 AND ub(X) > 0 then
      [|ln_lb(lb(X),n),ln_ub(ub(X),n)|]
    else 
      EmptyInterval
    endif 

  % lemmas

  Ln_fundamental: LEMMA
    Pos?(Y) AND Proper?(X) AND
    X << Y IMPLIES
    Ln(n)(X) << Ln(n)(Y)

  Exp_inclusion : LEMMA
    x ## X IMPLIES
    exp(x) ## Exp(n)(X)

  % En
  En(n) : (Pos?) = Exp(n)([|1|])

  Ln_inclusion : LEMMA
    Pos?(X) AND
    x ## X IMPLIES
    ln(x) ## Ln(n)(X)

  %% Safe version of ln and exp
  IMPORTING safe_arith

  safe_Ln(n) : [Interval->Interval] = Safe1(Ln(n))
  safe_Exp(n) : [Interval->Interval] = Safe1(Exp(n))

  %% Proper version of ln and exp
  IMPORTING proper_arith

  Xp   : VAR ProperInterval
  XP   : VAR PosInterval

  Proper_Ln : JUDGEMENT
    Ln(n)(XP) HAS_TYPE ProperInterval

  Proper_Exp : JUDGEMENT
    Exp(n)(Xp) HAS_TYPE ProperInterval

  proper_Ln(n)(XP) : ProperInterval = Ln(n)(XP)

  proper_Exp(n)(Xp) : PosInterval = Exp(n)(Xp)

END interval_lnexp