author  huffman 
Thu, 10 Jul 2008 07:15:19 +0200  
changeset 27516  9a5d4a8d4aac 
parent 26274  2bdb61a28971 
child 27651  16a26996c30e 
permissions  rwrr 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

1 
(* Title: HOL/Ring_and_Field.thy 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

2 
ID: $Id$ 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

3 
Author: Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel, 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

4 
with contributions by Jeremy Avigad 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

5 
*) 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

6 

14738  7 
header {* (Ordered) Rings and Fields *} 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

8 

15229  9 
theory Ring_and_Field 
15140  10 
imports OrderedGroup 
15131  11 
begin 
14504  12 

14738  13 
text {* 
14 
The theory of partially ordered rings is taken from the books: 

15 
\begin{itemize} 

16 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 

17 
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 

18 
\end{itemize} 

19 
Most of the used notions can also be looked up in 

20 
\begin{itemize} 

14770  21 
\item \url{http://www.mathworld.com} by Eric Weisstein et. al. 
14738  22 
\item \emph{Algebra I} by van der Waerden, Springer. 
23 
\end{itemize} 

24 
*} 

14504  25 

22390  26 
class semiring = ab_semigroup_add + semigroup_mult + 
25062  27 
assumes left_distrib: "(a + b) * c = a * c + b * c" 
28 
assumes right_distrib: "a * (b + c) = a * b + a * c" 

25152  29 
begin 
30 

31 
text{*For the @{text combine_numerals} simproc*} 

32 
lemma combine_common_factor: 

33 
"a * e + (b * e + c) = (a + b) * e + c" 

34 
by (simp add: left_distrib add_ac) 

35 

36 
end 

14504  37 

22390  38 
class mult_zero = times + zero + 
25062  39 
assumes mult_zero_left [simp]: "0 * a = 0" 
40 
assumes mult_zero_right [simp]: "a * 0 = 0" 

21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

41 

22390  42 
class semiring_0 = semiring + comm_monoid_add + mult_zero 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

43 

22390  44 
class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add 
25186  45 
begin 
14504  46 

25186  47 
subclass semiring_0 
48 
proof unfold_locales 

21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

49 
fix a :: 'a 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

50 
have "0 * a + 0 * a = 0 * a + 0" 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

51 
by (simp add: left_distrib [symmetric]) 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

52 
thus "0 * a = 0" 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

53 
by (simp only: add_left_cancel) 
25152  54 
next 
55 
fix a :: 'a 

21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

56 
have "a * 0 + a * 0 = a * 0 + 0" 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

57 
by (simp add: right_distrib [symmetric]) 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

58 
thus "a * 0 = 0" 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

59 
by (simp only: add_left_cancel) 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

60 
qed 
14940  61 

25186  62 
end 
25152  63 

22390  64 
class comm_semiring = ab_semigroup_add + ab_semigroup_mult + 
25062  65 
assumes distrib: "(a + b) * c = a * c + b * c" 
25152  66 
begin 
14504  67 

25152  68 
subclass semiring 
69 
proof unfold_locales 

14738  70 
fix a b c :: 'a 
71 
show "(a + b) * c = a * c + b * c" by (simp add: distrib) 

72 
have "a * (b + c) = (b + c) * a" by (simp add: mult_ac) 

73 
also have "... = b * a + c * a" by (simp only: distrib) 

74 
also have "... = a * b + a * c" by (simp add: mult_ac) 

75 
finally show "a * (b + c) = a * b + a * c" by blast 

14504  76 
qed 
77 

25152  78 
end 
14504  79 

25152  80 
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero 
81 
begin 

82 

27516  83 
subclass semiring_0 .. 
25152  84 

85 
end 

14504  86 

22390  87 
class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add 
25186  88 
begin 
14940  89 

27516  90 
subclass semiring_0_cancel .. 
14940  91 

25186  92 
end 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

93 

22390  94 
class zero_neq_one = zero + one + 
25062  95 
assumes zero_neq_one [simp]: "0 \<noteq> 1" 
26193  96 
begin 
97 

98 
lemma one_neq_zero [simp]: "1 \<noteq> 0" 

99 
by (rule not_sym) (rule zero_neq_one) 

100 

101 
end 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

102 

22390  103 
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 
14504  104 

22390  105 
class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult 
106 
(*previously almost_semiring*) 

25152  107 
begin 
14738  108 

27516  109 
subclass semiring_1 .. 
25152  110 

111 
end 

14421
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14398
diff
changeset

112 

22390  113 
class no_zero_divisors = zero + times + 
25062  114 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
14504  115 

22390  116 
class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one 
117 
+ cancel_ab_semigroup_add + monoid_mult 

25267  118 
begin 
14940  119 

27516  120 
subclass semiring_0_cancel .. 
25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

121 

27516  122 
subclass semiring_1 .. 
25267  123 

124 
end 

21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

125 

22390  126 
class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult 
127 
+ zero_neq_one + cancel_ab_semigroup_add 

25267  128 
begin 
14738  129 

27516  130 
subclass semiring_1_cancel .. 
131 
subclass comm_semiring_0_cancel .. 

132 
subclass comm_semiring_1 .. 

25267  133 

134 
end 

25152  135 

22390  136 
class ring = semiring + ab_group_add 
25267  137 
begin 
25152  138 

27516  139 
subclass semiring_0_cancel .. 
25152  140 

141 
text {* Distribution rules *} 

142 

143 
lemma minus_mult_left: " (a * b) =  a * b" 

144 
by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 

145 

146 
lemma minus_mult_right: " (a * b) = a *  b" 

147 
by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 

148 

149 
lemma minus_mult_minus [simp]: " a *  b = a * b" 

150 
by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric]) 

151 

152 
lemma minus_mult_commute: " a * b = a *  b" 

153 
by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric]) 

154 

155 
lemma right_diff_distrib: "a * (b  c) = a * b  a * c" 

156 
by (simp add: right_distrib diff_minus 

157 
minus_mult_left [symmetric] minus_mult_right [symmetric]) 

158 

159 
lemma left_diff_distrib: "(a  b) * c = a * c  b * c" 

160 
by (simp add: left_distrib diff_minus 

161 
minus_mult_left [symmetric] minus_mult_right [symmetric]) 

162 

163 
lemmas ring_distribs = 

164 
right_distrib left_distrib left_diff_distrib right_diff_distrib 

165 

25230  166 
lemmas ring_simps = 
167 
add_ac 

168 
add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 

169 
diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff 

170 
ring_distribs 

171 

172 
lemma eq_add_iff1: 

173 
"a * e + c = b * e + d \<longleftrightarrow> (a  b) * e + c = d" 

174 
by (simp add: ring_simps) 

175 

176 
lemma eq_add_iff2: 

177 
"a * e + c = b * e + d \<longleftrightarrow> c = (b  a) * e + d" 

178 
by (simp add: ring_simps) 

179 

25152  180 
end 
181 

182 
lemmas ring_distribs = 

183 
right_distrib left_distrib left_diff_distrib right_diff_distrib 

184 

22390  185 
class comm_ring = comm_semiring + ab_group_add 
25267  186 
begin 
14738  187 

27516  188 
subclass ring .. 
189 
subclass comm_semiring_0 .. 

25267  190 

191 
end 

14738  192 

22390  193 
class ring_1 = ring + zero_neq_one + monoid_mult 
25267  194 
begin 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

195 

27516  196 
subclass semiring_1_cancel .. 
25267  197 

198 
end 

25152  199 

22390  200 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
201 
(*previously ring*) 

25267  202 
begin 
14738  203 

27516  204 
subclass ring_1 .. 
205 
subclass comm_semiring_1_cancel .. 

25267  206 

207 
end 

25152  208 

22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

209 
class ring_no_zero_divisors = ring + no_zero_divisors 
25230  210 
begin 
211 

212 
lemma mult_eq_0_iff [simp]: 

213 
shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)" 

214 
proof (cases "a = 0 \<or> b = 0") 

215 
case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto 

216 
then show ?thesis using no_zero_divisors by simp 

217 
next 

218 
case True then show ?thesis by auto 

219 
qed 

220 

26193  221 
text{*Cancellation of equalities with a common factor*} 
222 
lemma mult_cancel_right [simp, noatp]: 

223 
"a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" 

224 
proof  

225 
have "(a * c = b * c) = ((a  b) * c = 0)" 

226 
by (simp add: ring_distribs right_minus_eq) 

227 
thus ?thesis 

228 
by (simp add: disj_commute right_minus_eq) 

229 
qed 

230 

231 
lemma mult_cancel_left [simp, noatp]: 

232 
"c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" 

233 
proof  

234 
have "(c * a = c * b) = (c * (a  b) = 0)" 

235 
by (simp add: ring_distribs right_minus_eq) 

236 
thus ?thesis 

237 
by (simp add: right_minus_eq) 

238 
qed 

239 

25230  240 
end 
22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

241 

23544  242 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  243 
begin 
244 

245 
lemma mult_cancel_right1 [simp]: 

246 
"c = b * c \<longleftrightarrow> c = 0 \<or> b = 1" 

247 
by (insert mult_cancel_right [of 1 c b], force) 

248 

249 
lemma mult_cancel_right2 [simp]: 

250 
"a * c = c \<longleftrightarrow> c = 0 \<or> a = 1" 

251 
by (insert mult_cancel_right [of a c 1], simp) 

252 

253 
lemma mult_cancel_left1 [simp]: 

254 
"c = c * b \<longleftrightarrow> c = 0 \<or> b = 1" 

255 
by (insert mult_cancel_left [of c 1 b], force) 

256 

257 
lemma mult_cancel_left2 [simp]: 

258 
"c * a = c \<longleftrightarrow> c = 0 \<or> a = 1" 

259 
by (insert mult_cancel_left [of c a 1], simp) 

260 

261 
end 

22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

262 

22390  263 
class idom = comm_ring_1 + no_zero_divisors 
25186  264 
begin 
14421
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14398
diff
changeset

265 

27516  266 
subclass ring_1_no_zero_divisors .. 
22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

267 

25186  268 
end 
25152  269 

22390  270 
class division_ring = ring_1 + inverse + 
25062  271 
assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
272 
assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1" 

25186  273 
begin 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

274 

25186  275 
subclass ring_1_no_zero_divisors 
276 
proof unfold_locales 

22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

277 
fix a b :: 'a 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

278 
assume a: "a \<noteq> 0" and b: "b \<noteq> 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

279 
show "a * b \<noteq> 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

280 
proof 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

281 
assume ab: "a * b = 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

282 
hence "0 = inverse a * (a * b) * inverse b" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

283 
by simp 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

284 
also have "\<dots> = (inverse a * a) * (b * inverse b)" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

285 
by (simp only: mult_assoc) 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

286 
also have "\<dots> = 1" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

287 
using a b by simp 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

288 
finally show False 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

289 
by simp 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

290 
qed 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

291 
qed 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

292 

26274  293 
lemma nonzero_imp_inverse_nonzero: 
294 
"a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0" 

295 
proof 

296 
assume ianz: "inverse a = 0" 

297 
assume "a \<noteq> 0" 

298 
hence "1 = a * inverse a" by simp 

299 
also have "... = 0" by (simp add: ianz) 

300 
finally have "1 = 0" . 

301 
thus False by (simp add: eq_commute) 

302 
qed 

303 

304 
lemma inverse_zero_imp_zero: 

305 
"inverse a = 0 \<Longrightarrow> a = 0" 

306 
apply (rule classical) 

307 
apply (drule nonzero_imp_inverse_nonzero) 

308 
apply auto 

309 
done 

310 

311 
lemma nonzero_inverse_minus_eq: 

312 
assumes "a \<noteq> 0" 

313 
shows "inverse ( a) =  inverse a" 

314 
proof  

315 
have " a * inverse ( a) =  a *  inverse a" 

316 
using assms by simp 

317 
then show ?thesis unfolding mult_cancel_left using assms by simp 

318 
qed 

319 

320 
lemma nonzero_inverse_inverse_eq: 

321 
assumes "a \<noteq> 0" 

322 
shows "inverse (inverse a) = a" 

323 
proof  

324 
have "(inverse (inverse a) * inverse a) * a = a" 

325 
using assms by (simp add: nonzero_imp_inverse_nonzero) 

326 
then show ?thesis using assms by (simp add: mult_assoc) 

327 
qed 

328 

329 
lemma nonzero_inverse_eq_imp_eq: 

330 
assumes inveq: "inverse a = inverse b" 

331 
and anz: "a \<noteq> 0" 

332 
and bnz: "b \<noteq> 0" 

333 
shows "a = b" 

334 
proof  

335 
have "a * inverse b = a * inverse a" 

336 
by (simp add: inveq) 

337 
hence "(a * inverse b) * b = (a * inverse a) * b" 

338 
by simp 

339 
then show "a = b" 

340 
by (simp add: mult_assoc anz bnz) 

341 
qed 

342 

343 
lemma inverse_1 [simp]: "inverse 1 = 1" 

344 
proof  

345 
have "inverse 1 * 1 = 1" 

346 
by (rule left_inverse) (rule one_neq_zero) 

347 
then show ?thesis by simp 

348 
qed 

349 

350 
lemma inverse_unique: 

351 
assumes ab: "a * b = 1" 

352 
shows "inverse a = b" 

353 
proof  

354 
have "a \<noteq> 0" using ab by (cases "a = 0") simp_all 

355 
moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 

356 
ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 

357 
qed 

358 

359 
lemma nonzero_inverse_mult_distrib: 

360 
assumes anz: "a \<noteq> 0" 

361 
and bnz: "b \<noteq> 0" 

362 
shows "inverse (a * b) = inverse b * inverse a" 

363 
proof  

364 
have "inverse (a * b) * (a * b) * inverse b = inverse b" 

365 
by (simp add: anz bnz) 

366 
hence "inverse (a * b) * a = inverse b" 

367 
by (simp add: mult_assoc bnz) 

368 
hence "inverse (a * b) * a * inverse a = inverse b * inverse a" 

369 
by simp 

370 
thus ?thesis 

371 
by (simp add: mult_assoc anz) 

372 
qed 

373 

374 
lemma division_ring_inverse_add: 

375 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b" 

376 
by (simp add: ring_simps mult_assoc) 

377 

378 
lemma division_ring_inverse_diff: 

379 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a  inverse b = inverse a * (b  a) * inverse b" 

380 
by (simp add: ring_simps mult_assoc) 

381 

25186  382 
end 
25152  383 

22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

384 
class field = comm_ring_1 + inverse + 
25062  385 
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
386 
assumes divide_inverse: "a / b = a * inverse b" 

25267  387 
begin 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

388 

25267  389 
subclass division_ring 
25186  390 
proof unfold_locales 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

391 
fix a :: 'a 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

392 
assume "a \<noteq> 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

393 
thus "inverse a * a = 1" by (rule field_inverse) 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

394 
thus "a * inverse a = 1" by (simp only: mult_commute) 
14738  395 
qed 
25230  396 

27516  397 
subclass idom .. 
25230  398 

399 
lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b" 

400 
proof 

401 
assume neq: "b \<noteq> 0" 

402 
{ 

403 
hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) 

404 
also assume "a / b = 1" 

405 
finally show "a = b" by simp 

406 
next 

407 
assume "a = b" 

408 
with neq show "a / b = 1" by (simp add: divide_inverse) 

409 
} 

410 
qed 

411 

412 
lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a" 

413 
by (simp add: divide_inverse) 

414 

415 
lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1" 

416 
by (simp add: divide_inverse) 

417 

418 
lemma divide_zero_left [simp]: "0 / a = 0" 

419 
by (simp add: divide_inverse) 

420 

421 
lemma inverse_eq_divide: "inverse a = 1 / a" 

422 
by (simp add: divide_inverse) 

423 

424 
lemma add_divide_distrib: "(a+b) / c = a/c + b/c" 

425 
by (simp add: divide_inverse ring_distribs) 

426 

427 
end 

428 

22390  429 
class division_by_zero = zero + inverse + 
25062  430 
assumes inverse_zero [simp]: "inverse 0 = 0" 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

431 

25230  432 
lemma divide_zero [simp]: 
433 
"a / 0 = (0::'a::{field,division_by_zero})" 

434 
by (simp add: divide_inverse) 

435 

436 
lemma divide_self_if [simp]: 

437 
"a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" 

438 
by (simp add: divide_self) 

439 

22390  440 
class mult_mono = times + zero + ord + 
25062  441 
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
442 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

443 

22390  444 
class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
25230  445 
begin 
446 

447 
lemma mult_mono: 

448 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c 

449 
\<Longrightarrow> a * c \<le> b * d" 

450 
apply (erule mult_right_mono [THEN order_trans], assumption) 

451 
apply (erule mult_left_mono, assumption) 

452 
done 

453 

454 
lemma mult_mono': 

455 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c 

456 
\<Longrightarrow> a * c \<le> b * d" 

457 
apply (rule mult_mono) 

458 
apply (fast intro: order_trans)+ 

459 
done 

460 

461 
end 

21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

462 

22390  463 
class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

464 
+ semiring + comm_monoid_add + cancel_ab_semigroup_add 
25267  465 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

466 

27516  467 
subclass semiring_0_cancel .. 
468 
subclass pordered_semiring .. 

23521  469 

25230  470 
lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b" 
471 
by (drule mult_left_mono [of zero b], auto) 

472 

473 
lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0" 

474 
by (drule mult_left_mono [of b zero], auto) 

475 

476 
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 

477 
by (drule mult_right_mono [of b zero], auto) 

478 

26234  479 
lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0)  (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
25230  480 
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) 
481 

482 
end 

483 

484 
class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono 

25267  485 
begin 
25230  486 

27516  487 
subclass pordered_cancel_semiring .. 
25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

488 

27516  489 
subclass pordered_comm_monoid_add .. 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

490 

25230  491 
lemma mult_left_less_imp_less: 
492 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

493 
by (force simp add: mult_left_mono not_le [symmetric]) 

494 

495 
lemma mult_right_less_imp_less: 

496 
"a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

497 
by (force simp add: mult_right_mono not_le [symmetric]) 

23521  498 

25186  499 
end 
25152  500 

22390  501 
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + 
25062  502 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
503 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

25267  504 
begin 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14334
diff
changeset

505 

27516  506 
subclass semiring_0_cancel .. 
14940  507 

25267  508 
subclass ordered_semiring 
25186  509 
proof unfold_locales 
23550  510 
fix a b c :: 'a 
511 
assume A: "a \<le> b" "0 \<le> c" 

512 
from A show "c * a \<le> c * b" 

25186  513 
unfolding le_less 
514 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  515 
from A show "a * c \<le> b * c" 
25152  516 
unfolding le_less 
25186  517 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  518 
qed 
519 

25230  520 
lemma mult_left_le_imp_le: 
521 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

522 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 

523 

524 
lemma mult_right_le_imp_le: 

525 
"a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

526 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 

527 

528 
lemma mult_pos_pos: 

529 
"0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b" 

530 
by (drule mult_strict_left_mono [of zero b], auto) 

531 

532 
lemma mult_pos_neg: 

533 
"0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0" 

534 
by (drule mult_strict_left_mono [of b zero], auto) 

535 

536 
lemma mult_pos_neg2: 

537 
"0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 

538 
by (drule mult_strict_right_mono [of b zero], auto) 

539 

540 
lemma zero_less_mult_pos: 

541 
"0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" 

542 
apply (cases "b\<le>0") 

543 
apply (auto simp add: le_less not_less) 

544 
apply (drule_tac mult_pos_neg [of a b]) 

545 
apply (auto dest: less_not_sym) 

546 
done 

547 

548 
lemma zero_less_mult_pos2: 

549 
"0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" 

550 
apply (cases "b\<le>0") 

551 
apply (auto simp add: le_less not_less) 

552 
apply (drule_tac mult_pos_neg2 [of a b]) 

553 
apply (auto dest: less_not_sym) 

554 
done 

555 

26193  556 
text{*Strict monotonicity in both arguments*} 
557 
lemma mult_strict_mono: 

558 
assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c" 

559 
shows "a * c < b * d" 

560 
using assms apply (cases "c=0") 

561 
apply (simp add: mult_pos_pos) 

562 
apply (erule mult_strict_right_mono [THEN less_trans]) 

563 
apply (force simp add: le_less) 

564 
apply (erule mult_strict_left_mono, assumption) 

565 
done 

566 

567 
text{*This weaker variant has more natural premises*} 

568 
lemma mult_strict_mono': 

569 
assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c" 

570 
shows "a * c < b * d" 

571 
by (rule mult_strict_mono) (insert assms, auto) 

572 

573 
lemma mult_less_le_imp_less: 

574 
assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c" 

575 
shows "a * c < b * d" 

576 
using assms apply (subgoal_tac "a * c < b * c") 

577 
apply (erule less_le_trans) 

578 
apply (erule mult_left_mono) 

579 
apply simp 

580 
apply (erule mult_strict_right_mono) 

581 
apply assumption 

582 
done 

583 

584 
lemma mult_le_less_imp_less: 

585 
assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c" 

586 
shows "a * c < b * d" 

587 
using assms apply (subgoal_tac "a * c \<le> b * c") 

588 
apply (erule le_less_trans) 

589 
apply (erule mult_strict_left_mono) 

590 
apply simp 

591 
apply (erule mult_right_mono) 

592 
apply simp 

593 
done 

594 

595 
lemma mult_less_imp_less_left: 

596 
assumes less: "c * a < c * b" and nonneg: "0 \<le> c" 

597 
shows "a < b" 

598 
proof (rule ccontr) 

599 
assume "\<not> a < b" 

600 
hence "b \<le> a" by (simp add: linorder_not_less) 

601 
hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono) 

602 
with this and less show False 

603 
by (simp add: not_less [symmetric]) 

604 
qed 

605 

606 
lemma mult_less_imp_less_right: 

607 
assumes less: "a * c < b * c" and nonneg: "0 \<le> c" 

608 
shows "a < b" 

609 
proof (rule ccontr) 

610 
assume "\<not> a < b" 

611 
hence "b \<le> a" by (simp add: linorder_not_less) 

612 
hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono) 

613 
with this and less show False 

614 
by (simp add: not_less [symmetric]) 

615 
qed 

616 

25230  617 
end 
618 

22390  619 
class mult_mono1 = times + zero + ord + 
25230  620 
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
14270  621 

22390  622 
class pordered_comm_semiring = comm_semiring_0 
623 
+ pordered_ab_semigroup_add + mult_mono1 

25186  624 
begin 
25152  625 

25267  626 
subclass pordered_semiring 
25186  627 
proof unfold_locales 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

628 
fix a b c :: 'a 
23550  629 
assume "a \<le> b" "0 \<le> c" 
25230  630 
thus "c * a \<le> c * b" by (rule mult_mono1) 
23550  631 
thus "a * c \<le> b * c" by (simp only: mult_commute) 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

632 
qed 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

633 

25267  634 
end 
635 

636 
class pordered_cancel_comm_semiring = comm_semiring_0_cancel 

637 
+ pordered_ab_semigroup_add + mult_mono1 

638 
begin 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

639 

27516  640 
subclass pordered_comm_semiring .. 
641 
subclass pordered_cancel_semiring .. 

25267  642 

643 
end 

644 

645 
class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add + 

26193  646 
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  647 
begin 
648 

649 
subclass ordered_semiring_strict 

25186  650 
proof unfold_locales 
23550  651 
fix a b c :: 'a 
652 
assume "a < b" "0 < c" 

26193  653 
thus "c * a < c * b" by (rule mult_strict_left_mono_comm) 
23550  654 
thus "a * c < b * c" by (simp only: mult_commute) 
655 
qed 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14270
diff
changeset

656 

25267  657 
subclass pordered_cancel_comm_semiring 
25186  658 
proof unfold_locales 
23550  659 
fix a b c :: 'a 
660 
assume "a \<le> b" "0 \<le> c" 

661 
thus "c * a \<le> c * b" 

25186  662 
unfolding le_less 
26193  663 
using mult_strict_left_mono by (cases "c = 0") auto 
23550  664 
qed 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14270
diff
changeset

665 

25267  666 
end 
25230  667 

25267  668 
class pordered_ring = ring + pordered_cancel_semiring 
669 
begin 

25230  670 

27516  671 
subclass pordered_ab_group_add .. 
14270  672 

25230  673 
lemmas ring_simps = ring_simps group_simps 
674 

675 
lemma less_add_iff1: 

676 
"a * e + c < b * e + d \<longleftrightarrow> (a  b) * e + c < d" 

677 
by (simp add: ring_simps) 

678 

679 
lemma less_add_iff2: 

680 
"a * e + c < b * e + d \<longleftrightarrow> c < (b  a) * e + d" 

681 
by (simp add: ring_simps) 

682 

683 
lemma le_add_iff1: 

684 
"a * e + c \<le> b * e + d \<longleftrightarrow> (a  b) * e + c \<le> d" 

685 
by (simp add: ring_simps) 

686 

687 
lemma le_add_iff2: 

688 
"a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b  a) * e + d" 

689 
by (simp add: ring_simps) 

690 

691 
lemma mult_left_mono_neg: 

692 
"b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b" 

693 
apply (drule mult_left_mono [of _ _ "uminus c"]) 

694 
apply (simp_all add: minus_mult_left [symmetric]) 

695 
done 

696 

697 
lemma mult_right_mono_neg: 

698 
"b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c" 

699 
apply (drule mult_right_mono [of _ _ "uminus c"]) 

700 
apply (simp_all add: minus_mult_right [symmetric]) 

701 
done 

702 

703 
lemma mult_nonpos_nonpos: 

704 
"a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b" 

705 
by (drule mult_right_mono_neg [of a zero b]) auto 

706 

707 
lemma split_mult_pos_le: 

708 
"(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b" 

709 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 

25186  710 

711 
end 

14270  712 

25762  713 
class abs_if = minus + uminus + ord + zero + abs + 
714 
assumes abs_if: "\<bar>a\<bar> = (if a < 0 then  a else a)" 

715 

716 
class sgn_if = minus + uminus + zero + one + ord + sgn + 

25186  717 
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else  1)" 
24506  718 

25564  719 
lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0" 
720 
by(simp add:sgn_if) 

721 

25230  722 
class ordered_ring = ring + ordered_semiring 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

723 
+ ordered_ab_group_add + abs_if 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

724 
begin 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

725 

27516  726 
subclass pordered_ring .. 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

727 

7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

728 
subclass pordered_ab_group_add_abs 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

729 
proof unfold_locales 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

730 
fix a b 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

731 
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

732 
by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

733 
(auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric] 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

734 
neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg, 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

735 
auto intro!: less_imp_le add_neg_neg) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

736 
qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

737 

7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

738 
end 
23521  739 

25230  740 
(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors. 
741 
Basically, ordered_ring + no_zero_divisors = ordered_ring_strict. 

742 
*) 

743 
class ordered_ring_strict = ring + ordered_semiring_strict 

25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

744 
+ ordered_ab_group_add + abs_if 
25230  745 
begin 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

746 

27516  747 
subclass ordered_ring .. 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

748 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

749 
lemma mult_strict_left_mono_neg: 
25230  750 
"b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b" 
751 
apply (drule mult_strict_left_mono [of _ _ "uminus c"]) 

752 
apply (simp_all add: minus_mult_left [symmetric]) 

753 
done 

14738  754 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

755 
lemma mult_strict_right_mono_neg: 
25230  756 
"b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c" 
757 
apply (drule mult_strict_right_mono [of _ _ "uminus c"]) 

758 
apply (simp_all add: minus_mult_right [symmetric]) 

759 
done 

14738  760 

25230  761 
lemma mult_neg_neg: 
762 
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 

763 
by (drule mult_strict_right_mono_neg, auto) 

14738  764 

25917  765 
subclass ring_no_zero_divisors 
766 
proof unfold_locales 

767 
fix a b 

768 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

769 
assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff) 

770 
have "a * b < 0 \<or> 0 < a * b" 

771 
proof (cases "a < 0") 

772 
case True note A' = this 

773 
show ?thesis proof (cases "b < 0") 

774 
case True with A' 

775 
show ?thesis by (auto dest: mult_neg_neg) 

776 
next 

777 
case False with B have "0 < b" by auto 

778 
with A' show ?thesis by (auto dest: mult_strict_right_mono) 

779 
qed 

780 
next 

781 
case False with A have A': "0 < a" by auto 

782 
show ?thesis proof (cases "b < 0") 

783 
case True with A' 

784 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

785 
next 

786 
case False with B have "0 < b" by auto 

787 
with A' show ?thesis by (auto dest: mult_pos_pos) 

788 
qed 

789 
qed 

790 
then show "a * b \<noteq> 0" by (simp add: neq_iff) 

791 
qed 

25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

792 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

793 
lemma zero_less_mult_iff: 
25917  794 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
795 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

796 
apply (simp_all add: not_less le_less) 

797 
apply (erule disjE) apply assumption defer 

798 
apply (erule disjE) defer apply (drule sym) apply simp 

799 
apply (erule disjE) defer apply (drule sym) apply simp 

800 
apply (erule disjE) apply assumption apply (drule sym) apply simp 

801 
apply (drule sym) apply simp 

802 
apply (blast dest: zero_less_mult_pos) 

25230  803 
apply (blast dest: zero_less_mult_pos2) 
804 
done 

22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

805 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

806 
lemma zero_le_mult_iff: 
25917  807 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
808 
by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

809 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

810 
lemma mult_less_0_iff: 
25917  811 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
812 
apply (insert zero_less_mult_iff [of "a" b]) 

813 
apply (force simp add: minus_mult_left[symmetric]) 

814 
done 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

815 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

816 
lemma mult_le_0_iff: 
25917  817 
"a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b" 
818 
apply (insert zero_le_mult_iff [of "a" b]) 

819 
apply (force simp add: minus_mult_left[symmetric]) 

820 
done 

821 

822 
lemma zero_le_square [simp]: "0 \<le> a * a" 

823 
by (simp add: zero_le_mult_iff linear) 

824 

825 
lemma not_square_less_zero [simp]: "\<not> (a * a < 0)" 

826 
by (simp add: not_less) 

827 

26193  828 
text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, 
829 
also with the relations @{text "\<le>"} and equality.*} 

830 

831 
text{*These ``disjunction'' versions produce two cases when the comparison is 

832 
an assumption, but effectively four when the comparison is a goal.*} 

833 

834 
lemma mult_less_cancel_right_disj: 

835 
"a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a" 

836 
apply (cases "c = 0") 

837 
apply (auto simp add: neq_iff mult_strict_right_mono 

838 
mult_strict_right_mono_neg) 

839 
apply (auto simp add: not_less 

840 
not_le [symmetric, of "a*c"] 

841 
not_le [symmetric, of a]) 

842 
apply (erule_tac [!] notE) 

843 
apply (auto simp add: less_imp_le mult_right_mono 

844 
mult_right_mono_neg) 

845 
done 

846 

847 
lemma mult_less_cancel_left_disj: 

848 
"c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a" 

849 
apply (cases "c = 0") 

850 
apply (auto simp add: neq_iff mult_strict_left_mono 

851 
mult_strict_left_mono_neg) 

852 
apply (auto simp add: not_less 

853 
not_le [symmetric, of "c*a"] 

854 
not_le [symmetric, of a]) 

855 
apply (erule_tac [!] notE) 

856 
apply (auto simp add: less_imp_le mult_left_mono 

857 
mult_left_mono_neg) 

858 
done 

859 

860 
text{*The ``conjunction of implication'' lemmas produce two cases when the 

861 
comparison is a goal, but give four when the comparison is an assumption.*} 

862 

863 
lemma mult_less_cancel_right: 

864 
"a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)" 

865 
using mult_less_cancel_right_disj [of a c b] by auto 

866 

867 
lemma mult_less_cancel_left: 

868 
"c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)" 

869 
using mult_less_cancel_left_disj [of c a b] by auto 

870 

871 
lemma mult_le_cancel_right: 

872 
"a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 

873 
by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 

874 

875 
lemma mult_le_cancel_left: 

876 
"c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 

877 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 

878 

25917  879 
end 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

880 

25230  881 
text{*This list of rewrites simplifies ring terms by multiplying 
882 
everything out and bringing sums and products into a canonical form 

883 
(by ordered rewriting). As a result it decides ring equalities but 

884 
also helps with inequalities. *} 

885 
lemmas ring_simps = group_simps ring_distribs 

886 

887 

888 
class pordered_comm_ring = comm_ring + pordered_comm_semiring 

25267  889 
begin 
25230  890 

27516  891 
subclass pordered_ring .. 
892 
subclass pordered_cancel_comm_semiring .. 

25230  893 

25267  894 
end 
25230  895 

896 
class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + 

897 
(*previously ordered_semiring*) 

898 
assumes zero_less_one [simp]: "0 < 1" 

899 
begin 

900 

901 
lemma pos_add_strict: 

902 
shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" 

903 
using add_strict_mono [of zero a b c] by simp 

904 

26193  905 
lemma zero_le_one [simp]: "0 \<le> 1" 
906 
by (rule zero_less_one [THEN less_imp_le]) 

907 

908 
lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0" 

909 
by (simp add: not_le) 

910 

911 
lemma not_one_less_zero [simp]: "\<not> 1 < 0" 

912 
by (simp add: not_less) 

913 

914 
lemma less_1_mult: 

915 
assumes "1 < m" and "1 < n" 

916 
shows "1 < m * n" 

917 
using assms mult_strict_mono [of 1 m 1 n] 

918 
by (simp add: less_trans [OF zero_less_one]) 

919 

25230  920 
end 
921 

26193  922 
class ordered_idom = comm_ring_1 + 
923 
ordered_comm_semiring_strict + ordered_ab_group_add + 

25230  924 
abs_if + sgn_if 
925 
(*previously ordered_ring*) 

25917  926 
begin 
927 

27516  928 
subclass ordered_ring_strict .. 
929 
subclass pordered_comm_ring .. 

930 
subclass idom .. 

25917  931 

932 
subclass ordered_semidom 

933 
proof unfold_locales 

26193  934 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
935 
thus "0 < 1" by (simp add: le_less) 

25917  936 
qed 
937 

26193  938 
lemma linorder_neqE_ordered_idom: 
939 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 

940 
using assms by (rule neqE) 

941 

26274  942 
text {* These cancellation simprules also produce two cases when the comparison is a goal. *} 
943 

944 
lemma mult_le_cancel_right1: 

945 
"c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)" 

946 
by (insert mult_le_cancel_right [of 1 c b], simp) 

947 

948 
lemma mult_le_cancel_right2: 

949 
"a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)" 

950 
by (insert mult_le_cancel_right [of a c 1], simp) 

951 

952 
lemma mult_le_cancel_left1: 

953 
"c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)" 

954 
by (insert mult_le_cancel_left [of c 1 b], simp) 

955 

956 
lemma mult_le_cancel_left2: 

957 
"c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)" 

958 
by (insert mult_le_cancel_left [of c a 1], simp) 

959 

960 
lemma mult_less_cancel_right1: 

961 
"c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)" 

962 
by (insert mult_less_cancel_right [of 1 c b], simp) 

963 

964 
lemma mult_less_cancel_right2: 

965 
"a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)" 

966 
by (insert mult_less_cancel_right [of a c 1], simp) 

967 

968 
lemma mult_less_cancel_left1: 

969 
"c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)" 

970 
by (insert mult_less_cancel_left [of c 1 b], simp) 

971 

972 
lemma mult_less_cancel_left2: 

973 
"c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)" 

974 
by (insert mult_less_cancel_left [of c a 1], simp) 

975 

25917  976 
end 
25230  977 

978 
class ordered_field = field + ordered_idom 

979 

26274  980 
text {* Simprules for comparisons where common factors can be cancelled. *} 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

981 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

982 
lemmas mult_compare_simps = 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

983 
mult_le_cancel_right mult_le_cancel_left 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

984 
mult_le_cancel_right1 mult_le_cancel_right2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

985 
mult_le_cancel_left1 mult_le_cancel_left2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

986 
mult_less_cancel_right mult_less_cancel_left 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

987 
mult_less_cancel_right1 mult_less_cancel_right2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

988 
mult_less_cancel_left1 mult_less_cancel_left2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

989 
mult_cancel_right mult_cancel_left 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

990 
mult_cancel_right1 mult_cancel_right2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

991 
mult_cancel_left1 mult_cancel_left2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

992 

26274  993 
 {* FIXME continue localization here *} 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

994 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

995 
lemma inverse_nonzero_iff_nonzero [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

996 
"(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))" 
26274  997 
by (force dest: inverse_zero_imp_zero) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

998 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

999 
lemma inverse_minus_eq [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1000 
"inverse(a) = inverse(a::'a::{division_ring,division_by_zero})" 
14377  1001 
proof cases 
1002 
assume "a=0" thus ?thesis by (simp add: inverse_zero) 

1003 
next 

1004 
assume "a\<noteq>0" 

1005 
thus ?thesis by (simp add: nonzero_inverse_minus_eq) 

1006 
qed 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1007 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1008 
lemma inverse_eq_imp_eq: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1009 
"inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" 
21328  1010 
apply (cases "a=0  b=0") 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1011 
apply (force dest!: inverse_zero_imp_zero 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1012 
simp add: eq_commute [of "0::'a"]) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1013 
apply (force dest!: nonzero_inverse_eq_imp_eq) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1014 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1015 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1016 
lemma inverse_eq_iff_eq [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1017 
"(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))" 
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1018 
by (force dest!: inverse_eq_imp_eq) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1019 

14270  1020 
lemma inverse_inverse_eq [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1021 
"inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" 
14270  1022 
proof cases 
1023 
assume "a=0" thus ?thesis by simp 

1024 
next 

1025 
assume "a\<noteq>0" 

1026 
thus ?thesis by (simp add: nonzero_inverse_inverse_eq) 

1027 
qed 

1028 

1029 
text{*This version builds in division by zero while also reorienting 

1030 
the righthand side.*} 

1031 
lemma inverse_mult_distrib [simp]: 

1032 
"inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" 

1033 
proof cases 

1034 
assume "a \<noteq> 0 & b \<noteq> 0" 

22993  1035 
thus ?thesis 
1036 
by (simp add: nonzero_inverse_mult_distrib mult_commute) 

14270  1037 
next 
1038 
assume "~ (a \<noteq> 0 & b \<noteq> 0)" 

22993  1039 
thus ?thesis 
1040 
by force 

14270  1041 
qed 
1042 

1043 
text{*There is no slick version using division by zero.*} 

1044 
lemma inverse_add: 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1045 
"[a \<noteq> 0; b \<noteq> 0] 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1046 
==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)" 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1047 
by (simp add: division_ring_inverse_add mult_ac) 
14270  1048 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1049 
lemma inverse_divide [simp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1050 
"inverse (a/b) = b / (a::'a::{field,division_by_zero})" 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1051 
by (simp add: divide_inverse mult_commute) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1052 

23389  1053 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1054 
subsection {* Calculations with fractions *} 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1055 

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1056 
text{* There is a whole bunch of simprules just for class @{text 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1057 
field} but none for class @{text field} and @{text nonzero_divides} 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1058 
because the latter are covered by a simproc. *} 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1059 

24427  1060 
lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1061 
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)" 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1062 
proof  
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1063 
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" 
23482  1064 
by (simp add: divide_inverse nonzero_inverse_mult_distrib) 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1065 
also have "... = a * inverse b * (inverse c * c)" 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1066 
by (simp only: mult_ac) 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1067 
also have "... = a * inverse b" 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1068 
by simp 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1069 
finally show ?thesis 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1070 
by (simp add: divide_inverse) 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1071 
qed 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1072 

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1073 
lemma mult_divide_mult_cancel_left: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1074 
"c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" 
21328  1075 
apply (cases "b = 0") 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1076 
apply (simp_all add: nonzero_mult_divide_mult_cancel_left) 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1077 
done 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1078 

24427  1079 
lemma nonzero_mult_divide_mult_cancel_right [noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1080 
"[b\<noteq>0; c\<noteq>0] ==> (a*c) / (b*c) = a/(b::'a::field)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1081 
by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
14321  1082 

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1083 
lemma mult_divide_mult_cancel_right: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1084 
"c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})" 
21328  1085 
apply (cases "b = 0") 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1086 
apply (simp_all add: nonzero_mult_divide_mult_cancel_right) 
14321  1087 
done 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1088 

14284
f1abe67c448a
reorganisation of Real/RealArith0.ML; more `Isar scripts
paulson
parents:
14277
diff
changeset

1089 
lemma divide_1 [simp]: "a/1 = (a::'a::field)" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1090 
by (simp add: divide_inverse) 
14284
f1abe67c448a
reorganisation of Real/RealArith0.ML; more `Isar scripts
paulson
parents:
14277
diff
changeset

1091 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1092 
lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1093 
by (simp add: divide_inverse mult_assoc) 
14288  1094 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1095 
lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1096 
by (simp add: divide_inverse mult_ac) 
14288  1097 

23482  1098 
lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left 
1099 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset

1100 
lemma divide_divide_eq_right [simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1101 
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1102 
by (simp add: divide_inverse mult_ac) 
14288  1103 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset

1104 
lemma divide_divide_eq_left [simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1105 
"(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1106 
by (simp add: divide_inverse mult_assoc) 
14288  1107 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1108 
lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==> 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1109 
x / y + w / z = (x * z + w * y) / (y * z)" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1110 
apply (subgoal_tac "x / y = (x * z) / (y * z)") 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1111 
apply (erule ssubst) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1112 
apply (subgoal_tac "w / z = (w * y) / (y * z)") 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1113 
apply (erule ssubst) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1114 
apply (rule add_divide_distrib [THEN sym]) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1115 
apply (subst mult_commute) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1116 
apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym]) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1117 
apply assumption 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1118 
apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym]) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1119 
apply assumption 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1120 
done 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1121 

23389  1122 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1123 
subsubsection{*Special Cancellation Simprules for Division*} 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1124 

24427  1125 
lemma mult_divide_mult_cancel_left_if[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1126 
fixes c :: "'a :: {field,division_by_zero}" 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1127 
shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1128 
by (simp add: mult_divide_mult_cancel_left) 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1129 

24427  1130 
lemma nonzero_mult_divide_cancel_right[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1131 
"b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1132 
using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1133 

24427  1134 
lemma nonzero_mult_divide_cancel_left[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1135 
"a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1136 
using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1137 

5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1138 

24427  1139 
lemma nonzero_divide_mult_cancel_right[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1140 
"\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1141 
using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1142 

24427  1143 
lemma nonzero_divide_mult_cancel_left[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1144 
"\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1145 
using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1146 

5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1147 

24427  1148 
lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1149 
"[b\<noteq>0; c\<noteq>0] ==> (c*a) / (b*c) = a/(b::'a::field)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1150 
using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac) 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1151 

24427  1152 
lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1153 
"[b\<noteq>0; c\<noteq>0] ==> (a*c) / (c*b) = a/(b::'a::field)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1154 
using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac) 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1155 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1156 

14293  1157 
subsection {* Division and Unary Minus *} 
1158 

1159 
lemma nonzero_minus_divide_left: "b \<noteq> 0 ==>  (a/b) = (a) / (b::'a::field)" 

1160 
by (simp add: divide_inverse minus_mult_left) 

1161 

1162 
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==>  (a/b) = a / (b::'a::field)" 

1163 
by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right) 

1164 

1165 
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (a)/(b) = a / (b::'a::field)" 

1166 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 

1167 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1168 
lemma minus_divide_left: " (a/b) = (a) / (b::'a::field)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1169 
by (simp add: divide_inverse minus_mult_left [symmetric]) 
14293  1170 

1171 
lemma minus_divide_right: " (a/b) = a / (b::'a::{field,division_by_zero})" 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1172 
by (simp add: divide_inverse minus_mult_right [symmetric]) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1173 

14293  1174 

1175 
text{*The effect is to extract signs from divisions*} 

17085  1176 
lemmas divide_minus_left = minus_divide_left [symmetric] 
1177 
lemmas divide_minus_right = minus_divide_right [symmetric] 

1178 
declare divide_minus_left [simp] divide_minus_right [simp] 

14293  1179 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

1180 
text{*Also, extract signs from products*} 
17085  1181 
lemmas mult_minus_left = minus_mult_left [symmetric] 
1182 
lemmas mult_minus_right = minus_mult_right [symmetric] 

1183 
declare mult_minus_left [simp] mult_minus_right [simp] 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

1184 

14293  1185 
lemma minus_divide_divide [simp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1186 
"(a)/(b) = a / (b::'a::{field,division_by_zero})" 
21328  1187 
apply (cases "b=0", simp) 
14293  1188 
apply (simp add: nonzero_minus_divide_divide) 
1189 
done 

1190 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1191 
lemma diff_divide_distrib: "(ab)/(c::'a::field) = a/c  b/c" 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

1192 
by (simp add: diff_minus add_divide_distrib) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

1193 

23482  1194 
lemma add_divide_eq_iff: 
1195 
"(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z" 

1196 
by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left) 

1197 

1198 
lemma divide_add_eq_iff: 

1199 
"(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z" 

1200 
by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left) 

1201 

1202 
lemma diff_divide_eq_iff: 

1203 
"(z::'a::field) \<noteq> 0 \<Longrightarrow> x  y/z = (z*x  y)/z" 

1204 
by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left) 

1205 

1206 
lemma divide_diff_eq_iff: 

1207 
"(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z  y = (x  z*y)/z" 

1208 
by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left) 

1209 

1210 
lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)" 

1211 
proof  

1212 
assume [simp]: "c\<noteq>0" 

23496  1213 
have "(a = b/c) = (a*c = (b/c)*c)" by simp 
1214 
also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc) 

23482  1215 
finally show ?thesis . 
1216 
qed 

1217 

1218 
lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)" 

1219 
proof  

1220 
assume [simp]: "c\<noteq>0" 

23496  1221 
have "(b/c = a) = ((b/c)*c = a*c)" by simp 
1222 
also have "... = (b = a*c)" by (simp add: divide_inverse mult_assoc) 

23482  1223 
finally show ?thesis . 
1224 
qed 

1225 

1226 
lemma eq_divide_eq: 

1227 
"((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)" 

1228 
by (simp add: nonzero_eq_divide_eq) 

1229 

1230 
lemma divide_eq_eq: 

1231 
"(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)" 

1232 
by (force simp add: nonzero_divide_eq_eq) 

1233 

1234 
lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==> 

1235 
b = a * c ==> b / c = a" 

1236 
by (subst divide_eq_eq, simp) 

1237 

1238 
lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==> 

1239 
a * c = b ==> a = b / c" 

1240 
by (subst eq_divide_eq, simp) 

1241 

1242 

1243 
lemmas field_eq_simps = ring_simps 

1244 
(* pull / out*) 

1245 
add_divide_eq_iff divide_add_eq_iff 

1246 
diff_divide_eq_iff divide_diff_eq_iff 

1247 
(* multiply eqn *) 

1248 
nonzero_eq_divide_eq nonzero_divide_eq_eq 

1249 
(* is added later: 

1250 
times_divide_eq_left times_divide_eq_right 

1251 
*) 

1252 

1253 
text{*An example:*} 

1254 
lemma fixes a b c d e f :: "'a::field" 

1255 
shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((ab)*(cd)*(ef))/((cd)*(ef)*(ab)) = 1" 

1256 
apply(subgoal_tac "(cd)*(ef)*(ab) \<noteq> 0") 

1257 
apply(simp add:field_eq_simps) 

1258 
apply(simp) 

1259 
done 

1260 

1261 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1262 
lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==> 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1263 
x / y  w / z = (x * z  w * y) / (y * z)" 
23482  1264 
by (simp add:field_eq_simps times_divide_eq) 
1265 

1266 
lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==> 

1267 
(x / y = w / z) = (x * z = w * y)" 

1268 
by (simp add:field_eq_simps times_divide_eq) 

14293  1269 

23389  1270 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1271 
subsection {* Ordered Fields *} 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1272 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1273 
lemma positive_imp_inverse_positive: 
23482  1274 
assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::ordered_field)" 
1275 
proof  

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1276 
have "0 < a * inverse a" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1277 
by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1278 
thus "0 < inverse a" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1279 
by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff) 
23482  1280 
qed 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1281 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1282 
lemma negative_imp_inverse_negative: 
23482  1283 
"a < 0 ==> inverse a < (0::'a::ordered_field)" 
1284 
by (insert positive_imp_inverse_positive [of "a"], 

1285 
simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1286 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1287 
lemma inverse_le_imp_le: 
23482  1288 
assumes invle: "inverse a \<le> inverse b" and apos: "0 < a" 
1289 
shows "b \<le> (a::'a::ordered_field)" 

1290 
proof (rule classical) 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1291 
assume "~ b \<le> a" 
23482  1292 
hence "a < b" by (simp add: linorder_not_le) 
1293 
hence bpos: "0 < b" by (blast intro: apos order_less_trans) 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1294 
hence "a * inverse a \<le> a * inverse b" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1295 
by (simp add: apos invle order_less_imp_le mult_left_mono) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1296 
hence "(a * inverse a) * b \<le> (a * inverse b) * b" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1297 
by (simp add: bpos order_less_imp_le mult_right_mono) 
23482  1298 
thus "b \<le> a" by (simp add: mult_assoc apos bpos order_less_imp_not_eq2) 
2f4be6844f7c
tuned and used field_simps
ni 