src/floating-point/binary_ieeeScript.sml

30    float = <| Sign : word1; Exponent : 'w word; Significand : 't word |>`
124          Exponent := UINT_MAXw: 'w word;
125          Significand := 0w: 't word |>`
130          Exponent := 0w: 'w word;
131          Significand := 0w: 't word |>`
136          Exponent := UINT_MAXw - 1w: 'w word;
137          Significand := UINT_MAXw: 't word |>`
142          Exponent := 0w: 'w word;
143          Significand := 1w: 't word |>`
218    ULP (e:'w word, (:'t)) =
223 val ulp_def = Define `ulp (:'t # 'w) = ULP (0w:'w word, (:'t))`
776    `!a:'a word. a <> -1w ==> w2n a + 1 < 2 ** dimindex(:'a)`,
785    |> Q.SPECL [`2`, `w2n (a:'w word)`]
884   `(1w #>> 1 <> 0w : 'a word) /\ word_msb (1w : 'a word #>> 1)`,
903                       Exponent := UINT_MAXw: 'b word;
904                       Significand := (1w #>> 1): 'a word |>)) :
1100                 Exponent := UINT_MAXw: 'b word;
1101                 Significand := (1w #>> 1): 'a word |>))`
1145    `0w <+ (-2w:'a word) = (dimindex(:'a) <> 1)`,
1152    `dimindex(:'a) <> 1 ==> -2w <+ (-1w:'a word)`,
1357    `!e. 0 < ULP (e:'w word, (:'t))`,
1371    `!e: 'w word. ulp (:'t # 'w) <= ULP (e,(:'t))`,
1587   !x:'a word. x <> -1w ==> w2n x < 2 ** dimindex(:'a) - 1
1598   !w:'t word. &w2n w / 2 pow precision (:'t) < 1
1604   !w:'t word. 2 * (&w2n w / 2 pow precision (:'t)) < 2
1612     2 / 2 pow bias (:'w) * (&w2n (x:'t word) / 2 pow precision (:'t)) <
1613     2 pow w2n (y:'w word) / 2 pow bias (:'w) *
1614     (1 + &w2n (z:'t word) / 2 pow precision (:'t))
1744                 (1 + &w2n (-1w: 't word) / 2 pow precision (:'t))`]
2074         [wordsLib.WORD_DECIDE ``a:'a word <> 0w /\ a <> 1w ==> 1w <+ a``]
2353                   ``a:'a word <> b + -1w ==> b <> a + 1w``],
2381              wordsLib.WORD_DECIDE ``a <> b /\ a <=+ b ==> a <+ b:'a word``]
2655    `ULP (0w:'w word, (:'t)) = ULP (1w:'w word, (:'t))`,
2829 val not_one_lem = wordsLib.WORD_DECIDE ``(x:'a word) <> 1w ==> w2n x <> 1``
3387    `!s e:'w word f:'t word.
3413   `w2n (n2w (UINT_MAX (:'w)) + -1w : 'w word) = UINT_MAX (:'w) - 1`,
3440   \\ `UINT_MAXw - 1w <> 0w : 'w word` by simp []