Quellcode-Bibliothek interval.pvs Sprache: PVS

%% interval.pvs
interval : THEORY
BEGIN

%% Comparison and arithmetic interl operators defined in this theory assume, without checking,
%% that their operands are non-empty. Their correctness lemmas have as hypotheses that the operands
%% are "proper", e.g., non-empty. Proper and safe versions arithmetic operators are defined in
%% the theories proper_arith and safe_arith.
%%
%% Since version 6.0.5 of the NASA PVS Library, symbols <,<=,>,>=,+,-,*,/,^ are no longer used in
%% the interval arithmetic library. For convenience and backward compatibility the following theories
%% are provided:
%% - symbols_as_interval: Defines those symbols as the basic interval operators defined in this theory.
%% - symbols_as_proper: Defines those symbols as the interval operators defined in the theory proper_arith.
%% - symbols_as_safe: Defines those symbols as the interval operators defined in the theory safe_arith.
%% To avoid name clashes only one these 3 theories may be included in an imported chain.

  IMPORTING reals@sq,reals@sigma_nat,ints@div_nat

%%-------------------
%% Type and Notations
%%-------------------

  Interval : TYPE = [#
               lb : real,
               ub : real
             #]
  X,Y,Z : VAR Interval
  x,y   : VAR real
  n     : VAR nat
  i     : VAR int
  p     : VAR posnat
  f     : VAR [nat->real]
  F     : VAR [nat->Interval]

%%----------
%% Operators
%%----------

  ;##(x,X) : bool =
    lb(X) <= x AND x <= ub(X)

  % membership
  Member?(X)(x) : MACRO bool =
    x ## X

  CONVERSION Member?

  % Type of reals in interval X
  IntervalType(X) : TYPE = (Member?(X))

  % interval is non-empty
  Proper?(X:Interval) : bool =
    lb(X) <= ub(X)

  ProperInterval : TYPE = (Proper?)

  Member_Proper : LEMMA
    x ## X IMPLIES
    Proper?(X)

  Proper_Member : LEMMA
    Proper?(X) IMPLIES
    EXISTS (x): x ## X

  % interval has more than one element
  StrictInterval?(X:Interval) : bool =
    lb(X) < ub(X)

  StrictInterval : TYPE = (StrictInterval?)

  [||](x,y) : Interval  = (# lb := x, ub := y #)

  [||](x)   : Interval = (# lb := x, ub := x #)

  r2i_Proper : JUDGEMENT
    [||](x) HAS_TYPE ProperInterval

  EmptyInterval : Interval = [|1,0|]

  EmptyInterval?(X) :  bool =
    lb(X) > ub(X)

  Proper_eq_NonEmpty : LEMMA
    Proper?(X) IFF NOT EmptyInterval?(X)

  Proper_NonEmpty : LEMMA
    NOT Proper?(EmptyInterval)

  % inclusion
  ;<<(X,Y) : bool =
    lb(Y) <= lb(X) AND ub(X) <= ub(Y)

  eq_Incl : LEMMA
    X = Y IFF X << Y AND Y << X

  Incl_Member : LEMMA
    X << Y IMPLIES FORALL (x:real) : x ## X IMPLIES x ## Y

  Member_Incl : LEMMA
    Proper?(X) AND
    (FORALL (x:real) : x ## X IMPLIES x ## Y) IMPLIES
    X << Y

  Incl_Proper : LEMMA
    X << Y AND Proper?(X) IMPLIES
      Proper?(Y)

  % Type of subintervals included in interval X
  SubInterval(X) : TYPE = {Y | Y << X}

  % Type of proper subintervals included in interval X
  ProperIntervalOf(X) : TYPE = {Y:ProperInterval | Y << X}

  % Type of strictly proper subintervals included in interval X
  StrictIntervalOf(X) : TYPE = {Y:StrictInterval | Y << X}

  slice(X,p) :  real =
    ((p-1)*lb(X) + ub(X))/p

  % Midpoint of interval
  midpoint(X) : real =
    slice(X,2)

  midpoint_inclusion : LEMMA
    Proper?(X) IMPLIES
    midpoint(X) ## X

  % Interval size
  size(X) : real =
    ub(X) - lb(X)

  % Halves
  HalfLeft(X) : Interval =
    [| lb(X),midpoint(X) |]

  HalfRight(X) : Interval =
    [| midpoint(X),ub(X) |]

  % lt
  Lt(X,x) : bool =
    lb(X) < x AND ub(X) < x

  % le
  Le(X,x) : bool =
     lb(X) <= x AND ub(X) <= x

  % gt
  Gt(X,x) : bool =
     lb(X) > x AND ub(X) > x

  % ge
  Ge(X,x) : bool =
     lb(X) >= x AND ub(X) >= x

  Pos?(X) : bool  = Gt(X,0)

  Neg?(X) : bool  = Lt(X,0)

  NonNeg?(X) : bool = Ge(X,0)

  Lt_Ge : LEMMA
    Lt(X,x) AND Ge(X,x) IMPLIES
    EmptyInterval?(X)

  Le_Gt : LEMMA
    Le(X,x) AND Gt(X,x) IMPLIES
    EmptyInterval?(X)

  % 0 is in X
  Zeroin?(X) :  bool =
    lb(X) < 0 AND 0 < ub(X)

  % 0 is not in X
  Zeroless?(X) : bool =
    lb(X) > 0 OR ub(X) < 0

  Trichotomy : LEMMA
    Proper?(X) IMPLIES
      (Ge(X,0) OR Le(X,0) OR Zeroin?(X))

  % Addition
  Add(X,Y) : Interval =
    [|lb(X)+lb(Y),ub(X)+ub(Y)|]

  % Subtraction
  Sub(X,Y) : Interval =
    [|lb(X)-ub(Y),ub(X)-lb(Y)|]

  % Negation
  Neg(X): Interval =
    [|-ub(X),-lb(X)|]

  % Absolute value
  Abs(X) : (NonNeg?) =
    if Zeroin?(X) then
     [|0,max(abs(lb(X)),abs(ub(X)))|]
    else
     [|min(abs(lb(X)),abs(ub(X))),max(abs(lb(X)),abs(ub(X)))|]
    endif

  % pos * pos
  pXp(X,Y) : Interval =
    [|lb(X)*lb(Y),ub(X)*ub(Y)|]

  % neg * pos
  nXp(X,Y) : Interval =
    Neg(pXp(Neg(X),Y))

  % pos * neg
  pXn(X,Y) : Interval =
    nXp(Y,X)

  % neg * neg
  nXn(X,Y) : Interval =
    pXp(Neg(X),Neg(Y))

  % pos * med
  pXm(X,Y) : Interval =
    [|ub(X)*lb(Y),ub(X)*ub(Y)|]

  % med * pos
  mXp(X,Y) : Interval =
    pXm(Y,X)

  % neg * med
  nXm(X,Y) : Interval =
    Neg(pXm(Neg(X),Y))

  % med * neg
  mXn(X,Y) : Interval =
    nXm(Y,X)

  % med * med
  mXm(X,Y) : Interval =
    [|min(lb(X)*ub(Y),ub(X)*lb(Y)),
      max(lb(X)*lb(Y),ub(X)*ub(Y))|]

  % Multiplication
  Mult(X,Y) : Interval =
    IF    Ge(X,0) AND Ge(Y,0) THEN pXp(X,Y)
    ELSIF Ge(X,0) AND Le(Y,0) THEN pXn(X,Y)
    ELSIF Ge(X,0)             THEN pXm(X,Y)
    ELSIF Le(X,0) AND Le(Y,0) THEN nXn(X,Y)
    ELSIF Le(X,0) AND Ge(Y,0) THEN nXp(X,Y)
    ELSIF Le(X,0)             THEN nXm(X,Y)
    ELSIF Ge(Y,0)             THEN mXp(X,Y)
    ELSIF Le(Y,0)             THEN mXn(X,Y)
    ELSE                           mXm(X,Y)
    ENDIF

  % Square function
  Sq(X) : (NonNeg?) =
    IF    Ge(X,0) THEN [|sq(lb(X)),sq(ub(X))|]
    ELSIF Le(X,0) THEN [|sq(ub(X)),sq(lb(X))|]
    ELSE               [|0,max(sq(lb(X)),sq(ub(X)))|]
    ENDIF

  % Power by a natural number
  Pow(X,n) : Interval =
    IF    n = 0 THEN [|1|]
    ELSIF Ge(X,0) OR odd?(n) THEN [|lb(X)^n,ub(X)^n|]
    ELSIF Le(X,0) THEN [|ub(X)^n,lb(X)^n|]
    ELSE  [|0,max(lb(X)^n,ub(X)^n)|]
    ENDIF

  % Division
  Div(X,Y) : Interval =
    IF ub(Y) /= 0 AND lb(Y) /= 0 then Mult(X,[|1/ub(Y),1/lb(Y)|])
    ELSE EmptyInterval
    ENDIF

  % Union
  Union(X,Y) : Interval =
    [|min(lb(X),lb(Y)),max(ub(X),ub(Y))|]

  Intersection(X,Y): Interval =
    [|max(lb(X),lb(Y)),min(ub(X),ub(Y))|]

  Intersection_inclusion: LEMMA
    x ## Intersection(X,Y) IFF
    (x ## X AND x ## Y)

  Intersection_left_Empty : LEMMA
    EmptyInterval?(X) IMPLIES
    EmptyInterval?(Intersection(X,Y))

  Intersection_right_Empty : LEMMA
    EmptyInterval?(Y) IMPLIES
    EmptyInterval?(Intersection(X,Y))

%%---------------
%% Support Lemmas
%%---------------

  Add_comm : LEMMA
    Add(X,Y) = Add(Y,X)

  Mult_comm : LEMMA
    Mult(X,Y) = Mult(Y,X)

  Neg_Incl : LEMMA
     X << Y IMPLIES
    Neg(X) << Neg(Y)

  Zeroless0 : LEMMA
    x ## X AND
    Zeroless?(X) IMPLIES
    x /= 0

  Neg_Ge_0 : LEMMA
    Le(X,0) IMPLIES
    Ge(Neg(X),0)

  Strict_Lt : LEMMA
    x < y  AND
    x ## X AND
    y ## X IMPLIES
    StrictInterval?(X)

  Halves : LEMMA
    2*size(HalfLeft(X))  = size(X) AND
    2*size(HalfRight(X)) = size(X)

  Halves_Incl : LEMMA
    Proper?(X) IMPLIES
    (HalfLeft(X)  << X AND
     HalfRight(X) << X)

  Halves_inclusion : LEMMA
    x ## X IMPLIES
    x ## HalfLeft(X) OR x ## HalfRight(X)

  Incl_trans : LEMMA
    X << Y AND
    Y << Z IMPLIES
    X << Z

  Pow2_Sq : LEMMA
    Pow(X,2) = Sq(X)

  Mult_Neg_Neg : LEMMA
    Mult(X,Y) = Mult(Neg(X),Neg(Y))

  Mult_Neg_left : LEMMA
    Mult(X,Y) = Neg(Mult(Neg(X),Y))

  Mult_Neg_right : LEMMA
    Mult(X,Y) = Neg(Mult(X,Neg(Y)))

  Sq_Neg_eq : LEMMA
    Sq(X) = Sq(Neg(X))

  Union_id : LEMMA
    Union(X,X) = X

  Union_symm : LEMMA
    Union(X,Y) = Union(Y,X)

  Union_Incl_left : LEMMA
    X << Union(X,Y)

  Union_Incl_right : LEMMA
    X << Union(Y,X)

%%---------------
%% Rewrite Lemmas
%%---------------

  Add_0_r : LEMMA
    Add(X,[|0|]) = X

  Add_0_l : LEMMA
    Add([|0|],X) = X

  Mult_1_r : LEMMA
    Mult(X,[|1|]) = X

  Mult_1_l : LEMMA
    Mult([|1|],X) = X

  Div_1 : LEMMA
    Div(X,[|1|]) = X

  Pow_0 : LEMMA
    Pow(X,0) = [|1|]

  Pow_1 : LEMMA
    Pow(X,1) = X

  lb_interval : LEMMA
    lb([|x,y|]) = x

  lb_r2i : LEMMA
    lb([|x|]) = x

  ub_interval : LEMMA
    ub([|x,y|]) = y

  ub_r2i : LEMMA
    ub([|y|]) = y

  Incl_reflx : LEMMA
    X << X

  Incl_r2i : LEMMA
    ([|x|] << X) = (x ## X)

  Neg_Neg : LEMMA
    Neg(Neg(X)) = X

  AUTO_REWRITE+ Add_0_l,Add_0_r,Mult_1_l,Mult_1_r,Div_1,Pow_0,Pow_1,
         lb_interval,lb_r2i,ub_interval,ub_r2i,
         Incl_reflx, Incl_r2i,Neg_Neg

  ub_inclusion : LEMMA
    Proper?(X) IMPLIES
    ub(X) ## X

  lb_inclusion : LEMMA
    Proper?(X) IMPLIES
    lb(X) ## X

  Neg_interval : LEMMA
    Neg([|x,y|]) = [|-y,-x|]

  Pos_Gt_0 : LEMMA
    Pos?(X) IMPLIES
    Gt(X,0)

  NonNeg_Ge_0 : LEMMA
    NonNeg?(X) IMPLIES
    Ge(X,0)

  Pos_Neg_Lt_0 : LEMMA
     Pos?(X) IMPLIES
     Lt(Neg(X),0)

  NonNeg_Neg_Le_0 : LEMMA
    NonNeg?(X) IMPLIES
    Le(Neg(X),0)

  r2i_sharp_eq : LEMMA
    x ## [| y |] IFF x = y

  r2i_Le : LEMMA
    x <= y IMPLIES
    Le([|x|],y)

  r2i_Lt : LEMMA
    x < y IMPLIES
    Lt([|x|],y)

  r2i_Ge : LEMMA
    x >= y IMPLIES
    Ge([|x|],y)

  r2i_Gt : LEMMA
    x > y IMPLIES
    Gt([|x|],y)

  Lt_Le : LEMMA
    Lt(X,x) IMPLIES
    Le(X,x)

  Gt_Ge : LEMMA
    Gt(X,x) IMPLIES
    Ge(X,x)

%%-----------------
%% Inclusion Lemmas
%%-----------------

  inclusion_Gt : LEMMA
    x ## X AND
    Gt(X,y) IMPLIES
    x > y

  inclusion_Ge : LEMMA
    x ## X AND
    Ge(X,y) IMPLIES
    x >= y

  inclusion_Lt : LEMMA
    x ## X AND
    Lt(X,y) IMPLIES
    x < y

  inclusion_Le : LEMMA
    x ## X AND
    Le(X,y) IMPLIES
    x <= y

  r2i_trans : LEMMA
     x ## X   AND
     X << Y IMPLIES
     [|x|] << Y

  add2sub : LEMMA
     y ## Y AND
     x+y ## Z IMPLIES
     x ## Sub(Z,Y)

  sub2add : LEMMA
     y ## Y AND
     x-y ## Z IMPLIES
     x ## Add(Z,Y)

  Member_trans : LEMMA
     x ## X AND
     X << Y IMPLIES
     x ## Y

  r2i_inclusion : LEMMA
    x ## [|x|]

  Add_inclusion : LEMMA
    x ## X AND y ## Y IMPLIES
    x+y ## Add(X,Y)

  Sub_inclusion : LEMMA
    x ## X AND y ## Y IMPLIES
    x-y ## Sub(X,Y)

  Neg_inclusion : LEMMA
    x ## X IMPLIES
    -x ## Neg(X)

  pXp : LEMMA
    Ge(X,0) AND Ge(Y,0) AND
    x ## X AND y ## Y IMPLIES
    x*y ## pXp(X,Y)

  nXp : LEMMA
    Le(X,0) AND Ge(Y,0) AND
    x ## X AND y ## Y IMPLIES
    x*y ## nXp(X,Y)

  pXn : LEMMA
    Ge(X,0) AND Le(Y,0) AND
    x ## X AND y ## Y IMPLIES
    x*y ## pXn(X,Y)

  nXn : LEMMA
    Le(X,0) AND Le(Y,0) AND
    x ## X AND y ## Y IMPLIES
    x*y ## nXn(X,Y)

  pXm : LEMMA
    Ge(X,0) AND Zeroin?(Y) AND
    x ## X AND y ## Y IMPLIES
    x*y ## pXm(X,Y)

  mXp : LEMMA
    Zeroin?(X) AND Ge(Y,0) AND
    x ## X AND y ## Y IMPLIES
    x*y ## mXp(X,Y)

  nXm : LEMMA
    Le(X,0) AND Zeroin?(Y) AND
    x ## X AND y ## Y IMPLIES
    x*y ## nXm(X,Y)

  mXn : LEMMA
    Zeroin?(X) AND Le(Y,0) AND
    x ## X AND y ## Y IMPLIES
    x*y ## mXn(X,Y)

  mXm : LEMMA
    Zeroin?(X) AND Zeroin?(Y) AND
    x ## X AND y ## Y IMPLIES
    x*y ## mXm(X,Y)

  Mult_inclusion : LEMMA
    x ## X AND
    y ## Y IMPLIES
    x*y ## Mult(X,Y)

  Abs_inclusion : LEMMA
    x ## X IMPLIES
    abs(x) ## Abs(X)

  abs_sharp_le : LEMMA
    abs(x) <= y IFF x ## [|-y,y|]

  abs_sharp_lt : LEMMA
    abs(x) < y IMPLIES x ## [|-y,y|]

  pow_0_0 : LEMMA
    0^p = 0

  pow_sq : LEMMA
    x^2 = sq(x)

  pow_neg_n_odd : LEMMA
    (-x)^(2*n+1) = -(x^(2*n+1))

  pow_neg_odd : LEMMA
    odd?(n) IMPLIES
    (-x)^n = -(x^n)

  pow_neg_n_even : LEMMA
    (-x)^(2*n) = x^(2*n)

  pow_neg_even : LEMMA
    even?(n) IMPLIES
    (-x)^n = x^n

  pow_pos : LEMMA
    x   >= 0 IMPLIES
    x^n >= 0

  pow_even_n_pos : LEMMA
    x^(2*n) >= 0

  pow_even_pos : LEMMA
    even?(n) IMPLIES
    x^n >= 0

  pow_odd_n_neg : LEMMA
    x         <= 0 IMPLIES
    x^(2*n+1) <= 0

  pow_odd_neg : LEMMA
    odd?(n) AND
    x <= 0 IMPLIES
    x^n <= 0

  pow_incr_pos : LEMMA
    x >= 0 AND
    x <= y AND
    (x > 0 OR n > 0) IMPLIES
    x^n <= y^n

  pow_incr_odd : LEMMA
     odd?(n) AND
     x <= y     IMPLIES
     x^n <= y^n

  pow_decr_even : LEMMA
     even?(n) AND
     x <= 0      AND
     x >= y      AND
    (x < 0 OR n > 0) IMPLIES
     x^n <= y^n

  Pow_Neg_even : LEMMA
    even?(n) AND
    Proper?(X) IMPLIES
    Pow(X,n) = Pow(Neg(X),n)

  Pow_inclusion : LEMMA
    x ## X IMPLIES
    x^n ## Pow(X,n)

  Sq_inclusion : LEMMA
    x ## X IMPLIES
    sq(x) ## Sq(X)

  Div_inclusion : LEMMA
    x ## X AND
    y ## Y AND
    Zeroless?(Y) IMPLIES
    x/y ## Div(X,Y)

  Union_inclusion : LEMMA
    x ## Y OR x ## Z IMPLIES x ## Union(Y,Z)

  Overlap?(X,Y) : bool =
    lb(X) ## Y OR
    lb(Y) ## X

  Reunion : LEMMA
    x ## Z AND
    Z << Union(X,Y) AND
    Overlap?(X,Y)
    IMPLIES
      x ## X OR x ## Y

  Sigma(n,i,F) : RECURSIVE Interval =
    IF n > i THEN [|0|]
    ELSE  Add(F(i),Sigma(n,i-1, F))
    ENDIF
    MEASURE (abs(i+1-n))

  Sigma_inclusion : LEMMA
    (FORALL (k:subrange(n,i)):f(k) ## F(k)) IMPLIES
    sigma(n,i,f) ## Sigma(n,i,F)

%%-----------------
%% Fundamental Lemmas
%%-----------------

  X1,Y1 : VAR Interval

  Add_fundamental : LEMMA
    X1 << X AND Y1 << Y IMPLIES
    Add(X1,Y1) << Add(X,Y)

  Sub_fundamental : LEMMA
    X1 << X AND Y1 << Y IMPLIES
    Sub(X1,Y1) << Sub(X,Y)

  Abs_fundamental : LEMMA
    Proper?(X) AND
    X << Y IMPLIES
    Abs(X) << Abs(Y)

  Neg_fundamental : LEMMA
    X << Y IMPLIES
    Neg(X) << Neg(Y)

  pXp_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Ge(X,0) AND Ge(Y,0) AND
    X1 << X AND Y1 << Y IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  pXpm_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Ge(X,0) AND Zeroin?(Y) AND
    X1 << X AND Y1 << Y AND Ge(Y1,0) IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  pXmm_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Ge(X,0) AND Zeroin?(Y) AND
    X1 << X AND Y1 << Y AND Zeroin?(Y1) IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  pX_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Ge(X,0) AND
    X1 << X AND Y1 << Y IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  nX_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Le(X,0) AND
    X1 << X AND Y1 << Y IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  pmXpm_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Zeroin?(X) AND Zeroin?(Y) AND
    X1 << X AND Y1 << Y AND Ge(X1,0) AND Ge(Y1,0) IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  pmXmm_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Zeroin?(X) AND Zeroin?(Y) AND
    X1 << X AND Y1 << Y AND Ge(X1,0) AND Zeroin?(Y1) IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  mmXmm_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Zeroin?(X) AND Zeroin?(Y) AND
    X1 << X AND Y1 << Y AND Zeroin?(X1) AND Zeroin?(Y1) IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  mX_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    Zeroin?(X) AND X1 << X AND Y1 << Y IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  Mult_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    X1 << X AND Y1 << Y IMPLIES
    Mult(X1,Y1) << Mult(X,Y)

  Sq_p_fundamental : LEMMA
    Proper?(X1) AND
    X1 << X AND Ge(X,0) IMPLIES
    Sq(X1) << Sq(X)

  Sq_pm_fundamental : LEMMA
    Proper?(X1) AND
    X1 << X AND Zeroin?(X) AND Ge(X1,0) IMPLIES
    Sq(X1) << Sq(X)

  Sq_fundamental : LEMMA
    Proper?(X1) AND
    X1 << X IMPLIES
    Sq(X1) << Sq(X)

  Div_fundamental : LEMMA
    Proper?(X1) AND Proper?(Y1) AND
    X1 << X AND Y1 << Y AND Zeroless?(Y) IMPLIES
    Div(X1,Y1) << Div(X,Y)

  Pow_p_fundamental : LEMMA
    Proper?(X1) AND
    X1 << X AND n > 0 AND (odd?(n) OR Ge(X,0)) IMPLIES
    Pow(X1,n) << Pow(X,n)

  Pow_pm_fundamental : LEMMA
    Proper?(X1) AND
    X1 << X AND n > 0 AND even?(n) AND Zeroin?(X) AND Ge(X1,0) IMPLIES
    Pow(X1,n) << Pow(X,n)

  Pow_m_fundamental : LEMMA
    Proper?(X1) AND
    X1 << X AND n > 0 AND even?(n) AND Zeroin?(X) IMPLIES
    Pow(X1,n) << Pow(X,n)

  Pow_fundamental : LEMMA
    Proper?(X1) AND
    X1 << X IMPLIES
    Pow(X1,n) << Pow(X,n)

  Union_fundamental : LEMMA
    X1 << X AND
    Y1 << Y IMPLIES
    Union(X1,Y1) << Union(X,Y)

  Includes?(x)(X:Interval) : bool = x ## X

  Inclusion?(Pre:PRED[Interval],f:[real->real])(F:[Interval->Interval]):bool =
    FORALL(x:real,X:(Pre)): x ## X IMPLIES f(x) ## F(X)

  Fundamental?(Pre:PRED[Interval])(F:[Interval->Interval]):bool =
    FORALL(X1:ProperInterval,X:(Pre)): X1 << X IMPLIES F(X1) << F(X)

  Precondition?(Pre:PRED[Interval]):bool =
    FORALL (X1:ProperInterval,X:Interval): X1 << X AND Pre(X) IMPLIES Pre(X1)

  Mult_Strict_r2i : LEMMA
      StrictInterval?(X) AND
      x /= 0 IMPLIES
      StrictInterval?(Mult([|x|],X))

  Mult_r2i_Strict : LEMMA
      StrictInterval?(X) AND
      x /= 0 IMPLIES
      StrictInterval?(Mult([|x|],X))

%%----------
%% Judgments
%%----------

  Pos_Zeroless   : JUDGEMENT (Pos?) SUBTYPE_OF (Zeroless?)

  Neg_Zeroless   : JUDGEMENT (Neg?) SUBTYPE_OF (Zeroless?)

  Pos_NonNeg     : JUDGEMENT (Pos?) SUBTYPE_OF (NonNeg?)

  Pos_Add_NonNeg : JUDGEMENT Add(X:(Pos?),Y:(NonNeg?)) HAS_TYPE (Pos?)

  NonNeg_Add_Pos : JUDGEMENT Add(X:(NonNeg?),Y:(Pos?)) HAS_TYPE (Pos?)

  Neg_Add        : JUDGEMENT Add(X,Y:(Neg?)) HAS_TYPE (Neg?)

  NonNeg_Add     : JUDGEMENT Add(X,Y:(NonNeg?)) HAS_TYPE (NonNeg?)

  Neg_Pos        : JUDGEMENT Neg(X:(Neg?)) HAS_TYPE (Pos?)

  Pos_Neg        : JUDGEMENT Neg(X:(Pos?)) HAS_TYPE (Neg?)

  Pos_Mult       : JUDGEMENT Mult(X,Y:(Pos?)) HAS_TYPE (Pos?)

  Neg_Mult       : JUDGEMENT Mult(X,Y:(Neg?)) HAS_TYPE (Pos?)

  NonNeg_Mult    : JUDGEMENT Mult(X,Y:(NonNeg?)) HAS_TYPE (NonNeg?)

  Pos_Div        : JUDGEMENT Div(X,Y:(Pos?)) HAS_TYPE (Pos?)

  Neg_Div        : JUDGEMENT Div(X,Y:(Neg?)) HAS_TYPE (Pos?)

  NonNeg_Div     : JUDGEMENT Div(X:(NonNeg?),Y:(Pos?)) HAS_TYPE (NonNeg?)

  r2i_Pos        : JUDGEMENT [||](x:posreal) HAS_TYPE (Pos?)

  r2i_Neg        : JUDGEMENT [||](x:negreal) HAS_TYPE (Neg?)

  r2i_Nneg       : JUDGEMENT [||](x:nnreal) HAS_TYPE (NonNeg?)

  Sq_Pos         : JUDGEMENT Sq(X:(Pos?)) HAS_TYPE (Pos?)

  Sq_Neg         : JUDGEMENT Sq(X:(Neg?)) HAS_TYPE (Pos?)

  Abs_Pos        : JUDGEMENT Abs(X:(Pos?)) HAS_TYPE (Pos?)

  Abs_Neg        : JUDGEMENT Abs(X:(Neg?)) HAS_TYPE (Pos?)

  Proper_midpoint: JUDGEMENT midpoint(X:ProperInterval) HAS_TYPE IntervalType(X)

  Includes_Proper : JUDGEMENT (Includes?(x)) SUBTYPE_OF ProperInterval

  Strict_Proper  : JUDGEMENT StrictInterval SUBTYPE_OF ProperInterval

  Strict_Add     : JUDGEMENT Add(X:StrictInterval,Y:ProperInterval)
                              HAS_TYPE StrictInterval

  Add_Strict     : JUDGEMENT Add(X:ProperInterval,Y:StrictInterval)
                              HAS_TYPE StrictInterval

  Proper_Add     : JUDGEMENT Add(X,Y:ProperInterval) HAS_TYPE ProperInterval

  Strict_Sub     : JUDGEMENT Sub(X:StrictInterval,Y:ProperInterval)
                              HAS_TYPE StrictInterval

  Sub_Strict     : JUDGEMENT Sub(X:ProperInterval,Y:StrictInterval)
                              HAS_TYPE StrictInterval

  Proper_Sub     : JUDGEMENT Sub(X,Y:ProperInterval) HAS_TYPE ProperInterval

  Strict_Neg     : JUDGEMENT Neg(X:StrictInterval)
                              HAS_TYPE StrictInterval

  Proper_Neg     : JUDGEMENT Neg(X:ProperInterval) HAS_TYPE ProperInterval

  Strict_Abs     : JUDGEMENT Abs(X:StrictInterval)
                             HAS_TYPE StrictInterval

  Proper_Abs     : JUDGEMENT Abs(X:ProperInterval) HAS_TYPE ProperInterval

  Proper_Mult    : JUDGEMENT Mult(X,Y:ProperInterval) HAS_TYPE ProperInterval

  Proper_Div     : JUDGEMENT Div(X:ProperInterval,(Y:ProperInterval|Zeroless?(Y))) HAS_TYPE ProperInterval

  Strict_Sq      : JUDGEMENT Sq(X:StrictInterval)
                             HAS_TYPE StrictInterval

  Proper_Pow     : JUDGEMENT Pow(X:ProperInterval,n:nat) HAS_TYPE ProperInterval

  Proper_Sq      : JUDGEMENT Sq(X:ProperInterval) HAS_TYPE ProperInterval

  Proper_size    : JUDGEMENT size(X:ProperInterval) HAS_TYPE nnreal

  Strict_size    : JUDGEMENT size(X:StrictInterval) HAS_TYPE posreal

  Proper_HalfLeft : JUDGEMENT HalfLeft(X:ProperInterval) HAS_TYPE ProperInterval

  Strict_HalfLeft : JUDGEMENT HalfLeft(X:StrictInterval) HAS_TYPE
                       StrictInterval

  Proper_HalfRight : JUDGEMENT HalfRight(X:ProperInterval) HAS_TYPE ProperInterval

  Strict_HalfRightt : JUDGEMENT HalfRight(X:StrictInterval) HAS_TYPE
                         StrictInterval

  Zeroless_Precondition : JUDGEMENT Zeroless? HAS_TYPE (Precondition?)

  NonNeg_Precondition : JUDGEMENT NonNeg? HAS_TYPE (Precondition?)

  Pos_Precondition : JUDGEMENT Pos? HAS_TYPE (Precondition?)

  Neg_Precondition : JUDGEMENT Neg? HAS_TYPE (Precondition?)

END interval

quality95%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.18Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.