More floating point theorems

[michael-roe]

More floating point theorems

[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 02db589)