More floating point theorems

[michael-roe]

(Feature request)

Add proofs of the following floating point theorems:

!x . not float_equal x x <=> float_is_nan x

!x . float_unordered x x <=> float_is_nan x

!x . (float_equal x (float_plus_infinity (:'t # 'w))) \/ (float_equal x (float_minus_infinity (:'t # 'w))) <=> float_is_infinite x;

!x . float_equal x (float_plus_zero (:'w # 't)) <=> float_is_zero x

These theorems prove that the typical implementations of fp_is_nan etc. (if you don't have fp_classify) are correct.

[michael-roe]

The third one of these theorems is closely related to float_infinities in binary_ieeeScript.sml. The critical difference is that it uses float_equal rather than =.

(testing for x = float_minus_infinity is equivalent to testing for float_equal x float_minus_infinity, but you need to prove that)

[michael-roe]

We might also need:

! x y . (float_is_infinite x) ==> ((float_equal x y) <=> (x = y))

float_equal is not the same as = for zeros and nans, but is is for infinities, normal numbers and submormal numbers.

P.S. I had a try at proving this, but it turned out to be difficult:

Basic plan:

Case split on float_value x simp[float_is_infinite_def] deals with cases where x is not an infinity

in remaining case, simp[float_equal_def,float_compare_def] Case split on float value y

... which gets us down to the tricky case where x and y are both infinities

[mn200]

First in the list now done (by 02db589c4)