diff --git a/basis/DoubleProgScript.sml b/basis/DoubleProgScript.sml
index b0021d4277..8caa1962e1 100644
--- a/basis/DoubleProgScript.sml
+++ b/basis/DoubleProgScript.sml
@@ -6,9 +6,10 @@
 *)
 Theory DoubleProg
 Ancestors
-  words CommandLineProg
+  words CommandLineProg machine_ieee binary_ieee binary_ieeeProps real
 Libs
-  preamble ml_translatorLib ml_progLib basisFunctionsLib
+  preamble ml_translatorLib ml_progLib basisFunctionsLib realSimps[qualified]
+  RealArith
 
 val _ = translation_extends "CommandLineProg";
 
@@ -287,6 +288,477 @@ val _ = append_prog $ monop “"abs"” “FP_Abs”;
 val _ = append_prog $ monop “"sqrt"” “FP_Sqrt”;
 val _ = append_prog $ monop “"~"” “FP_Neg”;
 
+(* ----------------------------------------------------------------------
+    Taking floats apart
+   ---------------------------------------------------------------------- *)
+
+Type float64 = “:(52,11)float”
+
+Definition significand_def:
+  significand f = float_to_fp64 f && 0xFFFFFFFFFFFFFw
+End
+
+Theorem significand_correct:
+  significand f = w2w (f.Significand)
+Proof
+  simp[machine_ieeeTheory.float_to_fp64_def, significand_def, word_concat_def,
+       word_join_def, word_bits_w2w, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, WORD_ALL_BITS, w2w_w2w, GSYM WORD_w2w_OVER_BITWISE,
+       WORD_LEFT_AND_OVER_OR, w2w_LSL, word_and_lsl_eq_0] >>
+  ‘0xFFFFFFFFFFFFFw : word64 = w2w (UINT_MAXw : 52 word)’
+    by (ONCE_REWRITE_TAC[EQ_SYM_EQ] >> simp[w2w_eq_n2w]) >>
+  pop_assum SUBST1_TAC >>
+  simp[WORD_w2w_OVER_BITWISE]
+QED
+
+Theorem significand_correct':
+  f.Significand = w2w (significand f)
+Proof
+  simp[machine_ieeeTheory.float_to_fp64_def, significand_def, word_concat_def,
+       word_join_def, word_bits_w2w, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, WORD_ALL_BITS, w2w_w2w, GSYM WORD_w2w_OVER_BITWISE,
+       WORD_LEFT_AND_OVER_OR, w2w_LSL, word_and_lsl_eq_0]
+QED
+
+Definition exponent_def:
+  exponent f = (float_to_fp64 f >>> 52) && 0x7FFw
+End
+
+Theorem exponent_correct:
+  exponent f = w2w f.Exponent
+Proof
+  simp[machine_ieeeTheory.float_to_fp64_def, exponent_def, word_concat_def,
+       word_join_def, word_bits_w2w, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, WORD_ALL_BITS, w2w_w2w, GSYM WORD_w2w_OVER_BITWISE,
+       WORD_LEFT_AND_OVER_OR, w2w_LSL, word_and_lsl_eq_0, lsl_lsr,
+       LSR_LIMIT, word_lsr_n2w, WORD_BITS_ZERO3] >>
+  ‘2047w : word64 = w2w (UINT_MAXw : 11 word)’
+    by (ONCE_REWRITE_TAC[EQ_SYM_EQ] >> simp[w2w_eq_n2w]) >>
+  pop_assum SUBST1_TAC >>
+  simp[WORD_w2w_OVER_BITWISE]
+QED
+
+Theorem exponent_correct':
+  f.Exponent = w2w (exponent f)
+Proof
+  simp[machine_ieeeTheory.float_to_fp64_def, exponent_def, word_concat_def,
+       word_join_def, word_bits_w2w, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, WORD_ALL_BITS, w2w_w2w, GSYM WORD_w2w_OVER_BITWISE,
+       WORD_LEFT_AND_OVER_OR, w2w_LSL, word_and_lsl_eq_0, lsl_lsr,
+       LSR_LIMIT, word_lsr_n2w, WORD_BITS_ZERO3]
+QED
+
+Definition sign_def:
+  sign f = (float_to_fp64 f >>> 63) && 1w
+End
+
+Theorem sign_correct:
+  sign f = w2w f.Sign
+Proof
+  simp[machine_ieeeTheory.float_to_fp64_def, sign_def, word_concat_def,
+       word_join_def, word_bits_w2w, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, WORD_ALL_BITS, w2w_w2w, GSYM WORD_w2w_OVER_BITWISE,
+       WORD_LEFT_AND_OVER_OR, w2w_LSL, word_and_lsl_eq_0, lsl_lsr,
+       LSR_LIMIT, word_lsr_n2w, WORD_BITS_ZERO3] >>
+  ‘1w : word64 = w2w (UINT_MAXw : word1)’
+    by (ONCE_REWRITE_TAC[EQ_SYM_EQ] >> simp[w2w_eq_n2w]) >>
+  pop_assum SUBST1_TAC >>
+  simp[WORD_w2w_OVER_BITWISE]
+QED
+
+Theorem sign_correct':
+  f.Sign = w2w (sign f)
+Proof
+  simp[machine_ieeeTheory.float_to_fp64_def, sign_def, word_concat_def,
+       word_join_def, word_bits_w2w, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, WORD_ALL_BITS, w2w_w2w, GSYM WORD_w2w_OVER_BITWISE,
+       WORD_LEFT_AND_OVER_OR, w2w_LSL, word_and_lsl_eq_0, lsl_lsr,
+       LSR_LIMIT, word_lsr_n2w, WORD_BITS_ZERO3] >>
+  ‘1w : word1 = UINT_MAXw : word1’
+    by (ONCE_REWRITE_TAC[EQ_SYM_EQ] >> simp[w2w_eq_n2w]) >>
+  pop_assum SUBST1_TAC >>
+  simp[WORD_AND_CLAUSES]
+QED
+
+val _ = translate significand_def
+val _ = translate exponent_def
+val _ = translate sign_def
+
+(* ----------------------------------------------------------------------
+    Putting a float together from its constituent parts (layout order)
+   ---------------------------------------------------------------------- *)
+
+Definition construct_def:
+  construct (sgn:word64) (exp:word64) (sgf:word64) =
+    fp64_to_float (
+      ((sgn && 1w) << 63) ||
+      ((exp && 0x7FFw) << 52) ||
+      (sgf && 0xFFFFFFFFFFFFFw)
+    )
+End
+
+Theorem w2w'_11 = w2w_w2w |> GSYM |> INST_TYPE [beta |-> “:11”] |> SRULE[]
+Theorem w2w'_52 = w2w_w2w |> GSYM |> INST_TYPE [beta |-> “:52”] |> SRULE[]
+Theorem w2w'_01 = w2w_w2w |> GSYM |> INST_TYPE [beta |-> “:1”] |> SRULE[]
+
+Theorem w2w_range_11 =
+        word_bits_w2w |> INST_TYPE [alpha |-> “:64”, beta |-> “:11”]
+                      |> SPEC_ALL |> Q.INST [‘h’ |-> ‘10’, ‘l’ |-> ‘0’]
+                      |> SRULE[WORD_ALL_BITS] |> SYM
+Theorem w2w_range_52 =
+        word_bits_w2w |> INST_TYPE [alpha |-> “:64”, beta |-> “:52”]
+                      |> SPEC_ALL
+                      |> Q.INST [‘h’ |-> ‘51’, ‘l’ |-> ‘0’]
+                      |> SRULE[WORD_ALL_BITS] |> SYM
+Theorem w2w_range_01 =
+        word_bits_w2w |> INST_TYPE [alpha |-> “:64”, beta |-> “:1”]
+                      |> SPEC_ALL
+                      |> Q.INST [‘h’ |-> ‘0’, ‘l’ |-> ‘0’]
+                      |> SRULE[WORD_ALL_BITS] |> SYM
+
+
+Theorem construct_correct:
+  construct sig exp sgf = <|
+    Sign := w2w sig;
+    Exponent := w2w exp;
+    Significand := w2w sgf
+  |>
+Proof
+  simp[construct_def, machine_ieeeTheory.fp64_to_float_def,
+       word_extract_def, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, GSYM WORD_w2w_OVER_BITWISE] >>
+  simp[w2w'_11, w2w'_52, w2w'_01] >>
+  ‘1w : word1 = UINT_MAXw : word1’
+    by (ONCE_REWRITE_TAC[EQ_SYM_EQ] >> simp[w2w_eq_n2w]) >>
+  pop_assum SUBST1_TAC >>
+  simp[WORD_AND_CLAUSES]
+QED
+
+Theorem construct_correct':
+  <| Sign := sig; Exponent := exp; Significand := sgf |> =
+  construct (w2w sig) (w2w exp) (w2w sgf)
+Proof
+  simp[construct_def, machine_ieeeTheory.fp64_to_float_def,
+       word_extract_def, GSYM WORD_BITS_OVER_BITWISE,
+       WORD_BITS_LSL, GSYM WORD_w2w_OVER_BITWISE,
+       w2w_range_11, w2w_range_52, w2w_range_01] >>
+  simp[w2w_w2w, WORD_ALL_BITS] >>
+  ‘1w : word1 = UINT_MAXw : word1’
+    by (ONCE_REWRITE_TAC[EQ_SYM_EQ] >> simp[w2w_eq_n2w]) >>
+  pop_assum SUBST1_TAC >>
+  simp[WORD_AND_CLAUSES]
+QED
+
+val _ = translate construct_def
+
+Definition fnext_hi_def:
+  fnext_hi f = fp64_to_float (float_to_fp64 f + 1w)
+End
+
+Definition fnext_lo_def:
+  fnext_lo f = fp64_to_float (float_to_fp64 f - 1w)
+End
+
+val _ = translate fnext_hi_def
+val _ = translate fnext_lo_def
+
+Overload f2r[local] = “float_to_real”
+Overload nl[local] = “next_lo”
+
+Theorem float_is_finite_characterisation:
+  float_is_finite f ⇔ exponent f ≠ 0x7FFw
+Proof
+  simp[binary_ieeeTheory.float_is_finite,
+       binary_ieeeTheory.float_is_subnormal_def,
+       binary_ieeeTheory.float_is_normal_def,
+       binary_ieeeTheory.float_is_zero, exponent_correct] >>
+  Cases_on ‘f.Exponent = 0w’ >> simp[w2w_eq_n2w] >>
+  ‘2047w : word11 = UINT_MAXw’ by simp[] >>
+  pop_assum SUBST1_TAC >> simp[]
+QED
+
+val _ = translate float_is_finite_characterisation
+
+Theorem float_is_zero_characterisation:
+  float_is_zero f ⇔ exponent f = 0w ∧ significand f = 0w
+Proof
+  simp[binary_ieeeTheory.float_is_zero, exponent_correct,
+       significand_correct, w2w_eq_n2w]
+QED
+
+val _ = translate float_is_zero_characterisation
+
+Definition flt_max_def:
+  flt_max = float_top(:52#11)
+End
+
+Theorem flt_max_characterisation:
+  flt_max = construct 0w 0x7FEw 0xFFFFFFFFFFFFFw
+Proof
+  simp[binary_ieeeTheory.float_top_def, construct_correct', flt_max_def]
+QED
+
+val _ = translate flt_max_characterisation
+
+Overload precision[local] = “dimindex”
+
+Definition maxulp_def:
+  maxulp : (52,11) float = <|
+    Sign := 0w; Significand := 0w;
+    Exponent := 1994w
+  |>
+End
+
+Theorem maxulp_thm:
+  maxulp = construct  0w 1994w 0w
+Proof
+  simp[maxulp_def, construct_correct, w2w_n2w]
+QED
+
+val _ = translate maxulp_thm
+
+Definition twicemaxulp_def:
+  twicemaxulp = float64_add maxulp maxulp
+End
+
+val _ = translate twicemaxulp_def
+
+Definition ffloat_ulp_def:
+  ffloat_ulp (f0:(52,11)float) =
+  let f = float64_abs f0
+  in
+    if float_is_finite f then
+      if f = flt_max then maxulp
+      else float64_sub (fnext_hi f) f
+    else
+      twicemaxulp
+End
+val _ = translate ffloat_ulp_def
+
+Definition posinf64_def:
+  posinf64 = construct 0w 0x7ffw 0w
+End
+val _ = translate posinf64_def
+
+Definition neginf64_def:
+  neginf64 = construct 1w 0x7ffw 0w
+End
+val _ = translate neginf64_def
+
+Definition posmin64_def:
+  posmin64 = fp64_to_float 1w
+End
+val _ = translate posmin64_def
+
+Definition poszero64_def:
+  poszero64 = fp64_to_float 0w
+End
+val _ = translate poszero64_def
+
+Theorem word_addR_concat:
+  FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ∧
+  w2n w2 + y < 2 ** precision(:β) ⇒
+  (w1:α word) @@ (w2:β word) + n2w y = (w1 @@ (w2 + n2w y)) : γ word
+Proof
+  simp[word_concat_def, word_join_def, w2w_def] >>
+  Cases_on ‘w2’ >> simp[] >> strip_tac >>
+  simp[word_add_n2w, word_mul_n2w, dimword_def,
+       word_T_def, dimword_def, UINT_MAX_def, WORD_MUL_LSL] >>
+  ‘n2w (w2n w1 * 2 ** precision(:β)) && n2w (n + y) : (α + β) word = 0w’
+    by (simp[word_and_n2w, dimword_def, bitTheory.BITWISE_LT_2EXP] >>
+        dep_rewrite.DEP_ONCE_REWRITE_TAC[bitTheory.BITWISE_COMM] >>
+        simp[CONJ_COMM] >>
+        irule bitTheory.BITWISE_AND_SHIFT_EQ_0 >> simp[]) >>
+  drule_then (assume_tac o SYM) WORD_ADD_OR >>
+  simp[word_add_n2w, dimword_def] >>
+  cong_tac (SOME 1) >>
+  ‘n2w (w2n w1 * 2 ** precision(:β)) && n2w n : (α + β) word = 0w’
+    by (simp[word_and_n2w, dimword_def, bitTheory.BITWISE_LT_2EXP] >>
+        dep_rewrite.DEP_ONCE_REWRITE_TAC[bitTheory.BITWISE_COMM] >>
+        simp[CONJ_COMM] >>
+        irule bitTheory.BITWISE_AND_SHIFT_EQ_0 >> simp[]) >>
+  drule_then (assume_tac o SYM) WORD_ADD_OR >>
+  simp[word_add_n2w, dimword_def, Once WORD_OR_COMM] >>
+  Cases_on ‘w1’ >> simp[] >>
+  rename [‘n1 < dimword(:α)’, ‘n2 + y  < 2 ** precision(:β)’] >>
+  ‘n2 + n1 * 2 ** precision(:β) < 2 ** precision(:α + β)’
+    by (simp[fcpTheory.index_sum] >> rw[] >>
+        simp[EXP_ADD] >> gvs[dimword_def] >>
+        irule LESS_EQ_LESS_TRANS >>
+        qexists
+        ‘(2 ** precision(:β) - 1) +
+         (2 ** precision(:α) - 1) * (2 ** precision(:β))’ >>
+        irule_at Any (DECIDE “a ≤ m ∧ b ≤ n ⇒ a + b ≤ m + n:num”) >>
+        simp[RIGHT_SUB_DISTRIB] >>
+        ‘2 ** precision(:β) ≤ 2 ** precision(:α) * 2 ** precision(:β)’
+          by simp[] >>
+        ‘1 ≤ 2 ** precision(:β)’ by simp[] >>
+        simp[DECIDE “1 ≤ x ∧ x ≤ y ⇒ x - 1n + (y - x) = y - 1”]) >>
+  simp[] >>
+  simp[fcpTheory.index_sum] >> rw[] >>
+  simp[EXP_ADD] >> gvs[dimword_def] >>
+  irule LESS_EQ_LESS_TRANS >>
+  qexists
+  ‘(2 ** precision(:β) - 1) +
+   (2 ** precision(:α) - 1) * (2 ** precision(:β))’ >>
+  irule_at Any (DECIDE “a + b ≤ m ∧ c ≤ n ⇒ a + (b + c) ≤ m + n:num”) >>
+  simp[RIGHT_SUB_DISTRIB] >>
+  ‘2 ** precision(:β) ≤ 2 ** precision(:α) * 2 ** precision(:β)’
+    by simp[] >>
+  ‘1 ≤ 2 ** precision(:β)’ by simp[] >>
+  simp[DECIDE “1 ≤ x ∧ x ≤ y ⇒ x - 1n + (y - x) = y - 1”]
+QED
+
+Theorem fp64_word_concat_assoc:
+  (w1 : unit word) @@ ((w2 : 11 word) @@ (w3 : 52 word)):63 word =
+  ((w1 @@ w2) : 12 word @@ w3) : word64
+Proof
+  ‘precision(:unit) + precision(:11) = precision(:12)’
+    by (simp[fcpTheory.finite_bit0, fcpTheory.index_bit0,
+             fcpTheory.index_bit1, fcpTheory.index_one,
+             fcpTheory.finite_bit1, fcpTheory.finite_one]) >>
+  dxrule_at_then Any irule (GSYM word_concat_assoc) >>
+  simp[fcpTheory.finite_bit0, fcpTheory.index_bit0,
+       fcpTheory.index_bit1, fcpTheory.index_one,
+       fcpTheory.finite_bit1, fcpTheory.finite_one]
+QED
+
+val _ = diminish_srw_ss [
+    "word arith", "word ground", "word logic", "word shift",
+    "word subtract", "words"
+  ]
+
+val _ = augment_srw_ss [
+    rewrites [w2n_n2w, WORD_AND_CLAUSES, n2w_11, WORD_ADD_0]
+  ]
+
+Theorem next_hi_fnext_hi:
+  float_is_finite f ⇒ next_hi f = fnext_hi f
+Proof
+  rw[next_hi_def, fnext_hi_def]
+  >- (irule (iffLR float_to_fp64_11) >>
+      simp[float_to_fp64_fp64_to_float, float_to_fp64_def,
+           fp64_word_concat_assoc] >>
+      irule (GSYM word_addR_concat) >>
+      gvs[word_T_def, UINT_MAX_def, dimword_def, fcpTheory.finite_bit0,
+          fcpTheory.finite_bit1, fcpTheory.finite_one] >>
+      Cases_on ‘f.Significand’ >>
+      gvs[dimword_def, WORD_LO_word_T, word_lo_n2w]) >>
+  irule (iffLR float_to_fp64_11) >>
+  simp[float_to_fp64_fp64_to_float, float_to_fp64_def,
+       GSYM fp64_word_concat_assoc] >>
+  Cases_on ‘f.Significand’ >> gvs[word_T_def, word_lo_n2w] >>
+  rename [‘f.Significand = n2w fS’] >> ‘fS = 4503599627370495’ by simp[] >>
+  gvs[WORD_LO_word_T, GSYM fp64_word_concat_assoc] >>
+  mp_tac $
+    Q.INST [
+      ‘w1’ |-> ‘(f:(52,11)float).Sign’, ‘y’ |-> ‘1’,
+      ‘w2’ |-> ‘((f:(52,11)float).Exponent : 11 word) @@
+                (0xFFFFFFFFFFFFFw : 52 word)’]
+       (INST_TYPE [alpha |-> “:one”, beta |-> “:63”, gamma |-> “:64”]
+                  word_addR_concat) >>
+  impl_tac
+  >- (simp[fcpTheory.finite_bit1, fcpTheory.finite_bit0] >>
+      simp[word_concat_def, w2w_def, word_join_def] >>
+      Cases_on ‘f.Exponent’ >>
+      gvs[dimword_def, float_is_finite_Exponent,
+          NOT_LESS_EQUAL] >>
+      dep_rewrite.DEP_REWRITE_TAC[GSYM WORD_ADD_OR] >>
+      ONCE_REWRITE_TAC [WORD_AND_COMM] >>
+      irule_at Any (GSYM word_and_lsl_eq_0) >> simp[] >>
+      simp[WORD_MUL_LSL, word_mul_n2w, word_add_n2w] >>
+      gvs[word_T_def, n2w_11, dimword_def]) >>
+  strip_tac >> simp[] >>
+  cong_tac (SOME 1) >>
+  simp[word_concat_def, w2w_def, word_join_def] >>
+  Cases_on ‘f.Exponent’ >>
+  gvs[dimword_def, float_is_finite_Exponent,
+      NOT_LESS_EQUAL, word_add_n2w, word_T_def] >>
+  cong_tac (SOME 1) >>
+  dep_rewrite.DEP_REWRITE_TAC[GSYM WORD_ADD_OR] >>
+  ONCE_REWRITE_TAC [WORD_AND_COMM] >> simp[] >>
+  irule_at Any word_and_lsl_eq_0 >> simp[] >>
+  simp[WORD_MUL_LSL, word_mul_n2w, word_add_n2w]
+QED
+
+Theorem next_lo_fnext_lo:
+  float_is_finite f ∧ ¬float_is_zero f ⇒ next_lo f = fnext_lo f
+Proof
+  rw[fnext_lo_def] >>
+  ‘next_hi (nl f) = f’ by simp[] >>
+  ‘float_is_finite (nl f)’ by simp[float_is_finite_next_lo] >>
+  dxrule_then assume_tac next_hi_fnext_hi >>
+  gvs[WORD_ADD_EQ_SUB, fnext_lo_def, fnext_hi_def] >>
+  qpat_x_assum ‘fp64_to_float _ = f’ (mp_tac o Q.AP_TERM ‘float_to_fp64’)>>
+  REWRITE_TAC[float_to_fp64_fp64_to_float] >>
+  disch_then (mp_tac o Q.AP_TERM ‘λw. w - 1w’) >> simp[WORD_ADD_SUB] >>
+  disch_then (mp_tac o Q.AP_TERM ‘fp64_to_float’) >>
+  REWRITE_TAC[fp64_to_float_float_to_fp64]
+QED
+
+Theorem maxulp_correct:
+  f2r maxulp = ulpᶠ (float_top (:52 # 11))
+Proof
+  simp[float_to_real_def, float_ulp_def, float_top_def, maxulp_def,
+       word_T_def, ULP_def, WORD_EQ_SUB_ZERO, realTheory.REAL_DIV_LZERO,
+       GSYM n2w_sub, SF realSimps.RMULRELNORM_ss, SF realSimps.RMULCANON_ss]
+QED
+
+Overload abs[local] = “realax$abs”
+
+Theorem ABS_REFL' = iffRL ABS_REFL
+
+val _ = augment_srw_ss [realSimps.REAL_ARITH_ss]
+
+Theorem abs_sub_lemma =
+        REAL_ARITH “(0 ≤ x ⇔ 0 ≤ y) ∧ abs y < abs x ⇒
+                    abs (x - y) = abs x - abs y”
+
+Theorem ffloat_ulp_correct:
+  float_is_finite f ⇒
+  float_to_real (ffloat_ulp f) = ulpᶠ f
+Proof
+  rw[ffloat_ulp_def, maxulp_correct, flt_max_def,
+     ml_translatorTheory.float64_abs_thm]
+  >- metis_tac[float_ulp_abs] >>
+  simp[GSYM next_hi_fnext_hi, ml_translatorTheory.float64_sub_thm] >>
+  drule_then assume_tac float_is_finite_float_value >>
+  ‘float_is_finite (next_hi (float_abs f))’
+    by (irule float_is_finite_next_hi >> simp[float_to_real_float_abs] >>
+        ‘abs (f2r f) ≤ largest(:52 # 11)’
+          by simp[abs_float_bounds, GSYM float_to_real_float_abs,
+                  Excl "float_to_real_float_abs"] >>
+        ‘abs (f2r f) ≠ largest(:52 # 11)’ suffices_by simp[] >>
+        strip_tac >> gvs[] >>
+        qpat_x_assum ‘x ≠ y’ mp_tac >> simp[] >>
+        gvs[largest_is_top, GSYM float_to_real_float_abs, float_to_real_eq,
+            Excl "float_to_real_float_abs"]) >>
+  ‘float_value (next_hi (float_abs f)) = Float (f2r (next_hi (float_abs f)))’
+    by simp[float_is_finite_float_value] >>
+  ‘float_value (float_abs f) = Float (f2r (float_abs f))’
+    by simp[float_is_finite_float_value] >>
+  simp[float_sub_def] >> simp[float_round_with_flags_def] >>
+  simp[float_round_def] >>
+  ‘f2r (next_hi (float_abs f)) - abs (f2r f) = ulpᶠ f’
+    by (simp[REAL_EQ_SUB_RADD] >>
+        ONCE_REWRITE_TAC[REAL_ADD_COMM] >>
+        simp[GSYM next_hi_difference, next_hi_float_abs] >>
+        Cases_on ‘f2r f = 0’ >- simp[] >>
+        ‘abs (f2r f) < abs (f2r (next_hi f))’ by simp[next_hi_larger] >>
+        ‘0 ≤ f2r (next_hi f) ⇔ 0 ≤ f2r f’
+          by (simp[] >> ‘f ≠ NEG0’ by (strip_tac >> gvs[])>> simp[]) >>
+        simp[abs_sub_lemma]) >>
+  simp[] >>
+  rev_drule ulp_multiples_representable >> simp[] >>
+  disch_then (qspecl_then [‘ulpᶠ f’, ‘1’] mp_tac) >> simp[] >>
+  disch_then (qx_choose_then ‘uf’ assume_tac)>>
+  drule float_value_float_to_real >> disch_then (assume_tac o SYM) >> gvs[] >>
+  ‘f2r uf ≠ 0’ by metis_tac[float_ulp_EQ0] >>
+  ‘float_is_finite uf’ by simp[float_is_finite_thm] >>
+  simp[round_representable_nonzero, float_is_zero_to_real]
+QED
+
+
 (* --------------------------------------------------------------------------
  * Pretty-printer
  * ------------------------------------------------------------------------- *)
diff --git a/basis/types.txt b/basis/types.txt
index bd9e57c343..e8257a5a0b 100644
--- a/basis/types.txt
+++ b/basis/types.txt
@@ -317,6 +317,22 @@ Double.=: Double.double -> Double.double -> bool
 Double.abs: Double.double -> Double.double
 Double.sqrt: Double.double -> Double.double
 Double.~: Double.double -> Double.double
+Double.significand: Double.double -> Word64.word
+Double.exponent: Double.double -> Word64.word
+Double.sign: Double.double -> Word64.word
+Double.construct: Word64.word -> Word64.word -> Word64.word -> Double.double
+Double.fnext_hi: Double.double -> Double.double
+Double.fnext_lo: Double.double -> Double.double
+Double.float_is_finite: Double.double -> bool
+Double.float_is_zero: Double.double -> bool
+Double.flt_max: Double.double
+Double.maxulp: Double.double
+Double.twicemaxulp: Double.double
+Double.ffloat_ulp: Double.double -> Double.double
+Double.posinf64: Double.double
+Double.neginf64: Double.double
+Double.posmin64: Double.double
+Double.poszero64: Double.double
 Double.pp_double: Double.double -> PrettyPrinter.pp_data
 Marshalling.n2w2: int -> byte_array -> int -> unit
 Marshalling.w22n: byte_array -> int -> int
diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml
index 788a615efc..b4936f904c 100644
--- a/translator/ml_translatorLib.sml
+++ b/translator/ml_translatorLib.sml
@@ -2940,6 +2940,8 @@ val builtin_monops =
    Eval_FLOAT_ABS,
    Eval_FLOAT_SQRT,
    Eval_FLOAT_NEG,
+   Eval_FP_fromWord,
+   Eval_FP_toWord,
    Eval_empty_ffi,
    Eval_force_out_of_memory_error,
    Eval_Chr,
diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml
index 5ad1b4bb79..176296d303 100644
--- a/translator/ml_translatorScript.sml
+++ b/translator/ml_translatorScript.sml
@@ -440,9 +440,9 @@ Theorem EqualityType_NUM_BOOL:
   EqualityType BOOL /\ EqualityType WORD /\
   EqualityType CHAR /\ EqualityType STRING_TYPE /\
   EqualityType UNIT_TYPE /\ EqualityType HOL_STRING_TYPE /\
-  EqualityType WORD
+  EqualityType WORD /\ EqualityType FLOAT64
 Proof
-  EVAL_TAC \\ fs [no_closures_def,
+  EVAL_TAC \\ fs [no_closures_def, float_to_fp64_11,
     types_match_def, lit_same_type_def,
     stringTheory.ORD_11,mlstringTheory.explode_11]
   \\ SRW_TAC [] [] \\ EVAL_TAC