times_divide_eq rules are already [simp] despite of comment
authorhaftmann
Sun Feb 15 17:01:22 2015 +0100 (2015-02-15)
changeset 595463850a2d20f19
parent 59545 12a6088ed195
child 59547 239bf09ee36f
times_divide_eq rules are already [simp] despite of comment
src/HOL/Fields.thy
     1.1 --- a/src/HOL/Fields.thy	Sun Feb 15 17:01:22 2015 +0100
     1.2 +++ b/src/HOL/Fields.thy	Sun Feb 15 17:01:22 2015 +0100
     1.3 @@ -346,13 +346,6 @@
     1.4  lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
     1.5    by (simp add: divide_inverse ac_simps)
     1.6  
     1.7 -text{*It's not obvious whether @{text times_divide_eq} should be
     1.8 -  simprules or not. Their effect is to gather terms into one big
     1.9 -  fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
    1.10 -  many proofs seem to need them.*}
    1.11 -
    1.12 -lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
    1.13 -
    1.14  lemma add_frac_eq:
    1.15    assumes "y \<noteq> 0" and "z \<noteq> 0"
    1.16    shows "x / y + w / z = (x * z + w * y) / (y * z)"
    1.17 @@ -682,83 +675,91 @@
    1.18    "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
    1.19    using le_imp_inverse_le [of a 1, unfolded inverse_1] .
    1.20  
    1.21 -lemma pos_le_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> b / c \<longleftrightarrow> a * c \<le> b"
    1.22 +lemma pos_le_divide_eq [field_simps]:
    1.23 +  assumes "0 < c"
    1.24 +  shows "a \<le> b / c \<longleftrightarrow> a * c \<le> b"
    1.25  proof -
    1.26 -  assume less: "0<c"
    1.27 -  hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
    1.28 -    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
    1.29 -  also have "... = (a*c \<le> b)"
    1.30 -    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) 
    1.31 +  from assms have "a \<le> b / c \<longleftrightarrow> a * c \<le> (b / c) * c"
    1.32 +    using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps)
    1.33 +  also have "... \<longleftrightarrow> a * c \<le> b"
    1.34 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
    1.35    finally show ?thesis .
    1.36  qed
    1.37  
    1.38 -lemma neg_le_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> b / c \<longleftrightarrow> b \<le> a * c"
    1.39 +lemma pos_less_divide_eq [field_simps]:
    1.40 +  assumes "0 < c"
    1.41 +  shows "a < b / c \<longleftrightarrow> a * c < b"
    1.42  proof -
    1.43 -  assume less: "c<0"
    1.44 -  hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
    1.45 -    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
    1.46 -  also have "... = (b \<le> a*c)"
    1.47 -    by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) 
    1.48 +  from assms have "a < b / c \<longleftrightarrow> a * c < (b / c) * c"
    1.49 +    using mult_less_cancel_right [of a c "b / c"] by auto
    1.50 +  also have "... = (a*c < b)"
    1.51 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
    1.52    finally show ?thesis .
    1.53  qed
    1.54  
    1.55 -lemma pos_less_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b"
    1.56 +lemma neg_less_divide_eq [field_simps]:
    1.57 +  assumes "c < 0"
    1.58 +  shows "a < b / c \<longleftrightarrow> b < a * c"
    1.59  proof -
    1.60 -  assume less: "0<c"
    1.61 -  hence "(a < b/c) = (a*c < (b/c)*c)"
    1.62 -    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
    1.63 -  also have "... = (a*c < b)"
    1.64 -    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) 
    1.65 +  from assms have "a < b / c \<longleftrightarrow> (b / c) * c < a * c"
    1.66 +    using mult_less_cancel_right [of "b / c" c a] by auto
    1.67 +  also have "... \<longleftrightarrow> b < a * c"
    1.68 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
    1.69    finally show ?thesis .
    1.70  qed
    1.71  
    1.72 -lemma neg_less_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < b / c \<longleftrightarrow> b < a * c"
    1.73 +lemma neg_le_divide_eq [field_simps]:
    1.74 +  assumes "c < 0"
    1.75 +  shows "a \<le> b / c \<longleftrightarrow> b \<le> a * c"
    1.76  proof -
    1.77 -  assume less: "c<0"
    1.78 -  hence "(a < b/c) = ((b/c)*c < a*c)"
    1.79 -    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
    1.80 -  also have "... = (b < a*c)"
    1.81 -    by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) 
    1.82 +  from assms have "a \<le> b / c \<longleftrightarrow> (b / c) * c \<le> a * c"
    1.83 +    using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps)
    1.84 +  also have "... \<longleftrightarrow> b \<le> a * c"
    1.85 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
    1.86    finally show ?thesis .
    1.87  qed
    1.88  
    1.89 -lemma pos_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> b / c < a \<longleftrightarrow> b < a * c"
    1.90 +lemma pos_divide_le_eq [field_simps]:
    1.91 +  assumes "0 < c"
    1.92 +  shows "b / c \<le> a \<longleftrightarrow> b \<le> a * c"
    1.93  proof -
    1.94 -  assume less: "0<c"
    1.95 -  hence "(b/c < a) = ((b/c)*c < a*c)"
    1.96 -    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
    1.97 -  also have "... = (b < a*c)"
    1.98 -    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) 
    1.99 +  from assms have "b / c \<le> a \<longleftrightarrow> (b / c) * c \<le> a * c"
   1.100 +    using mult_le_cancel_right [of "b / c" c a] by auto
   1.101 +  also have "... \<longleftrightarrow> b \<le> a * c"
   1.102 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
   1.103    finally show ?thesis .
   1.104  qed
   1.105  
   1.106 -lemma neg_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> b / c < a \<longleftrightarrow> a * c < b"
   1.107 +lemma pos_divide_less_eq [field_simps]:
   1.108 +  assumes "0 < c"
   1.109 +  shows "b / c < a \<longleftrightarrow> b < a * c"
   1.110  proof -
   1.111 -  assume less: "c<0"
   1.112 -  hence "(b/c < a) = (a*c < (b/c)*c)"
   1.113 -    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   1.114 -  also have "... = (a*c < b)"
   1.115 -    by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) 
   1.116 +  from assms have "b / c < a \<longleftrightarrow> (b / c) * c < a * c"
   1.117 +    using mult_less_cancel_right [of "b / c" c a] by auto
   1.118 +  also have "... \<longleftrightarrow> b < a * c"
   1.119 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
   1.120    finally show ?thesis .
   1.121  qed
   1.122  
   1.123 -lemma pos_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> b / c \<le> a \<longleftrightarrow> b \<le> a * c"
   1.124 +lemma neg_divide_le_eq [field_simps]:
   1.125 +  assumes "c < 0"
   1.126 +  shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b"
   1.127  proof -
   1.128 -  assume less: "0<c"
   1.129 -  hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
   1.130 -    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   1.131 -  also have "... = (b \<le> a*c)"
   1.132 -    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) 
   1.133 +  from assms have "b / c \<le> a \<longleftrightarrow> a * c \<le> (b / c) * c"
   1.134 +    using mult_le_cancel_right [of a c "b / c"] by auto 
   1.135 +  also have "... \<longleftrightarrow> a * c \<le> b"
   1.136 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
   1.137    finally show ?thesis .
   1.138  qed
   1.139  
   1.140 -lemma neg_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> b / c \<le> a \<longleftrightarrow> a * c \<le> b"
   1.141 +lemma neg_divide_less_eq [field_simps]:
   1.142 +  assumes "c < 0"
   1.143 +  shows "b / c < a \<longleftrightarrow> a * c < b"
   1.144  proof -
   1.145 -  assume less: "c<0"
   1.146 -  hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
   1.147 -    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   1.148 -  also have "... = (a*c \<le> b)"
   1.149 -    by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) 
   1.150 +  from assms have "b / c < a \<longleftrightarrow> a * c < b / c * c"
   1.151 +    using mult_less_cancel_right [of a c "b / c"] by auto
   1.152 +  also have "... \<longleftrightarrow> a * c < b"
   1.153 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
   1.154    finally show ?thesis .
   1.155  qed
   1.156