--- 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)
--- 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"