author  haftmann 
Wed, 10 Feb 2010 08:49:26 +0100  
changeset 35083  3246e66b0874 
parent 35050  9f841f20dca6 
child 35092  cfe605c54e50 
permissions  rwrr 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

1 
(* Title: HOL/Rings.thy 
32960
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 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

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

11 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

12 
theory Rings 
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

13 
imports Groups 
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 

35083  413 
class inverse = 
414 
fixes inverse :: "'a \<Rightarrow> 'a" 

415 
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70) 

416 

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

35083  420 
assumes divide_inverse: "a / b = a * inverse b" 
25186  421 
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

422 

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

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

426 
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

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

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

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

431 
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

432 
by (simp only: mult_assoc) 
29667  433 
also have "\<dots> = 1" using a b by simp 
434 
finally show False by simp 

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

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

436 
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

437 

26274  438 
lemma nonzero_imp_inverse_nonzero: 
439 
"a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0" 

440 
proof 

441 
assume ianz: "inverse a = 0" 

442 
assume "a \<noteq> 0" 

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

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

445 
finally have "1 = 0" . 

446 
thus False by (simp add: eq_commute) 

447 
qed 

448 

449 
lemma inverse_zero_imp_zero: 

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

451 
apply (rule classical) 

452 
apply (drule nonzero_imp_inverse_nonzero) 

453 
apply auto 

454 
done 

455 

456 
lemma inverse_unique: 

457 
assumes ab: "a * b = 1" 

458 
shows "inverse a = b" 

459 
proof  

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

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

26274  463 
qed 
464 

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

29667  467 
by (rule inverse_unique) simp 
29406  468 

469 
lemma nonzero_inverse_inverse_eq: 

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

29667  471 
by (rule inverse_unique) simp 
29406  472 

473 
lemma nonzero_inverse_eq_imp_eq: 

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

475 
shows "a = b" 

476 
proof  

477 
from `inverse a = inverse b` 

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

481 
qed 

482 

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

29667  484 
by (rule inverse_unique) simp 
29406  485 

26274  486 
lemma nonzero_inverse_mult_distrib: 
29406  487 
assumes "a \<noteq> 0" and "b \<noteq> 0" 
26274  488 
shows "inverse (a * b) = inverse b * inverse a" 
489 
proof  

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

492 
thus ?thesis by (rule inverse_unique) 

26274  493 
qed 
494 

495 
lemma division_ring_inverse_add: 

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

29667  497 
by (simp add: algebra_simps) 
26274  498 

499 
lemma division_ring_inverse_diff: 

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

29667  501 
by (simp add: algebra_simps) 
26274  502 

25186  503 
end 
25152  504 

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

508 

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

509 
class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
25230  510 
begin 
511 

512 
lemma mult_mono: 

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

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

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

516 
apply (erule mult_left_mono, assumption) 

517 
done 

518 

519 
lemma mult_mono': 

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

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

522 
apply (rule mult_mono) 

523 
apply (fast intro: order_trans)+ 

524 
done 

525 

526 
end 

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

527 

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

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

531 

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

533 
subclass ordered_semiring .. 
23521  534 

25230  535 
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

536 
using mult_left_mono [of zero b a] by simp 
25230  537 

538 
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

539 
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

540 

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

541 
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

542 
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

543 

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

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

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

551 
end 

552 

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

553 
class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono 
25267  554 
begin 
25230  555 

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

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

557 

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

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

559 

25230  560 
lemma mult_left_less_imp_less: 
561 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  562 
by (force simp add: mult_left_mono not_le [symmetric]) 
25230  563 

564 
lemma mult_right_less_imp_less: 

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

29667  566 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  567 

25186  568 
end 
25152  569 

35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

570 
class linordered_semiring_1 = linordered_semiring + semiring_1 
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

571 

07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

572 
class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + 
25062  573 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
574 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

576 

27516  577 
subclass semiring_0_cancel .. 
14940  578 

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

579 
subclass linordered_semiring 
28823  580 
proof 
23550  581 
fix a b c :: 'a 
582 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  584 
unfolding le_less 
585 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  586 
from A show "a * c \<le> b * c" 
25152  587 
unfolding le_less 
25186  588 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  589 
qed 
590 

25230  591 
lemma mult_left_le_imp_le: 
592 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

29667  593 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 
25230  594 

595 
lemma mult_right_le_imp_le: 

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

29667  597 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 
25230  598 

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

599 
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

600 
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

601 

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

602 
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

603 
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

604 

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

605 
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

606 
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

607 

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

608 
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

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

612 
lemma zero_less_mult_pos: 

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

614 
apply (cases "b\<le>0") 
25230  615 
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

616 
apply (drule_tac mult_pos_neg [of a b]) 
25230  617 
apply (auto dest: less_not_sym) 
618 
done 

619 

620 
lemma zero_less_mult_pos2: 

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

622 
apply (cases "b\<le>0") 
25230  623 
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

624 
apply (drule_tac mult_pos_neg2 [of a b]) 
25230  625 
apply (auto dest: less_not_sym) 
626 
done 

627 

26193  628 
text{*Strict monotonicity in both arguments*} 
629 
lemma mult_strict_mono: 

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

631 
shows "a * c < b * d" 

632 
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

633 
apply (simp add: mult_pos_pos) 
26193  634 
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

635 
apply (force simp add: le_less) 
26193  636 
apply (erule mult_strict_left_mono, assumption) 
637 
done 

638 

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

640 
lemma mult_strict_mono': 

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

642 
shows "a * c < b * d" 

29667  643 
by (rule mult_strict_mono) (insert assms, auto) 
26193  644 

645 
lemma mult_less_le_imp_less: 

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

647 
shows "a * c < b * d" 

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

649 
apply (erule less_le_trans) 

650 
apply (erule mult_left_mono) 

651 
apply simp 

652 
apply (erule mult_strict_right_mono) 

653 
apply assumption 

654 
done 

655 

656 
lemma mult_le_less_imp_less: 

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

658 
shows "a * c < b * d" 

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

660 
apply (erule le_less_trans) 

661 
apply (erule mult_strict_left_mono) 

662 
apply simp 

663 
apply (erule mult_right_mono) 

664 
apply simp 

665 
done 

666 

667 
lemma mult_less_imp_less_left: 

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

669 
shows "a < b" 

670 
proof (rule ccontr) 

671 
assume "\<not> a < b" 

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

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

29667  674 
with this and less show False by (simp add: not_less [symmetric]) 
26193  675 
qed 
676 

677 
lemma mult_less_imp_less_right: 

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

679 
shows "a < b" 

680 
proof (rule ccontr) 

681 
assume "\<not> a < b" 

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

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

29667  684 
with this and less show False by (simp add: not_less [symmetric]) 
26193  685 
qed 
686 

25230  687 
end 
688 

35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

689 
class linlinordered_semiring_1_strict = linordered_semiring_strict + semiring_1 
33319  690 

22390  691 
class mult_mono1 = times + zero + ord + 
25230  692 
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
14270  693 

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

694 
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

695 
+ ordered_ab_semigroup_add + mult_mono1 
25186  696 
begin 
25152  697 

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

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

700 
fix a b c :: 'a 
23550  701 
assume "a \<le> b" "0 \<le> c" 
25230  702 
thus "c * a \<le> c * b" by (rule mult_mono1) 
23550  703 
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

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

705 

25267  706 
end 
707 

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

708 
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

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

711 

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

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

713 
subclass ordered_cancel_semiring .. 
25267  714 

715 
end 

716 

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

717 
class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add + 
26193  718 
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  719 
begin 
720 

35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

721 
subclass linordered_semiring_strict 
28823  722 
proof 
23550  723 
fix a b c :: 'a 
724 
assume "a < b" "0 < c" 

26193  725 
thus "c * a < c * b" by (rule mult_strict_left_mono_comm) 
23550  726 
thus "a * c < b * c" by (simp only: mult_commute) 
727 
qed 

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

728 

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

729 
subclass ordered_cancel_comm_semiring 
28823  730 
proof 
23550  731 
fix a b c :: 'a 
732 
assume "a \<le> b" "0 \<le> c" 

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

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

737 

25267  738 
end 
25230  739 

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

740 
class ordered_ring = ring + ordered_cancel_semiring 
25267  741 
begin 
25230  742 

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

743 
subclass ordered_ab_group_add .. 
14270  744 

29667  745 
text{*Legacy  use @{text algebra_simps} *} 
29833  746 
lemmas ring_simps[noatp] = algebra_simps 
25230  747 

748 
lemma less_add_iff1: 

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

29667  750 
by (simp add: algebra_simps) 
25230  751 

752 
lemma less_add_iff2: 

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

29667  754 
by (simp add: algebra_simps) 
25230  755 

756 
lemma le_add_iff1: 

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

29667  758 
by (simp add: algebra_simps) 
25230  759 

760 
lemma le_add_iff2: 

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

29667  762 
by (simp add: algebra_simps) 
25230  763 

764 
lemma mult_left_mono_neg: 

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

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

767 
apply (simp_all add: minus_mult_left [symmetric]) 

768 
done 

769 

770 
lemma mult_right_mono_neg: 

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

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

773 
apply (simp_all add: minus_mult_right [symmetric]) 

774 
done 

775 

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

776 
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

777 
using mult_right_mono_neg [of a zero b] by simp 
25230  778 

779 
lemma split_mult_pos_le: 

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

29667  781 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 
25186  782 

783 
end 

14270  784 

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

787 

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

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

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

793 

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

794 
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

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

796 

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

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

798 

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

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

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

802 
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

803 
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

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

805 
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

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

807 
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

808 

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

809 
end 
23521  810 

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

811 
(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors. 
35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

812 
Basically, linordered_ring + no_zero_divisors = linordered_ring_strict. 
25230  813 
*) 
35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

814 
class linordered_ring_strict = ring + linordered_semiring_strict 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

817 

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

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

819 

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

820 
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

821 
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

822 

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

823 
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

824 
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

825 

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

826 
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

827 
using mult_strict_right_mono_neg [of a zero b] by simp 
14738  828 

25917  829 
subclass ring_no_zero_divisors 
28823  830 
proof 
25917  831 
fix a b 
832 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

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

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

835 
proof (cases "a < 0") 

836 
case True note A' = this 

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

838 
case True with A' 

839 
show ?thesis by (auto dest: mult_neg_neg) 

840 
next 

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

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

843 
qed 

844 
next 

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

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

847 
case True with A' 

848 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

849 
next 

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

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

852 
qed 

853 
qed 

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

855 
qed 

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

856 

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

857 
lemma zero_less_mult_iff: 
25917  858 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
859 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

860 
apply (simp_all add: not_less le_less) 

861 
apply (erule disjE) apply assumption defer 

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

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

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

865 
apply (drule sym) apply simp 

866 
apply (blast dest: zero_less_mult_pos) 

25230  867 
apply (blast dest: zero_less_mult_pos2) 
868 
done 

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

869 

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

870 
lemma zero_le_mult_iff: 
25917  871 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
29667  872 
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

873 

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

874 
lemma mult_less_0_iff: 
25917  875 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
876 
apply (insert zero_less_mult_iff [of "a" b]) 

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

878 
done 

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

879 

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

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

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

884 
done 

885 

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

29667  887 
by (simp add: zero_le_mult_iff linear) 
25917  888 

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

29667  890 
by (simp add: not_less) 
25917  891 

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

894 

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

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

897 

898 
lemma mult_less_cancel_right_disj: 

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

900 
apply (cases "c = 0") 

901 
apply (auto simp add: neq_iff mult_strict_right_mono 

902 
mult_strict_right_mono_neg) 

903 
apply (auto simp add: not_less 

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

905 
not_le [symmetric, of a]) 

906 
apply (erule_tac [!] notE) 

907 
apply (auto simp add: less_imp_le mult_right_mono 

908 
mult_right_mono_neg) 

909 
done 

910 

911 
lemma mult_less_cancel_left_disj: 

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

913 
apply (cases "c = 0") 

914 
apply (auto simp add: neq_iff mult_strict_left_mono 

915 
mult_strict_left_mono_neg) 

916 
apply (auto simp add: not_less 

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

918 
not_le [symmetric, of a]) 

919 
apply (erule_tac [!] notE) 

920 
apply (auto simp add: less_imp_le mult_left_mono 

921 
mult_left_mono_neg) 

922 
done 

923 

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

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

926 

927 
lemma mult_less_cancel_right: 

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

929 
using mult_less_cancel_right_disj [of a c b] by auto 

930 

931 
lemma mult_less_cancel_left: 

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

933 
using mult_less_cancel_left_disj [of c a b] by auto 

934 

935 
lemma mult_le_cancel_right: 

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

29667  937 
by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 
26193  938 

939 
lemma mult_le_cancel_left: 

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

29667  941 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 
26193  942 

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

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

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

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

946 

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

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

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

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

950 

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

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

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

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

954 

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

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

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

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

958 

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

960 

29667  961 
text{*Legacy  use @{text algebra_simps} *} 
29833  962 
lemmas ring_simps[noatp] = algebra_simps 
25230  963 

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

964 
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

965 
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

966 
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

967 
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

968 
mult_neg_pos mult_neg_neg 
25230  969 

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

970 
class ordered_comm_ring = comm_ring + ordered_comm_semiring 
25267  971 
begin 
25230  972 

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

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

974 
subclass ordered_cancel_comm_semiring .. 
25230  975 

25267  976 
end 
25230  977 

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

978 
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

979 
(*previously linordered_semiring*) 
25230  980 
assumes zero_less_one [simp]: "0 < 1" 
981 
begin 

982 

983 
lemma pos_add_strict: 

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

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

986 

26193  987 
lemma zero_le_one [simp]: "0 \<le> 1" 
29667  988 
by (rule zero_less_one [THEN less_imp_le]) 
26193  989 

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

29667  991 
by (simp add: not_le) 
26193  992 

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

29667  994 
by (simp add: not_less) 
26193  995 

996 
lemma less_1_mult: 

997 
assumes "1 < m" and "1 < n" 

998 
shows "1 < m * n" 

999 
using assms mult_strict_mono [of 1 m 1 n] 

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

1001 

25230  1002 
end 
1003 

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

1004 
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

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

1007 
(*previously linordered_ring*) 
25917  1008 
begin 
1009 

35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset

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

1011 
subclass ordered_comm_ring .. 
27516  1012 
subclass idom .. 
25917  1013 

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

1014 
subclass linordered_semidom 
28823  1015 
proof 
26193  1016 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
1017 
thus "0 < 1" by (simp add: le_less) 

25917  1018 
qed 
1019 

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

1020 
lemma linorder_neqE_linordered_idom: 
26193  1021 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 
1022 
using assms by (rule neqE) 

1023 

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

1026 
lemma mult_le_cancel_right1: 

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

29667  1028 
by (insert mult_le_cancel_right [of 1 c b], simp) 
26274  1029 

1030 
lemma mult_le_cancel_right2: 

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

29667  1032 
by (insert mult_le_cancel_right [of a c 1], simp) 
26274  1033 

1034 
lemma mult_le_cancel_left1: 

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

29667  1036 
by (insert mult_le_cancel_left [of c 1 b], simp) 
26274  1037 

1038 
lemma mult_le_cancel_left2: 

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

29667  1040 
by (insert mult_le_cancel_left [of c a 1], simp) 
26274  1041 

1042 
lemma mult_less_cancel_right1: 

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

29667  1044 
by (insert mult_less_cancel_right [of 1 c b], simp) 
26274  1045 

1046 
lemma mult_less_cancel_right2: 

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

29667  1048 
by (insert mult_less_cancel_right [of a c 1], simp) 
26274  1049 

1050 
lemma mult_less_cancel_left1: 

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

29667  1052 
by (insert mult_less_cancel_left [of c 1 b], simp) 
26274  1053 

1054 
lemma mult_less_cancel_left2: 

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

29667  1056 
by (insert mult_less_cancel_left [of c a 1], simp) 
26274  1057 

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

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

1059 
"sgn (sgn a) = sgn a" 
29700  1060 
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

1061 

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

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

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

1065 

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

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

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

1069 

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

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

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

1073 

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

1076 
unfolding sgn_1_pos . 

1077 

1078 
lemma sgn_neg [simp]: 

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

1080 
unfolding sgn_1_neg . 

1081 

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

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

1083 
"sgn (a * b) = sgn a * sgn b" 
29667  1084 
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

1085 

29653  1086 
lemma abs_sgn: "abs k = k * sgn k" 
29700  1087 
unfolding sgn_if abs_if by auto 
1088 

29940  1089 
lemma sgn_greater [simp]: 
1090 
"0 < sgn a \<longleftrightarrow> 0 < a" 

1091 
unfolding sgn_if by auto 

1092 

1093 
lemma sgn_less [simp]: 

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

1095 
unfolding sgn_if by auto 

1096 

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

1099 

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

1101 
by (simp add: abs_if) 

29653  1102 

33676
802f5e233e48
moved lemma from Algebra/IntRing to Ring_and_Field
nipkow
parents:
33364
diff
changeset

1103 
lemma dvd_if_abs_eq: 
802f5e233e48
moved lemma from Algebra/IntRing to Ring_and_Field
nipkow
parents:
33364
diff
changeset

1104 
"abs l = abs (k) \<Longrightarrow> l dvd k" 
802f5e233e48
moved lemma from Algebra/IntRing to Ring_and_Field
nipkow
parents:
33364
diff
changeset

1105 
by(subst abs_dvd_iff[symmetric]) simp 
802f5e233e48
moved lemma from Algebra/IntRing to Ring_and_Field
nipkow
parents:
33364
diff
changeset

1106 

25917  1107 
end 
25230  1108 

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

1110 

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

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

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

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

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

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

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

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

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

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

1121 

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

1123 

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

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

1125 

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

1126 
lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1127 
==> x * y <= x" 
33319  1128 
by (auto simp add: mult_compare_simps) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1129 

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

1130 
lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1131 
==> y * x <= x" 
33319  1132 
by (auto simp add: mult_compare_simps) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1133 

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

1134 
context linordered_semidom 
25193  1135 
begin 
1136 

1137 
lemma less_add_one: "a < a + 1" 

14293  1138 
proof  
25193  1139 
have "a + 0 < a + 1" 
23482  1140 
by (blast intro: zero_less_one add_strict_left_mono) 
14293  1141 
thus ?thesis by simp 
1142 
qed 

1143 

25193  1144 
lemma zero_less_two: "0 < 1 + 1" 
29667  1145 
by (blast intro: less_trans zero_less_one less_add_one) 
25193  1146 

1147 
end 

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

1148 

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

1149 

14293  1150 
subsection {* Absolute Value *} 
1151 

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

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

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

1154 

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

1155 
lemma mult_sgn_abs: "sgn x * abs x = x" 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1156 
unfolding abs_if sgn_if by auto 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1157 

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

1158 
end 
24491  1159 

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

1160 
lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)" 
29667  1161 
by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1162 

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

1163 
class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs + 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

1165 
"(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1166 

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

1167 
context linordered_idom 
30961  1168 
begin 
1169 

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

1170 
subclass ordered_ring_abs proof 
30961  1171 
qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff) 
1172 

1173 
lemma abs_mult: 

1174 
"abs (a * b) = abs a * abs b" 

1175 
by (rule abs_eq_mult) auto 

1176 

1177 
lemma abs_mult_self: 

1178 
"abs a * abs a = a * a" 

1179 
by (simp add: abs_if) 

1180 

1181 
end 

14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1182 

f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

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

1184 
"[ abs a < c; abs b < d ] ==> abs a * abs b < c*(d::'a::linordered_idom)" 
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1185 
proof  
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1186 
assume ac: "abs a < c" 
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1187 
hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero) 
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1188 
assume "abs b < d" 
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1189 
thus ?thesis by (simp add: ac cpos mult_strict_mono) 
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1190 
qed 
14293  1191 

29833  1192 
lemmas eq_minus_self_iff[noatp] = equal_neg_zero 
14738  1193 

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

1194 
lemma less_minus_self_iff: "(a < a) = (a < (0::'a::linordered_idom))" 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1195 
unfolding order_less_le less_eq_neg_nonpos equal_neg_zero .. 
14738  1196 

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

1197 
lemma abs_less_iff: "(abs a < b) = (a < b & a < (b::'a::linordered_idom))" 
14738  1198 
apply (simp add: order_less_le abs_le_iff) 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1199 
apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos) 
14738  1200 
done 
1201 

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

1202 
lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1203 
(abs y) * x = abs (y * x)" 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1204 
apply (subst abs_mult) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

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

1207 

33364  1208 
code_modulename SML 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

1209 
Rings Arith 
33364  1210 

1211 
code_modulename OCaml 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

1212 
Rings Arith 
33364  1213 

1214 
code_modulename Haskell 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

1215 
Rings Arith 
33364  1216 

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

1217 
end 