author haftmann Thu, 20 Oct 2016 20:03:32 +0200 changeset 64329 8f9d27c89241 parent 64328 2284011c341a child 64330 d9a9ae3956f6
more on sgn in linear ordered fields
 src/HOL/Fields.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Fields.thy	Thu Oct 20 23:42:41 2016 +0200
+++ b/src/HOL/Fields.thy	Thu Oct 20 20:03:32 2016 +0200
@@ -976,6 +976,14 @@

subclass field_abs_sgn ..

+lemma inverse_sgn [simp]:
+  "inverse (sgn a) = sgn a"
+  by (cases a 0 rule: linorder_cases) simp_all
+
+lemma divide_sgn [simp]:
+  "a / sgn b = a * sgn b"
+  by (cases b 0 rule: linorder_cases) simp_all
+
lemma nonzero_abs_inverse:
"a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
by (rule abs_inverse)
@@ -1200,10 +1208,6 @@
lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 | b = 0)"
by (auto simp: divide_le_0_iff)

-lemma inverse_sgn:
-  "sgn (inverse a) = inverse (sgn a)"
-  by (fact sgn_inverse)
-
lemma field_le_mult_one_interval:
assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
shows "x \<le> y"```