# HG changeset patch
# User immler
# Date 1456484025 -3600
# Node ID 28d2c75dd180d58818fdf3eef36d47b052357f2b
# Parent  c7666166c24ee659c9e01399ede426039c7a5aa7
finite precision computation to determine sign for comparison

diff -r c7666166c24e -r 28d2c75dd180 src/HOL/Library/Float.thy
--- 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