[STATEMENT]
lemma is_finite_double_eq:
  "is_finite_Float TYPE((11, 52)float) f \<longleftrightarrow>
    (let e = Float.exponent f; bm = bitlen (abs (mantissa f))
    in (bm \<le> 53 \<and> e + bm < 1025 \<and> - 1075 < e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_finite_Float TYPE((11, 52) IEEE.float) f = (let e = Float.exponent f; bm = bitlen \<bar>mantissa f\<bar> in bm \<le> 53 \<and> e + bm < 1025 \<and> - 1075 < e)
[PROOF STEP]
unfolding is_finite_Float_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let e = Float.exponent f; bm = bitlen \<bar>mantissa f\<bar> in bm \<le> int (Suc LENGTH(52)) \<and> bm \<le> 2 ^ (LENGTH(11) - 1) - e \<and> 1 - 2 ^ (LENGTH(11) - 1) - int LENGTH(52) < e) = (let e = Float.exponent f; bm = bitlen \<bar>mantissa f\<bar> in bm \<le> 53 \<and> e + bm < 1025 \<and> - 1075 < e)
[PROOF STEP]
by (auto simp: Let_def)