src/floating-point/binary_ieeeScript.sml

631    rw [realTheory.REAL_LE_DIV, realTheory.REAL_LT_IMP_LE])
635    rw [realTheory.REAL_EQ_LDIV_EQ])
679    >- (`(n = 1) \/ (n = 2)` by decide_tac \\ rw [])
701    rw [DECIDE ``0 < a /\ a <> 1 ==> 2n <= a``])
719    \\ rw [realTheory.pow]
920    \\ rw [float_value_def]
953    rw [float_plus_infinity_def, float_minus_infinity_def,
995    rw [float_component_equality, float_components, two_mod_not_one, sign_neq,
1008    rw [float_plus_infinity_def, float_minus_infinity_def,
1019    rw [float_plus_zero_def, float_minus_zero_def,
1032    rw [FUN_EQ_THM, float_is_infinite_def, float_is_zero_def, float_value_def,
1036    \\ rw [sign_not_zero, realLib.REAL_ARITH ``0r <= n ==> 1 + n <> 0``]
1042    rw [float_is_nan_def, float_is_normal_def, float_is_subnormal_def,
1046    \\ rw [float_plus_infinity_def, float_minus_infinity_def,
1199    rw [float_is_zero_def, float_value_def, float_to_real_def, sign_not_zero,
1206   rw [float_is_finite_def, float_is_normal_def, float_is_subnormal_def,
1215   rw [float_is_nan_def, float_is_infinite_def, float_is_finite_def]
1224   rw [float_is_nan_def, float_is_infinite_def, float_is_finite_def]
1246   rw []
1282    rw [float_to_real_def, float_negate_def]
1359    rw [ULP_def, realTheory.REAL_LT_RDIV_0])
1373    rw [ulp_def]
1381    \\ rw [Once realTheory.pow]
1396    \\ rw [GSYM realTheory.REAL_LT_ADD_SUB, realTheory.POW_2_LE1, lem]
1409    \\ rw [realTheory.POW_2_LE1, GSYM realTheory.REAL_LT_ADD_SUB,
1452    \\ rw [ulp_def, ULP_def, float_to_real_def, abs_float_value, abs_significand,
1482    rw [float_is_finite_def])
1487    rw [float_value_def])
1491    rw [float_is_zero_def, float_value_def]
1512    rw [realTheory.REAL_LE_DIV, realTheory.REAL_LE_MUL,
1518    rw [realTheory.REAL_LE_DIV, realTheory.REAL_LE_MUL,
1537    \\ rw [ULP_def, float_to_real_def, float_is_zero, realTheory.ABS_NEG,
1542    \\ rw [realTheory.REAL_LDISTRIB]
1558    \\ rw [ULP_def, float_to_real_def, float_is_zero, realTheory.ABS_NEG,
1598    rw [realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_OF_NUM_POW, w2n_lt_pow])
1602    rw [realLib.REAL_ARITH ``2r * n < 2 = n < 1``, nobias_denormal_lt_1])
1619    \\ rw [nobias_denormal_lt_2, pow_ge2, realTheory.REAL_LE_MUL])
1748    rw [ULP_def, exponent_boundary_def, float_to_real_def]
1800       \\ rw []
1975    rw [ULP_def, float_to_real_def]
1992    rw [ULP_def, float_to_real_def]
2016    rw [ULP_def, float_to_real_def, realTheory.ABS_NEG, abs_float_value,
2048    rw [ULP_def, float_to_real_def, realTheory.ABS_NEG, abs_float_value,
2092    rw [float_to_real_def, realTheory.ABS_NEG, abs_float_value,
2167    rw [ULP_def, float_to_real_def]
2189    rw [diff_significand_ULP_mul, ULP_gt0, diff_ge1,
2235    \\ rw [float_to_real_def, sign_not_zero, div_twopow]
2242    rw [float_to_real_eq, float_component_equality]
2278    rw [realTheory.REAL_SUB, bitTheory.SUC_SUB, DECIDE ``~(SUC n <= n)``,
2336       rw []
2337       \\ rw [float_to_real_def, abs_float_value, abs_significand,
2366       rw []
2367       \\ rw [float_to_real_def, abs_float_value, abs_significand,
2393       rw []
2394       \\ rw [float_to_real_def, abs_float_value, abs_significand,
2413    >- rw [GSYM neg_ulp, GSYM ulp, float_minus_min_def, float_components,
2417    \\ rw [float_to_real_def, ULP_def, abs_float_value, abs_significand,
2523    rw [exponent_boundary_def, float_is_zero]
2531    rw [ULP_def, float_to_real_def, abs_float_value, abs_significand,
2566    \\ rw []
2570       \\ rw [Float_is_finite]
2630    rw [ULP_def]
2644    rw [exponent_boundary_def, wordsTheory.WORD_LO]
2687    \\ rw []
2692       \\ rw []
2825    \\ rw []
2830       \\ rw []
2838             \\ rw [pow_add1, realTheory.mult_ratr]
2916        \\ rw [float_is_zero]
2982    \\ rw []
3007    rw [float_plus_min_def, float_negate_def, ulp_def, ULP_def,
3067    rw [float_plus_min_def, float_negate_def]
3081    \\ rw []
3086       \\ rw [float_plus_zero_def]
3432   rw [largest, threshold, realTheory.REAL_LT_RDIV, realTheory.REAL_LT_LMUL,
3460    rw [float_is_nan_def, float_is_signalling_def, float_is_infinite_def,
3463    \\ rw [float_sets, float_minus_zero_def, float_plus_zero_def,
3478     rw [float_plus_infinity_def, float_minus_infinity_def,
3765    rw [float_mul_def, float_values]
3781    rw [float_mul_def, float_values]
3797    rw [float_mul_def, float_values]
3814    rw [float_mul_def, float_values]
3898    rw [float_div_def, float_values]
3910    rw [float_div_def, float_values]
3922    rw [float_div_def, float_values]
3935    rw [float_div_def, float_values]