1.1 --- a/src/HOL/Deriv.thy Wed Apr 09 09:37:47 2014 +0200
1.2 +++ b/src/HOL/Deriv.thy Wed Apr 09 09:37:48 2014 +0200
1.3 @@ -427,7 +427,7 @@
1.4 shows "((\<lambda>x. f x / g x) has_derivative
1.5 (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)"
1.6 using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
1.7 - by (simp add: divide_inverse field_simps)
1.8 + by (simp add: field_simps)
1.9
1.10 text{*Conventional form requires mult-AC laws. Types real and complex only.*}
1.11
1.12 @@ -439,7 +439,7 @@
1.13 { fix h
1.14 have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
1.15 (f' h * g x - f x * g' h) / (g x * g x)"
1.16 - by (simp add: divide_inverse field_simps nonzero_inverse_mult_distrib x)
1.17 + by (simp add: field_simps x)
1.18 }
1.19 then show ?thesis
1.20 using has_derivative_divide [OF f g] x
1.21 @@ -728,7 +728,7 @@
1.22 (g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
1.23 ((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
1.24 by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide])
1.25 - (auto dest: has_field_derivative_imp_has_derivative simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
1.26 + (auto dest: has_field_derivative_imp_has_derivative simp: field_simps)
1.27
1.28 lemma DERIV_quotient:
1.29 "(f has_field_derivative d) (at x within s) \<Longrightarrow>
2.1 --- a/src/HOL/Fields.thy Wed Apr 09 09:37:47 2014 +0200
2.2 +++ b/src/HOL/Fields.thy Wed Apr 09 09:37:48 2014 +0200
2.3 @@ -131,7 +131,7 @@
2.4 lemma divide_zero_left [simp]: "0 / a = 0"
2.5 by (simp add: divide_inverse)
2.6
2.7 -lemma inverse_eq_divide: "inverse a = 1 / a"
2.8 +lemma inverse_eq_divide [field_simps]: "inverse a = 1 / a"
2.9 by (simp add: divide_inverse)
2.10
2.11 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
2.12 @@ -174,13 +174,11 @@
2.13 finally show ?thesis .
2.14 qed
2.15
2.16 -lemma nonzero_neg_divide_eq_eq[field_simps]:
2.17 - "b \<noteq> 0 \<Longrightarrow> -(a/b) = c \<longleftrightarrow> -a = c*b"
2.18 -using nonzero_divide_eq_eq[of b "-a" c] by (simp add: divide_minus_left)
2.19 +lemma nonzero_neg_divide_eq_eq [field_simps]: "b \<noteq> 0 \<Longrightarrow> - (a / b) = c \<longleftrightarrow> - a = c * b"
2.20 + using nonzero_divide_eq_eq[of b "-a" c] by (simp add: divide_minus_left)
2.21
2.22 -lemma nonzero_neg_divide_eq_eq2[field_simps]:
2.23 - "b \<noteq> 0 \<Longrightarrow> c = -(a/b) \<longleftrightarrow> c*b = -a"
2.24 -using nonzero_neg_divide_eq_eq[of b a c] by auto
2.25 +lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \<noteq> 0 \<Longrightarrow> c = - (a / b) \<longleftrightarrow> c * b = - a"
2.26 + using nonzero_neg_divide_eq_eq[of b a c] by auto
2.27
2.28 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
2.29 by (simp add: divide_inverse mult_assoc)
2.30 @@ -200,10 +198,18 @@
2.31 "z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z"
2.32 by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)
2.33
2.34 +lemma minus_divide_add_eq_iff [field_simps]:
2.35 + "z \<noteq> 0 \<Longrightarrow> - (x / z) + y = (- x + y * z) / z"
2.36 + by (simp add: add_divide_distrib diff_divide_eq_iff divide_minus_left)
2.37 +
2.38 lemma divide_diff_eq_iff [field_simps]:
2.39 "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
2.40 by (simp add: field_simps)
2.41
2.42 +lemma minus_divide_diff_eq_iff [field_simps]:
2.43 + "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
2.44 + by (simp add: divide_diff_eq_iff[symmetric] divide_minus_left)
2.45 +
2.46 end
2.47
2.48 class division_ring_inverse_zero = division_ring +
2.49 @@ -635,7 +641,7 @@
2.50 "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
2.51 using le_imp_inverse_le [of a 1, unfolded inverse_1] .
2.52
2.53 -lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
2.54 +lemma pos_le_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> b / c \<longleftrightarrow> a * c \<le> b"
2.55 proof -
2.56 assume less: "0<c"
2.57 hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
2.58 @@ -645,7 +651,7 @@
2.59 finally show ?thesis .
2.60 qed
2.61
2.62 -lemma neg_le_divide_eq [field_simps]: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
2.63 +lemma neg_le_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> b / c \<longleftrightarrow> b \<le> a * c"
2.64 proof -
2.65 assume less: "c<0"
2.66 hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
2.67 @@ -655,8 +661,7 @@
2.68 finally show ?thesis .
2.69 qed
2.70
2.71 -lemma pos_less_divide_eq [field_simps]:
2.72 - "0 < c ==> (a < b/c) = (a*c < b)"
2.73 +lemma pos_less_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b"
2.74 proof -
2.75 assume less: "0<c"
2.76 hence "(a < b/c) = (a*c < (b/c)*c)"
2.77 @@ -666,8 +671,7 @@
2.78 finally show ?thesis .
2.79 qed
2.80
2.81 -lemma neg_less_divide_eq [field_simps]:
2.82 - "c < 0 ==> (a < b/c) = (b < a*c)"
2.83 +lemma neg_less_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < b / c \<longleftrightarrow> b < a * c"
2.84 proof -
2.85 assume less: "c<0"
2.86 hence "(a < b/c) = ((b/c)*c < a*c)"
2.87 @@ -677,8 +681,7 @@
2.88 finally show ?thesis .
2.89 qed
2.90
2.91 -lemma pos_divide_less_eq [field_simps]:
2.92 - "0 < c ==> (b/c < a) = (b < a*c)"
2.93 +lemma pos_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> b / c < a \<longleftrightarrow> b < a * c"
2.94 proof -
2.95 assume less: "0<c"
2.96 hence "(b/c < a) = ((b/c)*c < a*c)"
2.97 @@ -688,8 +691,7 @@
2.98 finally show ?thesis .
2.99 qed
2.100
2.101 -lemma neg_divide_less_eq [field_simps]:
2.102 - "c < 0 ==> (b/c < a) = (a*c < b)"
2.103 +lemma neg_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> b / c < a \<longleftrightarrow> a * c < b"
2.104 proof -
2.105 assume less: "c<0"
2.106 hence "(b/c < a) = (a*c < (b/c)*c)"
2.107 @@ -699,7 +701,7 @@
2.108 finally show ?thesis .
2.109 qed
2.110
2.111 -lemma pos_divide_le_eq [field_simps]: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
2.112 +lemma pos_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> b / c \<le> a \<longleftrightarrow> b \<le> a * c"
2.113 proof -
2.114 assume less: "0<c"
2.115 hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
2.116 @@ -709,7 +711,7 @@
2.117 finally show ?thesis .
2.118 qed
2.119
2.120 -lemma neg_divide_le_eq [field_simps]: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
2.121 +lemma neg_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> b / c \<le> a \<longleftrightarrow> a * c \<le> b"
2.122 proof -
2.123 assume less: "c<0"
2.124 hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
2.125 @@ -719,6 +721,33 @@
2.126 finally show ?thesis .
2.127 qed
2.128
2.129 +text{* The following @{text field_simps} rules are necessary, as minus is always moved atop of
2.130 +division but we want to get rid of division. *}
2.131 +
2.132 +lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> a * c \<le> - b"
2.133 + unfolding minus_divide_left by (rule pos_le_divide_eq)
2.134 +
2.135 +lemma neg_le_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> - b \<le> a * c"
2.136 + unfolding minus_divide_left by (rule neg_le_divide_eq)
2.137 +
2.138 +lemma pos_less_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < - (b / c) \<longleftrightarrow> a * c < - b"
2.139 + unfolding minus_divide_left by (rule pos_less_divide_eq)
2.140 +
2.141 +lemma neg_less_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < - (b / c) \<longleftrightarrow> - b < a * c"
2.142 + unfolding minus_divide_left by (rule neg_less_divide_eq)
2.143 +
2.144 +lemma pos_minus_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) < a \<longleftrightarrow> - b < a * c"
2.145 + unfolding minus_divide_left by (rule pos_divide_less_eq)
2.146 +
2.147 +lemma neg_minus_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) < a \<longleftrightarrow> a * c < - b"
2.148 + unfolding minus_divide_left by (rule neg_divide_less_eq)
2.149 +
2.150 +lemma pos_minus_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> - b \<le> a * c"
2.151 + unfolding minus_divide_left by (rule pos_divide_le_eq)
2.152 +
2.153 +lemma neg_minus_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> a * c \<le> - b"
2.154 + unfolding minus_divide_left by (rule neg_divide_le_eq)
2.155 +
2.156 lemma frac_less_eq:
2.157 "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0"
2.158 by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )
2.159 @@ -897,15 +926,6 @@
2.160 class linordered_field_inverse_zero = linordered_field + field_inverse_zero
2.161 begin
2.162
2.163 -lemma le_divide_eq:
2.164 - "(a \<le> b/c) =
2.165 - (if 0 < c then a*c \<le> b
2.166 - else if c < 0 then b \<le> a*c
2.167 - else a \<le> 0)"
2.168 -apply (cases "c=0", simp)
2.169 -apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
2.170 -done
2.171 -
2.172 lemma inverse_positive_iff_positive [simp]:
2.173 "(0 < inverse a) = (0 < a)"
2.174 apply (cases "a = 0", simp)
2.175 @@ -926,26 +946,11 @@
2.176 "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
2.177 by (simp add: not_less [symmetric])
2.178
2.179 -lemma one_less_inverse_iff:
2.180 - "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
2.181 -proof cases
2.182 - assume "0 < x"
2.183 - with inverse_less_iff_less [OF zero_less_one, of x]
2.184 - show ?thesis by simp
2.185 -next
2.186 - assume notless: "~ (0 < x)"
2.187 - have "~ (1 < inverse x)"
2.188 - proof
2.189 - assume *: "1 < inverse x"
2.190 - also from notless and * have "... \<le> 0" by simp
2.191 - also have "... < 1" by (rule zero_less_one)
2.192 - finally show False by auto
2.193 - qed
2.194 - with notless show ?thesis by simp
2.195 -qed
2.196 +lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
2.197 + using less_trans[of 1 x 0 for x]
2.198 + by (cases x 0 rule: linorder_cases) (auto simp add: field_simps)
2.199
2.200 -lemma one_le_inverse_iff:
2.201 - "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
2.202 +lemma one_le_inverse_iff: "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
2.203 proof (cases "x = 1")
2.204 case True then show ?thesis by simp
2.205 next
2.206 @@ -955,78 +960,37 @@
2.207 with False show ?thesis by (auto simp add: one_less_inverse_iff)
2.208 qed
2.209
2.210 -lemma inverse_less_1_iff:
2.211 - "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
2.212 +lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
2.213 by (simp add: not_le [symmetric] one_le_inverse_iff)
2.214
2.215 -lemma inverse_le_1_iff:
2.216 - "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
2.217 +lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
2.218 by (simp add: not_less [symmetric] one_less_inverse_iff)
2.219
2.220 -lemma divide_le_eq:
2.221 - "(b/c \<le> a) =
2.222 - (if 0 < c then b \<le> a*c
2.223 - else if c < 0 then a*c \<le> b
2.224 - else 0 \<le> a)"
2.225 -apply (cases "c=0", simp)
2.226 -apply (force simp add: pos_divide_le_eq neg_divide_le_eq)
2.227 -done
2.228 -
2.229 -lemma less_divide_eq:
2.230 - "(a < b/c) =
2.231 - (if 0 < c then a*c < b
2.232 - else if c < 0 then b < a*c
2.233 - else a < 0)"
2.234 -apply (cases "c=0", simp)
2.235 -apply (force simp add: pos_less_divide_eq neg_less_divide_eq)
2.236 -done
2.237 -
2.238 -lemma divide_less_eq:
2.239 - "(b/c < a) =
2.240 - (if 0 < c then b < a*c
2.241 - else if c < 0 then a*c < b
2.242 - else 0 < a)"
2.243 -apply (cases "c=0", simp)
2.244 -apply (force simp add: pos_divide_less_eq neg_divide_less_eq)
2.245 -done
2.246 +lemma
2.247 + 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)"
2.248 + 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)"
2.249 + 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)"
2.250 + 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)"
2.251 + by (auto simp: field_simps not_less dest: antisym)
2.252
2.253 text {*Division and Signs*}
2.254
2.255 -lemma zero_less_divide_iff:
2.256 - "(0 < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
2.257 -by (simp add: divide_inverse zero_less_mult_iff)
2.258 -
2.259 -lemma divide_less_0_iff:
2.260 - "(a/b < 0) =
2.261 - (0 < a & b < 0 | a < 0 & 0 < b)"
2.262 -by (simp add: divide_inverse mult_less_0_iff)
2.263 -
2.264 -lemma zero_le_divide_iff:
2.265 - "(0 \<le> a/b) =
2.266 - (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
2.267 -by (simp add: divide_inverse zero_le_mult_iff)
2.268 -
2.269 -lemma divide_le_0_iff:
2.270 - "(a/b \<le> 0) =
2.271 - (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
2.272 -by (simp add: divide_inverse mult_le_0_iff)
2.273 +lemma
2.274 + shows zero_less_divide_iff: "0 < a / b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
2.275 + and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
2.276 + 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"
2.277 + 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"
2.278 + by (simp_all add: divide_inverse zero_less_mult_iff mult_less_0_iff zero_le_mult_iff mult_le_0_iff)
2.279
2.280 text {* Division and the Number One *}
2.281
2.282 text{*Simplify expressions equated with 1*}
2.283
2.284 -lemma zero_eq_1_divide_iff [simp]:
2.285 - "(0 = 1/a) = (a = 0)"
2.286 -apply (cases "a=0", simp)
2.287 -apply (auto simp add: nonzero_eq_divide_eq)
2.288 -done
2.289 +lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a \<longleftrightarrow> a = 0"
2.290 + by (cases "a = 0") (auto simp: field_simps)
2.291
2.292 -lemma one_divide_eq_0_iff [simp]:
2.293 - "(1/a = 0) = (a = 0)"
2.294 -apply (cases "a=0", simp)
2.295 -apply (insert zero_neq_one [THEN not_sym])
2.296 -apply (auto simp add: nonzero_divide_eq_eq)
2.297 -done
2.298 +lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0"
2.299 + using zero_eq_1_divide_iff[of a] by simp
2.300
2.301 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
2.302
2.303 @@ -1062,37 +1026,17 @@
2.304 apply (auto simp add: mult_commute)
2.305 done
2.306
2.307 -lemma inverse_le_iff:
2.308 - "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
2.309 -proof -
2.310 - { assume "a < 0"
2.311 - then have "inverse a < 0" by simp
2.312 - moreover assume "0 < b"
2.313 - then have "0 < inverse b" by simp
2.314 - ultimately have "inverse a < inverse b" by (rule less_trans)
2.315 - then have "inverse a \<le> inverse b" by simp }
2.316 - moreover
2.317 - { assume "b < 0"
2.318 - then have "inverse b < 0" by simp
2.319 - moreover assume "0 < a"
2.320 - then have "0 < inverse a" by simp
2.321 - ultimately have "inverse b < inverse a" by (rule less_trans)
2.322 - then have "\<not> inverse a \<le> inverse b" by simp }
2.323 - ultimately show ?thesis
2.324 - by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
2.325 - (auto simp: not_less zero_less_mult_iff mult_le_0_iff)
2.326 -qed
2.327 +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)"
2.328 + by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
2.329 + (auto simp add: field_simps zero_less_mult_iff mult_le_0_iff)
2.330
2.331 -lemma inverse_less_iff:
2.332 - "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
2.333 +lemma inverse_less_iff: "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
2.334 by (subst less_le) (auto simp: inverse_le_iff)
2.335
2.336 -lemma divide_le_cancel:
2.337 - "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
2.338 +lemma divide_le_cancel: "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
2.339 by (simp add: divide_inverse mult_le_cancel_right)
2.340
2.341 -lemma divide_less_cancel:
2.342 - "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
2.343 +lemma divide_less_cancel: "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
2.344 by (auto simp add: divide_inverse mult_less_cancel_right)
2.345
2.346 text{*Simplify quotients that are compared with the value 1.*}
3.1 --- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 09 09:37:47 2014 +0200
3.2 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 09 09:37:48 2014 +0200
3.3 @@ -2006,17 +2006,8 @@
3.4
3.5 *)
3.6 lemma eq_divide_imp':
3.7 - assumes c0: "(c::'a::field) \<noteq> 0"
3.8 - and eq: "a * c = b"
3.9 - shows "a = b / c"
3.10 -proof -
3.11 - from eq have "a * c * inverse c = b * inverse c"
3.12 - by simp
3.13 - then have "a * (inverse c * c) = b/c"
3.14 - by (simp only: field_simps divide_inverse)
3.15 - then show "a = b/c"
3.16 - unfolding field_inverse[OF c0] by simp
3.17 -qed
3.18 + fixes c :: "'a::field" shows "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
3.19 + by (simp add: field_simps)
3.20
3.21 lemma radical_unique:
3.22 assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"
4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 09 09:37:47 2014 +0200
4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 09 09:37:48 2014 +0200
4.3 @@ -5964,10 +5964,10 @@
4.4 by (auto simp add: field_simps)
4.5 then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
4.6 "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
4.7 - by (auto simp add:field_simps) }
4.8 + using `0<d` by (auto simp add: field_simps) }
4.9 then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
4.10 unfolding mem_box using assms
4.11 - by (auto simp add: field_simps inner_simps)
4.12 + by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
4.13 then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
4.14 apply -
4.15 apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
5.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 09 09:37:47 2014 +0200
5.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 09 09:37:48 2014 +0200
5.3 @@ -569,12 +569,8 @@
5.4 unfolding real_of_nat_def by (rule ex_le_of_nat)
5.5
5.6 lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
5.7 - using reals_Archimedean
5.8 - apply (auto simp add: field_simps)
5.9 - apply (subgoal_tac "inverse (real n) > 0")
5.10 - apply arith
5.11 - apply simp
5.12 - done
5.13 + using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
5.14 + by (auto simp add: field_simps cong: conj_cong)
5.15
5.16 lemma real_pow_lbound: "0 \<le> x \<Longrightarrow> 1 + real n * x \<le> (1 + x) ^ n"
5.17 proof (induct n)
5.18 @@ -629,7 +625,7 @@
5.19 from real_arch_pow[OF ix, of "1/y"]
5.20 obtain n where n: "1/y < (1/x)^n" by blast
5.21 then show ?thesis using y `x > 0`
5.22 - by (auto simp add: field_simps power_divide)
5.23 + by (auto simp add: field_simps)
5.24 next
5.25 case False
5.26 with y x1 show ?thesis
5.27 @@ -1147,7 +1143,7 @@
5.28 using fS SP vS by auto
5.29 have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =
5.30 setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
5.31 - using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps)
5.32 + using fS vS uv by (simp add: setsum_diff1 field_simps)
5.33 also have "\<dots> = ?a"
5.34 unfolding scaleR_right.setsum [symmetric] u using uv by simp
5.35 finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
6.1 --- a/src/HOL/Power.thy Wed Apr 09 09:37:47 2014 +0200
6.2 +++ b/src/HOL/Power.thy Wed Apr 09 09:37:48 2014 +0200
6.3 @@ -108,7 +108,7 @@
6.4 context comm_monoid_mult
6.5 begin
6.6
6.7 -lemma power_mult_distrib:
6.8 +lemma power_mult_distrib [field_simps]:
6.9 "(a * b) ^ n = (a ^ n) * (b ^ n)"
6.10 by (induct n) (simp_all add: mult_ac)
6.11
6.12 @@ -661,7 +661,7 @@
6.13 "1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n"
6.14 by (simp add: divide_inverse) (rule power_inverse)
6.15
6.16 -lemma power_divide:
6.17 +lemma power_divide [field_simps]:
6.18 "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
6.19 apply (cases "b = 0")
6.20 apply (simp add: power_0_left)
7.1 --- a/src/HOL/Rings.thy Wed Apr 09 09:37:47 2014 +0200
7.2 +++ b/src/HOL/Rings.thy Wed Apr 09 09:37:48 2014 +0200
7.3 @@ -830,22 +830,12 @@
7.4 then show "a * b \<noteq> 0" by (simp add: neq_iff)
7.5 qed
7.6
7.7 -lemma zero_less_mult_iff:
7.8 - "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
7.9 - apply (auto simp add: mult_pos_pos mult_neg_neg)
7.10 - apply (simp_all add: not_less le_less)
7.11 - apply (erule disjE) apply assumption defer
7.12 - apply (erule disjE) defer apply (drule sym) apply simp
7.13 - apply (erule disjE) defer apply (drule sym) apply simp
7.14 - apply (erule disjE) apply assumption apply (drule sym) apply simp
7.15 - apply (drule sym) apply simp
7.16 - apply (blast dest: zero_less_mult_pos)
7.17 - apply (blast dest: zero_less_mult_pos2)
7.18 - done
7.19 +lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
7.20 + by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
7.21 + (auto simp add: mult_pos_pos mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
7.22
7.23 -lemma zero_le_mult_iff:
7.24 - "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
7.25 -by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
7.26 +lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
7.27 + by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
7.28
7.29 lemma mult_less_0_iff:
7.30 "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
8.1 --- a/src/HOL/Set_Interval.thy Wed Apr 09 09:37:47 2014 +0200
8.2 +++ b/src/HOL/Set_Interval.thy Wed Apr 09 09:37:48 2014 +0200
8.3 @@ -1594,13 +1594,7 @@
8.4 proof -
8.5 from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
8.6 moreover have "(\<Sum>i<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
8.7 - proof (induct n)
8.8 - case 0 then show ?case by simp
8.9 - next
8.10 - case (Suc n)
8.11 - moreover from Suc `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
8.12 - ultimately show ?case by (simp add: field_simps divide_inverse)
8.13 - qed
8.14 + by (induct n) (simp_all add: field_simps `y \<noteq> 0`)
8.15 ultimately show ?thesis by simp
8.16 qed
8.17