author  haftmann 
Fri, 19 Jun 2015 07:53:35 +0200  
changeset 60517  f16e4fb20652 
parent 60516  0826b7025d07 
child 60529  24c2ef12318b 
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 

58889  10 
section {* 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 + 
58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58649
diff
changeset

17 
assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c" 
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58649
diff
changeset

18 
assumes distrib_left[algebra_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" 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

24 
by (simp add: distrib_right ac_simps) 
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" 

58195  31 
begin 
32 

33 
lemma mult_not_zero: 

34 
"a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0" 

35 
by auto 

36 

37 
end 

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

38 

58198  39 
class semiring_0 = semiring + comm_monoid_add + mult_zero 
40 

29904  41 
class semiring_0_cancel = semiring + cancel_comm_monoid_add 
25186  42 
begin 
14504  43 

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

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

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

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

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

53 
qed 
14940  54 

25186  55 
end 
25152  56 

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

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

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

65 
have "a * (b + c) = (b + c) * a" by (simp add: ac_simps) 
14738  66 
also have "... = b * a + c * a" by (simp only: distrib) 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

67 
also have "... = a * b + a * c" by (simp add: ac_simps) 
14738  68 
finally show "a * (b + c) = a * b + a * c" by blast 
14504  69 
qed 
70 

25152  71 
end 
14504  72 

25152  73 
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero 
74 
begin 

75 

27516  76 
subclass semiring_0 .. 
25152  77 

78 
end 

14504  79 

29904  80 
class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add 
25186  81 
begin 
14940  82 

27516  83 
subclass semiring_0_cancel .. 
14940  84 

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

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

86 

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

88 

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

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

29667  94 
by (rule not_sym) (rule zero_neq_one) 
26193  95 

54225  96 
definition of_bool :: "bool \<Rightarrow> 'a" 
97 
where 

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

99 

100 
lemma of_bool_eq [simp, code]: 

101 
"of_bool False = 0" 

102 
"of_bool True = 1" 

103 
by (simp_all add: of_bool_def) 

104 

105 
lemma of_bool_eq_iff: 

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

107 
by (simp add: of_bool_def) 

108 

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

111 
by (cases p) simp_all 

112 

113 
lemma split_of_bool_asm: 

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

115 
by (cases p) simp_all 

116 

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

118 

22390  119 
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 
14504  120 

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

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

122 

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

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

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

125 

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

128 

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

129 
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

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

131 

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

132 
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

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

134 

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

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

136 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

137 
context comm_monoid_mult 
25152  138 
begin 
14738  139 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

140 
subclass dvd . 
25152  141 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

142 
lemma dvd_refl [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

143 
"a dvd a" 
28559  144 
proof 
145 
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

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

147 

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

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

149 
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

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

151 
proof  
28559  152 
from assms obtain v where "b = a * v" by (auto elim!: dvdE) 
153 
moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56544
diff
changeset

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

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

157 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

158 
lemma one_dvd [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

159 
"1 dvd a" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

160 
by (auto intro!: dvdI) 
28559  161 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

162 
lemma dvd_mult [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

163 
"a dvd c \<Longrightarrow> a dvd (b * c)" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

164 
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

165 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

166 
lemma dvd_mult2 [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

167 
"a dvd b \<Longrightarrow> a dvd (b * c)" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

168 
using dvd_mult [of a b c] by (simp add: ac_simps) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

169 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

170 
lemma dvd_triv_right [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

171 
"a dvd b * a" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

172 
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

173 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

174 
lemma dvd_triv_left [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

175 
"a dvd a * b" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

176 
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

177 

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

178 
lemma mult_dvd_mono: 
30042  179 
assumes "a dvd b" 
180 
and "c dvd d" 

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

181 
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

182 
proof  
30042  183 
from `a dvd b` obtain b' where "b = a * b'" .. 
184 
moreover from `c dvd d` obtain d' where "d = c * d'" .. 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

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

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

188 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

189 
lemma dvd_mult_left: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

190 
"a * b dvd c \<Longrightarrow> a dvd c" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

191 
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

192 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

193 
lemma dvd_mult_right: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

194 
"a * b dvd c \<Longrightarrow> b dvd c" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

195 
using dvd_mult_left [of b a c] by (simp add: ac_simps) 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

196 

348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

197 
end 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

198 

348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

199 
class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

200 
begin 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

201 

348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

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

203 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

204 
lemma dvd_0_left_iff [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

205 
"0 dvd a \<longleftrightarrow> a = 0" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

206 
by (auto intro: dvd_refl elim!: dvdE) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

207 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

208 
lemma dvd_0_right [iff]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

209 
"a dvd 0" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

210 
proof 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

211 
show "0 = a * 0" by simp 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

212 
qed 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

213 

348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

214 
lemma dvd_0_left: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

215 
"0 dvd a \<Longrightarrow> a = 0" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

216 
by simp 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

217 

348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

218 
lemma dvd_add [simp]: 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

219 
assumes "a dvd b" and "a dvd c" 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

220 
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

221 
proof  
29925  222 
from `a dvd b` obtain b' where "b = a * b'" .. 
223 
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

224 
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

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

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

227 

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

229 

29904  230 
class semiring_1_cancel = semiring + cancel_comm_monoid_add 
231 
+ zero_neq_one + monoid_mult 

25267  232 
begin 
14940  233 

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

235 

27516  236 
subclass semiring_1 .. 
25267  237 

238 
end 

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

239 

29904  240 
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add 
241 
+ zero_neq_one + comm_monoid_mult 

25267  242 
begin 
14738  243 

27516  244 
subclass semiring_1_cancel .. 
245 
subclass comm_semiring_0_cancel .. 

246 
subclass comm_semiring_1 .. 

25267  247 

248 
end 

25152  249 

59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

250 
class comm_semiring_1_diff_distrib = comm_semiring_1_cancel + 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

251 
assumes right_diff_distrib' [algebra_simps]: "a * (b  c) = a * b  a * c" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

252 
begin 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

253 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

254 
lemma left_diff_distrib' [algebra_simps]: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

255 
"(b  c) * a = b * a  c * a" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

256 
by (simp add: algebra_simps) 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

257 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

258 
lemma dvd_add_times_triv_left_iff [simp]: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

259 
"a dvd c * a + b \<longleftrightarrow> a dvd b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

260 
proof  
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

261 
have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q") 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

262 
proof 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

263 
assume ?Q then show ?P by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

264 
next 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

265 
assume ?P 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

266 
then obtain d where "a * c + b = a * d" .. 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

267 
then have "a * c + b  a * c = a * d  a * c" by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

268 
then have "b = a * d  a * c" by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

269 
then have "b = a * (d  c)" by (simp add: algebra_simps) 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

270 
then show ?Q .. 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

271 
qed 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

272 
then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps) 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

273 
qed 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

274 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

275 
lemma dvd_add_times_triv_right_iff [simp]: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

276 
"a dvd b + c * a \<longleftrightarrow> a dvd b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

277 
using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps) 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

278 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

279 
lemma dvd_add_triv_left_iff [simp]: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

280 
"a dvd a + b \<longleftrightarrow> a dvd b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

281 
using dvd_add_times_triv_left_iff [of a 1 b] by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

282 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

283 
lemma dvd_add_triv_right_iff [simp]: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

284 
"a dvd b + a \<longleftrightarrow> a dvd b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

285 
using dvd_add_times_triv_right_iff [of a b 1] by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

286 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

287 
lemma dvd_add_right_iff: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

288 
assumes "a dvd b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

289 
shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q") 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

290 
proof 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

291 
assume ?P then obtain d where "b + c = a * d" .. 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

292 
moreover from `a dvd b` obtain e where "b = a * e" .. 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

293 
ultimately have "a * e + c = a * d" by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

294 
then have "a * e + c  a * e = a * d  a * e" by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

295 
then have "c = a * d  a * e" by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

296 
then have "c = a * (d  e)" by (simp add: algebra_simps) 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

297 
then show ?Q .. 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

298 
next 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

299 
assume ?Q with assms show ?P by simp 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

300 
qed 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

301 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

302 
lemma dvd_add_left_iff: 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

303 
assumes "a dvd c" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

304 
shows "a dvd b + c \<longleftrightarrow> a dvd b" 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

305 
using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps) 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

306 

034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

307 
end 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

308 

22390  309 
class ring = semiring + ab_group_add 
25267  310 
begin 
25152  311 

27516  312 
subclass semiring_0_cancel .. 
25152  313 

314 
text {* Distribution rules *} 

315 

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

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

317 
by (rule minus_unique) (simp add: distrib_right [symmetric]) 
25152  318 

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

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

320 
by (rule minus_unique) (simp add: distrib_left [symmetric]) 
25152  321 

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

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

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

324 
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

325 

25152  326 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  327 
by simp 
25152  328 

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

29667  330 
by simp 
331 

58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58649
diff
changeset

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

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

334 
using distrib_left [of a b "c "] by simp 
29667  335 

58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58649
diff
changeset

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

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

338 
using distrib_right [of a " b" c] by simp 
25152  339 

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

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

341 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  342 

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

29667  345 
by (simp add: algebra_simps) 
25230  346 

347 
lemma eq_add_iff2: 

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

29667  349 
by (simp add: algebra_simps) 
25230  350 

25152  351 
end 
352 

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

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

354 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  355 

22390  356 
class comm_ring = comm_semiring + ab_group_add 
25267  357 
begin 
14738  358 

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

360 
subclass comm_semiring_0_cancel .. 
25267  361 

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

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

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

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

365 

25267  366 
end 
14738  367 

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

370 

27516  371 
subclass semiring_1_cancel .. 
25267  372 

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

373 
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

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

375 
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

376 

25267  377 
end 
25152  378 

22390  379 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
25267  380 
begin 
14738  381 

27516  382 
subclass ring_1 .. 
383 
subclass comm_semiring_1_cancel .. 

25267  384 

59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

385 
subclass comm_semiring_1_diff_distrib 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

386 
by unfold_locales (simp add: algebra_simps) 
58647  387 

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

388 
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

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

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

391 
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

392 
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

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

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

395 
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

396 
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

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

398 

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

399 
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

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

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

402 
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

403 
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

404 
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

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

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

407 
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

408 
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

409 
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

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

411 

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

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

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

414 
using dvd_add [of x y " z"] by simp 
29409  415 

25267  416 
end 
25152  417 

59833
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

418 
class semiring_no_zero_divisors = semiring_0 + 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

419 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
25230  420 
begin 
421 

59833
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

422 
lemma divisors_zero: 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

423 
assumes "a * b = 0" 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

424 
shows "a = 0 \<or> b = 0" 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

425 
proof (rule classical) 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

426 
assume "\<not> (a = 0 \<or> b = 0)" 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

427 
then have "a \<noteq> 0" and "b \<noteq> 0" by auto 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

428 
with no_zero_divisors have "a * b \<noteq> 0" by blast 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

429 
with assms show ?thesis by simp 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

430 
qed 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

431 

25230  432 
lemma mult_eq_0_iff [simp]: 
58952
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

433 
shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 
25230  434 
proof (cases "a = 0 \<or> b = 0") 
435 
case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto 

436 
then show ?thesis using no_zero_divisors by simp 

437 
next 

438 
case True then show ?thesis by auto 

439 
qed 

440 

58952
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

441 
end 
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

442 

60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

443 
class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors + 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

444 
assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

445 
and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" 
58952
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

446 
begin 
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

447 

5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

448 
lemma mult_left_cancel: 
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

449 
"c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b" 
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

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

451 

58952
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

452 
lemma mult_right_cancel: 
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

453 
"c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b" 
5d82cdef6c1b
equivalence rules for structures without zero divisors
haftmann
parents:
58889
diff
changeset

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

455 

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

457 

60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

458 
class ring_no_zero_divisors = ring + semiring_no_zero_divisors 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

459 
begin 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

460 

0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

461 
subclass semiring_no_zero_divisors_cancel 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

462 
proof 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

463 
fix a b c 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

464 
have "a * c = b * c \<longleftrightarrow> (a  b) * c = 0" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

465 
by (simp add: algebra_simps) 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

466 
also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

467 
by auto 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

468 
finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" . 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

469 
have "c * a = c * b \<longleftrightarrow> c * (a  b) = 0" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

470 
by (simp add: algebra_simps) 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

471 
also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

472 
by auto 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

473 
finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" . 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

474 
qed 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

475 

0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

476 
end 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

477 

23544  478 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  479 
begin 
480 

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

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

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

484 
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

485 
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

486 
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

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

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

489 
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

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

491 

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

29667  494 
by (insert mult_cancel_right [of 1 c b], force) 
26274  495 

496 
lemma mult_cancel_right2 [simp]: 

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

29667  498 
by (insert mult_cancel_right [of a c 1], simp) 
26274  499 

500 
lemma mult_cancel_left1 [simp]: 

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

29667  502 
by (insert mult_cancel_left [of c 1 b], force) 
26274  503 

504 
lemma mult_cancel_left2 [simp]: 

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

29667  506 
by (insert mult_cancel_left [of c a 1], simp) 
26274  507 

508 
end 

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

509 

59910
815de5506080
semidom contains distributive minus, by convention
haftmann
parents:
59865
diff
changeset

510 
class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors 
59833
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

511 

ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

512 
class idom = comm_ring_1 + semiring_no_zero_divisors 
25186  513 
begin 
14421
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14398
diff
changeset

514 

59833
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

515 
subclass semidom .. 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

516 

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

518 

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

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

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

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

522 
have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

524 
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

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

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

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

528 

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

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

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

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

532 
have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

534 
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

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

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

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

538 

60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

539 
lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a =  b" 
59833
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

540 
proof 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

541 
assume "a * a = b * b" 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

542 
then have "(a  b) * (a + b) = 0" 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

543 
by (simp add: algebra_simps) 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

544 
then show "a = b \<or> a =  b" 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

545 
by (simp add: eq_neg_iff_add_eq_0) 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

546 
next 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

547 
assume "a = b \<or> a =  b" 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

548 
then show "a * a = b * b" by auto 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

549 
qed 
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

550 

25186  551 
end 
25152  552 

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

555 
\begin{itemize} 

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

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

558 
\end{itemize} 

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

560 
\begin{itemize} 

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

564 
*} 

565 

60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

566 
class divide = 
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

567 
fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70) 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

568 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

569 
setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *} 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

570 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

571 
context semiring 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

572 
begin 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

573 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

574 
lemma [field_simps]: 
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

575 
shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c" 
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

576 
and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c" 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

577 
by (rule distrib_left distrib_right)+ 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

578 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

579 
end 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

580 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

581 
context ring 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

582 
begin 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

583 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

584 
lemma [field_simps]: 
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

585 
shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a  b) * c = a * c  b * c" 
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

586 
and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b  c) = a * b  a * c" 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

587 
by (rule left_diff_distrib right_diff_distrib)+ 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

588 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

589 
end 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

590 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

591 
setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *} 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

592 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

593 
class semidom_divide = semidom + divide + 
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

594 
assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a" 
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

595 
assumes divide_zero [simp]: "a div 0 = 0" 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

596 
begin 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

597 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

598 
lemma nonzero_mult_divide_cancel_left [simp]: 
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60353
diff
changeset

599 
"a \<noteq> 0 \<Longrightarrow> (a * b) div a = b" 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

600 
using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps) 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

601 

60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

602 
subclass semiring_no_zero_divisors_cancel 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

603 
proof 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

604 
fix a b c 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

605 
{ fix a b c 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

606 
show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

607 
proof (cases "c = 0") 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

608 
case True then show ?thesis by simp 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

609 
next 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

610 
case False 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

611 
{ assume "a * c = b * c" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

612 
then have "a * c div c = b * c div c" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

613 
by simp 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

614 
with False have "a = b" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

615 
by simp 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

616 
} then show ?thesis by auto 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

617 
qed 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

618 
} 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

619 
from this [of a c b] 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

620 
show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

621 
by (simp add: ac_simps) 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

622 
qed 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

623 

0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

624 
lemma div_self [simp]: 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

625 
assumes "a \<noteq> 0" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

626 
shows "a div a = 1" 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

627 
using assms nonzero_mult_divide_cancel_left [of a 1] by simp 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

628 

60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

629 
end 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

630 

838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

631 
class idom_divide = idom + semidom_divide 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

632 

60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

633 
class algebraic_semidom = semidom_divide 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

634 
begin 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

635 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

636 
lemma dvd_div_mult_self [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

637 
"a dvd b \<Longrightarrow> b div a * a = b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

638 
by (cases "a = 0") (auto elim: dvdE simp add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

639 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

640 
lemma dvd_mult_div_cancel [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

641 
"a dvd b \<Longrightarrow> a * (b div a) = b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

642 
using dvd_div_mult_self [of a b] by (simp add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

643 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

644 
lemma div_mult_swap: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

645 
assumes "c dvd b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

646 
shows "a * (b div c) = (a * b) div c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

647 
proof (cases "c = 0") 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

648 
case True then show ?thesis by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

649 
next 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

650 
case False from assms obtain d where "b = c * d" .. 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

651 
moreover from False have "a * divide (d * c) c = ((a * d) * c) div c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

652 
by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

653 
ultimately show ?thesis by (simp add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

654 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

655 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

656 
lemma dvd_div_mult: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

657 
assumes "c dvd b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

658 
shows "b div c * a = (b * a) div c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

659 
using assms div_mult_swap [of c b a] by (simp add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

660 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

661 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

662 
text \<open>Units: invertible elements in a ring\<close> 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

663 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

664 
abbreviation is_unit :: "'a \<Rightarrow> bool" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

665 
where 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

666 
"is_unit a \<equiv> a dvd 1" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

667 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

668 
lemma not_is_unit_0 [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

669 
"\<not> is_unit 0" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

670 
by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

671 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

672 
lemma unit_imp_dvd [dest]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

673 
"is_unit b \<Longrightarrow> b dvd a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

674 
by (rule dvd_trans [of _ 1]) simp_all 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

675 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

676 
lemma unit_dvdE: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

677 
assumes "is_unit a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

678 
obtains c where "a \<noteq> 0" and "b = a * c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

679 
proof  
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

680 
from assms have "a dvd b" by auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

681 
then obtain c where "b = a * c" .. 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

682 
moreover from assms have "a \<noteq> 0" by auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

683 
ultimately show thesis using that by blast 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

684 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

685 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

686 
lemma dvd_unit_imp_unit: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

687 
"a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

688 
by (rule dvd_trans) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

689 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

690 
lemma unit_div_1_unit [simp, intro]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

691 
assumes "is_unit a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

692 
shows "is_unit (1 div a)" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

693 
proof  
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

694 
from assms have "1 = 1 div a * a" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

695 
then show "is_unit (1 div a)" by (rule dvdI) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

696 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

697 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

698 
lemma is_unitE [elim?]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

699 
assumes "is_unit a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

700 
obtains b where "a \<noteq> 0" and "b \<noteq> 0" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

701 
and "is_unit b" and "1 div a = b" and "1 div b = a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

702 
and "a * b = 1" and "c div a = c * b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

703 
proof (rule that) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

704 
def b \<equiv> "1 div a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

705 
then show "1 div a = b" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

706 
from b_def `is_unit a` show "is_unit b" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

707 
from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

708 
from b_def `is_unit a` show "a * b = 1" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

709 
then have "1 = a * b" .. 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

710 
with b_def `b \<noteq> 0` show "1 div b = a" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

711 
from `is_unit a` have "a dvd c" .. 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

712 
then obtain d where "c = a * d" .. 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

713 
with `a \<noteq> 0` `a * b = 1` show "c div a = c * b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

714 
by (simp add: mult.assoc mult.left_commute [of a]) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

715 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

716 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

717 
lemma unit_prod [intro]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

718 
"is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

719 
by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

720 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

721 
lemma unit_div [intro]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

722 
"is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

723 
by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

724 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

725 
lemma mult_unit_dvd_iff: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

726 
assumes "is_unit b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

727 
shows "a * b dvd c \<longleftrightarrow> a dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

728 
proof 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

729 
assume "a * b dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

730 
with assms show "a dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

731 
by (simp add: dvd_mult_left) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

732 
next 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

733 
assume "a dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

734 
then obtain k where "c = a * k" .. 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

735 
with assms have "c = (a * b) * (1 div b * k)" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

736 
by (simp add: mult_ac) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

737 
then show "a * b dvd c" by (rule dvdI) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

738 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

739 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

740 
lemma dvd_mult_unit_iff: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

741 
assumes "is_unit b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

742 
shows "a dvd c * b \<longleftrightarrow> a dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

743 
proof 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

744 
assume "a dvd c * b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

745 
with assms have "c * b dvd c * (b * (1 div b))" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

746 
by (subst mult_assoc [symmetric]) simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

747 
also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

748 
finally have "c * b dvd c" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

749 
with `a dvd c * b` show "a dvd c" by (rule dvd_trans) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

750 
next 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

751 
assume "a dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

752 
then show "a dvd c * b" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

753 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

754 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

755 
lemma div_unit_dvd_iff: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

756 
"is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

757 
by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

758 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

759 
lemma dvd_div_unit_iff: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

760 
"is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

761 
by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

762 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

763 
lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

764 
dvd_mult_unit_iff dvd_div_unit_iff  \<open>FIXME consider fact collection\<close> 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

765 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

766 
lemma unit_mult_div_div [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

767 
"is_unit a \<Longrightarrow> b * (1 div a) = b div a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

768 
by (erule is_unitE [of _ b]) simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

769 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

770 
lemma unit_div_mult_self [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

771 
"is_unit a \<Longrightarrow> b div a * a = b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

772 
by (rule dvd_div_mult_self) auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

773 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

774 
lemma unit_div_1_div_1 [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

775 
"is_unit a \<Longrightarrow> 1 div (1 div a) = a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

776 
by (erule is_unitE) simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

777 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

778 
lemma unit_div_mult_swap: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

779 
"is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

780 
by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c]) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

781 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

782 
lemma unit_div_commute: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

783 
"is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

784 
using unit_div_mult_swap [of b c a] by (simp add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

785 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

786 
lemma unit_eq_div1: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

787 
"is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

788 
by (auto elim: is_unitE) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

789 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

790 
lemma unit_eq_div2: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

791 
"is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

792 
using unit_eq_div1 [of b c a] by auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

793 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

794 
lemma unit_mult_left_cancel: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

795 
assumes "is_unit a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

796 
shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q") 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

797 
using assms mult_cancel_left [of a b c] by auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

798 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

799 
lemma unit_mult_right_cancel: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

800 
"is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

801 
using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

802 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

803 
lemma unit_div_cancel: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

804 
assumes "is_unit a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

805 
shows "b div a = c div a \<longleftrightarrow> b = c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

806 
proof  
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

807 
from assms have "is_unit (1 div a)" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

808 
then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

809 
by (rule unit_mult_right_cancel) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

810 
with assms show ?thesis by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

811 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

812 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

813 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

814 
text \<open>Associated elements in a ring â€“ an equivalence relation induced by the quasiorder divisibility \<close> 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

815 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

816 
definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

817 
where 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

818 
"associated a b \<longleftrightarrow> a dvd b \<and> b dvd a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

819 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

820 
lemma associatedI: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

821 
"a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

822 
by (simp add: associated_def) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

823 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

824 
lemma associatedD1: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

825 
"associated a b \<Longrightarrow> a dvd b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

826 
by (simp add: associated_def) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

827 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

828 
lemma associatedD2: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

829 
"associated a b \<Longrightarrow> b dvd a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

830 
by (simp add: associated_def) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

831 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

832 
lemma associated_refl [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

833 
"associated a a" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

834 
by (auto intro: associatedI) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

835 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

836 
lemma associated_sym: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

837 
"associated b a \<longleftrightarrow> associated a b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

838 
by (auto intro: associatedI dest: associatedD1 associatedD2) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

839 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

840 
lemma associated_trans: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

841 
"associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

842 
by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

843 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

844 
lemma associated_0 [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

845 
"associated 0 b \<longleftrightarrow> b = 0" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

846 
"associated a 0 \<longleftrightarrow> a = 0" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

847 
by (auto dest: associatedD1 associatedD2) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

848 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

849 
lemma associated_unit: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

850 
"associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

851 
using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

852 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

853 
lemma is_unit_associatedI: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

854 
assumes "is_unit c" and "a = c * b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

855 
shows "associated a b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

856 
proof (rule associatedI) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

857 
from `a = c * b` show "b dvd a" by auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

858 
from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

859 
moreover from `a = c * b` have "d * a = d * (c * b)" by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

860 
ultimately have "b = a * d" by (simp add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

861 
then show "a dvd b" .. 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

862 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

863 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

864 
lemma associated_is_unitE: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

865 
assumes "associated a b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

866 
obtains c where "is_unit c" and "a = c * b" 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

867 
proof (cases "b = 0") 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

868 
case True with assms have "is_unit 1" and "a = 1 * b" by simp_all 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

869 
with that show thesis . 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

870 
next 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

871 
case False 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

872 
from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

873 
then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

874 
then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps) 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

875 
with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

876 
then have "is_unit c" by auto 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

877 
with `a = c * b` that show thesis by blast 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

878 
qed 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

879 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

880 
lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

881 
dvd_div_unit_iff unit_div_mult_swap unit_div_commute 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

882 
unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

883 
unit_eq_div1 unit_eq_div2 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

884 

f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

885 
end 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

886 

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

887 
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

888 
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

889 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 
25230  890 
begin 
891 

892 
lemma mult_mono: 

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

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

896 
done 

897 

898 
lemma mult_mono': 

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

899 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 
25230  900 
apply (rule mult_mono) 
901 
apply (fast intro: order_trans)+ 

902 
done 

903 

904 
end 

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

905 

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

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

908 

27516  909 
subclass semiring_0_cancel .. 
23521  910 

56536  911 
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

912 
using mult_left_mono [of 0 b a] by simp 
25230  913 

914 
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

915 
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

916 

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

917 
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

918 
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

919 

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

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

922 
by (drule mult_right_mono [of b 0], auto) 
25230  923 

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

927 
end 

928 

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

929 
class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add 
25267  930 
begin 
25230  931 

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

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

933 

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

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

935 

25230  936 
lemma mult_left_less_imp_less: 
937 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  938 
by (force simp add: mult_left_mono not_le [symmetric]) 
25230  939 

940 
lemma mult_right_less_imp_less: 

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

29667  942 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  943 

25186  944 
end 
25152  945 

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

946 
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

947 
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

948 

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

949 
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

950 
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

951 
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

952 
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

953 
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

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

955 
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

956 
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

957 

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

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

959 

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

960 
class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + 
25062  961 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
962 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

964 

27516  965 
subclass semiring_0_cancel .. 
14940  966 

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

967 
subclass linordered_semiring 
28823  968 
proof 
23550  969 
fix a b c :: 'a 
970 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  972 
unfolding le_less 
973 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  974 
from A show "a * c \<le> b * c" 
25152  975 
unfolding le_less 
25186  976 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  977 
qed 
978 

25230  979 
lemma mult_left_le_imp_le: 
980 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

29667  981 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 
25230  982 

983 
lemma mult_right_le_imp_le: 

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

29667  985 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 
25230  986 

56544  987 
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

988 
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

989 

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

990 
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

991 
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

992 

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

993 
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

994 
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

995 

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

996 
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

997 
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

998 
by (drule mult_strict_right_mono [of b 0], auto) 
25230  999 

1000 
lemma zero_less_mult_pos: 

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

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

1004 
apply (drule_tac mult_pos_neg [of a b]) 
25230  1005 
apply (auto dest: less_not_sym) 
1006 
done 

1007 

1008 
lemma zero_less_mult_pos2: 

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

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

1012 
apply (drule_tac mult_pos_neg2 [of a b]) 
25230  1013 
apply (auto dest: less_not_sym) 
1014 
done 

1015 

26193  1016 
text{*Strict monotonicity in both arguments*} 
1017 
lemma mult_strict_mono: 

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

1019 
shows "a * c < b * d" 

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

56544  1021 
apply (simp) 
26193  1022 
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

1023 
apply (force simp add: le_less) 
26193  1024 
apply (erule mult_strict_left_mono, assumption) 
1025 
done 

1026 

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

1028 
lemma mult_strict_mono': 

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

1030 
shows "a * c < b * d" 

29667  1031 
by (rule mult_strict_mono) (insert assms, auto) 
26193  1032 

1033 
lemma mult_less_le_imp_less: 

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

1035 
shows "a * c < b * d" 

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

1037 
apply (erule less_le_trans) 

1038 
apply (erule mult_left_mono) 

1039 
apply simp 

1040 
apply (erule mult_strict_right_mono) 

1041 
apply assumption 

1042 
done 

1043 

1044 
lemma mult_le_less_imp_less: 

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

1046 
shows "a * c < b * d" 

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

1048 
apply (erule le_less_trans) 

1049 
apply (erule mult_strict_left_mono) 

1050 
apply simp 

1051 
apply (erule mult_right_mono) 

1052 
apply simp 

1053 
done 

1054 

25230  1055 
end 
1056 

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

1057 
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

1058 
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

1059 

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

1060 
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

1061 

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

1062 
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

1063 
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

1064 
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

1065 
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

1066 
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

1067 
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

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

1069 
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

1070 
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

1071 

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

1072 
end 
33319  1073 

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

1074 
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

1075 
assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
25186  1076 
begin 
25152  1077 

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

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

1080 
fix a b c :: 'a 
23550  1081 
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

1082 
thus "c * a \<le> c * b" by (rule comm_mult_left_mono) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56544
diff
changeset

1083 
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

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

1085 

25267  1086 
end 
1087 

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

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

1090 

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

1091 
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

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

1093 
subclass ordered_cancel_semiring .. 
25267  1094 

1095 
end 

1096 

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

1097 
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

1098 
assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  1099 
begin 
1100 

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

1101 
subclass linordered_semiring_strict 
28823  1102 
proof 
23550  1103 
fix a b c :: 'a 
1104 
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

1105 
thus "c * a < c * b" by (rule comm_mult_strict_left_mono) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56544
diff
changeset

1106 
thus "a * c < b * c" by (simp only: mult.commute) 
23550  1107 
qed 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14270
diff
changeset

1108 

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

1109 
subclass ordered_cancel_comm_semiring 
28823  1110 
proof 
23550  1111 
fix a b c :: 'a 
1112 
assume "a \<le> b" "0 \<le> c" 

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

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

1117 

25267  1118 
end 
25230  1119 

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

1120 
class ordered_ring = ring + ordered_cancel_semiring 
25267  1121 
begin 
25230  1122 

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

1123 
subclass ordered_ab_group_add .. 
14270  1124 

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

29667  1127 
by (simp add: algebra_simps) 
25230  1128 

1129 
lemma less_add_iff2: 

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

29667  1131 
by (simp add: algebra_simps) 
25230  1132 

1133 
lemma le_add_iff1: 

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

29667  1135 
by (simp add: algebra_simps) 
25230  1136 

1137 
lemma le_add_iff2: 

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

29667  1139 
by (simp add: algebra_simps) 
25230  1140 

1141 
lemma mult_left_mono_neg: 

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

1143 
apply (drule mult_left_mono [of _ _ " c"]) 
35216  1144 
apply simp_all 
25230  1145 
done 
1146 

1147 
lemma mult_right_mono_neg: 

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

1149 
apply (drule mult_right_mono [of _ _ " c"]) 
35216  1150 
apply simp_all 
25230  1151 
done 
1152 

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

1153 
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

1154 
using mult_right_mono_neg [of a 0 b] by simp 
25230  1155 

1156 
lemma split_mult_pos_le: 

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

56536  1158 
by (auto simp add: mult_nonpos_nonpos) 
25186  1159 

1160 
end 

14270  1161 

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

1162 
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

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

1164 

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

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

1166 

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

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

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

1170 
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

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

1173 

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

1174 
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

1175 
using linear [of 0 a] 
56536  1176 
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

1177 

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

1178 
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

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

1180 

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

1181 
end 
23521  1182 

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

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

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

1186 

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

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

1188 

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

1189 
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

1190 
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

1191 

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

1192 
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

1193 
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

1194 

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

1195 
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

1196 
using mult_strict_right_mono_neg [of a 0 b] by simp 
14738  1197 

25917  1198 
subclass ring_no_zero_divisors 
28823  1199 
proof 
25917  1200 
fix a b 
1201 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

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

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

1204 
proof (cases "a < 0") 

1205 
case True note A' = this 

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

1207 
case True with A' 

1208 
show ?thesis by (auto dest: mult_neg_neg) 

1209 
next 

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

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

1212 
qed 

1213 
next 

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

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

1216 
case True with A' 

1217 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

1218 
next 

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

56544  1220 
with A' show ?thesis by auto 
25917  1221 
qed 
1222 
qed 

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

1224 
qed 

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

1225 

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

1226 
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

1227 
by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) 
56544  1228 
(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

1229 

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

1230 
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

1231 
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

1232 

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

1233 
lemma mult_less_0_iff: 
25917  1234 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
35216  1235 
apply (insert zero_less_mult_iff [of "a" b]) 
1236 
apply force 

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

1238 

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

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

35216  1242 
apply force 
25917  1243 
done 
1244 

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

1247 

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

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

1250 

1251 
lemma mult_less_cancel_right_disj: 

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

1253 
apply (cases "c = 0") 

1254 
apply (auto simp add: neq_iff mult_strict_right_mono 

1255 
mult_strict_right_mono_neg) 

1256 
apply (auto simp add: not_less 

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

1258 
not_le [symmetric, of a]) 

1259 
apply (erule_tac [!] notE) 

1260 
apply (auto simp add: less_imp_le mult_right_mono 

1261 
mult_right_mono_neg) 

1262 
done 

1263 

1264 
lemma mult_less_cancel_left_disj: 

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

1266 
apply (cases "c = 0") 

1267 
apply (auto simp add: neq_iff mult_strict_left_mono 

1268 
mult_strict_left_mono_neg) 
