Theory "ieee"

Parents transc

Signature

Type	Arity
ccode	0
float	0
roundmode	0
Constant	Type
Eq	:ccode
Exponent	:ieee$float -> num
Finite	:ieee$float -> bool
Float	:real -> ieee$float
Fraction	:ieee$float -> num
Gt	:ccode
Infinity	:ieee$float -> bool
Isdenormal	:ieee$float -> bool
Isintegral	:ieee$float -> bool
Isnan	:ieee$float -> bool
Isnormal	:ieee$float -> bool
Iszero	:ieee$float -> bool
Lt	:ccode
Minus_infinity	:ieee$float
Minus_zero	:ieee$float
Plus_infinity	:ieee$float
Plus_zero	:ieee$float
ROUNDFLOAT	:ieee$float -> ieee$float
Sign	:ieee$float -> num
To_nearest	:roundmode
To_ninfinity	:roundmode
To_pinfinity	:roundmode
Ulp	:ieee$float -> real
Un	:ccode
Val	:ieee$float -> real
bias	:num # num -> num
bottomfloat	:num # num -> num # num # num
ccode2num	:ccode -> num
ccode_CASE	:ccode -> α -> α -> α -> α -> α
ccode_size	:ccode -> num
closest	:(α -> real) -> (α -> bool) -> (α -> bool) -> real -> α
defloat	:ieee$float -> num # num # num
emax	:num # num -> num
encoding	:num # num -> num # num # num -> num
exponent	:num # num # num -> num
expwidth	:num # num -> num
fadd	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
fcompare	:num # num -> num # num # num -> num # num # num -> ccode
fdiv	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
feq	:num # num -> num # num # num -> num # num # num -> bool
fge	:num # num -> num # num # num -> num # num # num -> bool
fgt	:num # num -> num # num # num -> num # num # num -> bool
fintrnd	:num # num -> roundmode -> num # num # num -> num # num # num
fle	:num # num -> num # num # num -> num # num # num -> bool
float	:num # num # num -> ieee$float
float_To_zero	:roundmode
float_abs	:ieee$float -> ieee$float
float_add	:ieee$float -> ieee$float -> ieee$float
float_div	:ieee$float -> ieee$float -> ieee$float
float_eq	:ieee$float -> ieee$float -> bool
float_format	:num # num
float_ge	:ieee$float -> ieee$float -> bool
float_gt	:ieee$float -> ieee$float -> bool
float_le	:ieee$float -> ieee$float -> bool
float_lt	:ieee$float -> ieee$float -> bool
float_mul	:ieee$float -> ieee$float -> ieee$float
float_neg	:ieee$float -> ieee$float
float_rem	:ieee$float -> ieee$float -> ieee$float
float_sqrt	:ieee$float -> ieee$float
float_sub	:ieee$float -> ieee$float -> ieee$float
flt	:num # num -> num # num # num -> num # num # num -> bool
fmul	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
fneg	:num # num -> roundmode -> num # num # num -> num # num # num
fraction	:num # num # num -> num
fracwidth	:num # num -> num
frem	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
fsqrt	:num # num -> roundmode -> num # num # num -> num # num # num
fsub	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
intround	:num # num -> roundmode -> real -> num # num # num
is_closest	:(α -> real) -> (α -> bool) -> real -> α -> bool
is_denormal	:num # num -> num # num # num -> bool
is_double	:num # num -> bool
is_double_extended	:num # num -> bool
is_finite	:num # num -> num # num # num -> bool
is_infinity	:num # num -> num # num # num -> bool
is_integral	:num # num -> num # num # num -> bool
is_nan	:num # num -> num # num # num -> bool
is_normal	:num # num -> num # num # num -> bool
is_single	:num # num -> bool
is_single_extended	:num # num -> bool
is_valid	:num # num -> num # num # num -> bool
is_zero	:num # num -> num # num # num -> bool
largest	:num # num -> real
minus	:num # num -> num # num # num -> num # num # num
minus_infinity	:num # num -> num # num # num
minus_zero	:num # num -> num # num # num
num2ccode	:num -> ccode
num2roundmode	:num -> roundmode
plus_infinity	:num # num -> num # num # num
plus_zero	:num # num -> num # num # num
rem	:real -> real -> real
round	:num # num -> roundmode -> real -> num # num # num
roundmode2num	:roundmode -> num
roundmode_CASE	:roundmode -> α -> α -> α -> α -> α
roundmode_size	:roundmode -> num
sign	:num # num # num -> num
some_nan	:num # num -> num # num # num
threshold	:num # num -> real
topfloat	:num # num -> num # num # num
ulp	:num # num -> num # num # num -> real
valof	:num # num -> num # num # num -> real
wordlength	:num # num -> num
zerosign	:num # num -> num -> num # num # num -> num # num # num

Definitions

Exponent

⊢ ∀a. Exponent a = exponent (defloat a)

Finite

⊢ ∀a. Finite a ⇔ Isnormal a ∨ Isdenormal a ∨ Iszero a

Float

⊢ ∀x. Float x = float (round float_format To_nearest x)

Fraction

⊢ ∀a. Fraction a = fraction (defloat a)

Infinity

⊢ ∀a. Infinity a ⇔ is_infinity float_format (defloat a)

Isdenormal

⊢ ∀a. Isdenormal a ⇔ is_denormal float_format (defloat a)

Isintegral

⊢ ∀a. Isintegral a ⇔ is_integral float_format (defloat a)

Isnan

⊢ ∀a. Isnan a ⇔ is_nan float_format (defloat a)

Isnormal

⊢ ∀a. Isnormal a ⇔ is_normal float_format (defloat a)

Iszero

⊢ ∀a. Iszero a ⇔ is_zero float_format (defloat a)

Minus_infinity

⊢ Minus_infinity = float (minus_infinity float_format)

Minus_zero

⊢ Minus_zero = float (minus_zero float_format)

Plus_infinity

⊢ Plus_infinity = float (plus_infinity float_format)

Plus_zero

⊢ Plus_zero = float (plus_zero float_format)

ROUNDFLOAT

⊢ ∀a. ROUNDFLOAT a = float (fintrnd float_format To_nearest (defloat a))

Sign

⊢ ∀a. Sign a = sign (defloat a)

Ulp

⊢ ∀a. Ulp a = ulp float_format (defloat a)

Val

⊢ ∀a. Val a = valof float_format (defloat a)

bias

⊢ ∀X. bias X = 2 ** (expwidth X − 1) − 1

bottomfloat

⊢ ∀X. bottomfloat X = (1,emax X − 1,2 ** fracwidth X − 1)

ccode_BIJ

⊢ (∀a. num2ccode (ccode2num a) = a) ∧
  ∀r. (λn. n < 4) r ⇔ (ccode2num (num2ccode r) = r)

ccode_CASE

⊢ ∀x v0 v1 v2 v3.
    (case x of Gt => v0 | Lt => v1 | Eq => v2 | Un => v3) =
    (λm. if m < 1 then v0 else if m < 2 then v1 else if m = 2 then v2 else v3)
      (ccode2num x)

ccode_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep

ccode_size_def

⊢ ∀x. ccode_size x = 0

closest

⊢ ∀v p s x.
    closest v p s x =
    @a. is_closest v s x a ∧ ((∃b. is_closest v s x b ∧ p b) ⇒ p a)

emax

⊢ ∀X. emax X = 2 ** expwidth X − 1

encoding

⊢ ∀X s e f.
    encoding X (s,e,f) =
    s * 2 ** (wordlength X − 1) + e * 2 ** fracwidth X + f

exponent

⊢ ∀s e f. exponent (s,e,f) = e

expwidth

⊢ ∀ew fw. expwidth (ew,fw) = ew

fadd

⊢ ∀X m a b.
    fadd X m a b =
    if
      is_nan X a ∨ is_nan X b ∨
      is_infinity X a ∧ is_infinity X b ∧ sign a ≠ sign b
    then
      some_nan X
    else if is_infinity X a then a
    else if is_infinity X b then b
    else
      zerosign X
        (if is_zero X a ∧ is_zero X b ∧ (sign a = sign b) then sign a
         else if m = To_ninfinity then 1
         else 0) (round X m (valof X a + valof X b))

fcompare

⊢ ∀X a b.
    fcompare X a b =
    if is_nan X a ∨ is_nan X b then Un
    else if is_infinity X a ∧ (sign a = 1) then
      if is_infinity X b ∧ (sign b = 1) then Eq else Lt
    else if is_infinity X a ∧ (sign a = 0) then
      if is_infinity X b ∧ (sign b = 0) then Eq else Gt
    else if is_infinity X b ∧ (sign b = 1) then Gt
    else if is_infinity X b ∧ (sign b = 0) then Lt
    else if valof X a < valof X b then Lt
    else if valof X a = valof X b then Eq
    else Gt

fdiv

⊢ ∀X m a b.
    fdiv X m a b =
    if
      is_nan X a ∨ is_nan X b ∨ is_zero X a ∧ is_zero X b ∨
      is_infinity X a ∧ is_infinity X b
    then
      some_nan X
    else if is_infinity X a ∨ is_zero X b then
      if sign a = sign b then plus_infinity X else minus_infinity X
    else if is_infinity X b then
      if sign a = sign b then plus_zero X else minus_zero X
    else
      zerosign X (if sign a = sign b then 0 else 1)
        (round X m (valof X a / valof X b))

feq

⊢ ∀X a b. feq X a b ⇔ (fcompare X a b = Eq)

fge

⊢ ∀X a b. fge X a b ⇔ (fcompare X a b = Gt) ∨ (fcompare X a b = Eq)

fgt

⊢ ∀X a b. fgt X a b ⇔ (fcompare X a b = Gt)

fintrnd

⊢ ∀X m a.
    fintrnd X m a =
    if is_nan X a then some_nan X
    else if is_infinity X a then a
    else zerosign X (sign a) (intround X m (valof X a))

fle

⊢ ∀X a b. fle X a b ⇔ (fcompare X a b = Lt) ∨ (fcompare X a b = Eq)

float_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (is_valid float_format) rep

float_abs

⊢ ∀a. float_abs a = if a ≥ Plus_zero then a else ~a

float_add

⊢ ∀a b. a + b = float (fadd float_format To_nearest (defloat a) (defloat b))

float_div

⊢ ∀a b. a / b = float (fdiv float_format To_nearest (defloat a) (defloat b))

float_eq

⊢ ∀a b. a == b ⇔ feq float_format (defloat a) (defloat b)

float_format

⊢ float_format = (8,23)

float_ge

⊢ ∀a b. a ≥ b ⇔ fge float_format (defloat a) (defloat b)

float_gt

⊢ ∀a b. a > b ⇔ fgt float_format (defloat a) (defloat b)

float_le

⊢ ∀a b. a ≤ b ⇔ fle float_format (defloat a) (defloat b)

float_lt

⊢ ∀a b. a < b ⇔ flt float_format (defloat a) (defloat b)

float_mul

⊢ ∀a b. a * b = float (fmul float_format To_nearest (defloat a) (defloat b))

float_neg

⊢ ∀a. ~a = float (fneg float_format To_nearest (defloat a))

float_rem

⊢ ∀a b.
    a float_rem b =
    float (frem float_format To_nearest (defloat a) (defloat b))

float_sqrt

⊢ ∀a. float_sqrt a = float (fsqrt float_format To_nearest (defloat a))

float_sub

⊢ ∀a b. a − b = float (fsub float_format To_nearest (defloat a) (defloat b))

float_tybij

⊢ (∀a. float (defloat a) = a) ∧
  ∀r. is_valid float_format r ⇔ (defloat (float r) = r)

flt

⊢ ∀X a b. flt X a b ⇔ (fcompare X a b = Lt)

fmul

⊢ ∀X m a b.
    fmul X m a b =
    if
      is_nan X a ∨ is_nan X b ∨ is_zero X a ∧ is_infinity X b ∨
      is_infinity X a ∧ is_zero X b
    then
      some_nan X
    else if is_infinity X a ∨ is_infinity X b then
      if sign a = sign b then plus_infinity X else minus_infinity X
    else
      zerosign X (if sign a = sign b then 0 else 1)
        (round X m (valof X a * valof X b))

fneg

⊢ ∀X m a. fneg X m a = (1 − sign a,exponent a,fraction a)

fraction

⊢ ∀s e f. fraction (s,e,f) = f

fracwidth

⊢ ∀ew fw. fracwidth (ew,fw) = fw

frem

⊢ ∀X m a b.
    frem X m a b =
    if is_nan X a ∨ is_nan X b ∨ is_infinity X a ∨ is_zero X b then some_nan X
    else if is_infinity X b then a
    else zerosign X (sign a) (round X m (valof X a rem valof X b))

fsqrt

⊢ ∀X m a.
    fsqrt X m a =
    if is_nan X a then some_nan X
    else if is_zero X a ∨ is_infinity X a ∧ (sign a = 0) then a
    else if sign a = 1 then some_nan X
    else zerosign X (sign a) (round X m (sqrt (valof X a)))

fsub

⊢ ∀X m a b.
    fsub X m a b =
    if
      is_nan X a ∨ is_nan X b ∨
      is_infinity X a ∧ is_infinity X b ∧ (sign a = sign b)
    then
      some_nan X
    else if is_infinity X a then a
    else if is_infinity X b then minus X b
    else
      zerosign X
        (if is_zero X a ∧ is_zero X b ∧ sign a ≠ sign b then sign a
         else if m = To_ninfinity then 1
         else 0) (round X m (valof X a − valof X b))

intround_def

⊢ (∀X x.
     intround X To_nearest x =
     if x ≤ -threshold X then minus_infinity X
     else if x ≥ threshold X then plus_infinity X
     else
       closest (valof X) (λa. ∃n. EVEN n ∧ (abs (valof X a) = &n))
         {a | is_integral X a} x) ∧
  (∀X x.
     intround X float_To_zero x =
     if x < -largest X then bottomfloat X
     else if x > largest X then topfloat X
     else
       closest (valof X) (λx. T)
         {a | is_integral X a ∧ abs (valof X a) ≤ abs x} x) ∧
  (∀X x.
     intround X To_pinfinity x =
     if x < -largest X then bottomfloat X
     else if x > largest X then plus_infinity X
     else closest (valof X) (λx. T) {a | is_integral X a ∧ valof X a ≥ x} x) ∧
  ∀X x.
    intround X To_ninfinity x =
    if x < -largest X then minus_infinity X
    else if x > largest X then topfloat X
    else closest (valof X) (λx. T) {a | is_integral X a ∧ valof X a ≤ x} x

is_closest

⊢ ∀v s x a.
    is_closest v s x a ⇔ a ∈ s ∧ ∀b. b ∈ s ⇒ abs (v a − x) ≤ abs (v b − x)

is_denormal

⊢ ∀X a. is_denormal X a ⇔ (exponent a = 0) ∧ fraction a ≠ 0

is_double

⊢ ∀X. is_double X ⇔ (expwidth X = 11) ∧ (wordlength X = 64)

is_double_extended

⊢ ∀X. is_double_extended X ⇔ expwidth X ≥ 15 ∧ wordlength X ≥ 79

is_finite

⊢ ∀X a.
    is_finite X a ⇔
    is_valid X a ∧ (is_normal X a ∨ is_denormal X a ∨ is_zero X a)

is_infinity

⊢ ∀X a. is_infinity X a ⇔ (exponent a = emax X) ∧ (fraction a = 0)

is_integral

⊢ ∀X a. is_integral X a ⇔ is_finite X a ∧ ∃n. abs (valof X a) = &n

is_nan

⊢ ∀X a. is_nan X a ⇔ (exponent a = emax X) ∧ fraction a ≠ 0

is_normal

⊢ ∀X a. is_normal X a ⇔ 0 < exponent a ∧ exponent a < emax X

is_single

⊢ ∀X. is_single X ⇔ (expwidth X = 8) ∧ (wordlength X = 32)

is_single_extended

⊢ ∀X. is_single_extended X ⇔ expwidth X ≥ 11 ∧ wordlength X ≥ 43

is_valid

⊢ ∀X s e f.
    is_valid X (s,e,f) ⇔
    s < SUC (SUC 0) ∧ e < 2 ** expwidth X ∧ f < 2 ** fracwidth X

is_zero

⊢ ∀X a. is_zero X a ⇔ (exponent a = 0) ∧ (fraction a = 0)

largest

⊢ ∀X. largest X =
      2 pow (emax X − 1) / 2 pow bias X * (2 − (2 pow fracwidth X)⁻¹)

minus

⊢ ∀X a. minus X a = (1 − sign a,exponent a,fraction a)

minus_infinity

⊢ ∀X. minus_infinity X = (1,emax X,0)

minus_zero

⊢ ∀X. minus_zero X = (1,0,0)

plus_infinity

⊢ ∀X. plus_infinity X = (0,emax X,0)

plus_zero

⊢ ∀X. plus_zero X = (0,0,0)

rem

⊢ ∀x y.
    x rem y =
    (let
       n =
         closest I (λx. ∃n. EVEN n ∧ (abs x = &n)) {x | (∃n. abs x = &n)}
           (x / y)
     in
       x − n * y)

round_def

⊢ (∀X x.
     round X To_nearest x =
     if x ≤ -threshold X then minus_infinity X
     else if x ≥ threshold X then plus_infinity X
     else closest (valof X) (λa. EVEN (fraction a)) {a | is_finite X a} x) ∧
  (∀X x.
     round X float_To_zero x =
     if x < -largest X then bottomfloat X
     else if x > largest X then topfloat X
     else
       closest (valof X) (λx. T) {a | is_finite X a ∧ abs (valof X a) ≤ abs x}
         x) ∧
  (∀X x.
     round X To_pinfinity x =
     if x < -largest X then bottomfloat X
     else if x > largest X then plus_infinity X
     else closest (valof X) (λx. T) {a | is_finite X a ∧ valof X a ≥ x} x) ∧
  ∀X x.
    round X To_ninfinity x =
    if x < -largest X then minus_infinity X
    else if x > largest X then topfloat X
    else closest (valof X) (λx. T) {a | is_finite X a ∧ valof X a ≤ x} x

roundmode_BIJ

⊢ (∀a. num2roundmode (roundmode2num a) = a) ∧
  ∀r. (λn. n < 4) r ⇔ (roundmode2num (num2roundmode r) = r)

roundmode_CASE

⊢ ∀x v0 v1 v2 v3.
    (case x of
       To_nearest => v0
     | float_To_zero => v1
     | To_pinfinity => v2
     | To_ninfinity => v3) =
    (λm. if m < 1 then v0 else if m < 2 then v1 else if m = 2 then v2 else v3)
      (roundmode2num x)

roundmode_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep

roundmode_size_def

⊢ ∀x. roundmode_size x = 0

sign

⊢ ∀s e f. sign (s,e,f) = s

some_nan

⊢ ∀X. some_nan X = @a. is_nan X a

threshold

⊢ ∀X. threshold X =
      2 pow (emax X − 1) / 2 pow bias X * (2 − (2 pow SUC (fracwidth X))⁻¹)

topfloat

⊢ ∀X. topfloat X = (0,emax X − 1,2 ** fracwidth X − 1)

ulp

⊢ ∀X a. ulp X a = valof X (0,exponent a,1) − valof X (0,exponent a,0)

valof

⊢ ∀X s e f.
    valof X (s,e,f) =
    if e = 0 then -1 pow s * (2 / 2 pow bias X) * (&f / 2 pow fracwidth X)
    else -1 pow s * (2 pow e / 2 pow bias X) * (1 + &f / 2 pow fracwidth X)

wordlength

⊢ ∀X. wordlength X = expwidth X + fracwidth X + 1

zerosign

⊢ ∀X s a.
    zerosign X s a =
    if is_zero X a then if s = 0 then plus_zero X else minus_zero X else a

Theorems

ccode2num_11

⊢ ∀a a'. (ccode2num a = ccode2num a') ⇔ (a = a')

ccode2num_ONTO

⊢ ∀r. r < 4 ⇔ ∃a. r = ccode2num a

ccode2num_num2ccode

⊢ ∀r. r < 4 ⇔ (ccode2num (num2ccode r) = r)

ccode2num_thm

⊢ (ccode2num Gt = 0) ∧ (ccode2num Lt = 1) ∧ (ccode2num Eq = 2) ∧
  (ccode2num Un = 3)

ccode_Axiom

⊢ ∀x0 x1 x2 x3. ∃f. (f Gt = x0) ∧ (f Lt = x1) ∧ (f Eq = x2) ∧ (f Un = x3)

ccode_EQ_ccode

⊢ ∀a a'. (a = a') ⇔ (ccode2num a = ccode2num a')

ccode_case_cong

⊢ ∀M M' v0 v1 v2 v3.
    (M = M') ∧ ((M' = Gt) ⇒ (v0 = v0')) ∧ ((M' = Lt) ⇒ (v1 = v1')) ∧
    ((M' = Eq) ⇒ (v2 = v2')) ∧ ((M' = Un) ⇒ (v3 = v3')) ⇒
    ((case M of Gt => v0 | Lt => v1 | Eq => v2 | Un => v3) =
     case M' of Gt => v0' | Lt => v1' | Eq => v2' | Un => v3')

ccode_case_def

⊢ (∀v0 v1 v2 v3. (case Gt of Gt => v0 | Lt => v1 | Eq => v2 | Un => v3) = v0) ∧
  (∀v0 v1 v2 v3. (case Lt of Gt => v0 | Lt => v1 | Eq => v2 | Un => v3) = v1) ∧
  (∀v0 v1 v2 v3. (case Eq of Gt => v0 | Lt => v1 | Eq => v2 | Un => v3) = v2) ∧
  ∀v0 v1 v2 v3. (case Un of Gt => v0 | Lt => v1 | Eq => v2 | Un => v3) = v3

ccode_case_eq

⊢ ((case x of Gt => v0 | Lt => v1 | Eq => v2 | Un => v3) = v) ⇔
  (x = Gt) ∧ (v0 = v) ∨ (x = Lt) ∧ (v1 = v) ∨ (x = Eq) ∧ (v2 = v) ∨
  (x = Un) ∧ (v3 = v)

ccode_distinct

⊢ Gt ≠ Lt ∧ Gt ≠ Eq ∧ Gt ≠ Un ∧ Lt ≠ Eq ∧ Lt ≠ Un ∧ Eq ≠ Un

ccode_induction

⊢ ∀P. P Eq ∧ P Gt ∧ P Lt ∧ P Un ⇒ ∀a. P a

ccode_nchotomy

⊢ ∀a. (a = Gt) ∨ (a = Lt) ∨ (a = Eq) ∨ (a = Un)

datatype_ccode

⊢ DATATYPE (ccode Gt Lt Eq Un)

datatype_roundmode

⊢ DATATYPE (roundmode To_nearest float_To_zero To_pinfinity To_ninfinity)

num2ccode_11

⊢ ∀r r'. r < 4 ⇒ r' < 4 ⇒ ((num2ccode r = num2ccode r') ⇔ (r = r'))

num2ccode_ONTO

⊢ ∀a. ∃r. (a = num2ccode r) ∧ r < 4

num2ccode_ccode2num

⊢ ∀a. num2ccode (ccode2num a) = a

num2ccode_thm

⊢ (num2ccode 0 = Gt) ∧ (num2ccode 1 = Lt) ∧ (num2ccode 2 = Eq) ∧
  (num2ccode 3 = Un)

num2roundmode_11

⊢ ∀r r'. r < 4 ⇒ r' < 4 ⇒ ((num2roundmode r = num2roundmode r') ⇔ (r = r'))

num2roundmode_ONTO

⊢ ∀a. ∃r. (a = num2roundmode r) ∧ r < 4

num2roundmode_roundmode2num

⊢ ∀a. num2roundmode (roundmode2num a) = a

num2roundmode_thm

⊢ (num2roundmode 0 = To_nearest) ∧ (num2roundmode 1 = float_To_zero) ∧
  (num2roundmode 2 = To_pinfinity) ∧ (num2roundmode 3 = To_ninfinity)

roundmode2num_11

⊢ ∀a a'. (roundmode2num a = roundmode2num a') ⇔ (a = a')

roundmode2num_ONTO

⊢ ∀r. r < 4 ⇔ ∃a. r = roundmode2num a

roundmode2num_num2roundmode

⊢ ∀r. r < 4 ⇔ (roundmode2num (num2roundmode r) = r)

roundmode2num_thm

⊢ (roundmode2num To_nearest = 0) ∧ (roundmode2num float_To_zero = 1) ∧
  (roundmode2num To_pinfinity = 2) ∧ (roundmode2num To_ninfinity = 3)

roundmode_Axiom

⊢ ∀x0 x1 x2 x3. ∃f.
    (f To_nearest = x0) ∧ (f float_To_zero = x1) ∧ (f To_pinfinity = x2) ∧
    (f To_ninfinity = x3)

roundmode_EQ_roundmode

⊢ ∀a a'. (a = a') ⇔ (roundmode2num a = roundmode2num a')

roundmode_case_cong

⊢ ∀M M' v0 v1 v2 v3.
    (M = M') ∧ ((M' = To_nearest) ⇒ (v0 = v0')) ∧
    ((M' = float_To_zero) ⇒ (v1 = v1')) ∧ ((M' = To_pinfinity) ⇒ (v2 = v2')) ∧
    ((M' = To_ninfinity) ⇒ (v3 = v3')) ⇒
    ((case M of
        To_nearest => v0
      | float_To_zero => v1
      | To_pinfinity => v2
      | To_ninfinity => v3) =
     case M' of
       To_nearest => v0'
     | float_To_zero => v1'
     | To_pinfinity => v2'
     | To_ninfinity => v3')

roundmode_case_def

⊢ (∀v0 v1 v2 v3.
     (case To_nearest of
        To_nearest => v0
      | float_To_zero => v1
      | To_pinfinity => v2
      | To_ninfinity => v3) = v0) ∧
  (∀v0 v1 v2 v3.
     (case float_To_zero of
        To_nearest => v0
      | float_To_zero => v1
      | To_pinfinity => v2
      | To_ninfinity => v3) = v1) ∧
  (∀v0 v1 v2 v3.
     (case To_pinfinity of
        To_nearest => v0
      | float_To_zero => v1
      | To_pinfinity => v2
      | To_ninfinity => v3) = v2) ∧
  ∀v0 v1 v2 v3.
    (case To_ninfinity of
       To_nearest => v0
     | float_To_zero => v1
     | To_pinfinity => v2
     | To_ninfinity => v3) = v3

roundmode_case_eq

⊢ ((case x of
      To_nearest => v0
    | float_To_zero => v1
    | To_pinfinity => v2
    | To_ninfinity => v3) = v) ⇔
  (x = To_nearest) ∧ (v0 = v) ∨ (x = float_To_zero) ∧ (v1 = v) ∨
  (x = To_pinfinity) ∧ (v2 = v) ∨ (x = To_ninfinity) ∧ (v3 = v)

roundmode_distinct

⊢ To_nearest ≠ float_To_zero ∧ To_nearest ≠ To_pinfinity ∧
  To_nearest ≠ To_ninfinity ∧ float_To_zero ≠ To_pinfinity ∧
  float_To_zero ≠ To_ninfinity ∧ To_pinfinity ≠ To_ninfinity

roundmode_induction

⊢ ∀P. P To_nearest ∧ P To_ninfinity ∧ P To_pinfinity ∧ P float_To_zero ⇒
      ∀a. P a

roundmode_nchotomy

⊢ ∀a. (a = To_nearest) ∨ (a = float_To_zero) ∨ (a = To_pinfinity) ∨
      (a = To_ninfinity)