# HG changeset patch
# User haftmann
# Date 1272028679 -7200
# Node ID 6984744e6b3427f4d7e489803f24b9a0c3808812
# Parent  80e3f43306cf07eed68b76ef50ec1615cbf61252
less special treatment of times_divide_eq [simp]

diff -r 80e3f43306cf -r 6984744e6b34 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Apr 23 15:17:59 2010 +0200
+++ b/src/HOL/Fields.thy	Fri Apr 23 15:17:59 2010 +0200
@@ -52,7 +52,7 @@
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
 by (simp add: mult_commute [of _ c])
 
-lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
+lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   by (simp add: divide_inverse mult_ac)
 
 text {* These are later declared as simp rules. *}
@@ -395,7 +395,7 @@
 proof -
   assume less: "0<c"
   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
-    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   also have "... = (a*c \<le> b)"
     by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -405,7 +405,7 @@
 proof -
   assume less: "c<0"
   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
-    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   also have "... = (b \<le> a*c)"
     by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -416,7 +416,7 @@
 proof -
   assume less: "0<c"
   hence "(a < b/c) = (a*c < (b/c)*c)"
-    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   also have "... = (a*c < b)"
     by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -427,7 +427,7 @@
 proof -
   assume less: "c<0"
   hence "(a < b/c) = ((b/c)*c < a*c)"
-    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   also have "... = (b < a*c)"
     by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -438,7 +438,7 @@
 proof -
   assume less: "0<c"
   hence "(b/c < a) = ((b/c)*c < a*c)"
-    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   also have "... = (b < a*c)"
     by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -449,7 +449,7 @@
 proof -
   assume less: "c<0"
   hence "(b/c < a) = (a*c < (b/c)*c)"
-    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   also have "... = (a*c < b)"
     by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -459,7 +459,7 @@
 proof -
   assume less: "0<c"
   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
-    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   also have "... = (b \<le> a*c)"
     by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -469,7 +469,7 @@
 proof -
   assume less: "c<0"
   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
-    by (simp add: mult_le_cancel_right less_not_sym [OF less])
+    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   also have "... = (a*c \<le> b)"
     by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -487,8 +487,6 @@
   pos_divide_le_eq neg_divide_le_eq
   pos_le_divide_eq neg_le_divide_eq
 
-thm field_eq_simps
-
 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
 of positivity/negativity needed for @{text field_simps}. Have not added @{text
 sign_simps} to @{text field_simps} because the former can lead to case
@@ -609,7 +607,6 @@
     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
   apply (rule mult_imp_div_pos_less)
   apply simp_all
-  apply (subst times_divide_eq_left)
   apply (rule mult_imp_less_div_pos, assumption)
   apply (erule mult_le_less_imp_less)
   apply simp_all
@@ -620,8 +617,6 @@
   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
   seem to need them.*}
 
-declare times_divide_eq [simp]
-
 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
 by (simp add: field_simps zero_less_two)
 
diff -r 80e3f43306cf -r 6984744e6b34 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Apr 23 15:17:59 2010 +0200
+++ b/src/HOL/Rings.thy	Fri Apr 23 15:17:59 2010 +0200
@@ -518,7 +518,7 @@
 lemma divide_1 [simp]: "a / 1 = a"
   by (simp add: divide_inverse)
 
-lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
+lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
   by (simp add: divide_inverse mult_assoc)
 
 lemma minus_divide_left: "- (a / b) = (-a) / b"