author immler Fri, 26 Feb 2016 11:53:45 +0100 changeset 62421 28d2c75dd180 parent 62420 c7666166c24e child 62426 bd650e3a210f
finite precision computation to determine sign for comparison
 src/HOL/Library/Float.thy file | annotate | diff | comparison | revisions
```--- 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

```