author  nipkow 
Sat, 12 Apr 2014 17:26:27 +0200  
changeset 56544  b60d5d119489 
parent 56536  aefb4a8da31f 
child 57512  cc97b347b301 
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 

55187  102 
lemma split_of_bool [split]: 
103 
"P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)" 

104 
by (cases p) simp_all 

105 

106 
lemma split_of_bool_asm: 

107 
"P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)" 

108 
by (cases p) simp_all 

109 

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

111 

22390  112 
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 
14504  113 

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

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

115 

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

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

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

118 

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

121 

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

122 
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

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

124 

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

125 
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

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

127 

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

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

129 

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

130 
class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd 
22390  131 
(*previously almost_semiring*) 
25152  132 
begin 
14738  133 

27516  134 
subclass semiring_1 .. 
25152  135 

29925  136 
lemma dvd_refl[simp]: "a dvd a" 
28559  137 
proof 
138 
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

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

140 

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

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

142 
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

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

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

147 
ultimately have "c = a * (v * w)" by (simp add: mult_assoc) 
28559  148 
then show ?thesis .. 
27651
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 

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

151 
lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0" 
29667  152 
by (auto intro: dvd_refl elim!: dvdE) 
28559  153 

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

155 
proof 

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

156 
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

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

158 

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

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

161 

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

164 

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

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

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

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

169 

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

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

172 

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

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

175 

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

176 
lemma mult_dvd_mono: 
30042  177 
assumes "a dvd b" 
178 
and "c dvd d" 

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

179 
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

180 
proof  
30042  181 
from `a dvd b` obtain b' where "b = a * b'" .. 
182 
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

183 
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

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

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

186 

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

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

189 

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

190 
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

191 
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

192 

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

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

195 

29925  196 
lemma dvd_add[simp]: 
197 
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

198 
proof  
29925  199 
from `a dvd b` obtain b' where "b = a * b'" .. 
200 
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

201 
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

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

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

204 

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

206 

22390  207 
class no_zero_divisors = zero + times + 
25062  208 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
36719  209 
begin 
210 

211 
lemma divisors_zero: 

212 
assumes "a * b = 0" 

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

214 
proof (rule classical) 

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

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

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

218 
with assms show ?thesis by simp 

219 
qed 

220 

221 
end 

14504  222 

29904  223 
class semiring_1_cancel = semiring + cancel_comm_monoid_add 
224 
+ zero_neq_one + monoid_mult 

25267  225 
begin 
14940  226 

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

228 

27516  229 
subclass semiring_1 .. 
25267  230 

231 
end 

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

232 

29904  233 
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add 
234 
+ zero_neq_one + comm_monoid_mult 

25267  235 
begin 
14738  236 

27516  237 
subclass semiring_1_cancel .. 
238 
subclass comm_semiring_0_cancel .. 

239 
subclass comm_semiring_1 .. 

25267  240 

241 
end 

25152  242 

22390  243 
class ring = semiring + ab_group_add 
25267  244 
begin 
25152  245 

27516  246 
subclass semiring_0_cancel .. 
25152  247 

248 
text {* Distribution rules *} 

249 

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

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

251 
by (rule minus_unique) (simp add: distrib_right [symmetric]) 
25152  252 

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

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

254 
by (rule minus_unique) (simp add: distrib_left [symmetric]) 
25152  255 

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

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

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

258 
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

259 

25152  260 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  261 
by simp 
25152  262 

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

29667  264 
by simp 
265 

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

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

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

268 
using distrib_left [of a b "c "] by simp 
29667  269 

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

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

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

272 
using distrib_right [of a " b" c] by simp 
25152  273 

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

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

275 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  276 

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

29667  279 
by (simp add: algebra_simps) 
25230  280 

281 
lemma eq_add_iff2: 

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

29667  283 
by (simp add: algebra_simps) 
25230  284 

25152  285 
end 
286 

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

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

288 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  289 

22390  290 
class comm_ring = comm_semiring + ab_group_add 
25267  291 
begin 
14738  292 

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

294 
subclass comm_semiring_0_cancel .. 
25267  295 

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

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

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

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

299 

25267  300 
end 
14738  301 

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

304 

27516  305 
subclass semiring_1_cancel .. 
25267  306 

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

307 
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

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

309 
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

310 

25267  311 
end 
25152  312 

22390  313 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
314 
(*previously ring*) 

25267  315 
begin 
14738  316 

27516  317 
subclass ring_1 .. 
318 
subclass comm_semiring_1_cancel .. 

25267  319 

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

320 
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

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

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

323 
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

324 
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

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

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

327 
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

328 
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

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

330 

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

331 
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

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

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

334 
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

335 
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

336 
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

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

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

339 
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

340 
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

341 
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

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

343 

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

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

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

346 
using dvd_add [of x y " z"] by simp 
29409  347 

25267  348 
end 
25152  349 

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

350 
class ring_no_zero_divisors = ring + no_zero_divisors 
25230  351 
begin 
352 

353 
lemma mult_eq_0_iff [simp]: 

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

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

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

357 
then show ?thesis using no_zero_divisors by simp 

358 
next 

359 
case True then show ?thesis by auto 

360 
qed 

361 

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

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

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

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

26193  369 
qed 
370 

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

371 
lemma mult_cancel_left [simp]: 
26193  372 
"c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" 
373 
proof  

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

35216  375 
by (simp add: algebra_simps) 
376 
thus ?thesis by simp 

26193  377 
qed 
378 

56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55912
diff
changeset

379 
lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)" 
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55912
diff
changeset

380 
by simp 
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55912
diff
changeset

381 

dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55912
diff
changeset

382 
lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)" 
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55912
diff
changeset

383 
by simp 
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55912
diff
changeset

384 

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

386 

23544  387 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  388 
begin 
389 

36970  390 
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

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

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

393 
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

394 
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

395 
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

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

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

398 
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

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

400 

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

29667  403 
by (insert mult_cancel_right [of 1 c b], force) 
26274  404 

405 
lemma mult_cancel_right2 [simp]: 

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

29667  407 
by (insert mult_cancel_right [of a c 1], simp) 
26274  408 

409 
lemma mult_cancel_left1 [simp]: 

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

29667  411 
by (insert mult_cancel_left [of c 1 b], force) 
26274  412 

413 
lemma mult_cancel_left2 [simp]: 

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

29667  415 
by (insert mult_cancel_left [of c a 1], simp) 
26274  416 

417 
end 

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

418 

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

421 

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

423 

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

424 
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

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

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

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

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

429 
then show "a = b \<or> a =  b" 
35216  430 
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

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

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

433 
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

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

435 

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

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

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

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

439 
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

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

441 
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

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

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

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

445 

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

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

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

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

449 
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

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

451 
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

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

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

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

455 

25186  456 
end 
25152  457 

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

460 
\begin{itemize} 

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

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

463 
\end{itemize} 

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

465 
\begin{itemize} 

54703  466 
\item @{url "http://www.mathworld.com"} by Eric Weisstein et. al. 
35302  467 
\item \emph{Algebra I} by van der Waerden, Springer. 
468 
\end{itemize} 

469 
*} 

470 

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

471 
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

472 
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

473 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 
25230  474 
begin 
475 

476 
lemma mult_mono: 

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

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

480 
done 

481 

482 
lemma mult_mono': 

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

483 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 
25230  484 
apply (rule mult_mono) 
485 
apply (fast intro: order_trans)+ 

486 
done 

487 

488 
end 

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

489 

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

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

492 

27516  493 
subclass semiring_0_cancel .. 
23521  494 

56536  495 
lemma mult_nonneg_nonneg[simp]: "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

496 
using mult_left_mono [of 0 b a] by simp 
25230  497 

498 
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

499 
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

500 

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

501 
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

502 
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

503 

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

504 
text {* Legacy  use @{text mult_nonpos_nonneg} *} 
25230  505 
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

506 
by (drule mult_right_mono [of b 0], auto) 
25230  507 

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

511 
end 

512 

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

513 
class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add 
25267  514 
begin 
25230  515 

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

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

517 

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

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

519 

25230  520 
lemma mult_left_less_imp_less: 
521 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  522 
by (force simp add: mult_left_mono not_le [symmetric]) 
25230  523 

524 
lemma mult_right_less_imp_less: 

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

29667  526 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  527 

25186  528 
end 
25152  529 

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

530 
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

531 
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

532 

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

533 
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

534 
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

535 
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

536 
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

537 
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

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

539 
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

540 
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

541 

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

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

543 

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

544 
class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + 
25062  545 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
546 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

548 

27516  549 
subclass semiring_0_cancel .. 
14940  550 

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

551 
subclass linordered_semiring 
28823  552 
proof 
23550  553 
fix a b c :: 'a 
554 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  556 
unfolding le_less 
557 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  558 
from A show "a * c \<le> b * c" 
25152  559 
unfolding le_less 
25186  560 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  561 
qed 
562 

25230  563 
lemma mult_left_le_imp_le: 
564 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

29667  565 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 
25230  566 

567 
lemma mult_right_le_imp_le: 

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

29667  569 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 
25230  570 

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

572 
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

573 

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

574 
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

575 
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

576 

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

577 
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

578 
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

579 

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

580 
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

581 
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

582 
by (drule mult_strict_right_mono [of b 0], auto) 
25230  583 

584 
lemma zero_less_mult_pos: 

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

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

588 
apply (drule_tac mult_pos_neg [of a b]) 
25230  589 
apply (auto dest: less_not_sym) 
590 
done 

591 

592 
lemma zero_less_mult_pos2: 

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

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

596 
apply (drule_tac mult_pos_neg2 [of a b]) 
25230  597 
apply (auto dest: less_not_sym) 
598 
done 

599 

26193  600 
text{*Strict monotonicity in both arguments*} 
601 
lemma mult_strict_mono: 

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

603 
shows "a * c < b * d" 

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

56544  605 
apply (simp) 
26193  606 
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

607 
apply (force simp add: le_less) 
26193  608 
apply (erule mult_strict_left_mono, assumption) 
609 
done 

610 

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

612 
lemma mult_strict_mono': 

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

614 
shows "a * c < b * d" 

29667  615 
by (rule mult_strict_mono) (insert assms, auto) 
26193  616 

617 
lemma mult_less_le_imp_less: 

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

619 
shows "a * c < b * d" 

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

621 
apply (erule less_le_trans) 

622 
apply (erule mult_left_mono) 

623 
apply simp 

624 
apply (erule mult_strict_right_mono) 

625 
apply assumption 

626 
done 

627 

628 
lemma mult_le_less_imp_less: 

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

630 
shows "a * c < b * d" 

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

632 
apply (erule le_less_trans) 

633 
apply (erule mult_strict_left_mono) 

634 
apply simp 

635 
apply (erule mult_right_mono) 

636 
apply simp 

637 
done 

638 

639 
lemma mult_less_imp_less_left: 

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

641 
shows "a < b" 

642 
proof (rule ccontr) 

643 
assume "\<not> a < b" 

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

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

29667  646 
with this and less show False by (simp add: not_less [symmetric]) 
26193  647 
qed 
648 

649 
lemma mult_less_imp_less_right: 

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

651 
shows "a < b" 

652 
proof (rule ccontr) 

653 
assume "\<not> a < b" 

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

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

29667  656 
with this and less show False by (simp add: not_less [symmetric]) 
26193  657 
qed 
658 

25230  659 
end 
660 

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

661 
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

662 
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

663 

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

664 
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

665 

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

666 
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

667 
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

668 
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

669 
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

670 
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

671 
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

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

673 
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

674 
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

675 

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

676 
end 
33319  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_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

679 
assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
25186  680 
begin 
25152  681 

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

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

684 
fix a b c :: 'a 
23550  685 
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

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

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

689 

25267  690 
end 
691 

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

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

694 

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

695 
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

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

697 
subclass ordered_cancel_semiring .. 
25267  698 

699 
end 

700 

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

701 
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

702 
assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  703 
begin 
704 

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

705 
subclass linordered_semiring_strict 
28823  706 
proof 
23550  707 
fix a b c :: 'a 
708 
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

709 
thus "c * a < c * b" by (rule comm_mult_strict_left_mono) 
23550  710 
thus "a * c < b * c" by (simp only: mult_commute) 
711 
qed 

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

712 

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

713 
subclass ordered_cancel_comm_semiring 
28823  714 
proof 
23550  715 
fix a b c :: 'a 
716 
assume "a \<le> b" "0 \<le> c" 

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

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

721 

25267  722 
end 
25230  723 

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

724 
class ordered_ring = ring + ordered_cancel_semiring 
25267  725 
begin 
25230  726 

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

727 
subclass ordered_ab_group_add .. 
14270  728 

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

29667  731 
by (simp add: algebra_simps) 
25230  732 

733 
lemma less_add_iff2: 

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

29667  735 
by (simp add: algebra_simps) 
25230  736 

737 
lemma le_add_iff1: 

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

29667  739 
by (simp add: algebra_simps) 
25230  740 

741 
lemma le_add_iff2: 

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

29667  743 
by (simp add: algebra_simps) 
25230  744 

745 
lemma mult_left_mono_neg: 

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

747 
apply (drule mult_left_mono [of _ _ " c"]) 
35216  748 
apply simp_all 
25230  749 
done 
750 

751 
lemma mult_right_mono_neg: 

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

753 
apply (drule mult_right_mono [of _ _ " c"]) 
35216  754 
apply simp_all 
25230  755 
done 
756 

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

757 
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

758 
using mult_right_mono_neg [of a 0 b] by simp 
25230  759 

760 
lemma split_mult_pos_le: 

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

56536  762 
by (auto simp add: mult_nonpos_nonpos) 
25186  763 

764 
end 

14270  765 

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

766 
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

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

768 

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

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

770 

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

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

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

774 
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

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

777 

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

778 
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

779 
using linear [of 0 a] 
56536  780 
by (auto simp add: mult_nonpos_nonpos) 
35631
0b8a5fd339ab
generalize some lemmas from class linordered_ring_strict to linordered_ring
huffman
parents:
35302
diff
changeset

781 

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

782 
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

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

784 

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

785 
end 
23521  786 

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

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

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

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

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

793 

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

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

795 

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

796 
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

797 
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

798 

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

799 
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

800 
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

801 

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

802 
lemma mult_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

803 
using mult_strict_right_mono_neg [of a 0 b] by simp 
14738  804 

25917  805 
subclass ring_no_zero_divisors 
28823  806 
proof 
25917  807 
fix a b 
808 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

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

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

811 
proof (cases "a < 0") 

812 
case True note A' = this 

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

814 
case True with A' 

815 
show ?thesis by (auto dest: mult_neg_neg) 

816 
next 

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

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

819 
qed 

820 
next 

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

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

823 
case True with A' 

824 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

825 
next 

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

56544  827 
with A' show ?thesis by auto 
25917  828 
qed 
829 
qed 

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

831 
qed 

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

832 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56217
diff
changeset

833 
lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56217
diff
changeset

834 
by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) 
56544  835 
(auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2) 
22990
775e9de3db48
added classes ring_no_zero_divisors and dom (noncommutative version of idom);
huffman
parents:
22987
diff
changeset

836 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56217
diff
changeset

837 
lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56217
diff
changeset

838 
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

839 

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

840 
lemma mult_less_0_iff: 
25917  841 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
35216  842 
apply (insert zero_less_mult_iff [of "a" b]) 
843 
apply force 

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

845 

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

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

35216  849 
apply force 
25917  850 
done 
851 

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

854 

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

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

857 

858 
lemma mult_less_cancel_right_disj: 

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

860 
apply (cases "c = 0") 

861 
apply (auto simp add: neq_iff mult_strict_right_mono 

862 
mult_strict_right_mono_neg) 

863 
apply (auto simp add: not_less 

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

865 
not_le [symmetric, of a]) 

866 
apply (erule_tac [!] notE) 

867 
apply (auto simp add: less_imp_le mult_right_mono 

868 
mult_right_mono_neg) 

869 
done 

870 

871 
lemma mult_less_cancel_left_disj: 

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

873 
apply (cases "c = 0") 

874 
apply (auto simp add: neq_iff mult_strict_left_mono 

875 
mult_strict_left_mono_neg) 

876 
apply (auto simp add: not_less 

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

878 
not_le [symmetric, of a]) 

879 
apply (erule_tac [!] notE) 

880 
apply (auto simp add: less_imp_le mult_left_mono 

881 
mult_left_mono_neg) 

882 
done 

883 

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

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

886 

887 
lemma mult_less_cancel_right: 

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

889 
using mult_less_cancel_right_disj [of a c b] by auto 

890 

891 
lemma mult_less_cancel_left: 

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

893 
using mult_less_cancel_left_disj [of c a b] by auto 

894 

895 
lemma mult_le_cancel_right: 

896 
"a * c \<le> b * c \<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_right_disj) 
26193  898 

899 
lemma mult_le_cancel_left: 

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

29667  901 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 
26193  902 

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

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

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

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_le_cancel_left_neg: 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

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

909 
by (auto simp: mult_le_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_pos: 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30242
diff
changeset

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

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

914 

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

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

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

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

918 

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

920 

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

921 
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

922 
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

923 
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

924 
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

925 
mult_neg_pos mult_neg_neg 
25230  926 

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

927 
class ordered_comm_ring = comm_ring + ordered_comm_semiring 
25267  928 
begin 
25230  929 

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

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

931 
subclass ordered_cancel_comm_semiring .. 
25230  932 

25267  933 
end 
25230  934 

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

935 
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

936 
(*previously linordered_semiring*) 
25230  937 
assumes zero_less_one [simp]: "0 < 1" 
938 
begin 

939 

940 
lemma pos_add_strict: 

941 
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

942 
using add_strict_mono [of 0 a b c] by simp 
25230  943 

26193  944 
lemma zero_le_one [simp]: "0 \<le> 1" 
29667  945 
by (rule zero_less_one [THEN less_imp_le]) 
26193  946 

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

29667  948 
by (simp add: not_le) 
26193  949 

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

29667  951 
by (simp add: not_less) 
26193  952 

953 
lemma less_1_mult: 

954 
assumes "1 < m" and "1 < n" 

955 
shows "1 < m * n" 

956 
using assms mult_strict_mono [of 1 m 1 n] 

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

958 

25230  959 
end 
960 

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

961 
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

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

964 
(*previously linordered_ring*) 
25917  965 
begin 
966 

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

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

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

969 
subclass ordered_comm_ring .. 
27516  970 
subclass idom .. 
25917  971 

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

972 
subclass linordered_semidom 
28823  973 
proof 
26193  974 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
975 
thus "0 < 1" by (simp add: le_less) 

25917  976 
qed 
977 

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

978 
lemma linorder_neqE_linordered_idom: 
26193  979 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 
980 
using assms by (rule neqE) 

981 

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

984 
lemma mult_le_cancel_right1: 

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

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

988 
lemma mult_le_cancel_right2: 

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

29667  990 
by (insert mult_le_cancel_right [of a c 1], simp) 
26274  991 

992 
lemma mult_le_cancel_left1: 

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

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

996 
lemma mult_le_cancel_left2: 

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

29667  998 
by (insert mult_le_cancel_left [of c a 1], simp) 
26274  999 

1000 
lemma mult_less_cancel_right1: 

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

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

1004 
lemma mult_less_cancel_right2: 

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

29667  1006 
by (insert mult_less_cancel_right [of a c 1], simp) 
26274  1007 

1008 
lemma mult_less_cancel_left1: 

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

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

1012 
lemma mult_less_cancel_left2: 

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

29667  1014 
by (insert mult_less_cancel_left [of c a 1], simp) 
26274  1015 

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

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

1017 
"sgn (sgn a) = sgn a" 
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_0_0: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1021 
"sgn a = 0 \<longleftrightarrow> a = 0" 
29700  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_pos: 
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 simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1027 

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

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

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

1031 

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

1034 
unfolding sgn_1_pos . 

1035 

1036 
lemma sgn_neg [simp]: 

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

1038 
unfolding sgn_1_neg . 

1039 

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

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

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

1043 

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

1044 
lemma abs_sgn: "\<bar>k\<bar> = k * sgn k" 
29700  1045 
unfolding sgn_if abs_if by auto 
1046 

29940  1047 
lemma sgn_greater [simp]: 
1048 
"0 < sgn a \<longleftrightarrow> 0 < a" 

1049 
unfolding sgn_if by auto 

1050 

1051 
lemma sgn_less [simp]: 

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

1053 
unfolding sgn_if by auto 

1054 

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

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

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

1058 
lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k" 
29949  1059 
by (simp add: abs_if) 
29653  1060 

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

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

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

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

1064 

55912  1065 
text {* The following lemmas can be proven in more general structures, but 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1066 
are dangerous as simp rules in absence of @{thm neg_equal_zero}, 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1067 
@{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *} 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1068 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1069 
lemma equation_minus_iff_1 [simp, no_atp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1070 
"1 =  a \<longleftrightarrow> a =  1" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1071 
by (fact equation_minus_iff) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1072 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1073 
lemma minus_equation_iff_1 [simp, no_atp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1074 
" a = 1 \<longleftrightarrow> a =  1" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1075 
by (subst minus_equation_iff, auto) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1076 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1077 
lemma le_minus_iff_1 [simp, no_atp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1078 
"1 \<le>  b \<longleftrightarrow> b \<le>  1" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1079 
by (fact le_minus_iff) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1080 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1081 
lemma minus_le_iff_1 [simp, no_atp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1082 
" a \<le> 1 \<longleftrightarrow>  1 \<le> a" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1083 
by (fact minus_le_iff) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1084 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1085 
lemma less_minus_iff_1 [simp, no_atp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1086 
"1 <  b \<longleftrightarrow> b <  1" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1087 
by (fact less_minus_iff) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1088 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1089 
lemma minus_less_iff_1 [simp, no_atp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1090 
" a < 1 \<longleftrightarrow>  1 < a" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1091 
by (fact minus_less_iff) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54250
diff
changeset

1092 

25917  1093 
end 
25230  1094 

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

1096 

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

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

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

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

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

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

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

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

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

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

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

1107 

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

1108 
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

1109 

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

1110 
context linordered_semidom 
25193  1111 
begin 
1112 

1113 
lemma less_add_one: "a < a + 1" 

14293  1114 
proof  
25193  1115 
have "a + 0 < a + 1" 
23482  1116 
by (blast intro: zero_less_one add_strict_left_mono) 
14293  1117 
thus ?thesis by simp 
1118 
qed 

1119 

25193  1120 
lemma zero_less_two: "0 < 1 + 1" 
29667  1121 
by (blast intro: less_trans zero_less_one less_add_one) 
25193  1122 

1123 
end 

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

1124 

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

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

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

1127 

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

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

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

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

1131 

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

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

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

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

1135 

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

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

1137 

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

1138 
text {* Absolute Value *} 
14293  1139 

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

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

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

1142 

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

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

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

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

1146 

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

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

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

1150 

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

1151 
end 
24491  1152 

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

1153 
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

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

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

1156 

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

1157 
context linordered_idom 
30961  1158 
begin 
1159 

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

1160 
subclass ordered_ring_abs proof 
35216  1161 
qed (auto simp add: abs_if not_less mult_less_0_iff) 
30961  1162 

1163 
lemma abs_mult: 

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

1164 
"\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
30961  1165 
by (rule abs_eq_mult) auto 
1166 

1167 
lemma abs_mult_self: 

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

1168 
"\<bar>a\<bar> * \<bar>a\<bar> = a * a" 
30961  1169 
by (simp add: abs_if) 
1170 

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

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

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

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

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

1175 
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

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

1177 
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

1178 
qed 
14293  1179 

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

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

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

1182 
by (simp add: less_le abs_le_iff) (auto simp add: abs_if) 
14738  1183 

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

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

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

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

1187 

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

1188 
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

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

1190 
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

1191 

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

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

1193 

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

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

1195 
code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 
33364  1196 

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

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

1198 