author  haftmann 
Fri, 05 Feb 2010 14:33:50 +0100  
changeset 35028  108662d50512 
parent 34146  14595e0c27e8 
child 35032  7efe662e41b4 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

1 
(* Title: HOL/Ring_and_Field.thy 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

2 
Author: Gertrud Bauer 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

3 
Author: Steven Obua 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

4 
Author: Tobias Nipkow 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

5 
Author: Lawrence C Paulson 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

6 
Author: Markus Wenzel 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

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

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

9 

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

11 

15229  12 
theory Ring_and_Field 
15140  13 
imports OrderedGroup 
15131  14 
begin 
14504  15 

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

18 
\begin{itemize} 

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

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

21 
\end{itemize} 

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

23 
\begin{itemize} 

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

27 
*} 

14504  28 

22390  29 
class semiring = ab_semigroup_add + semigroup_mult + 
29667  30 
assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c" 
31 
assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c" 

25152  32 
begin 
33 

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

35 
lemma combine_common_factor: 

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

29667  37 
by (simp add: left_distrib add_ac) 
25152  38 

39 
end 

14504  40 

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

44 

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

46 

29904  47 
class semiring_0_cancel = semiring + cancel_comm_monoid_add 
25186  48 
begin 
14504  49 

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

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

25152  55 
next 
56 
fix a :: 'a 

29667  57 
have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric]) 
58 
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

59 
qed 
14940  60 

25186  61 
end 
25152  62 

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

25152  67 
subclass semiring 
28823  68 
proof 
14738  69 
fix a b c :: 'a 
70 
show "(a + b) * c = a * c + b * c" by (simp add: distrib) 

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

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

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

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

14504  75 
qed 
76 

25152  77 
end 
14504  78 

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

81 

27516  82 
subclass semiring_0 .. 
25152  83 

84 
end 

14504  85 

29904  86 
class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add 
25186  87 
begin 
14940  88 

27516  89 
subclass semiring_0_cancel .. 
14940  90 

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

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

92 

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

94 

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

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

29667  100 
by (rule not_sym) (rule zero_neq_one) 
26193  101 

102 
end 

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

103 

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

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

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

107 

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

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

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

110 

28559  111 
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where 
112 
[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

113 

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

114 
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

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

116 

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

117 
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

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

119 

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

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

121 

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

122 
class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd 
22390  123 
(*previously almost_semiring*) 
25152  124 
begin 
14738  125 

27516  126 
subclass semiring_1 .. 
25152  127 

29925  128 
lemma dvd_refl[simp]: "a dvd a" 
28559  129 
proof 
130 
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

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

132 

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

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

134 
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

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

136 
proof  
28559  137 
from assms obtain v where "b = a * v" by (auto elim!: dvdE) 
138 
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

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

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

142 

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

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

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

147 
proof 

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

148 
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

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

150 

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

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

153 

30042  154 
lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)" 
29667  155 
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

156 

30042  157 
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

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

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

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

161 

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

162 
lemma dvd_triv_right [simp]: "a dvd b * a" 
29667  163 
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

164 

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

165 
lemma dvd_triv_left [simp]: "a dvd a * b" 
29667  166 
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

167 

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

168 
lemma mult_dvd_mono: 
30042  169 
assumes "a dvd b" 
170 
and "c dvd d" 

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

171 
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

172 
proof  
30042  173 
from `a dvd b` obtain b' where "b = a * b'" .. 
174 
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

175 
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

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

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

178 

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

179 
lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c" 
29667  180 
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

181 

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

182 
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

183 
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

184 

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

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

187 

29925  188 
lemma dvd_add[simp]: 
189 
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

190 
proof  
29925  191 
from `a dvd b` obtain b' where "b = a * b'" .. 
192 
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

193 
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

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

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

196 

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

198 

29925  199 

22390  200 
class no_zero_divisors = zero + times + 
25062  201 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
14504  202 

29904  203 
class semiring_1_cancel = semiring + cancel_comm_monoid_add 
204 
+ zero_neq_one + monoid_mult 

25267  205 
begin 
14940  206 

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

208 

27516  209 
subclass semiring_1 .. 
25267  210 

211 
end 

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

212 

29904  213 
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add 
214 
+ zero_neq_one + comm_monoid_mult 

25267  215 
begin 
14738  216 

27516  217 
subclass semiring_1_cancel .. 
218 
subclass comm_semiring_0_cancel .. 

219 
subclass comm_semiring_1 .. 

25267  220 

221 
end 

25152  222 

22390  223 
class ring = semiring + ab_group_add 
25267  224 
begin 
25152  225 

27516  226 
subclass semiring_0_cancel .. 
25152  227 

228 
text {* Distribution rules *} 

229 

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

34146
14595e0c27e8
rename equals_zero_I to minus_unique (keep old name too)
huffman
parents:
33676
diff
changeset

231 
by (rule minus_unique) (simp add: left_distrib [symmetric]) 
25152  232 

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

34146
14595e0c27e8
rename equals_zero_I to minus_unique (keep old name too)
huffman
parents:
33676
diff
changeset

234 
by (rule minus_unique) (simp add: right_distrib [symmetric]) 
25152  235 

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

236 
text{*Extract signs from products*} 
29833  237 
lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric] 
238 
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

239 

25152  240 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  241 
by simp 
25152  242 

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

29667  244 
by simp 
245 

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

247 
by (simp add: right_distrib diff_minus) 

248 

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

250 
by (simp add: left_distrib diff_minus) 

25152  251 

29833  252 
lemmas ring_distribs[noatp] = 
25152  253 
right_distrib left_distrib left_diff_distrib right_diff_distrib 
254 

29667  255 
text{*Legacy  use @{text algebra_simps} *} 
29833  256 
lemmas ring_simps[noatp] = algebra_simps 
25230  257 

258 
lemma eq_add_iff1: 

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

29667  260 
by (simp add: algebra_simps) 
25230  261 

262 
lemma eq_add_iff2: 

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

29667  264 
by (simp add: algebra_simps) 
25230  265 

25152  266 
end 
267 

29833  268 
lemmas ring_distribs[noatp] = 
25152  269 
right_distrib left_distrib left_diff_distrib right_diff_distrib 
270 

22390  271 
class comm_ring = comm_semiring + ab_group_add 
25267  272 
begin 
14738  273 

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

275 
subclass comm_semiring_0_cancel .. 
25267  276 

277 
end 

14738  278 

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

281 

27516  282 
subclass semiring_1_cancel .. 
25267  283 

284 
end 

25152  285 

22390  286 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
287 
(*previously ring*) 

25267  288 
begin 
14738  289 

27516  290 
subclass ring_1 .. 
291 
subclass comm_semiring_1_cancel .. 

25267  292 

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

293 
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

294 
proof 
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 
next 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

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

300 
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

301 
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

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

303 

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

304 
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

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

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

307 
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

308 
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

309 
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

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

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

312 
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

313 
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

314 
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

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

316 

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

29409  319 

25267  320 
end 
25152  321 

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

322 
class ring_no_zero_divisors = ring + no_zero_divisors 
25230  323 
begin 
324 

325 
lemma mult_eq_0_iff [simp]: 

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

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

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

329 
then show ?thesis using no_zero_divisors by simp 

330 
next 

331 
case True then show ?thesis by auto 

332 
qed 

333 

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

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

337 
proof  

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

29667  339 
by (simp add: algebra_simps right_minus_eq) 
340 
thus ?thesis by (simp add: disj_commute right_minus_eq) 

26193  341 
qed 
342 

343 
lemma mult_cancel_left [simp, noatp]: 

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

345 
proof  

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

29667  347 
by (simp add: algebra_simps right_minus_eq) 
348 
thus ?thesis by (simp add: right_minus_eq) 

26193  349 
qed 
350 

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

352 

23544  353 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  354 
begin 
355 

356 
lemma mult_cancel_right1 [simp]: 

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

29667  358 
by (insert mult_cancel_right [of 1 c b], force) 
26274  359 

360 
lemma mult_cancel_right2 [simp]: 

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

29667  362 
by (insert mult_cancel_right [of a c 1], simp) 
26274  363 

364 
lemma mult_cancel_left1 [simp]: 

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

29667  366 
by (insert mult_cancel_left [of c 1 b], force) 
26274  367 

368 
lemma mult_cancel_left2 [simp]: 

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

29667  370 
by (insert mult_cancel_left [of c a 1], simp) 
26274  371 

372 
end 

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

373 

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

376 

27516  377 
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

378 

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

379 
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

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

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

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

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

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

385 
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

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

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

388 
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

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

390 

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

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

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

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

394 
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

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

396 
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

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

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

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

400 

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

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

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

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

404 
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

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

406 
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

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

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

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

410 

25186  411 
end 
25152  412 

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

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

417 

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

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

421 
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

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

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

424 
assume ab: "a * b = 0" 
29667  425 
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

426 
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

427 
by (simp only: mult_assoc) 
29667  428 
also have "\<dots> = 1" using a b by simp 
429 
finally show False by simp 

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

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

431 
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

432 

26274  433 
lemma nonzero_imp_inverse_nonzero: 
434 
"a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0" 

435 
proof 

436 
assume ianz: "inverse a = 0" 

437 
assume "a \<noteq> 0" 

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

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

440 
finally have "1 = 0" . 

441 
thus False by (simp add: eq_commute) 

442 
qed 

443 

444 
lemma inverse_zero_imp_zero: 

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

446 
apply (rule classical) 

447 
apply (drule nonzero_imp_inverse_nonzero) 

448 
apply auto 

449 
done 

450 

451 
lemma inverse_unique: 

452 
assumes ab: "a * b = 1" 

453 
shows "inverse a = b" 

454 
proof  

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

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

26274  458 
qed 
459 

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

29667  462 
by (rule inverse_unique) simp 
29406  463 

464 
lemma nonzero_inverse_inverse_eq: 

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

29667  466 
by (rule inverse_unique) simp 
29406  467 

468 
lemma nonzero_inverse_eq_imp_eq: 

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

470 
shows "a = b" 

471 
proof  

472 
from `inverse a = inverse b` 

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

476 
qed 

477 

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

29667  479 
by (rule inverse_unique) simp 
29406  480 

26274  481 
lemma nonzero_inverse_mult_distrib: 
29406  482 
assumes "a \<noteq> 0" and "b \<noteq> 0" 
26274  483 
shows "inverse (a * b) = inverse b * inverse a" 
484 
proof  

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

487 
thus ?thesis by (rule inverse_unique) 

26274  488 
qed 
489 

490 
lemma division_ring_inverse_add: 

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

29667  492 
by (simp add: algebra_simps) 
26274  493 

494 
lemma division_ring_inverse_diff: 

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

29667  496 
by (simp add: algebra_simps) 
26274  497 

25186  498 
end 
25152  499 

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

500 
class field = comm_ring_1 + inverse + 
25062  501 
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
502 
assumes divide_inverse: "a / b = a * inverse b" 

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

504 

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

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

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

509 
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

510 
thus "a * inverse a = 1" by (simp only: mult_commute) 
14738  511 
qed 
25230  512 

27516  513 
subclass idom .. 
25230  514 

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

516 
proof 

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

518 
{ 

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

520 
also assume "a / b = 1" 

521 
finally show "a = b" by simp 

522 
next 

523 
assume "a = b" 

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

525 
} 

526 
qed 

527 

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

29667  529 
by (simp add: divide_inverse) 
25230  530 

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

29667  532 
by (simp add: divide_inverse) 
25230  533 

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

29667  535 
by (simp add: divide_inverse) 
25230  536 

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

29667  538 
by (simp add: divide_inverse) 
25230  539 

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

30630  541 
by (simp add: divide_inverse algebra_simps) 
542 

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

544 
lemma inverse_add: 

545 
"[ a \<noteq> 0; b \<noteq> 0 ] 

546 
==> inverse a + inverse b = (a + b) * inverse a * inverse b" 

547 
by (simp add: division_ring_inverse_add mult_ac) 

548 

549 
lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]: 

550 
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b" 

551 
proof  

552 
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" 

553 
by (simp add: divide_inverse nonzero_inverse_mult_distrib) 

554 
also have "... = a * inverse b * (inverse c * c)" 

555 
by (simp only: mult_ac) 

556 
also have "... = a * inverse b" by simp 

557 
finally show ?thesis by (simp add: divide_inverse) 

558 
qed 

559 

560 
lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]: 

561 
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b" 

562 
by (simp add: mult_commute [of _ c]) 

563 

564 
lemma divide_1 [simp]: "a / 1 = a" 

565 
by (simp add: divide_inverse) 

566 

567 
lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" 

568 
by (simp add: divide_inverse mult_assoc) 

569 

570 
lemma times_divide_eq_left: "(b / c) * a = (b * a) / c" 

571 
by (simp add: divide_inverse mult_ac) 

572 

573 
text {* These are later declared as simp rules. *} 

574 
lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left 

575 

576 
lemma add_frac_eq: 

577 
assumes "y \<noteq> 0" and "z \<noteq> 0" 

578 
shows "x / y + w / z = (x * z + w * y) / (y * z)" 

579 
proof  

580 
have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)" 

581 
using assms by simp 

582 
also have "\<dots> = (x * z + y * w) / (y * z)" 

583 
by (simp only: add_divide_distrib) 

584 
finally show ?thesis 

585 
by (simp only: mult_commute) 

586 
qed 

587 

588 
text{*Special Cancellation Simprules for Division*} 

589 

590 
lemma nonzero_mult_divide_cancel_right [simp, noatp]: 

591 
"b \<noteq> 0 \<Longrightarrow> a * b / b = a" 

592 
using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp 

593 

594 
lemma nonzero_mult_divide_cancel_left [simp, noatp]: 

595 
"a \<noteq> 0 \<Longrightarrow> a * b / a = b" 

596 
using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp 

597 

598 
lemma nonzero_divide_mult_cancel_right [simp, noatp]: 

599 
"\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a" 

600 
using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp 

601 

602 
lemma nonzero_divide_mult_cancel_left [simp, noatp]: 

603 
"\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b" 

604 
using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp 

605 

606 
lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]: 

607 
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b" 

608 
using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac) 

609 

610 
lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]: 

611 
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b" 

612 
using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac) 

613 

614 
lemma minus_divide_left: " (a / b) = (a) / b" 

615 
by (simp add: divide_inverse) 

616 

617 
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==>  (a / b) = a / ( b)" 

618 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 

619 

620 
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (a) / (b) = a / b" 

621 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 

622 

623 
lemma divide_minus_left [simp, noatp]: "(a) / b =  (a / b)" 

624 
by (simp add: divide_inverse) 

625 

626 
lemma diff_divide_distrib: "(a  b) / c = a / c  b / c" 

627 
by (simp add: diff_minus add_divide_distrib) 

628 

629 
lemma add_divide_eq_iff: 

630 
"z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z" 

631 
by (simp add: add_divide_distrib) 

632 

633 
lemma divide_add_eq_iff: 

634 
"z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z" 

635 
by (simp add: add_divide_distrib) 

636 

637 
lemma diff_divide_eq_iff: 

638 
"z \<noteq> 0 \<Longrightarrow> x  y / z = (z * x  y) / z" 

639 
by (simp add: diff_divide_distrib) 

640 

641 
lemma divide_diff_eq_iff: 

642 
"z \<noteq> 0 \<Longrightarrow> x / z  y = (x  z * y) / z" 

643 
by (simp add: diff_divide_distrib) 

644 

645 
lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b" 

646 
proof  

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

648 
have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp 

649 
also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc) 

650 
finally show ?thesis . 

651 
qed 

652 

653 
lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c" 

654 
proof  

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

656 
have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp 

657 
also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) 

658 
finally show ?thesis . 

659 
qed 

660 

661 
lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a" 

662 
by simp 

663 

664 
lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c" 

665 
by (erule subst, simp) 

666 

667 
lemmas field_eq_simps[noatp] = algebra_simps 

668 
(* pull / out*) 

669 
add_divide_eq_iff divide_add_eq_iff 

670 
diff_divide_eq_iff divide_diff_eq_iff 

671 
(* multiply eqn *) 

672 
nonzero_eq_divide_eq nonzero_divide_eq_eq 

673 
(* is added later: 

674 
times_divide_eq_left times_divide_eq_right 

675 
*) 

676 

677 
text{*An example:*} 

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

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

680 
apply(simp add:field_eq_simps) 

681 
apply(simp) 

682 
done 

683 

684 
lemma diff_frac_eq: 

685 
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y  w / z = (x * z  w * y) / (y * z)" 

686 
by (simp add: field_eq_simps times_divide_eq) 

687 

688 
lemma frac_eq_eq: 

689 
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)" 

690 
by (simp add: field_eq_simps times_divide_eq) 

25230  691 

692 
end 

693 

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

696 

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

29667  699 
by (simp add: divide_inverse) 
25230  700 

701 
lemma divide_self_if [simp]: 

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

29667  703 
by simp 
25230  704 

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

708 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

709 
class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
25230  710 
begin 
711 

712 
lemma mult_mono: 

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

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

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

716 
apply (erule mult_left_mono, assumption) 

717 
done 

718 

719 
lemma mult_mono': 

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

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

722 
apply (rule mult_mono) 

723 
apply (fast intro: order_trans)+ 

724 
done 

725 

726 
end 

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

727 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

728 
class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add 
29904  729 
+ semiring + cancel_comm_monoid_add 
25267  730 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

731 

27516  732 
subclass semiring_0_cancel .. 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

733 
subclass ordered_semiring .. 
23521  734 

25230  735 
lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b" 
30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

736 
using mult_left_mono [of zero b a] by simp 
25230  737 

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

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

739 
using mult_left_mono [of b zero a] by simp 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

740 

44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

741 
lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

742 
using mult_right_mono [of a zero b] by simp 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

743 

44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

744 
text {* Legacy  use @{text mult_nonpos_nonneg} *} 
25230  745 
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
29667  746 
by (drule mult_right_mono [of b zero], auto) 
25230  747 

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

751 
end 

752 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

753 
class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono 
25267  754 
begin 
25230  755 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

756 
subclass ordered_cancel_semiring .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

757 

108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

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

759 

25230  760 
lemma mult_left_less_imp_less: 
761 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  762 
by (force simp add: mult_left_mono not_le [symmetric]) 
25230  763 

764 
lemma mult_right_less_imp_less: 

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

29667  766 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  767 

25186  768 
end 
25152  769 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

770 
class linlinordered_semiring_1 = linordered_semiring + semiring_1 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

771 

108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

772 
class linlinordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + 
25062  773 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
774 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

776 

27516  777 
subclass semiring_0_cancel .. 
14940  778 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

779 
subclass linordered_semiring 
28823  780 
proof 
23550  781 
fix a b c :: 'a 
782 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  784 
unfolding le_less 
785 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  786 
from A show "a * c \<le> b * c" 
25152  787 
unfolding le_less 
25186  788 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  789 
qed 
790 

25230  791 
lemma mult_left_le_imp_le: 
792 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

29667  793 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 
25230  794 

795 
lemma mult_right_le_imp_le: 

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

29667  797 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 
25230  798 

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

799 
lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

800 
using mult_strict_left_mono [of zero b a] by simp 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

801 

44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

802 
lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

803 
using mult_strict_left_mono [of b zero a] by simp 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

804 

44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

805 
lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

806 
using mult_strict_right_mono [of a zero b] by simp 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

807 

44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

808 
text {* Legacy  use @{text mult_neg_pos} *} 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

809 
lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
29667  810 
by (drule mult_strict_right_mono [of b zero], auto) 
25230  811 

812 
lemma zero_less_mult_pos: 

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

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

814 
apply (cases "b\<le>0") 
25230  815 
apply (auto simp add: le_less not_less) 
30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

816 
apply (drule_tac mult_pos_neg [of a b]) 
25230  817 
apply (auto dest: less_not_sym) 
818 
done 

819 

820 
lemma zero_less_mult_pos2: 

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

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

822 
apply (cases "b\<le>0") 
25230  823 
apply (auto simp add: le_less not_less) 
30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

824 
apply (drule_tac mult_pos_neg2 [of a b]) 
25230  825 
apply (auto dest: less_not_sym) 
826 
done 

827 

26193  828 
text{*Strict monotonicity in both arguments*} 
829 
lemma mult_strict_mono: 

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

831 
shows "a * c < b * d" 

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

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

833 
apply (simp add: mult_pos_pos) 
26193  834 
apply (erule mult_strict_right_mono [THEN less_trans]) 
30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

835 
apply (force simp add: le_less) 
26193  836 
apply (erule mult_strict_left_mono, assumption) 
837 
done 

838 

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

840 
lemma mult_strict_mono': 

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

842 
shows "a * c < b * d" 

29667  843 
by (rule mult_strict_mono) (insert assms, auto) 
26193  844 

845 
lemma mult_less_le_imp_less: 

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

847 
shows "a * c < b * d" 

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

849 
apply (erule less_le_trans) 

850 
apply (erule mult_left_mono) 

851 
apply simp 

852 
apply (erule mult_strict_right_mono) 

853 
apply assumption 

854 
done 

855 

856 
lemma mult_le_less_imp_less: 

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

858 
shows "a * c < b * d" 

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

860 
apply (erule le_less_trans) 

861 
apply (erule mult_strict_left_mono) 

862 
apply simp 

863 
apply (erule mult_right_mono) 

864 
apply simp 

865 
done 

866 

867 
lemma mult_less_imp_less_left: 

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

869 
shows "a < b" 

870 
proof (rule ccontr) 

871 
assume "\<not> a < b" 

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

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

29667  874 
with this and less show False by (simp add: not_less [symmetric]) 
26193  875 
qed 
876 

877 
lemma mult_less_imp_less_right: 

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

879 
shows "a < b" 

880 
proof (rule ccontr) 

881 
assume "\<not> a < b" 

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

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

29667  884 
with this and less show False by (simp add: not_less [symmetric]) 
26193  885 
qed 
886 

25230  887 
end 
888 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

889 
class linlinlinordered_semiring_1_strict = linlinordered_semiring_strict + semiring_1 
33319  890 

22390  891 
class mult_mono1 = times + zero + ord + 
25230  892 
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
14270  893 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

894 
class ordered_comm_semiring = comm_semiring_0 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

895 
+ ordered_ab_semigroup_add + mult_mono1 
25186  896 
begin 
25152  897 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

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

900 
fix a b c :: 'a 
23550  901 
assume "a \<le> b" "0 \<le> c" 
25230  902 
thus "c * a \<le> c * b" by (rule mult_mono1) 
23550  903 
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

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

905 

25267  906 
end 
907 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

908 
class ordered_cancel_comm_semiring = comm_semiring_0_cancel 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

909 
+ ordered_ab_semigroup_add + mult_mono1 
25267  910 
begin 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

911 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

912 
subclass ordered_comm_semiring .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

913 
subclass ordered_cancel_semiring .. 
25267  914 

915 
end 

916 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

917 
class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add + 
26193  918 
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  919 
begin 
920 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

921 
subclass linlinordered_semiring_strict 
28823  922 
proof 
23550  923 
fix a b c :: 'a 
924 
assume "a < b" "0 < c" 

26193  925 
thus "c * a < c * b" by (rule mult_strict_left_mono_comm) 
23550  926 
thus "a * c < b * c" by (simp only: mult_commute) 
927 
qed 

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

928 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

929 
subclass ordered_cancel_comm_semiring 
28823  930 
proof 
23550  931 
fix a b c :: 'a 
932 
assume "a \<le> b" "0 \<le> c" 

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

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

937 

25267  938 
end 
25230  939 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

940 
class ordered_ring = ring + ordered_cancel_semiring 
25267  941 
begin 
25230  942 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

943 
subclass ordered_ab_group_add .. 
14270  944 

29667  945 
text{*Legacy  use @{text algebra_simps} *} 
29833  946 
lemmas ring_simps[noatp] = algebra_simps 
25230  947 

948 
lemma less_add_iff1: 

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

29667  950 
by (simp add: algebra_simps) 
25230  951 

952 
lemma less_add_iff2: 

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

29667  954 
by (simp add: algebra_simps) 
25230  955 

956 
lemma le_add_iff1: 

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

29667  958 
by (simp add: algebra_simps) 
25230  959 

960 
lemma le_add_iff2: 

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

29667  962 
by (simp add: algebra_simps) 
25230  963 

964 
lemma mult_left_mono_neg: 

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

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

967 
apply (simp_all add: minus_mult_left [symmetric]) 

968 
done 

969 

970 
lemma mult_right_mono_neg: 

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

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

973 
apply (simp_all add: minus_mult_right [symmetric]) 

974 
done 

975 

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

976 
lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

977 
using mult_right_mono_neg [of a zero b] by simp 
25230  978 

979 
lemma split_mult_pos_le: 

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

29667  981 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 
25186  982 

983 
end 

14270  984 

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

987 

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

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

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

993 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

994 
class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

996 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

997 
subclass ordered_ring .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

998 

108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

999 
subclass ordered_ab_group_add_abs 
28823  1000 
proof 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

1002 
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1003 
by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

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

1005 
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

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

1007 
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

1008 

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

1009 
end 
23521  1010 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1011 
(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1012 
Basically, linordered_ring + no_zero_divisors = linlinordered_ring_strict. 
25230  1013 
*) 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1014 
class linlinordered_ring_strict = ring + linlinordered_semiring_strict 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

1017 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

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

1019 

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1020 
lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1021 
using mult_strict_left_mono [of b a " c"] by simp 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1022 

44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1023 
lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1024 
using mult_strict_right_mono [of b a " c"] by simp 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1025 

44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1026 
lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1027 
using mult_strict_right_mono_neg [of a zero b] by simp 
14738  1028 

25917  1029 
subclass ring_no_zero_divisors 
28823  1030 
proof 
25917  1031 
fix a b 
1032 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

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

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

1035 
proof (cases "a < 0") 

1036 
case True note A' = this 

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

1038 
case True with A' 

1039 
show ?thesis by (auto dest: mult_neg_neg) 

1040 
next 

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

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

1043 
qed 

1044 
next 

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

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

1047 
case True with A' 

1048 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

1049 
next 

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

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

1052 
qed 

1053 
qed 

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

1055 
qed 

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

1056 

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

1057 
lemma zero_less_mult_iff: 
25917  1058 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
1059 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

1060 
apply (simp_all add: not_less le_less) 

1061 
apply (erule disjE) apply assumption defer 

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

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

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

1065 
apply (drule sym) apply simp 

1066 
apply (blast dest: zero_less_mult_pos) 

25230  1067 
apply (blast dest: zero_less_mult_pos2) 
1068 
done 

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

1069 

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

1070 
lemma zero_le_mult_iff: 
25917  1071 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
29667  1072 
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

1073 

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

1074 
lemma mult_less_0_iff: 
25917  1075 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
1076 
apply (insert zero_less_mult_iff [of "a" b]) 

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

1078 
done 

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

1079 

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

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

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

1084 
done 

1085 

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

29667  1087 
by (simp add: zero_le_mult_iff linear) 
25917  1088 

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

29667  1090 
by (simp add: not_less) 
25917  1091 

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

1094 

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

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

1097 

1098 
lemma mult_less_cancel_right_disj: 

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

1100 
apply (cases "c = 0") 

1101 
apply (auto simp add: neq_iff mult_strict_right_mono 

1102 
mult_strict_right_mono_neg) 

1103 
apply (auto simp add: not_less 

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

1105 
not_le [symmetric, of a]) 

1106 
apply (erule_tac [!] notE) 

1107 
apply (auto simp add: less_imp_le mult_right_mono 

1108 
mult_right_mono_neg) 

1109 
done 

1110 

1111 
lemma mult_less_cancel_left_disj: 

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

1113 
apply (cases "c = 0") 

1114 
apply (auto simp add: neq_iff mult_strict_left_mono 

1115 
mult_strict_left_mono_neg) 

1116 
apply (auto simp add: not_less 

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

1118 
not_le [symmetric, of a]) 

1119 
apply (erule_tac [!] notE) 

1120 
apply (auto simp add: less_imp_le mult_left_mono 

1121 
mult_left_mono_neg) 

1122 
done 

1123 

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

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

1126 

1127 
lemma mult_less_cancel_right: 

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

1129 
using mult_less_cancel_right_disj [of a c b] by auto 

1130 

1131 
lemma mult_less_cancel_left: 

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

1133 
using mult_less_cancel_left_disj [of c a b] by auto 

1134 

1135 
lemma mult_le_cancel_right: 

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

29667  1137 
by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 
26193  1138 

1139 
lemma mult_le_cancel_left: 

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

29667  1141 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 
26193  1142 

30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1143 
lemma mult_le_cancel_left_pos: 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1144 
"0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b" 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1145 
by (auto simp: mult_le_cancel_left) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1146 

57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1147 
lemma mult_le_cancel_left_neg: 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1148 
"c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a" 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1149 
by (auto simp: mult_le_cancel_left) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1150 

57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1151 
lemma mult_less_cancel_left_pos: 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1152 
"0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b" 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1153 
by (auto simp: mult_less_cancel_left) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1154 

57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1155 
lemma mult_less_cancel_left_neg: 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1156 
"c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a" 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1157 
by (auto simp: mult_less_cancel_left) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

1158 

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

1160 

29667  1161 
text{*Legacy  use @{text algebra_simps} *} 
29833  1162 
lemmas ring_simps[noatp] = algebra_simps 
25230  1163 

30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1164 
lemmas mult_sign_intros = 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1165 
mult_nonneg_nonneg mult_nonneg_nonpos 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1166 
mult_nonpos_nonneg mult_nonpos_nonpos 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1167 
mult_pos_pos mult_pos_neg 
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1168 
mult_neg_pos mult_neg_neg 
25230  1169 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1170 
class ordered_comm_ring = comm_ring + ordered_comm_semiring 
25267  1171 
begin 
25230  1172 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1173 
subclass ordered_ring .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1174 
subclass ordered_cancel_comm_semiring .. 
25230  1175 

25267  1176 
end 
25230  1177 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1178 
class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict + 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1179 
(*previously linordered_semiring*) 
25230  1180 
assumes zero_less_one [simp]: "0 < 1" 
1181 
begin 

1182 

1183 
lemma pos_add_strict: 

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

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

1186 

26193  1187 
lemma zero_le_one [simp]: "0 \<le> 1" 
29667  1188 
by (rule zero_less_one [THEN less_imp_le]) 
26193  1189 

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

29667  1191 
by (simp add: not_le) 
26193  1192 

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

29667  1194 
by (simp add: not_less) 
26193  1195 

1196 
lemma less_1_mult: 

1197 
assumes "1 < m" and "1 < n" 

1198 
shows "1 < m * n" 

1199 
using assms mult_strict_mono [of 1 m 1 n] 

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

1201 

25230  1202 
end 
1203 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1204 
class linordered_idom = comm_ring_1 + 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1205 
linordered_comm_semiring_strict + ordered_ab_group_add + 
25230  1206 
abs_if + sgn_if 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1207 
(*previously linordered_ring*) 
25917  1208 
begin 
1209 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1210 
subclass linlinordered_ring_strict .. 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1211 
subclass ordered_comm_ring .. 
27516  1212 
subclass idom .. 
25917  1213 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1214 
subclass linordered_semidom 
28823  1215 
proof 
26193  1216 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
1217 
thus "0 < 1" by (simp add: le_less) 

25917  1218 
qed 
1219 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34146
diff
changeset

1220 
lemma linorder_neqE_linordered_idom: 
26193  1221 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 
1222 
using assms by (rule neqE) 

1223 

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

1226 
lemma mult_le_cancel_right1: 

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

29667  1228 
by (insert mult_le_cancel_right [of 1 c b], simp) 
26274  1229 

1230 
lemma mult_le_cancel_right2: 

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

29667  1232 
by (insert mult_le_cancel_right [of a c 1], simp) 
26274  1233 

1234 
lemma mult_le_cancel_left1: 

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

29667  1236 
by (insert mult_le_cancel_left [of c 1 b], simp) 
26274  1237 

1238 
lemma mult_le_cancel_left2: 

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

29667  1240 
by (insert mult_le_cancel_left [of c a 1], simp) 
26274  1241 

1242 
lemma mult_less_cancel_right1: 

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

29667  1244 
by (insert mult_less_cancel_right [of 1 c b], simp) 
26274  1245 

1246 
lemma mult_less_cancel_right2: 

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

29667  1248 
by (insert mult_less_cancel_right [of a c 1], simp) 
26274  1249 

1250 
lemma mult_less_cancel_left1: 

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

29667  1252 
by (insert mult_less_cancel_left [of c 1 b], simp) 
26274  1253 

1254 
lemma mult_less_cancel_left2: 

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

29667  1256 
by (insert mult_less_cancel_left [of c a 1], simp) 
26274  1257 

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

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

1259 
"sgn (sgn a) = sgn a" 
29700  1260 
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

1261 

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

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

1263 
"sgn a = 0 \<longleftrightarrow> a = 0" 
29700  1264 
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

1265 

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

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

1267 
"sgn a = 1 \<longleftrightarrow> a > 0" 
29700  1268 
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

1269 

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

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

1271 
"sgn a =  1 \<longleftrightarrow> a < 0" 
29700  1272 
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

1273 

29940  1274 
lemma sgn_pos [simp]: 
83b373f61d41
mo 