author  nipkow 
Sat, 21 Feb 2009 20:52:30 +0100  
changeset 30042  31039ee583fa 
parent 29981  7d0ed261b712 
child 30242  aea5d7fa7ef5 
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 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

2 
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

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

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

5 

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

7 

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

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

14 
\begin{itemize} 

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

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

17 
\end{itemize} 

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

19 
\begin{itemize} 

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

23 
*} 

14504  24 

22390  25 
class semiring = ab_semigroup_add + semigroup_mult + 
29667  26 
assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c" 
27 
assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c" 

25152  28 
begin 
29 

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

31 
lemma combine_common_factor: 

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

29667  33 
by (simp add: left_distrib add_ac) 
25152  34 

35 
end 

14504  36 

22390  37 
class mult_zero = times + zero + 
25062  38 
assumes mult_zero_left [simp]: "0 * a = 0" 
39 
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

40 

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

42 

29904  43 
class semiring_0_cancel = semiring + cancel_comm_monoid_add 
25186  44 
begin 
14504  45 

25186  46 
subclass semiring_0 
28823  47 
proof 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

48 
fix a :: 'a 
29667  49 
have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric]) 
50 
thus "0 * a = 0" by (simp only: add_left_cancel) 

25152  51 
next 
52 
fix a :: 'a 

29667  53 
have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric]) 
54 
thus "a * 0 = 0" by (simp only: add_left_cancel) 

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

55 
qed 
14940  56 

25186  57 
end 
25152  58 

22390  59 
class comm_semiring = ab_semigroup_add + ab_semigroup_mult + 
25062  60 
assumes distrib: "(a + b) * c = a * c + b * c" 
25152  61 
begin 
14504  62 

25152  63 
subclass semiring 
28823  64 
proof 
14738  65 
fix a b c :: 'a 
66 
show "(a + b) * c = a * c + b * c" by (simp add: distrib) 

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

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

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

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

14504  71 
qed 
72 

25152  73 
end 
14504  74 

25152  75 
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero 
76 
begin 

77 

27516  78 
subclass semiring_0 .. 
25152  79 

80 
end 

14504  81 

29904  82 
class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add 
25186  83 
begin 
14940  84 

27516  85 
subclass semiring_0_cancel .. 
14940  86 

28141
193c3ea0f63b
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents:
27651
diff
changeset

87 
subclass comm_semiring_0 .. 
193c3ea0f63b
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents:
27651
diff
changeset

88 

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

90 

22390  91 
class zero_neq_one = zero + one + 
25062  92 
assumes zero_neq_one [simp]: "0 \<noteq> 1" 
26193  93 
begin 
94 

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

29667  96 
by (rule not_sym) (rule zero_neq_one) 
26193  97 

98 
end 

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

99 

22390  100 
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 
14504  101 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

102 
text {* Abstract divisibility *} 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

103 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

104 
class dvd = times 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

105 
begin 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

106 

28559  107 
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where 
108 
[code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)" 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

109 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

110 
lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

111 
unfolding dvd_def .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

112 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

113 
lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

114 
unfolding dvd_def by blast 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

115 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

116 
end 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

117 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

118 
class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd 
22390  119 
(*previously almost_semiring*) 
25152  120 
begin 
14738  121 

27516  122 
subclass semiring_1 .. 
25152  123 

29925  124 
lemma dvd_refl[simp]: "a dvd a" 
28559  125 
proof 
126 
show "a = a * 1" by simp 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

127 
qed 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

128 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

129 
lemma dvd_trans: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

130 
assumes "a dvd b" and "b dvd c" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

131 
shows "a dvd c" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

132 
proof  
28559  133 
from assms obtain v where "b = a * v" by (auto elim!: dvdE) 
134 
moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE) 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

135 
ultimately have "c = a * (v * w)" by (simp add: mult_assoc) 
28559  136 
then show ?thesis .. 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

137 
qed 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

138 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

139 
lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0" 
29667  140 
by (auto intro: dvd_refl elim!: dvdE) 
28559  141 

142 
lemma dvd_0_right [iff]: "a dvd 0" 

143 
proof 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

144 
show "0 = a * 0" by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

145 
qed 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

146 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

147 
lemma one_dvd [simp]: "1 dvd a" 
29667  148 
by (auto intro!: dvdI) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

149 

30042  150 
lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)" 
29667  151 
by (auto intro!: mult_left_commute dvdI elim!: dvdE) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

152 

30042  153 
lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)" 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

154 
apply (subst mult_commute) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

155 
apply (erule dvd_mult) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

156 
done 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

157 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

158 
lemma dvd_triv_right [simp]: "a dvd b * a" 
29667  159 
by (rule dvd_mult) (rule dvd_refl) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

160 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

161 
lemma dvd_triv_left [simp]: "a dvd a * b" 
29667  162 
by (rule dvd_mult2) (rule dvd_refl) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

163 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

164 
lemma mult_dvd_mono: 
30042  165 
assumes "a dvd b" 
166 
and "c dvd d" 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

167 
shows "a * c dvd b * d" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

168 
proof  
30042  169 
from `a dvd b` obtain b' where "b = a * b'" .. 
170 
moreover from `c dvd d` obtain d' where "d = c * d'" .. 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

171 
ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

172 
then show ?thesis .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

173 
qed 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

174 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

175 
lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c" 
29667  176 
by (simp add: dvd_def mult_assoc, blast) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

177 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

178 
lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

179 
unfolding mult_ac [of a] by (rule dvd_mult_left) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

180 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

181 
lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0" 
29667  182 
by simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

183 

29925  184 
lemma dvd_add[simp]: 
185 
assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)" 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

186 
proof  
29925  187 
from `a dvd b` obtain b' where "b = a * b'" .. 
188 
moreover from `a dvd c` obtain c' where "c = a * c'" .. 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

189 
ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

190 
then show ?thesis .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

191 
qed 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

192 

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

194 

29925  195 

22390  196 
class no_zero_divisors = zero + times + 
25062  197 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
14504  198 

29904  199 
class semiring_1_cancel = semiring + cancel_comm_monoid_add 
200 
+ zero_neq_one + monoid_mult 

25267  201 
begin 
14940  202 

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

204 

27516  205 
subclass semiring_1 .. 
25267  206 

207 
end 

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

208 

29904  209 
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add 
210 
+ zero_neq_one + comm_monoid_mult 

25267  211 
begin 
14738  212 

27516  213 
subclass semiring_1_cancel .. 
214 
subclass comm_semiring_0_cancel .. 

215 
subclass comm_semiring_1 .. 

25267  216 

217 
end 

25152  218 

22390  219 
class ring = semiring + ab_group_add 
25267  220 
begin 
25152  221 

27516  222 
subclass semiring_0_cancel .. 
25152  223 

224 
text {* Distribution rules *} 

225 

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

29667  227 
by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 
25152  228 

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

29667  230 
by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
25152  231 

29407
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

232 
text{*Extract signs from products*} 
29833  233 
lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric] 
234 
lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric] 

29407
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

235 

25152  236 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  237 
by simp 
25152  238 

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

29667  240 
by simp 
241 

242 
lemma right_diff_distrib[algebra_simps]: "a * (b  c) = a * b  a * c" 

243 
by (simp add: right_distrib diff_minus) 

244 

245 
lemma left_diff_distrib[algebra_simps]: "(a  b) * c = a * c  b * c" 

246 
by (simp add: left_distrib diff_minus) 

25152  247 

29833  248 
lemmas ring_distribs[noatp] = 
25152  249 
right_distrib left_distrib left_diff_distrib right_diff_distrib 
250 

29667  251 
text{*Legacy  use @{text algebra_simps} *} 
29833  252 
lemmas ring_simps[noatp] = algebra_simps 
25230  253 

254 
lemma eq_add_iff1: 

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

29667  256 
by (simp add: algebra_simps) 
25230  257 

258 
lemma eq_add_iff2: 

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

29667  260 
by (simp add: algebra_simps) 
25230  261 

25152  262 
end 
263 

29833  264 
lemmas ring_distribs[noatp] = 
25152  265 
right_distrib left_distrib left_diff_distrib right_diff_distrib 
266 

22390  267 
class comm_ring = comm_semiring + ab_group_add 
25267  268 
begin 
14738  269 

27516  270 
subclass ring .. 
28141
193c3ea0f63b
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
huffman
parents:
27651
diff
changeset

271 
subclass comm_semiring_0_cancel .. 
25267  272 

273 
end 

14738  274 

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

277 

27516  278 
subclass semiring_1_cancel .. 
25267  279 

280 
end 

25152  281 

22390  282 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
283 
(*previously ring*) 

25267  284 
begin 
14738  285 

27516  286 
subclass ring_1 .. 
287 
subclass comm_semiring_1_cancel .. 

25267  288 

29465
b2cfb5d0a59e
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
huffman
parents:
29461
diff
changeset

289 
lemma dvd_minus_iff [simp]: "x dvd  y \<longleftrightarrow> x dvd y" 
29408
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

290 
proof 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

291 
assume "x dvd  y" 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

292 
then have "x dvd  1 *  y" by (rule dvd_mult) 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

293 
then show "x dvd y" by simp 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

294 
next 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

295 
assume "x dvd y" 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

296 
then have "x dvd  1 * y" by (rule dvd_mult) 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

297 
then show "x dvd  y" by simp 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

298 
qed 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

299 

29465
b2cfb5d0a59e
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
huffman
parents:
29461
diff
changeset

300 
lemma minus_dvd_iff [simp]: " x dvd y \<longleftrightarrow> x dvd y" 
29408
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

301 
proof 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

302 
assume " x dvd y" 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

303 
then obtain k where "y =  x * k" .. 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

304 
then have "y = x *  k" by simp 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

305 
then show "x dvd y" .. 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

306 
next 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

307 
assume "x dvd y" 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

308 
then obtain k where "y = x * k" .. 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

309 
then have "y =  x *  k" by simp 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

310 
then show " x dvd y" .. 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

311 
qed 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

312 

30042  313 
lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y  z)" 
314 
by (simp add: diff_minus dvd_minus_iff) 

29409  315 

25267  316 
end 
25152  317 

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

318 
class ring_no_zero_divisors = ring + no_zero_divisors 
25230  319 
begin 
320 

321 
lemma mult_eq_0_iff [simp]: 

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

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

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

325 
then show ?thesis using no_zero_divisors by simp 

326 
next 

327 
case True then show ?thesis by auto 

328 
qed 

329 

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

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

333 
proof  

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

29667  335 
by (simp add: algebra_simps right_minus_eq) 
336 
thus ?thesis by (simp add: disj_commute right_minus_eq) 

26193  337 
qed 
338 

339 
lemma mult_cancel_left [simp, noatp]: 

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

341 
proof  

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

29667  343 
by (simp add: algebra_simps right_minus_eq) 
344 
thus ?thesis by (simp add: right_minus_eq) 

26193  345 
qed 
346 

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

348 

23544  349 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  350 
begin 
351 

352 
lemma mult_cancel_right1 [simp]: 

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

29667  354 
by (insert mult_cancel_right [of 1 c b], force) 
26274  355 

356 
lemma mult_cancel_right2 [simp]: 

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

29667  358 
by (insert mult_cancel_right [of a c 1], simp) 
26274  359 

360 
lemma mult_cancel_left1 [simp]: 

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

29667  362 
by (insert mult_cancel_left [of c 1 b], force) 
26274  363 

364 
lemma mult_cancel_left2 [simp]: 

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

29667  366 
by (insert mult_cancel_left [of c a 1], simp) 
26274  367 

368 
end 

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

369 

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

372 

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

374 

29915
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

375 
lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a =  b)" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

376 
proof 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

377 
assume "a * a = b * b" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

378 
then have "(a  b) * (a + b) = 0" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

379 
by (simp add: algebra_simps) 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

380 
then show "a = b \<or> a =  b" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

381 
by (simp add: right_minus_eq eq_neg_iff_add_eq_0) 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

382 
next 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

383 
assume "a = b \<or> a =  b" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

384 
then show "a * a = b * b" by auto 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

385 
qed 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

386 

29981
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

387 
lemma dvd_mult_cancel_right [simp]: 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

388 
"a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

389 
proof  
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

390 
have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

391 
unfolding dvd_def by (simp add: mult_ac) 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

392 
also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

393 
unfolding dvd_def by simp 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

394 
finally show ?thesis . 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

395 
qed 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

396 

7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

397 
lemma dvd_mult_cancel_left [simp]: 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

398 
"c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

399 
proof  
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

400 
have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

401 
unfolding dvd_def by (simp add: mult_ac) 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

402 
also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

403 
unfolding dvd_def by simp 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

404 
finally show ?thesis . 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

405 
qed 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

406 

25186  407 
end 
25152  408 

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

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

413 

25186  414 
subclass ring_1_no_zero_divisors 
28823  415 
proof 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

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

417 
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

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

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

420 
assume ab: "a * b = 0" 
29667  421 
hence "0 = inverse a * (a * b) * inverse b" by simp 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

422 
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

423 
by (simp only: mult_assoc) 
29667  424 
also have "\<dots> = 1" using a b by simp 
425 
finally show False by simp 

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

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

427 
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

428 

26274  429 
lemma nonzero_imp_inverse_nonzero: 
430 
"a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0" 

431 
proof 

432 
assume ianz: "inverse a = 0" 

433 
assume "a \<noteq> 0" 

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

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

436 
finally have "1 = 0" . 

437 
thus False by (simp add: eq_commute) 

438 
qed 

439 

440 
lemma inverse_zero_imp_zero: 

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

442 
apply (rule classical) 

443 
apply (drule nonzero_imp_inverse_nonzero) 

444 
apply auto 

445 
done 

446 

447 
lemma inverse_unique: 

448 
assumes ab: "a * b = 1" 

449 
shows "inverse a = b" 

450 
proof  

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

29406  452 
moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
453 
ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 

26274  454 
qed 
455 

29406  456 
lemma nonzero_inverse_minus_eq: 
457 
"a \<noteq> 0 \<Longrightarrow> inverse ( a) =  inverse a" 

29667  458 
by (rule inverse_unique) simp 
29406  459 

460 
lemma nonzero_inverse_inverse_eq: 

461 
"a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a" 

29667  462 
by (rule inverse_unique) simp 
29406  463 

464 
lemma nonzero_inverse_eq_imp_eq: 

465 
assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0" 

466 
shows "a = b" 

467 
proof  

468 
from `inverse a = inverse b` 

29667  469 
have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) 
29406  470 
with `a \<noteq> 0` and `b \<noteq> 0` show "a = b" 
471 
by (simp add: nonzero_inverse_inverse_eq) 

472 
qed 

473 

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

29667  475 
by (rule inverse_unique) simp 
29406  476 

26274  477 
lemma nonzero_inverse_mult_distrib: 
29406  478 
assumes "a \<noteq> 0" and "b \<noteq> 0" 
26274  479 
shows "inverse (a * b) = inverse b * inverse a" 
480 
proof  

29667  481 
have "a * (b * inverse b) * inverse a = 1" using assms by simp 
482 
hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc) 

483 
thus ?thesis by (rule inverse_unique) 

26274  484 
qed 
485 

486 
lemma division_ring_inverse_add: 

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

29667  488 
by (simp add: algebra_simps) 
26274  489 

490 
lemma division_ring_inverse_diff: 

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

29667  492 
by (simp add: algebra_simps) 
26274  493 

25186  494 
end 
25152  495 

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

496 
class field = comm_ring_1 + inverse + 
25062  497 
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
498 
assumes divide_inverse: "a / b = a * inverse b" 

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

500 

25267  501 
subclass division_ring 
28823  502 
proof 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

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

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

505 
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

506 
thus "a * inverse a = 1" by (simp only: mult_commute) 
14738  507 
qed 
25230  508 

27516  509 
subclass idom .. 
25230  510 

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

512 
proof 

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

514 
{ 

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

516 
also assume "a / b = 1" 

517 
finally show "a = b" by simp 

518 
next 

519 
assume "a = b" 

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

521 
} 

522 
qed 

523 

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

29667  525 
by (simp add: divide_inverse) 
25230  526 

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

29667  528 
by (simp add: divide_inverse) 
25230  529 

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

29667  531 
by (simp add: divide_inverse) 
25230  532 

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

29667  534 
by (simp add: divide_inverse) 
25230  535 

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

29667  537 
by (simp add: divide_inverse algebra_simps) 
25230  538 

539 
end 

540 

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

543 

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

29667  546 
by (simp add: divide_inverse) 
25230  547 

548 
lemma divide_self_if [simp]: 

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

29667  550 
by simp 
25230  551 

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

555 

22390  556 
class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
25230  557 
begin 
558 

559 
lemma mult_mono: 

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

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

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

563 
apply (erule mult_left_mono, assumption) 

564 
done 

565 

566 
lemma mult_mono': 

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

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

569 
apply (rule mult_mono) 

570 
apply (fast intro: order_trans)+ 

571 
done 

572 

573 
end 

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

574 

22390  575 
class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add 
29904  576 
+ semiring + cancel_comm_monoid_add 
25267  577 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

578 

27516  579 
subclass semiring_0_cancel .. 
580 
subclass pordered_semiring .. 

23521  581 

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

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

29667  586 
by (drule mult_left_mono [of b zero], auto) 
25230  587 

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

29667  589 
by (drule mult_right_mono [of b zero], auto) 
25230  590 

26234  591 
lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0)  (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
29667  592 
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) 
25230  593 

594 
end 

595 

596 
class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono 

25267  597 
begin 
25230  598 

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

600 

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

602 

25230  603 
lemma mult_left_less_imp_less: 
604 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  605 
by (force simp add: mult_left_mono not_le [symmetric]) 
25230  606 

607 
lemma mult_right_less_imp_less: 

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

29667  609 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  610 

25186  611 
end 
25152  612 

22390  613 
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + 
25062  614 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
615 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

617 

27516  618 
subclass semiring_0_cancel .. 
14940  619 

25267  620 
subclass ordered_semiring 
28823  621 
proof 
23550  622 
fix a b c :: 'a 
623 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  625 
unfolding le_less 
626 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  627 
from A show "a * c \<le> b * c" 
25152  628 
unfolding le_less 
25186  629 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  630 
qed 
631 

25230  632 
lemma mult_left_le_imp_le: 
633 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

29667  634 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 
25230  635 

636 
lemma mult_right_le_imp_le: 

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

29667  638 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 
25230  639 

640 
lemma mult_pos_pos: 

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

29667  642 
by (drule mult_strict_left_mono [of zero b], auto) 
25230  643 

644 
lemma mult_pos_neg: 

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

29667  646 
by (drule mult_strict_left_mono [of b zero], auto) 
25230  647 

648 
lemma mult_pos_neg2: 

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

29667  650 
by (drule mult_strict_right_mono [of b zero], auto) 
25230  651 

652 
lemma zero_less_mult_pos: 

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

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

655 
apply (auto simp add: le_less not_less) 

656 
apply (drule_tac mult_pos_neg [of a b]) 

657 
apply (auto dest: less_not_sym) 

658 
done 

659 

660 
lemma zero_less_mult_pos2: 

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

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

663 
apply (auto simp add: le_less not_less) 

664 
apply (drule_tac mult_pos_neg2 [of a b]) 

665 
apply (auto dest: less_not_sym) 

666 
done 

667 

26193  668 
text{*Strict monotonicity in both arguments*} 
669 
lemma mult_strict_mono: 

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

671 
shows "a * c < b * d" 

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

673 
apply (simp add: mult_pos_pos) 

674 
apply (erule mult_strict_right_mono [THEN less_trans]) 

675 
apply (force simp add: le_less) 

676 
apply (erule mult_strict_left_mono, assumption) 

677 
done 

678 

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

680 
lemma mult_strict_mono': 

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

682 
shows "a * c < b * d" 

29667  683 
by (rule mult_strict_mono) (insert assms, auto) 
26193  684 

685 
lemma mult_less_le_imp_less: 

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

687 
shows "a * c < b * d" 

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

689 
apply (erule less_le_trans) 

690 
apply (erule mult_left_mono) 

691 
apply simp 

692 
apply (erule mult_strict_right_mono) 

693 
apply assumption 

694 
done 

695 

696 
lemma mult_le_less_imp_less: 

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

698 
shows "a * c < b * d" 

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

700 
apply (erule le_less_trans) 

701 
apply (erule mult_strict_left_mono) 

702 
apply simp 

703 
apply (erule mult_right_mono) 

704 
apply simp 

705 
done 

706 

707 
lemma mult_less_imp_less_left: 

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

709 
shows "a < b" 

710 
proof (rule ccontr) 

711 
assume "\<not> a < b" 

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

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

29667  714 
with this and less show False by (simp add: not_less [symmetric]) 
26193  715 
qed 
716 

717 
lemma mult_less_imp_less_right: 

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

719 
shows "a < b" 

720 
proof (rule ccontr) 

721 
assume "\<not> a < b" 

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

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

29667  724 
with this and less show False by (simp add: not_less [symmetric]) 
26193  725 
qed 
726 

25230  727 
end 
728 

22390  729 
class mult_mono1 = times + zero + ord + 
25230  730 
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
14270  731 

22390  732 
class pordered_comm_semiring = comm_semiring_0 
733 
+ pordered_ab_semigroup_add + mult_mono1 

25186  734 
begin 
25152  735 

25267  736 
subclass pordered_semiring 
28823  737 
proof 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

738 
fix a b c :: 'a 
23550  739 
assume "a \<le> b" "0 \<le> c" 
25230  740 
thus "c * a \<le> c * b" by (rule mult_mono1) 
23550  741 
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

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

743 

25267  744 
end 
745 

746 
class pordered_cancel_comm_semiring = comm_semiring_0_cancel 

747 
+ pordered_ab_semigroup_add + mult_mono1 

748 
begin 

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

749 

27516  750 
subclass pordered_comm_semiring .. 
751 
subclass pordered_cancel_semiring .. 

25267  752 

753 
end 

754 

755 
class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add + 

26193  756 
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  757 
begin 
758 

759 
subclass ordered_semiring_strict 

28823  760 
proof 
23550  761 
fix a b c :: 'a 
762 
assume "a < b" "0 < c" 

26193  763 
thus "c * a < c * b" by (rule mult_strict_left_mono_comm) 
23550  764 
thus "a * c < b * c" by (simp only: mult_commute) 
765 
qed 

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

766 

25267  767 
subclass pordered_cancel_comm_semiring 
28823  768 
proof 
23550  769 
fix a b c :: 'a 
770 
assume "a \<le> b" "0 \<le> c" 

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

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

775 

25267  776 
end 
25230  777 

25267  778 
class pordered_ring = ring + pordered_cancel_semiring 
779 
begin 

25230  780 

27516  781 
subclass pordered_ab_group_add .. 
14270  782 

29667  783 
text{*Legacy  use @{text algebra_simps} *} 
29833  784 
lemmas ring_simps[noatp] = algebra_simps 
25230  785 

786 
lemma less_add_iff1: 

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

29667  788 
by (simp add: algebra_simps) 
25230  789 

790 
lemma less_add_iff2: 

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

29667  792 
by (simp add: algebra_simps) 
25230  793 

794 
lemma le_add_iff1: 

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

29667  796 
by (simp add: algebra_simps) 
25230  797 

798 
lemma le_add_iff2: 

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

29667  800 
by (simp add: algebra_simps) 
25230  801 

802 
lemma mult_left_mono_neg: 

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

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

805 
apply (simp_all add: minus_mult_left [symmetric]) 

806 
done 

807 

808 
lemma mult_right_mono_neg: 

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

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

811 
apply (simp_all add: minus_mult_right [symmetric]) 

812 
done 

813 

814 
lemma mult_nonpos_nonpos: 

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

29667  816 
by (drule mult_right_mono_neg [of a zero b]) auto 
25230  817 

818 
lemma split_mult_pos_le: 

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

29667  820 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 
25186  821 

822 
end 

14270  823 

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

826 

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

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

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

832 

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

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

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

836 

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

838 

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

839 
subclass pordered_ab_group_add_abs 
28823  840 
proof 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

842 
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
29667  843 
by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

845 
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

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

847 
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

848 

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

849 
end 
23521  850 

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

853 
*) 

854 
class ordered_ring_strict = ring + ordered_semiring_strict 

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

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

857 

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

859 

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

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

863 
apply (simp_all add: minus_mult_left [symmetric]) 

864 
done 

14738  865 

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

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

869 
apply (simp_all add: minus_mult_right [symmetric]) 

870 
done 

14738  871 

25230  872 
lemma mult_neg_neg: 
873 
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 

29667  874 
by (drule mult_strict_right_mono_neg, auto) 
14738  875 

25917  876 
subclass ring_no_zero_divisors 
28823  877 
proof 
25917  878 
fix a b 
879 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

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

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

882 
proof (cases "a < 0") 

883 
case True note A' = this 

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

885 
case True with A' 

886 
show ?thesis by (auto dest: mult_neg_neg) 

887 
next 

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

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

890 
qed 

891 
next 

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

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

894 
case True with A' 

895 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

896 
next 

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

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

899 
qed 

900 
qed 

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

902 
qed 

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

903 

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

904 
lemma zero_less_mult_iff: 
25917  905 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
906 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

907 
apply (simp_all add: not_less le_less) 

908 
apply (erule disjE) apply assumption defer 

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

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

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

912 
apply (drule sym) apply simp 

913 
apply (blast dest: zero_less_mult_pos) 

25230  914 
apply (blast dest: zero_less_mult_pos2) 
915 
done 

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

916 

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

917 
lemma zero_le_mult_iff: 
25917  918 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
29667  919 
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

920 

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

921 
lemma mult_less_0_iff: 
25917  922 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
923 
apply (insert zero_less_mult_iff [of "a" b]) 

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

925 
done 

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

926 

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

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

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

931 
done 

932 

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

29667  934 
by (simp add: zero_le_mult_iff linear) 
25917  935 

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

29667  937 
by (simp add: not_less) 
25917  938 

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

941 

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

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

944 

945 
lemma mult_less_cancel_right_disj: 

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

947 
apply (cases "c = 0") 

948 
apply (auto simp add: neq_iff mult_strict_right_mono 

949 
mult_strict_right_mono_neg) 

950 
apply (auto simp add: not_less 

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

952 
not_le [symmetric, of a]) 

953 
apply (erule_tac [!] notE) 

954 
apply (auto simp add: less_imp_le mult_right_mono 

955 
mult_right_mono_neg) 

956 
done 

957 

958 
lemma mult_less_cancel_left_disj: 

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

960 
apply (cases "c = 0") 

961 
apply (auto simp add: neq_iff mult_strict_left_mono 

962 
mult_strict_left_mono_neg) 

963 
apply (auto simp add: not_less 

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

965 
not_le [symmetric, of a]) 

966 
apply (erule_tac [!] notE) 

967 
apply (auto simp add: less_imp_le mult_left_mono 

968 
mult_left_mono_neg) 

969 
done 

970 

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

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

973 

974 
lemma mult_less_cancel_right: 

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

976 
using mult_less_cancel_right_disj [of a c b] by auto 

977 

978 
lemma mult_less_cancel_left: 

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

980 
using mult_less_cancel_left_disj [of c a b] by auto 

981 

982 
lemma mult_le_cancel_right: 

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

29667  984 
by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 
26193  985 

986 
lemma mult_le_cancel_left: 

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

29667  988 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 
26193  989 

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

991 

29667  992 
text{*Legacy  use @{text algebra_simps} *} 
29833  993 
lemmas ring_simps[noatp] = algebra_simps 
25230  994 

995 

996 
class pordered_comm_ring = comm_ring + pordered_comm_semiring 

25267  997 
begin 
25230  998 

27516  999 
subclass pordered_ring .. 
1000 
subclass pordered_cancel_comm_semiring .. 

25230  1001 

25267  1002 
end 
25230  1003 

1004 
class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + 

1005 
(*previously ordered_semiring*) 

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

1007 
begin 

1008 

1009 
lemma pos_add_strict: 

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

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

1012 

26193  1013 
lemma zero_le_one [simp]: "0 \<le> 1" 
29667  1014 
by (rule zero_less_one [THEN less_imp_le]) 
26193  1015 

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

29667  1017 
by (simp add: not_le) 
26193  1018 

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

29667  1020 
by (simp add: not_less) 
26193  1021 

1022 
lemma less_1_mult: 

1023 
assumes "1 < m" and "1 < n" 

1024 
shows "1 < m * n" 

1025 
using assms mult_strict_mono [of 1 m 1 n] 

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

1027 

25230  1028 
end 
1029 

26193  1030 
class ordered_idom = comm_ring_1 + 
1031 
ordered_comm_semiring_strict + ordered_ab_group_add + 

25230  1032 
abs_if + sgn_if 
1033 
(*previously ordered_ring*) 

25917  1034 
begin 
1035 

27516  1036 
subclass ordered_ring_strict .. 
1037 
subclass pordered_comm_ring .. 

1038 
subclass idom .. 

25917  1039 

1040 
subclass ordered_semidom 

28823  1041 
proof 
26193  1042 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
1043 
thus "0 < 1" by (simp add: le_less) 

25917  1044 
qed 
1045 

26193  1046 
lemma linorder_neqE_ordered_idom: 
1047 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 

1048 
using assms by (rule neqE) 

1049 

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

1052 
lemma mult_le_cancel_right1: 

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

29667  1054 
by (insert mult_le_cancel_right [of 1 c b], simp) 
26274  1055 

1056 
lemma mult_le_cancel_right2: 

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

29667  1058 
by (insert mult_le_cancel_right [of a c 1], simp) 
26274  1059 

1060 
lemma mult_le_cancel_left1: 

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

29667  1062 
by (insert mult_le_cancel_left [of c 1 b], simp) 
26274  1063 

1064 
lemma mult_le_cancel_left2: 

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

29667  1066 
by (insert mult_le_cancel_left [of c a 1], simp) 
26274  1067 

1068 
lemma mult_less_cancel_right1: 

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

29667  1070 
by (insert mult_less_cancel_right [of 1 c b], simp) 
26274  1071 

1072 
lemma mult_less_cancel_right2: 

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

29667  1074 
by (insert mult_less_cancel_right [of a c 1], simp) 
26274  1075 

1076 
lemma mult_less_cancel_left1: 

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

29667  1078 
by (insert mult_less_cancel_left [of c 1 b], simp) 
26274  1079 

1080 
lemma mult_less_cancel_left2: 

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

29667  1082 
by (insert mult_less_cancel_left [of c a 1], simp) 
26274  1083 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1084 
lemma sgn_sgn [simp]: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1085 
"sgn (sgn a) = sgn a" 
29700  1086 
unfolding sgn_if by simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1087 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1088 
lemma sgn_0_0: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1089 
"sgn a = 0 \<longleftrightarrow> a = 0" 
29700  1090 
unfolding sgn_if by simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1091 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1092 
lemma sgn_1_pos: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1093 
"sgn a = 1 \<longleftrightarrow> a > 0" 
29700  1094 
unfolding sgn_if by (simp add: neg_equal_zero) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1095 

16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1096 
lemma sgn_1_neg: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1097 
"sgn a =  1 \<longleftrightarrow> a < 0" 
29700  1098 
unfolding sgn_if by (auto simp add: equal_neg_zero) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1099 

29940  1100 
lemma sgn_pos [simp]: 
1101 
"0 < a \<Longrightarrow> sgn a = 1" 

1102 
unfolding sgn_1_pos . 

1103 

1104 
lemma sgn_neg [simp]: 

1105 
"a < 0 \<Longrightarrow> sgn a =  1" 

1106 
unfolding sgn_1_neg . 

1107 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1108 
lemma sgn_times: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1109 
"sgn (a * b) = sgn a * sgn b" 
29667  1110 
by (auto simp add: sgn_if zero_less_mult_iff) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1111 

29653  1112 
lemma abs_sgn: "abs k = k * sgn k" 
29700  1113 
unfolding sgn_if abs_if by auto 
1114 

29940  1115 
lemma sgn_greater [simp]: 
1116 
"0 < sgn a \<longleftrightarrow> 0 < a" 

1117 
unfolding sgn_if by auto 

1118 

1119 
lemma sgn_less [simp]: 

1120 
"sgn a < 0 \<longleftrightarrow> a < 0" 

1121 
unfolding sgn_if by auto 

1122 

29949  1123 
lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k" 
1124 
by (simp add: abs_if) 

1125 

1126 
lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k" 

1127 
by (simp add: abs_if) 

29653  1128 

25917  1129 
end 
25230  1130 

1131 
class ordered_field = field + ordered_idom 

1132 

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

1134 

29833  1135 
lemmas mult_compare_simps[noatp] = 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

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

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

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

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

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

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

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

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

1145 

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

1147 

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

1148 
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

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

1151 

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

1152 
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

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

1156 
next 

1157 
assume "a\<noteq>0" 

1158 
thus ?thesis by (simp add: nonzero_inverse_minus_eq) 

1159 
qed 

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

1160 

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

1161 
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

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

1164 
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

1165 
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

1166 
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

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

1168 

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

1169 
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

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

1171 
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

1172 

14270  1173 
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

1174 
"inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" 
14270  1175 
proof cases 
1176 
assume "a=0" thus ?thesis by simp 

1177 
next 

1178 
assume "a\<noteq>0" 

1179 
thus ?thesis by (simp add: nonzero_inverse_inverse_eq) 

1180 
qed 

1181 

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

1183 
the righthand side.*} 

1184 
lemma inverse_mult_distrib [simp]: 

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

1186 
proof cases 

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

29667  1188 
thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute) 
14270  1189 
next 
1190 
assume "~ (a \<noteq> 0 & b \<noteq> 0)" 

29667  1191 
thus ?thesis by force 
14270  1192 
qed 
1193 

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

1195 
lemma inverse_add: 

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

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

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

1198 
by (simp add: division_ring_inverse_add mult_ac) 
14270  1199 

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

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

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

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

1203 

23389  1204 

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

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

1206 

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

1207 
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

1208 
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

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

1210 

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

1212 
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

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

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

1216 
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

1217 
by (simp only: mult_ac) 
29667  1218 
also have "... = a * inverse b" by simp 
1219 
finally show ?thesis by (simp add: divide_inverse) 

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

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

1221 

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

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

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

1225 
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

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

1227 

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

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

1230 
by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
14321  1231 

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

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

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

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

1237 

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

1238 
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

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

1240 

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

1241 
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

1242 
by (simp add: divide_inverse mult_assoc) 
14288  1243 

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

1244 
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

1245 
by (simp add: divide_inverse mult_ac) 
14288  1246 

29833  1247 
lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left 
23482  1248 

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

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

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

1251 
by (simp add: divide_inverse mult_ac) 
14288  1252 

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

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

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

1255 
by (simp add: divide_inverse mult_assoc) 
14288  1256 

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

1257 
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

1258 
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

1259 
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

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

1261 
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

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

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

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

1265 
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

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

1267 
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

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

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

1270 

23389  1271 

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

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

1273 

24427 