MSBProp.v

Require Import Arith.
Require Export Float.
Require Export Fop.
Require Export Fnorm.
Require Export MSB.
Section MSBProp.
Variable b:Fbound.
Variable precision:nat.
Variable radix:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Theorem normal1:
  (a:float) (Fnormal radix b precision a) ->
  (Rle (Float (1) (MSB radix a)) (Rabsolu a)).

Theorem bounded1:
  (a:float) (Fbounded b a) ->
  (Rlt (Rabsolu a) (Float (1) (Zplus precision (Fexp a)))).

Theorem normal2:
  (x, y:float) (Fnormal radix b precision x) -> (Fbounded b y) ->
  (Rlt
     (Rmult (Rabsolu y) (Float (1) (Fexp x)))
     (Rmult radix (Rmult (Rabsolu x) (Float (1) (Fexp y))))).
End MSBProp.

30/05/01, 18:20