Quelle  interval_expr_lnexp.pvs

interval_expr_lnexp : THEORY
BEGIN

  IMPORTING interval_expr,
            interval_lnexp
  
  expr : VAR RealExpr
  n    : VAR nat

  ln_safe(x:real): real = IF x <= 0 THEN 0 ELSE ln(x) ENDIF

  Ln_Inclusion : JUDGEMENT
    Ln(n) HAS_TYPE (Inclusion?(Pos?,ln_safe))

  Ln_Fundamental : JUDGEMENT
    Ln(n) HAS_TYPE (Fundamental?(Pos?))

  LN_n(n:nat)(expr): MACRO RealExpr = FUN(Pos?,ln_safe,Ln(n),expr)

  exp_safe(x:real) : posreal  = exp(x)

  Exp_Inclusion : JUDGEMENT
    Exp(n) HAS_TYPE (Inclusion?(PreTrue,exp_safe))

  Exp_Fundamental : JUDGEMENT
    Exp(n) HAS_TYPE (Fundamental?(PreTrue))

  EXP_n(n:nat)(expr): MACRO RealExpr = FUN(PreTrue,exp_safe,Exp(n),expr)

  e_safe : [Unit->real] = LAMBDA(u:Unit) : e

  E_Inclusion : JUDGEMENT
    En(n) HAS_TYPE (Includes?(e_safe(unit)))

  E_n(n): MACRO RealExpr = CONST(e_safe,En(n))

END interval_expr_lnexp