--- a/src/HOL/Library/Float.thy Fri Feb 26 11:53:45 2016 +0100
+++ b/src/HOL/Library/Float.thy Fri Feb 26 11:53:45 2016 +0100
@@ -578,17 +578,11 @@
qualified lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
-qualified lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)"
- by transfer (simp add: field_simps)
-
lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" .
qualified lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
-qualified lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)"
- by transfer (simp add: field_simps)
-
lift_definition is_float_zero :: "float \<Rightarrow> bool" is "op = 0 :: real \<Rightarrow> bool" .
qualified lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
@@ -1905,6 +1899,14 @@
lemma mantissa_zero[simp]: "mantissa 0 = 0"
by (metis mantissa_0 zero_float.abs_eq)
+qualified lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (float_plus_down 0 b (- a))"
+ using truncate_down[of 0 "b - a"] truncate_down_pos[of "b - a" 0]
+ by transfer (auto simp: plus_down_def)
+
+qualified lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (float_plus_down 0 b (- a))"
+ using truncate_down[of 0 "b - a"] truncate_down_nonneg[of "b - a" 0]
+ by transfer (auto simp: plus_down_def)
+
end