author  haftmann 
Fri, 07 Mar 2008 13:53:03 +0100  
changeset 26234  1f6e28a88785 
parent 26193  37a7eb7fd5f7 
child 26274  2bdb61a28971 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

83 
subclass semiring_0 by intro_locales 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

90 
subclass semiring_0_cancel by intro_locales 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

109 
subclass semiring_1 by intro_locales 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

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

121 

4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

122 
subclass semiring_1 by intro_locales 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

130 
subclass semiring_1_cancel by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

131 
subclass comm_semiring_0_cancel by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

132 
subclass comm_semiring_1 by intro_locales 
25267  133 

134 
end 

25152  135 

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

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

139 
subclass semiring_0_cancel by intro_locales 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

188 
subclass ring by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

189 
subclass comm_semiring_0 by intro_locales 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

196 
subclass semiring_1_cancel by intro_locales 
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 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

204 
subclass ring_1 by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

205 
subclass comm_semiring_1_cancel by intro_locales 
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 
22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

243 

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

246 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

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

248 

25186  249 
end 
25152  250 

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

25186  254 
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

255 

25186  256 
subclass ring_1_no_zero_divisors 
257 
proof unfold_locales 

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

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

259 
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

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

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

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

263 
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

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

265 
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

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

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

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

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

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

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

272 
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

273 

25186  274 
end 
25152  275 

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

276 
class field = comm_ring_1 + inverse + 
25062  277 
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
278 
assumes divide_inverse: "a / b = a * inverse b" 

25267  279 
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

280 

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

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

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

285 
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

286 
thus "a * inverse a = 1" by (simp only: mult_commute) 
14738  287 
qed 
25230  288 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

289 
subclass idom by intro_locales 
25230  290 

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

292 
proof 

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

294 
{ 

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

296 
also assume "a / b = 1" 

297 
finally show "a = b" by simp 

298 
next 

299 
assume "a = b" 

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

301 
} 

302 
qed 

303 

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

305 
by (simp add: divide_inverse) 

306 

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

308 
by (simp add: divide_inverse) 

309 

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

311 
by (simp add: divide_inverse) 

312 

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

314 
by (simp add: divide_inverse) 

315 

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

317 
by (simp add: divide_inverse ring_distribs) 

318 

319 
end 

320 

22390  321 
class division_by_zero = zero + inverse + 
25062  322 
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

323 

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

326 
by (simp add: divide_inverse) 

327 

328 
lemma divide_self_if [simp]: 

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

330 
by (simp add: divide_self) 

331 

22390  332 
class mult_mono = times + zero + ord + 
25062  333 
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
334 
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

335 

22390  336 
class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
25230  337 
begin 
338 

339 
lemma mult_mono: 

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

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

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

343 
apply (erule mult_left_mono, assumption) 

344 
done 

345 

346 
lemma mult_mono': 

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

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

349 
apply (rule mult_mono) 

350 
apply (fast intro: order_trans)+ 

351 
done 

352 

353 
end 

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

354 

22390  355 
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

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

358 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

359 
subclass semiring_0_cancel by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

360 
subclass pordered_semiring by intro_locales 
23521  361 

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

364 

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

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

367 

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

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

370 

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

374 
end 

375 

376 
class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono 

25267  377 
begin 
25230  378 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

379 
subclass pordered_cancel_semiring by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

380 

4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

381 
subclass pordered_comm_monoid_add by intro_locales 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

382 

25230  383 
lemma mult_left_less_imp_less: 
384 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

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

386 

387 
lemma mult_right_less_imp_less: 

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

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

23521  390 

25186  391 
end 
25152  392 

22390  393 
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + 
25062  394 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
395 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

397 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

398 
subclass semiring_0_cancel by intro_locales 
14940  399 

25267  400 
subclass ordered_semiring 
25186  401 
proof unfold_locales 
23550  402 
fix a b c :: 'a 
403 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  405 
unfolding le_less 
406 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  407 
from A show "a * c \<le> b * c" 
25152  408 
unfolding le_less 
25186  409 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  410 
qed 
411 

25230  412 
lemma mult_left_le_imp_le: 
413 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

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

415 

416 
lemma mult_right_le_imp_le: 

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

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

419 

420 
lemma mult_pos_pos: 

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

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

423 

424 
lemma mult_pos_neg: 

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

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

427 

428 
lemma mult_pos_neg2: 

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

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

431 

432 
lemma zero_less_mult_pos: 

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

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

435 
apply (auto simp add: le_less not_less) 

436 
apply (drule_tac mult_pos_neg [of a b]) 

437 
apply (auto dest: less_not_sym) 

438 
done 

439 

440 
lemma zero_less_mult_pos2: 

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

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

443 
apply (auto simp add: le_less not_less) 

444 
apply (drule_tac mult_pos_neg2 [of a b]) 

445 
apply (auto dest: less_not_sym) 

446 
done 

447 

26193  448 
text{*Strict monotonicity in both arguments*} 
449 
lemma mult_strict_mono: 

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

451 
shows "a * c < b * d" 

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

453 
apply (simp add: mult_pos_pos) 

454 
apply (erule mult_strict_right_mono [THEN less_trans]) 

455 
apply (force simp add: le_less) 

456 
apply (erule mult_strict_left_mono, assumption) 

457 
done 

458 

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

460 
lemma mult_strict_mono': 

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

462 
shows "a * c < b * d" 

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

464 

465 
lemma mult_less_le_imp_less: 

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

467 
shows "a * c < b * d" 

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

469 
apply (erule less_le_trans) 

470 
apply (erule mult_left_mono) 

471 
apply simp 

472 
apply (erule mult_strict_right_mono) 

473 
apply assumption 

474 
done 

475 

476 
lemma mult_le_less_imp_less: 

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

478 
shows "a * c < b * d" 

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

480 
apply (erule le_less_trans) 

481 
apply (erule mult_strict_left_mono) 

482 
apply simp 

483 
apply (erule mult_right_mono) 

484 
apply simp 

485 
done 

486 

487 
lemma mult_less_imp_less_left: 

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

489 
shows "a < b" 

490 
proof (rule ccontr) 

491 
assume "\<not> a < b" 

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

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

494 
with this and less show False 

495 
by (simp add: not_less [symmetric]) 

496 
qed 

497 

498 
lemma mult_less_imp_less_right: 

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

500 
shows "a < b" 

501 
proof (rule ccontr) 

502 
assume "\<not> a < b" 

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

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

505 
with this and less show False 

506 
by (simp add: not_less [symmetric]) 

507 
qed 

508 

25230  509 
end 
510 

22390  511 
class mult_mono1 = times + zero + ord + 
25230  512 
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
14270  513 

22390  514 
class pordered_comm_semiring = comm_semiring_0 
515 
+ pordered_ab_semigroup_add + mult_mono1 

25186  516 
begin 
25152  517 

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

520 
fix a b c :: 'a 
23550  521 
assume "a \<le> b" "0 \<le> c" 
25230  522 
thus "c * a \<le> c * b" by (rule mult_mono1) 
23550  523 
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

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

525 

25267  526 
end 
527 

528 
class pordered_cancel_comm_semiring = comm_semiring_0_cancel 

529 
+ pordered_ab_semigroup_add + mult_mono1 

530 
begin 

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

531 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

532 
subclass pordered_comm_semiring by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

533 
subclass pordered_cancel_semiring by intro_locales 
25267  534 

535 
end 

536 

537 
class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add + 

26193  538 
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  539 
begin 
540 

541 
subclass ordered_semiring_strict 

25186  542 
proof unfold_locales 
23550  543 
fix a b c :: 'a 
544 
assume "a < b" "0 < c" 

26193  545 
thus "c * a < c * b" by (rule mult_strict_left_mono_comm) 
23550  546 
thus "a * c < b * c" by (simp only: mult_commute) 
547 
qed 

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

548 

25267  549 
subclass pordered_cancel_comm_semiring 
25186  550 
proof unfold_locales 
23550  551 
fix a b c :: 'a 
552 
assume "a \<le> b" "0 \<le> c" 

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

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

557 

25267  558 
end 
25230  559 

25267  560 
class pordered_ring = ring + pordered_cancel_semiring 
561 
begin 

25230  562 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

563 
subclass pordered_ab_group_add by intro_locales 
14270  564 

25230  565 
lemmas ring_simps = ring_simps group_simps 
566 

567 
lemma less_add_iff1: 

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

569 
by (simp add: ring_simps) 

570 

571 
lemma less_add_iff2: 

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

573 
by (simp add: ring_simps) 

574 

575 
lemma le_add_iff1: 

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

577 
by (simp add: ring_simps) 

578 

579 
lemma le_add_iff2: 

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

581 
by (simp add: ring_simps) 

582 

583 
lemma mult_left_mono_neg: 

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

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

586 
apply (simp_all add: minus_mult_left [symmetric]) 

587 
done 

588 

589 
lemma mult_right_mono_neg: 

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

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

592 
apply (simp_all add: minus_mult_right [symmetric]) 

593 
done 

594 

595 
lemma mult_nonpos_nonpos: 

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

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

598 

599 
lemma split_mult_pos_le: 

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

601 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 

25186  602 

603 
end 

14270  604 

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

607 

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

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

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

613 

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

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

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

617 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

618 
subclass pordered_ring by intro_locales 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

619 

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

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

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

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

623 
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

624 
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

625 
(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

626 
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

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

628 
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

629 

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

630 
end 
23521  631 

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

634 
*) 

635 
class ordered_ring_strict = ring + ordered_semiring_strict 

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

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

638 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

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

640 

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

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

644 
apply (simp_all add: minus_mult_left [symmetric]) 

645 
done 

14738  646 

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

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

650 
apply (simp_all add: minus_mult_right [symmetric]) 

651 
done 

14738  652 

25230  653 
lemma mult_neg_neg: 
654 
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 

655 
by (drule mult_strict_right_mono_neg, auto) 

14738  656 

25917  657 
subclass ring_no_zero_divisors 
658 
proof unfold_locales 

659 
fix a b 

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

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

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

663 
proof (cases "a < 0") 

664 
case True note A' = this 

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

666 
case True with A' 

667 
show ?thesis by (auto dest: mult_neg_neg) 

668 
next 

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

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

671 
qed 

672 
next 

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

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

675 
case True with A' 

676 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

677 
next 

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

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

680 
qed 

681 
qed 

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

683 
qed 

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

684 

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

685 
lemma zero_less_mult_iff: 
25917  686 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
687 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

688 
apply (simp_all add: not_less le_less) 

689 
apply (erule disjE) apply assumption defer 

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

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

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

693 
apply (drule sym) apply simp 

694 
apply (blast dest: zero_less_mult_pos) 

25230  695 
apply (blast dest: zero_less_mult_pos2) 
696 
done 

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

697 

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

698 
lemma zero_le_mult_iff: 
25917  699 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
700 
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

701 

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

702 
lemma mult_less_0_iff: 
25917  703 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
704 
apply (insert zero_less_mult_iff [of "a" b]) 

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

706 
done 

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

707 

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

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

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

712 
done 

713 

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

715 
by (simp add: zero_le_mult_iff linear) 

716 

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

718 
by (simp add: not_less) 

719 

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

722 

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

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

725 

726 
lemma mult_less_cancel_right_disj: 

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

728 
apply (cases "c = 0") 

729 
apply (auto simp add: neq_iff mult_strict_right_mono 

730 
mult_strict_right_mono_neg) 

731 
apply (auto simp add: not_less 

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

733 
not_le [symmetric, of a]) 

734 
apply (erule_tac [!] notE) 

735 
apply (auto simp add: less_imp_le mult_right_mono 

736 
mult_right_mono_neg) 

737 
done 

738 

739 
lemma mult_less_cancel_left_disj: 

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

741 
apply (cases "c = 0") 

742 
apply (auto simp add: neq_iff mult_strict_left_mono 

743 
mult_strict_left_mono_neg) 

744 
apply (auto simp add: not_less 

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

746 
not_le [symmetric, of a]) 

747 
apply (erule_tac [!] notE) 

748 
apply (auto simp add: less_imp_le mult_left_mono 

749 
mult_left_mono_neg) 

750 
done 

751 

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

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

754 

755 
lemma mult_less_cancel_right: 

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

757 
using mult_less_cancel_right_disj [of a c b] by auto 

758 

759 
lemma mult_less_cancel_left: 

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

761 
using mult_less_cancel_left_disj [of c a b] by auto 

762 

763 
lemma mult_le_cancel_right: 

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

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

766 

767 
lemma mult_le_cancel_left: 

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

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

770 

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

772 

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

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

776 
also helps with inequalities. *} 

777 
lemmas ring_simps = group_simps ring_distribs 

778 

779 

780 
class pordered_comm_ring = comm_ring + pordered_comm_semiring 

25267  781 
begin 
25230  782 

25512
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

783 
subclass pordered_ring by intro_locales 
4134f7c782e2
using intro_locales instead of unfold_locales if appropriate
haftmann
parents:
25450
diff
changeset

784 
subclass pordered_cancel_comm_semiring by intro_locales 
25230  785 

25267  786 
end 
25230  787 

788 
class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + 

789 
(*previously ordered_semiring*) 

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

791 
begin 

792 

793 
lemma pos_add_strict: 

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

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

796 

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

799 

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

801 
by (simp add: not_le) 

802 

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

804 
by (simp add: not_less) 

805 

806 
lemma less_1_mult: 

807 
assumes "1 < m" and "1 < n" 

808 
shows "1 < m * n" 

809 
using assms mult_strict_mono [of 1 m 1 n] 

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

811 

25230  812 
end 
813 

26193  814 
class ordered_idom = comm_ring_1 + 
815 
ordered_comm_semiring_strict + ordered_ab_group_add + 

25230  816 
abs_if + sgn_if 
817 
(*previously ordered_ring*) 

25917  818 
begin 
819 

820 
subclass ordered_ring_strict by intro_locales 

821 
subclass pordered_comm_ring by intro_locales 

822 
subclass idom by intro_locales 

823 

824 
subclass ordered_semidom 

825 
proof unfold_locales 

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

25917  828 
qed 
829 

26193  830 
lemma linorder_neqE_ordered_idom: 
831 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 

832 
using assms by (rule neqE) 

833 

25917  834 
end 
25230  835 

836 
class ordered_field = field + ordered_idom 

837 

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

838 
text{*All three types of comparision involving 0 and 1 are covered.*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

839 

26193  840 
 {* FIXME continue localization here *} 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

841 

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

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

843 

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

844 
text{*These also produce two cases when the comparison is a goal.*} 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

845 

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

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

847 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

848 
shows "(c \<le> b*c) = ((0<c > 1\<le>b) & (c<0 > b \<le> 1))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

849 
by (insert mult_le_cancel_right [of 1 c b], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

850 

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

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

852 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

853 
shows "(a*c \<le> c) = ((0<c > a\<le>1) & (c<0 > 1 \<le> a))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

854 
by (insert mult_le_cancel_right [of a c 1], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

855 

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

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

857 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

858 
shows "(c \<le> c*b) = ((0<c > 1\<le>b) & (c<0 > b \<le> 1))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

859 
by (insert mult_le_cancel_left [of c 1 b], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

860 

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

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

862 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

863 
shows "(c*a \<le> c) = ((0<c > a\<le>1) & (c<0 > 1 \<le> a))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

864 
by (insert mult_le_cancel_left [of c a 1], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

865 

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

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

867 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

868 
shows "(c < b*c) = ((0 \<le> c > 1<b) & (c \<le> 0 > b < 1))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

869 
by (insert mult_less_cancel_right [of 1 c b], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

870 

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

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

872 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

873 
shows "(a*c < c) = ((0 \<le> c > a<1) & (c \<le> 0 > 1 < a))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

874 
by (insert mult_less_cancel_right [of a c 1], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

875 

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

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

877 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

878 
shows "(c < c*b) = ((0 \<le> c > 1<b) & (c \<le> 0 > b < 1))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

879 
by (insert mult_less_cancel_left [of c 1 b], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

880 

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

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

882 
fixes c :: "'a :: ordered_idom" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

883 
shows "(c*a < c) = ((0 \<le> c > a<1) & (c \<le> 0 > 1 < a))" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

884 
by (insert mult_less_cancel_left [of c a 1], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

885 

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

886 
lemma mult_cancel_right1 [simp]: 
23544  887 
fixes c :: "'a :: ring_1_no_zero_divisors" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

888 
shows "(c = b*c) = (c = 0  b=1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

889 
by (insert mult_cancel_right [of 1 c b], force) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

890 

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

891 
lemma mult_cancel_right2 [simp]: 
23544  892 
fixes c :: "'a :: ring_1_no_zero_divisors" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

893 
shows "(a*c = c) = (c = 0  a=1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

894 
by (insert mult_cancel_right [of a c 1], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

895 

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

896 
lemma mult_cancel_left1 [simp]: 
23544  897 
fixes c :: "'a :: ring_1_no_zero_divisors" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

898 
shows "(c = c*b) = (c = 0  b=1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

899 
by (insert mult_cancel_left [of c 1 b], force) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

900 

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

901 
lemma mult_cancel_left2 [simp]: 
23544  902 
fixes c :: "'a :: ring_1_no_zero_divisors" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

903 
shows "(c*a = c) = (c = 0  a=1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

904 
by (insert mult_cancel_left [of c a 1], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

905 

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

906 

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

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

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

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

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

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

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

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

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

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

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

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

918 

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

919 

23482  920 
(* what ordering?? this is a straight instance of mult_eq_0_iff 
14270  921 
text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement 
922 
of an ordering.*} 

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

923 
lemma field_mult_eq_0_iff [simp]: 
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

924 
"(a*b = (0::'a::division_ring)) = (a = 0  b = 0)" 
22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

925 
by simp 
23482  926 
*) 
23496  927 
(* subsumed by mult_cancel lemmas on ring_no_zero_divisors 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

928 
text{*Cancellation of equalities with a common factor*} 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

929 
lemma field_mult_cancel_right_lemma: 
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

930 
assumes cnz: "c \<noteq> (0::'a::division_ring)" 
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

931 
and eq: "a*c = b*c" 
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

932 
shows "a=b" 
14377  933 
proof  
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

934 
have "(a * c) * inverse c = (b * c) * inverse c" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

935 
by (simp add: eq) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

936 
thus "a=b" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

937 
by (simp add: mult_assoc cnz) 
14377  938 
qed 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

939 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

940 
lemma field_mult_cancel_right [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

941 
"(a*c = b*c) = (c = (0::'a::division_ring)  a=b)" 
22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

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

943 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

944 
lemma field_mult_cancel_left [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

945 
"(c*a = c*b) = (c = (0::'a::division_ring)  a=b)" 
22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

946 
by simp 
23496  947 
*) 
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

948 
lemma nonzero_imp_inverse_nonzero: 
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

949 
"a \<noteq> 0 ==> inverse a \<noteq> (0::'a::division_ring)" 
14377  950 
proof 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

951 
assume ianz: "inverse a = 0" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

952 
assume "a \<noteq> 0" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

953 
hence "1 = a * inverse a" by simp 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

954 
also have "... = 0" by (simp add: ianz) 
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

955 
finally have "1 = (0::'a::division_ring)" . 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

956 
thus False by (simp add: eq_commute) 
14377  957 
qed 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

958 

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

959 

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

960 
subsection{*Basic Properties of @{term inverse}*} 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

961 

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

962 
lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::division_ring)" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

963 
apply (rule ccontr) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

964 
apply (blast dest: nonzero_imp_inverse_nonzero) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

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

966 

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

967 
lemma inverse_nonzero_imp_nonzero: 
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

968 
"inverse a = 0 ==> a = (0::'a::division_ring)" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

969 
apply (rule ccontr) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

970 
apply (blast dest: nonzero_imp_inverse_nonzero) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

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

972 

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

973 
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

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

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

976 

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

977 
lemma nonzero_inverse_minus_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

978 
assumes [simp]: "a\<noteq>0" 
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

979 
shows "inverse(a) = inverse(a::'a::division_ring)" 
14377  980 
proof  
981 
have "a * inverse ( a) = a *  inverse a" 

982 
by simp 

983 
thus ?thesis 

23496  984 
by (simp only: mult_cancel_left, simp) 
14377  985 
qed 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

986 

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

987 
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

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

991 
next 

992 
assume "a\<noteq>0" 

993 
thus ?thesis by (simp add: nonzero_inverse_minus_eq) 

994 
qed 

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

995 

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

996 
lemma nonzero_inverse_eq_imp_eq: 
14269  997 
assumes inveq: "inverse a = inverse b" 
998 
and anz: "a \<noteq> 0" 

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

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 
shows "a = (b::'a::division_ring)" 
14377  1001 
proof  
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

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

1003 
by (simp add: inveq) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

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

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

1006 
thus "a = b" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1007 
by (simp add: mult_assoc anz bnz) 
14377  1008 
qed 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1009 

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

1010 
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

1011 
"inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" 
21328  1012 
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

1013 
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

1014 
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

1015 
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

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

1017 

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

1018 
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

1019 
"(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

1020 
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

1021 

14270  1022 
lemma nonzero_inverse_inverse_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

1023 
assumes [simp]: "a \<noteq> 0" 
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

1024 
shows "inverse(inverse (a::'a::division_ring)) = a" 
14270  1025 
proof  
1026 
have "(inverse (inverse a) * inverse a) * a = a" 

1027 
by (simp add: nonzero_imp_inverse_nonzero) 

1028 
thus ?thesis 

1029 
by (simp add: mult_assoc) 

1030 
qed 

1031 

1032 
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

1033 
"inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" 
14270  1034 
proof cases 
1035 
assume "a=0" thus ?thesis by simp 

1036 
next 

1037 
assume "a\<noteq>0" 

1038 
thus ?thesis by (simp add: nonzero_inverse_inverse_eq) 

1039 
qed 

1040 

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

1041 
lemma inverse_1 [simp]: "inverse 1 = (1::'a::division_ring)" 
14270  1042 
proof  
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

1043 
have "inverse 1 * 1 = (1::'a::division_ring)" 
14270  1044 
by (rule left_inverse [OF zero_neq_one [symmetric]]) 
1045 
thus ?thesis by simp 

1046 
qed 

1047 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1048 
lemma inverse_unique: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1049 
assumes ab: "a*b = 1" 
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

1050 
shows "inverse a = (b::'a::division_ring)" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1051 
proof  
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1052 
have "a \<noteq> 0" using ab by auto 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1053 
moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1054 
ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1055 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15010
diff
changeset

1056 

14270  1057 
lemma nonzero_inverse_mult_distrib: 
1058 
assumes anz: "a \<noteq> 0" 

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

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

1060 
shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)" 
14270  1061 
proof  
1062 
have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" 

23482  1063 
by (simp add: anz bnz) 
14270  1064 
hence "inverse(a*b) * a = inverse(b)" 
1065 
by (simp add: mult_assoc bnz) 

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

1067 
by simp 

1068 
thus ?thesis 

1069 
by (simp add: mult_assoc anz) 

1070 
qed 

1071 

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

1073 
the righthand side.*} 

1074 
lemma inverse_mult_distrib [simp]: 

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

1076 
proof cases 

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

22993  1078 
thus ?thesis 
1079 
by (simp add: nonzero_inverse_mult_distrib mult_commute) 

14270  1080 
next 
1081 
assume "~ (a \<noteq> 0 & b \<noteq> 0)" 

22993  1082 
thus ?thesis 
1083 
by force 

14270  1084 
qed 
1085 

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

1086 
lemma division_ring_inverse_add: 
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

1087 
"[(a::'a::division_ring) \<noteq> 0; b \<noteq> 0] 
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

1088 
==> inverse a + inverse b = inverse a * (a+b) * inverse b" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1089 
by (simp add: ring_simps) 
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

1090 

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

1091 
lemma division_ring_inverse_diff: 
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

1092 
"[(a::'a::division_ring) \<noteq> 0; b \<noteq> 0] 
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

1093 
==> inverse a  inverse b = inverse a * (ba) * inverse b" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1094 
by (simp add: ring_simps) 
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

1095 

14270  1096 
text{*There is no slick version using division by zero.*} 
1097 
lemma inverse_add: 

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

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

1099 
==> 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

1100 
by (simp add: division_ring_inverse_add mult_ac) 
14270  1101 

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

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

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

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

1105 

23389  1106 

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

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

1108 

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

1109 
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

1110 
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

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

1112 

24427  1113 
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

1114 
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

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

1116 
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" 
23482  1117 
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

1118 
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

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

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

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

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

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

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

1125 

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

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

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

1129 
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

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

1131 

24427  1132 
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

1133 
"[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

1134 
by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
14321  1135 

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

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

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

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

1141 

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

1142 
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

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

1144 

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

1145 
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

1146 
by (simp add: divide_inverse mult_assoc) 
14288  1147 

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

1148 
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

1149 
by (simp add: divide_inverse mult_ac) 
14288  1150 

23482  1151 
lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left 
1152 

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

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

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

1155 
by (simp add: divide_inverse mult_ac) 
14288  1156 

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

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

1158 
"(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

1159 
by (simp add: divide_inverse mult_assoc) 
14288  1160 

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

1161 
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

1162 
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

1163 
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

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

1165 
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

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

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

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

1169 
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

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

1171 
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

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

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

1174 

23389  1175 

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

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

1177 

24427  1178 
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

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

1180 
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

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

1182 

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

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

1185 
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

1186 

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

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

1189 
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

1190 

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

1191 

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

1193 
"\<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

1194 
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

1195 

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

1197 
"\<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

1198 
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

1199 

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

1200 

24427  1201 
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

1202 
"[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

1203 
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

1204 

24427  1205 
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

1206 
"[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

1207 
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

1208 

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

1209 

14293  1210 
subsection {* Division and Unary Minus *} 
1211 

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

1213 
by (simp add: divide_inverse minus_mult_left) 

1214 

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

1216 
by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right) 

1217 

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

1219 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 

1220 

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

1221 
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

1222 
by (simp add: divide_inverse minus_mult_left [symmetric]) 
14293  1223 

1224 
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

1225 
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

1226 

14293  1227 

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

17085  1229 
lemmas divide_minus_left = minus_divide_left [symmetric] 
1230 
lemmas divide_minus_right = minus_divide_right [symmetric] 

1231 
declare divide_minus_left [simp] divide_minus_right [simp] 

14293  1232 

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

1233 
text{*Also, extract signs from products*} 
17085  1234 
lemmas mult_minus_left = minus_mult_left [symmetric] 
1235 
lemmas mult_minus_right = minus_mult_right [symmetric] 

1236 
declare mult_minus_left [simp] mult_minus_right [simp] 

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

1237 

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

1239 
"(a)/(b) = a / (b::'a::{field,division_by_zero})" 
21328  1240 
apply (cases "b=0", simp) 
14293  1241 
apply (simp add: nonzero_minus_divide_divide) 
1242 
done 

1243 

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

1244 
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

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

1246 

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

1249 
by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left) 

1250 

1251 
lemma divide_add_eq_iff: 

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

1253 
by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left) 

1254 

1255 
lemma diff_divide_eq_iff: 

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

1257 
by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left) 

1258 

1259 
lemma divide_diff_eq_iff: 

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

1261 
by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left) 

1262 

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

1264 
proof  

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

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

23482  1268 
finally show ?thesis . 
1269 
qed 

1270 

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

1272 
proof  

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

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

23482  1276 
finally show ?thesis . 
1277 
qed 

1278 

1279 
lemma eq_divide_eq: 

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

1281 
by (simp add: nonzero_eq_divide_eq) 

1282 

1283 
lemma divide_eq_eq: 
