# HG changeset patch
# User hoelzl
# Date 1305920312 -7200
# Node ID 4aedcff42de6450e65aa04e98551aa3bbec79fdf
# Parent  ec9eb1fbfcb88e3c08c9532ea09a5aa81046337e
add divide_.._cancel, inverse_.._iff

diff -r ec9eb1fbfcb8 -r 4aedcff42de6 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri May 20 21:38:32 2011 +0200
+++ b/src/HOL/Fields.thy	Fri May 20 21:38:32 2011 +0200
@@ -831,6 +831,39 @@
   apply (auto simp add: mult_commute)
 done
 
+lemma inverse_le_iff:
+  "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
+proof -
+  { assume "a < 0"
+    then have "inverse a < 0" by simp
+    moreover assume "0 < b"
+    then have "0 < inverse b" by simp
+    ultimately have "inverse a < inverse b" by (rule less_trans)
+    then have "inverse a \<le> inverse b" by simp }
+  moreover
+  { assume "b < 0"
+    then have "inverse b < 0" by simp
+    moreover assume "0 < a"
+    then have "0 < inverse a" by simp
+    ultimately have "inverse b < inverse a" by (rule less_trans)
+    then have "\<not> inverse a \<le> inverse b" by simp }
+  ultimately show ?thesis
+    by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
+       (auto simp: not_less zero_less_mult_iff mult_le_0_iff)
+qed
+
+lemma inverse_less_iff:
+  "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
+  by (subst less_le) (auto simp: inverse_le_iff)
+
+lemma divide_le_cancel:
+  "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
+  by (simp add: divide_inverse mult_le_cancel_right)
+
+lemma divide_less_cancel:
+  "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
+  by (auto simp add: divide_inverse mult_less_cancel_right)
+
 text{*Simplify quotients that are compared with the value 1.*}
 
 lemma le_divide_eq_1 [no_atp]: