author  haftmann 
Fri, 01 Nov 2013 18:51:14 +0100  
changeset 54230  b1d955791529 
parent 54225  8a49a5a30284 
child 54250  7d2544dd3988 
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 

22390  16 
class semiring = ab_semigroup_add + semigroup_mult + 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

17 
assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c" 
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

18 
assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c" 
25152  19 
begin 
20 

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

22 
lemma combine_common_factor: 

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

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

24 
by (simp add: distrib_right add_ac) 
25152  25 

26 
end 

14504  27 

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

31 

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

33 

29904  34 
class semiring_0_cancel = semiring + cancel_comm_monoid_add 
25186  35 
begin 
14504  36 

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

39 
fix a :: 'a 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

40 
have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric]) 
29667  41 
thus "0 * a = 0" by (simp only: add_left_cancel) 
25152  42 
next 
43 
fix a :: 'a 

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

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

46 
qed 
14940  47 

25186  48 
end 
25152  49 

22390  50 
class comm_semiring = ab_semigroup_add + ab_semigroup_mult + 
25062  51 
assumes distrib: "(a + b) * c = a * c + b * c" 
25152  52 
begin 
14504  53 

25152  54 
subclass semiring 
28823  55 
proof 
14738  56 
fix a b c :: 'a 
57 
show "(a + b) * c = a * c + b * c" by (simp add: distrib) 

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

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

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

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

14504  62 
qed 
63 

25152  64 
end 
14504  65 

25152  66 
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero 
67 
begin 

68 

27516  69 
subclass semiring_0 .. 
25152  70 

71 
end 

14504  72 

29904  73 
class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add 
25186  74 
begin 
14940  75 

27516  76 
subclass semiring_0_cancel .. 
14940  77 

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

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

79 

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

81 

22390  82 
class zero_neq_one = zero + one + 
25062  83 
assumes zero_neq_one [simp]: "0 \<noteq> 1" 
26193  84 
begin 
85 

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

29667  87 
by (rule not_sym) (rule zero_neq_one) 
26193  88 

54225  89 
definition of_bool :: "bool \<Rightarrow> 'a" 
90 
where 

91 
"of_bool p = (if p then 1 else 0)" 

92 

93 
lemma of_bool_eq [simp, code]: 

94 
"of_bool False = 0" 

95 
"of_bool True = 1" 

96 
by (simp_all add: of_bool_def) 

97 

98 
lemma of_bool_eq_iff: 

99 
"of_bool p = of_bool q \<longleftrightarrow> p = q" 

100 
by (simp add: of_bool_def) 

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 

50420  111 
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where 
37767  112 
"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 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

143 
lemma dvd_0_left_iff [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'" .. 

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

193 
ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left) 
27651
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 

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

203 
lemma divisors_zero: 

204 
assumes "a * b = 0" 

205 
shows "a = 0 \<or> b = 0" 

206 
proof (rule classical) 

207 
assume "\<not> (a = 0 \<or> b = 0)" 

208 
then have "a \<noteq> 0" and "b \<noteq> 0" by auto 

209 
with no_zero_divisors have "a * b \<noteq> 0" by blast 

210 
with assms show ?thesis by simp 

211 
qed 

212 

213 
end 

14504  214 

29904  215 
class semiring_1_cancel = semiring + cancel_comm_monoid_add 
216 
+ zero_neq_one + monoid_mult 

25267  217 
begin 
14940  218 

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

220 

27516  221 
subclass semiring_1 .. 
25267  222 

223 
end 

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

224 

29904  225 
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add 
226 
+ zero_neq_one + comm_monoid_mult 

25267  227 
begin 
14738  228 

27516  229 
subclass semiring_1_cancel .. 
230 
subclass comm_semiring_0_cancel .. 

231 
subclass comm_semiring_1 .. 

25267  232 

233 
end 

25152  234 

22390  235 
class ring = semiring + ab_group_add 
25267  236 
begin 
25152  237 

27516  238 
subclass semiring_0_cancel .. 
25152  239 

240 
text {* Distribution rules *} 

241 

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

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

243 
by (rule minus_unique) (simp add: distrib_right [symmetric]) 
25152  244 

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

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

246 
by (rule minus_unique) (simp add: distrib_left [symmetric]) 
25152  247 

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

248 
text{*Extract signs from products*} 
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

249 
lemmas mult_minus_left [simp] = minus_mult_left [symmetric] 
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

250 
lemmas mult_minus_right [simp] = minus_mult_right [symmetric] 
29407
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

251 

25152  252 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  253 
by simp 
25152  254 

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

29667  256 
by simp 
257 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

258 
lemma right_diff_distrib [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

259 
"a * (b  c) = a * b  a * c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

260 
using distrib_left [of a b "c "] by simp 
29667  261 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

262 
lemma left_diff_distrib [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

263 
"(a  b) * c = a * c  b * c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

264 
using distrib_right [of a " b" c] by simp 
25152  265 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

266 
lemmas ring_distribs = 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

267 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  268 

25230  269 
lemma eq_add_iff1: 
270 
"a * e + c = b * e + d \<longleftrightarrow> (a  b) * e + c = d" 

29667  271 
by (simp add: algebra_simps) 
25230  272 

273 
lemma eq_add_iff2: 

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

29667  275 
by (simp add: algebra_simps) 
25230  276 

25152  277 
end 
278 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

279 
lemmas ring_distribs = 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

280 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  281 

22390  282 
class comm_ring = comm_semiring + ab_group_add 
25267  283 
begin 
14738  284 

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

286 
subclass comm_semiring_0_cancel .. 
25267  287 

44350
63cddfbc5a09
replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents:
44346
diff
changeset

288 
lemma square_diff_square_factored: 
63cddfbc5a09
replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents:
44346
diff
changeset

289 
"x * x  y * y = (x + y) * (x  y)" 
63cddfbc5a09
replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents:
44346
diff
changeset

290 
by (simp add: algebra_simps) 
63cddfbc5a09
replace lemma realpow_two_diff with new lemma square_diff_square_factored
huffman
parents:
44346
diff
changeset

291 

25267  292 
end 
14738  293 

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

296 

27516  297 
subclass semiring_1_cancel .. 
25267  298 

44346
00dd3c4dabe0
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents:
44064
diff
changeset

299 
lemma square_diff_one_factored: 
00dd3c4dabe0
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents:
44064
diff
changeset

300 
"x * x  1 = (x + 1) * (x  1)" 
00dd3c4dabe0
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents:
44064
diff
changeset

301 
by (simp add: algebra_simps) 
00dd3c4dabe0
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
huffman
parents:
44064
diff
changeset

302 

25267  303 
end 
25152  304 

22390  305 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
306 
(*previously ring*) 

25267  307 
begin 
14738  308 

27516  309 
subclass ring_1 .. 
310 
subclass comm_semiring_1_cancel .. 

25267  311 

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

312 
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

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

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

315 
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

316 
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

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

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

319 
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

320 
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

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

322 

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

323 
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

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

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

326 
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

327 
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

328 
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

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

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

331 
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

332 
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

333 
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

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

335 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

336 
lemma dvd_diff [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

337 
"x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y  z)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

338 
using dvd_add [of x y " z"] by simp 
29409  339 

25267  340 
end 
25152  341 

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

342 
class ring_no_zero_divisors = ring + no_zero_divisors 
25230  343 
begin 
344 

345 
lemma mult_eq_0_iff [simp]: 

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

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

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

349 
then show ?thesis using no_zero_divisors by simp 

350 
next 

351 
case True then show ?thesis by auto 

352 
qed 

353 

26193  354 
text{*Cancellation of equalities with a common factor*} 
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

355 
lemma mult_cancel_right [simp]: 
26193  356 
"a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" 
357 
proof  

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

35216  359 
by (simp add: algebra_simps) 
360 
thus ?thesis by (simp add: disj_commute) 

26193  361 
qed 
362 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

363 
lemma mult_cancel_left [simp]: 
26193  364 
"c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" 
365 
proof  

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

35216  367 
by (simp add: algebra_simps) 
368 
thus ?thesis by simp 

26193  369 
qed 
370 

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

372 

23544  373 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  374 
begin 
375 

36970  376 
lemma square_eq_1_iff: 
36821
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

377 
"x * x = 1 \<longleftrightarrow> x = 1 \<or> x =  1" 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

378 
proof  
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

379 
have "(x  1) * (x + 1) = x * x  1" 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

380 
by (simp add: algebra_simps) 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

381 
hence "x * x = 1 \<longleftrightarrow> (x  1) * (x + 1) = 0" 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

382 
by simp 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

383 
thus ?thesis 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

384 
by (simp add: eq_neg_iff_add_eq_0) 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

385 
qed 
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

386 

26274  387 
lemma mult_cancel_right1 [simp]: 
388 
"c = b * c \<longleftrightarrow> c = 0 \<or> b = 1" 

29667  389 
by (insert mult_cancel_right [of 1 c b], force) 
26274  390 

391 
lemma mult_cancel_right2 [simp]: 

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

29667  393 
by (insert mult_cancel_right [of a c 1], simp) 
26274  394 

395 
lemma mult_cancel_left1 [simp]: 

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

29667  397 
by (insert mult_cancel_left [of c 1 b], force) 
26274  398 

399 
lemma mult_cancel_left2 [simp]: 

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

29667  401 
by (insert mult_cancel_left [of c a 1], simp) 
26274  402 

403 
end 

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

404 

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

407 

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

409 

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

410 
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

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

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

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

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

415 
then show "a = b \<or> a =  b" 
35216  416 
by (simp add: eq_neg_iff_add_eq_0) 
29915
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

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

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

419 
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

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

421 

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

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

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

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

425 
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

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

427 
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

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

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

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

431 

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

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

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

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

435 
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

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

437 
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

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

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

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

441 

25186  442 
end 
25152  443 

35302  444 
text {* 
445 
The theory of partially ordered rings is taken from the books: 

446 
\begin{itemize} 

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

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

449 
\end{itemize} 

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

451 
\begin{itemize} 

452 
\item \url{http://www.mathworld.com} by Eric Weisstein et. al. 

453 
\item \emph{Algebra I} by van der Waerden, Springer. 

454 
\end{itemize} 

455 
*} 

456 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

457 
class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add + 
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

458 
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

459 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 
25230  460 
begin 
461 

462 
lemma mult_mono: 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

463 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 
25230  464 
apply (erule mult_right_mono [THEN order_trans], assumption) 
465 
apply (erule mult_left_mono, assumption) 

466 
done 

467 

468 
lemma mult_mono': 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

469 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 
25230  470 
apply (rule mult_mono) 
471 
apply (fast intro: order_trans)+ 

472 
done 

473 

474 
end 

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

475 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

476 
class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add 
25267  477 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

478 

27516  479 
subclass semiring_0_cancel .. 
23521  480 

25230  481 
lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

482 
using mult_left_mono [of 0 b a] by simp 
25230  483 

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

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

486 

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

487 
lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

489 

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

490 
text {* Legacy  use @{text mult_nonpos_nonneg} *} 
25230  491 
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

492 
by (drule mult_right_mono [of b 0], auto) 
25230  493 

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

497 
end 

498 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

499 
class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add 
25267  500 
begin 
25230  501 

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

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

503 

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

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

505 

25230  506 
lemma mult_left_less_imp_less: 
507 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  508 
by (force simp add: mult_left_mono not_le [symmetric]) 
25230  509 

510 
lemma mult_right_less_imp_less: 

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

29667  512 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  513 

25186  514 
end 
25152  515 

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

516 
class linordered_semiring_1 = linordered_semiring + semiring_1 
36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

517 
begin 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

518 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

519 
lemma convex_bound_le: 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

520 
assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

521 
shows "u * x + v * y \<le> a" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

522 
proof 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

523 
from assms have "u * x + v * y \<le> u * a + v * a" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

524 
by (simp add: add_mono mult_left_mono) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

525 
thus ?thesis using assms unfolding distrib_right[symmetric] by simp 
36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

526 
qed 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

527 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

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

529 

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

530 
class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + 
25062  531 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
532 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

534 

27516  535 
subclass semiring_0_cancel .. 
14940  536 

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

537 
subclass linordered_semiring 
28823  538 
proof 
23550  539 
fix a b c :: 'a 
540 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  542 
unfolding le_less 
543 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  544 
from A show "a * c \<le> b * c" 
25152  545 
unfolding le_less 
25186  546 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  547 
qed 
548 

25230  549 
lemma mult_left_le_imp_le: 
550 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

29667  551 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 
25230  552 

553 
lemma mult_right_le_imp_le: 

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

29667  555 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 
25230  556 

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

557 
lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

559 

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

560 
lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

562 

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

563 
lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

565 

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

566 
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

567 
lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

568 
by (drule mult_strict_right_mono [of b 0], auto) 
25230  569 

570 
lemma zero_less_mult_pos: 

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

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

574 
apply (drule_tac mult_pos_neg [of a b]) 
25230  575 
apply (auto dest: less_not_sym) 
576 
done 

577 

578 
lemma zero_less_mult_pos2: 

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

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

582 
apply (drule_tac mult_pos_neg2 [of a b]) 
25230  583 
apply (auto dest: less_not_sym) 
584 
done 

585 

26193  586 
text{*Strict monotonicity in both arguments*} 
587 
lemma mult_strict_mono: 

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

589 
shows "a * c < b * d" 

590 
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

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

593 
apply (force simp add: le_less) 
26193  594 
apply (erule mult_strict_left_mono, assumption) 
595 
done 

596 

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

598 
lemma mult_strict_mono': 

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

600 
shows "a * c < b * d" 

29667  601 
by (rule mult_strict_mono) (insert assms, auto) 
26193  602 

603 
lemma mult_less_le_imp_less: 

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

605 
shows "a * c < b * d" 

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

607 
apply (erule less_le_trans) 

608 
apply (erule mult_left_mono) 

609 
apply simp 

610 
apply (erule mult_strict_right_mono) 

611 
apply assumption 

612 
done 

613 

614 
lemma mult_le_less_imp_less: 

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

616 
shows "a * c < b * d" 

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

618 
apply (erule le_less_trans) 

619 
apply (erule mult_strict_left_mono) 

620 
apply simp 

621 
apply (erule mult_right_mono) 

622 
apply simp 

623 
done 

624 

625 
lemma mult_less_imp_less_left: 

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

627 
shows "a < b" 

628 
proof (rule ccontr) 

629 
assume "\<not> a < b" 

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

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

29667  632 
with this and less show False by (simp add: not_less [symmetric]) 
26193  633 
qed 
634 

635 
lemma mult_less_imp_less_right: 

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

637 
shows "a < b" 

638 
proof (rule ccontr) 

639 
assume "\<not> a < b" 

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

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

29667  642 
with this and less show False by (simp add: not_less [symmetric]) 
26193  643 
qed 
644 

25230  645 
end 
646 

35097
4554bb2abfa3
dropped last occurence of the linlinordered accident
haftmann
parents:
35092
diff
changeset

647 
class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 
36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

648 
begin 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

649 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

650 
subclass linordered_semiring_1 .. 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

651 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

652 
lemma convex_bound_lt: 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

653 
assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

654 
shows "u * x + v * y < a" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

655 
proof  
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

656 
from assms have "u * x + v * y < u * a + v * a" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

657 
by (cases "u = 0") 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

658 
(auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44921
diff
changeset

659 
thus ?thesis using assms unfolding distrib_right[symmetric] by simp 
36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

660 
qed 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

661 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

662 
end 
33319  663 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

664 
class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

665 
assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
25186  666 
begin 
25152  667 

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

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

670 
fix a b c :: 'a 
23550  671 
assume "a \<le> b" "0 \<le> c" 
38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

672 
thus "c * a \<le> c * b" by (rule comm_mult_left_mono) 
23550  673 
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

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

675 

25267  676 
end 
677 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

678 
class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add 
25267  679 
begin 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

680 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

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

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

683 
subclass ordered_cancel_semiring .. 
25267  684 

685 
end 

686 

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

687 
class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add + 
38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

688 
assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  689 
begin 
690 

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

691 
subclass linordered_semiring_strict 
28823  692 
proof 
23550  693 
fix a b c :: 'a 
694 
assume "a < b" "0 < c" 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37767
diff
changeset

695 
thus "c * a < c * b" by (rule comm_mult_strict_left_mono) 
23550  696 
thus "a * c < b * c" by (simp only: mult_commute) 
697 
qed 

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

698 

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

699 
subclass ordered_cancel_comm_semiring 
28823  700 
proof 
23550  701 
fix a b c :: 'a 
702 
assume "a \<le> b" "0 \<le> c" 

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

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

707 

25267  708 
end 
25230  709 

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

710 
class ordered_ring = ring + ordered_cancel_semiring 
25267  711 
begin 
25230  712 

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

713 
subclass ordered_ab_group_add .. 
14270  714 

25230  715 
lemma less_add_iff1: 
716 
"a * e + c < b * e + d \<longleftrightarrow> (a  b) * e + c < d" 

29667  717 
by (simp add: algebra_simps) 
25230  718 

719 
lemma less_add_iff2: 

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

29667  721 
by (simp add: algebra_simps) 
25230  722 

723 
lemma le_add_iff1: 

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

29667  725 
by (simp add: algebra_simps) 
25230  726 

727 
lemma le_add_iff2: 

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

29667  729 
by (simp add: algebra_simps) 
25230  730 

731 
lemma mult_left_mono_neg: 

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

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

733 
apply (drule mult_left_mono [of _ _ " c"]) 
35216  734 
apply simp_all 
25230  735 
done 
736 

737 
lemma mult_right_mono_neg: 

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

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

739 
apply (drule mult_right_mono [of _ _ " c"]) 
35216  740 
apply simp_all 
25230  741 
done 
742 

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

743 
lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

744 
using mult_right_mono_neg [of a 0 b] by simp 
25230  745 

746 
lemma split_mult_pos_le: 

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

29667  748 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 
25186  749 

750 
end 

14270  751 

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

752 
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

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

754 

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

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

756 

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

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

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

760 
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

761 
by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg) 
35216  762 
qed (auto simp add: abs_if) 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

763 

35631
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

764 
lemma zero_le_square [simp]: "0 \<le> a * a" 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

765 
using linear [of 0 a] 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

766 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

767 

0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

768 
lemma not_square_less_zero [simp]: "\<not> (a * a < 0)" 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

769 
by (simp add: not_less) 
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

770 

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

771 
end 
23521  772 

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

773 
(* 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

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

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

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

779 

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

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

781 

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

782 
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

783 
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

784 

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

785 
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

786 
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

787 

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

788 
lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

789 
using mult_strict_right_mono_neg [of a 0 b] by simp 
14738  790 

25917  791 
subclass ring_no_zero_divisors 
28823  792 
proof 
25917  793 
fix a b 
794 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

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

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

797 
proof (cases "a < 0") 

798 
case True note A' = this 

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

800 
case True with A' 

801 
show ?thesis by (auto dest: mult_neg_neg) 

802 
next 

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

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

805 
qed 

806 
next 

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

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

809 
case True with A' 

810 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

811 
next 

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

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

814 
qed 

815 
qed 

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

817 
qed 

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

818 

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

819 
lemma zero_less_mult_iff: 
25917  820 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
821 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

822 
apply (simp_all add: not_less le_less) 

823 
apply (erule disjE) apply assumption defer 

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

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

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

827 
apply (drule sym) apply simp 

828 
apply (blast dest: zero_less_mult_pos) 

25230  829 
apply (blast dest: zero_less_mult_pos2) 
830 
done 

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

831 

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

832 
lemma zero_le_mult_iff: 
25917  833 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
29667  834 
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

835 

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

836 
lemma mult_less_0_iff: 
25917  837 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
35216  838 
apply (insert zero_less_mult_iff [of "a" b]) 
839 
apply force 

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

841 

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

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

35216  845 
apply force 
25917  846 
done 
847 

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

850 

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

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

853 

854 
lemma mult_less_cancel_right_disj: 

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

856 
apply (cases "c = 0") 

857 
apply (auto simp add: neq_iff mult_strict_right_mono 

858 
mult_strict_right_mono_neg) 

859 
apply (auto simp add: not_less 

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

861 
not_le [symmetric, of a]) 

862 
apply (erule_tac [!] notE) 

863 
apply (auto simp add: less_imp_le mult_right_mono 

864 
mult_right_mono_neg) 

865 
done 

866 

867 
lemma mult_less_cancel_left_disj: 

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

869 
apply (cases "c = 0") 

870 
apply (auto simp add: neq_iff mult_strict_left_mono 

871 
mult_strict_left_mono_neg) 

872 
apply (auto simp add: not_less 

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

874 
not_le [symmetric, of a]) 

875 
apply (erule_tac [!] notE) 

876 
apply (auto simp add: less_imp_le mult_left_mono 

877 
mult_left_mono_neg) 

878 
done 

879 

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

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

882 

883 
lemma mult_less_cancel_right: 

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

885 
using mult_less_cancel_right_disj [of a c b] by auto 

886 

887 
lemma mult_less_cancel_left: 

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

889 
using mult_less_cancel_left_disj [of c a b] by auto 

890 

891 
lemma mult_le_cancel_right: 

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

29667  893 
by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 
26193  894 

895 
lemma mult_le_cancel_left: 

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

29667  897 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 
26193  898 

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

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

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

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

902 

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

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

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

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

906 

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

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

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

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

910 

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

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

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

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

914 

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

916 

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

917 
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

918 
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

919 
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

920 
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

921 
mult_neg_pos mult_neg_neg 
25230  922 

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

923 
class ordered_comm_ring = comm_ring + ordered_comm_semiring 
25267  924 
begin 
25230  925 

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

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

927 
subclass ordered_cancel_comm_semiring .. 
25230  928 

25267  929 
end 
25230  930 

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

931 
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

932 
(*previously linordered_semiring*) 
25230  933 
assumes zero_less_one [simp]: "0 < 1" 
934 
begin 

935 

936 
lemma pos_add_strict: 

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

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

938 
using add_strict_mono [of 0 a b c] by simp 
25230  939 

26193  940 
lemma zero_le_one [simp]: "0 \<le> 1" 
29667  941 
by (rule zero_less_one [THEN less_imp_le]) 
26193  942 

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

29667  944 
by (simp add: not_le) 
26193  945 

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

29667  947 
by (simp add: not_less) 
26193  948 

949 
lemma less_1_mult: 

950 
assumes "1 < m" and "1 < n" 

951 
shows "1 < m * n" 

952 
using assms mult_strict_mono [of 1 m 1 n] 

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

954 

25230  955 
end 
956 

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

957 
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

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

960 
(*previously linordered_ring*) 
25917  961 
begin 
962 

36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

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

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

965 
subclass ordered_comm_ring .. 
27516  966 
subclass idom .. 
25917  967 

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

968 
subclass linordered_semidom 
28823  969 
proof 
26193  970 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
971 
thus "0 < 1" by (simp add: le_less) 

25917  972 
qed 
973 

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

974 
lemma linorder_neqE_linordered_idom: 
26193  975 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 
976 
using assms by (rule neqE) 

977 

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

980 
lemma mult_le_cancel_right1: 

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

29667  982 
by (insert mult_le_cancel_right [of 1 c b], simp) 
26274  983 

984 
lemma mult_le_cancel_right2: 

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

29667  986 
by (insert mult_le_cancel_right [of a c 1], simp) 
26274  987 

988 
lemma mult_le_cancel_left1: 

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

29667  990 
by (insert mult_le_cancel_left [of c 1 b], simp) 
26274  991 

992 
lemma mult_le_cancel_left2: 

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

29667  994 
by (insert mult_le_cancel_left [of c a 1], simp) 
26274  995 

996 
lemma mult_less_cancel_right1: 

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

29667  998 
by (insert mult_less_cancel_right [of 1 c b], simp) 
26274  999 

1000 
lemma mult_less_cancel_right2: 

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

29667  1002 
by (insert mult_less_cancel_right [of a c 1], simp) 
26274  1003 

1004 
lemma mult_less_cancel_left1: 

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

29667  1006 
by (insert mult_less_cancel_left [of c 1 b], simp) 
26274  1007 

1008 
lemma mult_less_cancel_left2: 

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

29667  1010 
by (insert mult_less_cancel_left [of c a 1], simp) 
26274  1011 

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

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

1013 
"sgn (sgn a) = sgn a" 
29700  1014 
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

1015 

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

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

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

1019 

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

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

1021 
"sgn a = 1 \<longleftrightarrow> a > 0" 
35216  1022 
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

1023 

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

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

1025 
"sgn a =  1 \<longleftrightarrow> a < 0" 
35216  1026 
unfolding sgn_if by auto 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1027 

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

1030 
unfolding sgn_1_pos . 

1031 

1032 
lemma sgn_neg [simp]: 

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

1034 
unfolding sgn_1_neg . 

1035 

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

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

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

1039 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1040 
lemma abs_sgn: "\<bar>k\<bar> = k * sgn k" 
29700  1041 
unfolding sgn_if abs_if by auto 
1042 

29940  1043 
lemma sgn_greater [simp]: 
1044 
"0 < sgn a \<longleftrightarrow> 0 < a" 

1045 
unfolding sgn_if by auto 

1046 

1047 
lemma sgn_less [simp]: 

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

1049 
unfolding sgn_if by auto 

1050 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1051 
lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k" 
29949  1052 
by (simp add: abs_if) 
1053 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1054 
lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k" 
29949  1055 
by (simp add: abs_if) 
29653  1056 

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

1057 
lemma dvd_if_abs_eq: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1058 
"\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k" 
33676
802f5e233e48
moved lemma from Algebra/IntRing to Ring_and_Field
nipkow
parents:
33364
diff
changeset

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

1060 

25917  1061 
end 
25230  1062 

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

1064 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

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

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

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

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

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

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

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

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

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

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

1075 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

1077 

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

1078 
context linordered_semidom 
25193  1079 
begin 
1080 

1081 
lemma less_add_one: "a < a + 1" 

14293  1082 
proof  
25193  1083 
have "a + 0 < a + 1" 
23482  1084 
by (blast intro: zero_less_one add_strict_left_mono) 
14293  1085 
thus ?thesis by simp 
1086 
qed 

1087 

25193  1088 
lemma zero_less_two: "0 < 1 + 1" 
29667  1089 
by (blast intro: less_trans zero_less_one less_add_one) 
25193  1090 

1091 
end 

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

1092 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1093 
context linordered_idom 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

1095 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1096 
lemma mult_right_le_one_le: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1097 
"0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1098 
by (auto simp add: mult_le_cancel_left2) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1099 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1100 
lemma mult_left_le_one_le: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1101 
"0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1102 
by (auto simp add: mult_le_cancel_right2) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1103 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1104 
end 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1105 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1106 
text {* Absolute Value *} 
14293  1107 

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

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

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

1110 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1111 
lemma mult_sgn_abs: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1112 
"sgn x * \<bar>x\<bar> = x" 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

1114 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1115 
lemma abs_one [simp]: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1116 
"\<bar>1\<bar> = 1" 
44921  1117 
by (simp add: abs_if) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1118 

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

1119 
end 
24491  1120 

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

1121 
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

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

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

1124 

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

1125 
context linordered_idom 
30961  1126 
begin 
1127 

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

1128 
subclass ordered_ring_abs proof 
35216  1129 
qed (auto simp add: abs_if not_less mult_less_0_iff) 
30961  1130 

1131 
lemma abs_mult: 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1132 
"\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
30961  1133 
by (rule abs_eq_mult) auto 
1134 

1135 
lemma abs_mult_self: 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1136 
"\<bar>a\<bar> * \<bar>a\<bar> = a * a" 
30961  1137 
by (simp add: abs_if) 
1138 

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

1139 
lemma abs_mult_less: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1140 
"\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d" 
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1141 
proof  
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1142 
assume ac: "\<bar>a\<bar> < c" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1143 
hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1144 
assume "\<bar>b\<bar> < d" 
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset

1145 
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

1146 
qed 
14293  1147 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1148 
lemma less_minus_self_iff: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1149 
"a <  a \<longleftrightarrow> a < 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1150 
by (simp only: less_le less_eq_neg_nonpos equal_neg_zero) 
14738  1151 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1152 
lemma abs_less_iff: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1153 
"\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and>  a < b" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1154 
by (simp add: less_le abs_le_iff) (auto simp add: abs_if) 
14738  1155 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1156 
lemma abs_mult_pos: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1157 
"0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1158 
by (simp add: abs_mult) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1159 

51520
e9b361845809
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
hoelzl
parents:
50420
diff
changeset

1160 
lemma abs_diff_less_iff: 
e9b361845809
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
hoelzl
parents:
50420
diff
changeset

1161 
"\<bar>x  a\<bar> < r \<longleftrightarrow> a  r < x \<and> x < a + r" 
e9b361845809
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
hoelzl
parents:
50420
diff
changeset

1162 
by (auto simp add: diff_less_eq ac_simps abs_less_iff) 
e9b361845809
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
hoelzl
parents:
50420
diff
changeset

1163 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

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

1165 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51520
diff
changeset

1166 
code_identifier 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51520
diff
changeset

1167 
code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 
33364  1168 

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

1169 
end 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51520
diff
changeset

1170 