Theory "ieee"

Signature

Definitions

expwidth

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

fracwidth

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

wordlength

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

emax

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

bias

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

is_single

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

is_double

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

is_single_extended

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

is_double_extended

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

sign

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

exponent

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

fraction

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

is_nan

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

is_infinity

⊢ ∀X a. is_infinity 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_denormal

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

is_zero

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

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_finite

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

plus_infinity

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

minus_infinity

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

plus_zero

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

minus_zero

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

topfloat

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

bottomfloat

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

minus

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

encoding

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

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)

largest

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

threshold

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

ulp

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

roundmode_TY_DEF

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

roundmode_BIJ

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

roundmode_size_def

⊢ ∀x. roundmode_size x = 0

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)

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)

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)

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

is_integral

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

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

some_nan

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

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

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)

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))

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))

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))

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))

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))

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)))

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))

fneg

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

ccode_TY_DEF

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

ccode_BIJ

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

ccode_size_def

⊢ ∀x. ccode_size x = 0

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)

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

flt

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

fle

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

fgt

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

fge

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

feq

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

float_format

⊢ float_format = (8,23)

float_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (is_valid float_format) rep

float_tybij

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

Val

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

Float

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

Sign

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

Exponent

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

Fraction

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

Ulp

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

Isnan

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

Infinity

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

Isnormal

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

Isdenormal

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

Iszero

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

Finite

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

Isintegral

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

Plus_zero

⊢ Plus_zero = float (plus_zero float_format)

Minus_zero

⊢ Minus_zero = float (minus_zero float_format)

Minus_infinity

⊢ Minus_infinity = float (minus_infinity float_format)

Plus_infinity

⊢ Plus_infinity = float (plus_infinity float_format)

float_add

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

float_sub

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

float_mul

⊢ ∀a b. a * b = float (fmul 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_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))

ROUNDFLOAT

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

float_lt

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

float_le

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

float_gt

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

float_ge

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

float_eq

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

float_neg

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

float_abs

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

Theorems

num2roundmode_roundmode2num

⊢ ∀a. num2roundmode (roundmode2num a) = a

roundmode2num_num2roundmode

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

num2roundmode_11

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

roundmode2num_11

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

num2roundmode_ONTO

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

roundmode2num_ONTO

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

num2roundmode_thm

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

roundmode2num_thm

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

roundmode_EQ_roundmode

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

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

datatype_roundmode

⊢ DATATYPE (roundmode To_nearest float_To_zero To_pinfinity To_ninfinity)

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_nchotomy

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

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_induction

⊢ ∀P.
      P To_nearest ∧ P To_ninfinity ∧ P To_pinfinity ∧ P float_To_zero ⇒
      ∀a. P 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_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

num2ccode_ccode2num

⊢ ∀a. num2ccode (ccode2num a) = a

ccode2num_num2ccode

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

num2ccode_11

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

ccode2num_11

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

num2ccode_ONTO

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

ccode2num_ONTO

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

num2ccode_thm

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

ccode2num_thm

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

ccode_EQ_ccode

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

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

datatype_ccode

⊢ DATATYPE (ccode Gt Lt Eq Un)

ccode_distinct

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

ccode_nchotomy

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

ccode_Axiom

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

ccode_induction

⊢ ∀P. P Eq ∧ P Gt ∧ P Lt ∧ P Un ⇒ ∀a. P 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_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