diff -r 093ea91498e6 -r 47500d0881f9 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Apr 09 09:37:48 2014 +0200
+++ b/src/HOL/Fields.thy	Wed Apr 09 09:37:49 2014 +0200
@@ -23,6 +23,19 @@
   fixes inverse :: "'a \<Rightarrow> 'a"
     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
 
+text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
+
+ML {*
+structure Divide_Simps = Named_Thms
+(
+  val name = @{binding divide_simps}
+  val description = "rewrite rules to eliminate divisions"
+)
+*}
+
+setup Divide_Simps.setup
+
+
 class division_ring = ring_1 + inverse +
   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
@@ -131,7 +144,7 @@
 lemma divide_zero_left [simp]: "0 / a = 0"
 by (simp add: divide_inverse)
 
-lemma inverse_eq_divide [field_simps]: "inverse a = 1 / a"
+lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a"
 by (simp add: divide_inverse)
 
 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
@@ -254,6 +267,23 @@
   "inverse a = inverse b \<longleftrightarrow> a = b"
   by (force dest!: inverse_eq_imp_eq)
 
+lemma add_divide_eq_if_simps [divide_simps]:
+    "a + b / z = (if z = 0 then a else (a * z + b) / z)"
+    "a / z + b = (if z = 0 then b else (a + b * z) / z)"
+    "- (a / z) + b = (if z = 0 then b else (-a + b * z) / z)"
+    "a - b / z = (if z = 0 then a else (a * z - b) / z)"
+    "a / z - b = (if z = 0 then -b else (a - b * z) / z)"
+    "- (a / z) - b = (if z = 0 then -b else (- a - b * z) / z)"
+  by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff
+      minus_divide_diff_eq_iff)
+
+lemma [divide_simps]:
+  shows divide_eq_eq: "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
+    and eq_divide_eq: "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
+    and minus_divide_eq_eq: "- (b / c) = a \<longleftrightarrow> (if c \<noteq> 0 then - b = a * c else a = 0)"
+    and eq_minus_divide_eq: "a = - (b / c) \<longleftrightarrow> (if c \<noteq> 0 then a * c = - b else a = 0)"
+  by (auto simp add:  field_simps)
+
 end
 
 subsection {* Fields *}
@@ -432,14 +462,6 @@
 apply (simp add: nonzero_minus_divide_divide) 
 done
 
-lemma eq_divide_eq:
-  "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
-  by (simp add: nonzero_eq_divide_eq)
-
-lemma divide_eq_eq:
-  "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
-  by (force simp add: nonzero_divide_eq_eq)
-
 lemma inverse_eq_1_iff [simp]:
   "inverse x = 1 \<longleftrightarrow> x = 1"
   by (insert inverse_eq_iff_eq [of x 1], simp) 
@@ -966,11 +988,15 @@
 lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
   by (simp add: not_less [symmetric] one_less_inverse_iff) 
 
-lemma 
+lemma [divide_simps]:
   shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)"
     and divide_le_eq: "b / c \<le> a \<longleftrightarrow> (if 0 < c then b \<le> a * c else if c < 0 then a * c \<le> b else 0 \<le> a)"
     and less_divide_eq: "a < b / c \<longleftrightarrow> (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)"
     and divide_less_eq: "b / c < a \<longleftrightarrow> (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)"
+    and le_minus_divide_eq: "a \<le> - (b / c) \<longleftrightarrow> (if 0 < c then a * c \<le> - b else if c < 0 then - b \<le> a * c else a \<le> 0)"
+    and minus_divide_le_eq: "- (b / c) \<le> a \<longleftrightarrow> (if 0 < c then - b \<le> a * c else if c < 0 then a * c \<le> - b else 0 \<le> a)"
+    and less_minus_divide_eq: "a < - (b / c) \<longleftrightarrow> (if 0 < c then a * c < - b else if c < 0 then - b < a * c else  a < 0)"
+    and minus_divide_less_eq: "- (b / c) < a \<longleftrightarrow> (if 0 < c then - b < a * c else if c < 0 then a * c < - b else 0 < a)"
   by (auto simp: field_simps not_less dest: antisym)
 
 text {*Division and Signs*}
@@ -980,7 +1006,7 @@
     and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
     and zero_le_divide_iff: "0 \<le> a / b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
     and divide_le_0_iff: "a / b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
-  by (simp_all add: divide_inverse zero_less_mult_iff mult_less_0_iff zero_le_mult_iff mult_le_0_iff)
+  by (auto simp add: divide_simps)
 
 text {* Division and the Number One *}