Theory IEEE_Single_NaN

(* Author: Tjark Weber, Uppsala University
*)

section ‹Specification of the IEEE standard with a single NaN value›

theory IEEE_Single_NaN
  imports
    IEEE_Properties
begin

text ‹This theory defines a type of floating-point numbers that contains a single NaN value, much
  like specification level~2 of IEEE-754 (which does not distinguish between a quiet and a
  signaling NaN, nor between different bit representations of NaN).

  In contrast, the type @{typ ‹('e, 'f) float›} defined in {\tt IEEE.thy} may contain several
  distinct (bit) representations of NaN, much like specification level~4 of IEEE-754.

  One aim of this theory is to define a floating-point type (along with arithmetic operations) whose
  semantics agrees with the semantics of the SMT-LIB floating-point theory at
  \url{https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml}. The following development
  therefore deviates from {\tt IEEE.thy} in some places to ensure alignment with the SMT-LIB
  theory.›

text ‹Note that we are using HOL equality (rather than IEEE-754 floating-point equality) in the
  following definition. This is because we do not want to identify~$+0$ and~$-0$.›
definition is_nan_equivalent :: "('e, 'f) float ⇒ ('e, 'f) float ⇒ bool"
  where "is_nan_equivalent a b ≡ a = b ∨ (is_nan a ∧ is_nan b)"

quotient_type (overloaded) ('e, 'f) floatSingleNaN = "('e, 'f) float" / is_nan_equivalent
  by (metis equivpI is_nan_equivalent_def reflpI sympI transpI)

text ‹Note that @{typ "('e, 'f) floatSingleNaN"} does not count the hidden bit in the significand.
  For instance, IEEE-754's double-precision binary floating point format {\tt binary64} corresponds
  to @{typ "(11,52) floatSingleNaN"}. The corresponding SMT-LIB sort is {\tt (\_ FloatingPoint 11 53)},
  where the hidden bit is counted.  Since the bit size is encoded as a type argument, and Isabelle/HOL
  does not permit arithmetic on type expressions, it would be difficult to resolve this difference
  without completely separating the definition of @{typ "('e, 'f) floatSingleNaN"} in this theory
  from the definition of @{typ "('e, 'f) float"} in IEEE.thy.›

syntax "_floatSingleNaN" :: "type ⇒ type ⇒ type" (‹'(_, _') floatSingleNaN›)
syntax_types "_floatSingleNaN" ⇌ floatSingleNaN
text ‹Parse ‹('a, 'b) floatSingleNaN› as ‹('a::len, 'b::len) floatSingleNaN›.›

parse_translation ‹
  let
    fun float t u = Syntax.const @{type_syntax floatSingleNaN} $ t $ u;
    fun len_tr u =
      (case Term_Position.strip_positions u of
        v as Free (x, _) =>
          if Lexicon.is_tid x then
            (Syntax.const @{syntax_const "_ofsort"} $ v $
              Syntax.const @{class_syntax len})
          else u
      | _ => u)
    fun len_float_tr [t, u] =
      float (len_tr t) (len_tr u)
  in
    [(@{syntax_const "_floatSingleNaN"}, K len_float_tr)]
  end
›


subsection ‹Value constructors›

subsubsection ‹FP literals as bit string triples, with the leading bit for the significand not
  represented (hidden bit)›

lift_definition fp :: "1 word ⇒ 'e word ⇒ 'f word ⇒ ('e, 'f) floatSingleNaN"
  is "λs e f. IEEE.Abs_float (s, e, f)" .

subsubsection ‹Plus and minus infinity›

lift_definition plus_infinity :: "('e, 'f) floatSingleNaN" (‹∞›) is IEEE.plus_infinity .

lift_definition minus_infinity :: "('e, 'f) floatSingleNaN" is IEEE.minus_infinity .

subsubsection ‹Plus and minus zero›

instantiation floatSingleNaN :: (len, len) zero begin

  lift_definition zero_floatSingleNaN :: "('a, 'b) floatSingleNaN" is 0 .

  instance ..

end

lift_definition minus_zero :: "('e, 'f) floatSingleNaN" is IEEE.minus_zero .

subsubsection ‹Non-numbers (NaN)›

lift_definition NaN :: "('e, 'f) floatSingleNaN" is some_nan .


subsection ‹Operators›

subsubsection ‹Absolute value›

setup ‹Sign.mandatory_path "abs_floatSingleNaN_inst"›  ― ‹workaround to avoid a duplicate fact declaration {\tt abs\_floatSingleNaN\_def} in lift\_definition below›

instantiation floatSingleNaN :: (len, len) abs
begin

  lift_definition abs_floatSingleNaN :: "('a, 'b) floatSingleNaN ⇒ ('a, 'b) floatSingleNaN" is abs
    unfolding is_nan_equivalent_def by (metis IEEE.abs_float_def is_nan_uminus)

  instance ..

end

setup ‹Sign.parent_path›

subsubsection ‹Negation (no rounding needed)›

instantiation floatSingleNaN :: (len, len) uminus
begin

  lift_definition uminus_floatSingleNaN :: "('a, 'b) floatSingleNaN ⇒ ('a, 'b) floatSingleNaN" is uminus
    unfolding is_nan_equivalent_def by (metis is_nan_uminus)

  instance ..

end

subsubsection ‹Addition›

lift_definition fadd :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.fadd
  unfolding is_nan_equivalent_def by (metis IEEE.fadd_def)

subsubsection ‹Subtraction›

lift_definition fsub :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.fsub
  unfolding is_nan_equivalent_def by (metis IEEE.fsub_def)

subsubsection ‹Multiplication›

lift_definition fmul :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.fmul
  unfolding is_nan_equivalent_def by (metis IEEE.fmul_def)

subsubsection ‹Division›

lift_definition fdiv :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.fdiv
  unfolding is_nan_equivalent_def by (metis IEEE.fdiv_def)

subsubsection ‹Fused multiplication and addition; $(x \cdot y) + z$›

lift_definition fmul_add :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.fmul_add
  unfolding is_nan_equivalent_def by (smt (verit) IEEE.fmul_add_def)

subsubsection ‹Square root›

lift_definition fsqrt :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.fsqrt
  unfolding is_nan_equivalent_def by (metis IEEE.fsqrt_def)

subsubsection ‹Remainder: $x - y \cdot n$, where $n \in \mathrm{Z}$ is nearest to $x/y$›

lift_definition frem :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.frem
  unfolding is_nan_equivalent_def by (metis IEEE.frem_def)

lift_definition float_rem :: "('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.float_rem
  unfolding is_nan_equivalent_def by (metis IEEE.frem_def IEEE.float_rem_def)

subsubsection ‹Rounding to integral›

lift_definition fintrnd :: "roundmode ⇒ ('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN" is IEEE.fintrnd
  unfolding is_nan_equivalent_def by (metis IEEE.fintrnd_def)

subsubsection ‹Minimum and maximum›

text ‹In IEEE 754-2019, the minNum and maxNum operations of the 2008 version of the standard have
been replaced by minimum, minimumNumber, maximum, maximumNumber (see Section~9.6 of the 2019
standard). These are not (yet) available in SMT-LIB. We currently do not implement any of these
operations.›

subsubsection ‹Comparison operators›

lift_definition fle :: "('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ bool" is IEEE.fle
  unfolding is_nan_equivalent_def by (smt (verit) IEEE.fcompare_def IEEE.fle_def)

lift_definition flt :: "('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ bool" is IEEE.flt
  unfolding is_nan_equivalent_def by (smt (verit) IEEE.fcompare_def IEEE.flt_def)

lift_definition fge :: "('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ bool" is IEEE.fge
  unfolding is_nan_equivalent_def by (smt (verit) IEEE.fcompare_def IEEE.fge_def)

lift_definition fgt :: "('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ bool" is IEEE.fgt
  unfolding is_nan_equivalent_def by (smt (verit) IEEE.fcompare_def IEEE.fgt_def)

subsubsection ‹IEEE 754 equality›

lift_definition feq :: "('e ,'f) floatSingleNaN ⇒ ('e ,'f) floatSingleNaN ⇒ bool" is IEEE.feq
  unfolding is_nan_equivalent_def by (smt (verit) IEEE.fcompare_def IEEE.feq_def)

subsubsection ‹Classification of numbers›

lift_definition is_normal :: "('e, 'f) floatSingleNaN ⇒ bool" is IEEE.is_normal
  unfolding is_nan_equivalent_def using float_distinct by blast

lift_definition is_subnormal :: "('e, 'f) floatSingleNaN ⇒ bool" is IEEE.is_denormal
  unfolding is_nan_equivalent_def using float_distinct by blast

lift_definition is_zero :: "('e, 'f) floatSingleNaN ⇒ bool" is IEEE.is_zero
  unfolding is_nan_equivalent_def using float_distinct by blast

lift_definition is_infinity :: "('e, 'f) floatSingleNaN ⇒ bool" is IEEE.is_infinity
  unfolding is_nan_equivalent_def using float_distinct by blast

lift_definition is_nan :: "('e, 'f) floatSingleNaN ⇒ bool" is IEEE.is_nan
  unfolding is_nan_equivalent_def by blast

lift_definition is_finite :: "('e, 'f) floatSingleNaN ⇒ bool" is IEEE.is_finite
  unfolding is_nan_equivalent_def using nan_not_finite by blast

definition is_negative :: "('e, 'f) floatSingleNaN ⇒ bool"
  where "is_negative x ≡ x = minus_zero ∨ flt x minus_zero"

definition is_positive :: "('e, 'f) floatSingleNaN ⇒ bool"
  where "is_positive x ≡ x = 0 ∨ flt 0 x"


subsection ‹Conversions to other sorts›

subsubsection ‹to real›

text ‹SMT-LIB leaves {\tt fp.to\_real} unspecified for $+\infty$, $-\infty$, NaN. In contrast,
@{const valof} is (partially) specified also for those arguments. This means that the SMT-LIB
semantics can prove fewer theorems about {\tt fp.to\_real} than Isabelle can prove about
@{const valof}.›

lift_definition valof :: "('e,'f) floatSingleNaN ⇒ real"
  is "λa. if IEEE.is_infinity a then undefined a
            else if IEEE.is_nan a then undefined  ― ‹returning the same value for all floats that satisfy @{const IEEE.is_nan} is necessary to obtain a function that can be lifted to the quotient type›
            else IEEE.valof a"
  unfolding is_nan_equivalent_def using float_distinct(1) by fastforce

subsubsection ‹to unsigned machine integer, represented as a bit vector›

definition unsigned_word_of_floatSingleNaN :: "roundmode ⇒ ('e,'f) floatSingleNaN ⇒ 'a::len word"
  where "unsigned_word_of_floatSingleNaN mode a ≡
    if is_infinity a ∨ is_nan a then undefined mode a
      else (SOME w. valof (fintrnd mode a) = real_of_word w)"

subsubsection ‹to signed machine integer, represented as a 2's complement bit vector›

definition signed_word_of_floatSingleNaN :: "roundmode ⇒ ('e,'f) floatSingleNaN ⇒ 'a::len word"
  where "signed_word_of_floatSingleNaN mode a ≡
    if is_infinity a ∨ is_nan a then undefined mode a
      else (SOME w. valof (fintrnd mode a) = real_of_int (sint w))"


subsection ‹Conversions from other sorts›

subsubsection ‹from single bitstring representation in IEEE 754 interchange format›

text ‹The intention is that @{prop ‹LENGTH('a::len) = 1 + LENGTH('e::len) + LENGTH('f::len)›}
  (recall that @{term ‹LENGTH('f::len)›} does not include the significand's hidden bit). Of course,
  the type system of Isabelle/HOL is not strong enough to enforce this.›

definition floatSingleNaN_of_IEEE754_word :: "'a::len word ⇒ ('e,'f) floatSingleNaN"
  where "floatSingleNaN_of_IEEE754_word w ≡
    let (se, f) = word_split w :: 'a word × _; (s, e) = word_split se in fp s e f"  ― ‹using @{typ ‹'a word›} ensures that no bits are lost in @{term ‹se›}›

subsubsection ‹from real›

lift_definition round :: "roundmode ⇒ real ⇒ ('e,'f) floatSingleNaN" is IEEE.round .

subsubsection ‹from another floating point sort›

definition floatSingleNaN_of_floatSingleNaN :: "roundmode ⇒ ('a,'b) floatSingleNaN ⇒ ('e,'f) floatSingleNaN"
  where "floatSingleNaN_of_floatSingleNaN mode a ≡
    if a = plus_infinity then plus_infinity
      else if a = minus_infinity then minus_infinity
      else if a = NaN then NaN
      else round mode (valof a)"

subsubsection ‹from signed machine integer, represented as a 2's complement bit vector›

definition floatSingleNaN_of_signed_word :: "roundmode ⇒ 'a::len word ⇒ ('e,'f) floatSingleNaN"
  where "floatSingleNaN_of_signed_word mode w ≡ round mode (real_of_int (sint w))"

subsubsection ‹from unsigned machine integer, represented as bit vector›

definition floatSingleNaN_of_unsigned_word :: "roundmode ⇒ 'a::len word ⇒ ('e,'f) floatSingleNaN"
  where "floatSingleNaN_of_unsigned_word mode w ≡ round mode (real_of_word w)"

end