author  haftmann 
Tue, 22 May 2018 18:14:29 +0000  
changeset 68252  8b284d24f434 
parent 68251  54a127873735 
child 68253  a8660a39e304 
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 

60758  10 
section \<open>Rings\<close> 
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 
63588  13 
imports Groups Set 
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 

63325  21 
text \<open>For the \<open>combine_numerals\<close> simproc\<close> 
22 
lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c" 

23 
by (simp add: distrib_right ac_simps) 

25152  24 

25 
end 

14504  26 

22390  27 
class mult_zero = times + zero + 
25062  28 
assumes mult_zero_left [simp]: "0 * a = 0" 
29 
assumes mult_zero_right [simp]: "a * 0 = 0" 

58195  30 
begin 
31 

63325  32 
lemma mult_not_zero: "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0" 
58195  33 
by auto 
34 

35 
end 

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

36 

58198  37 
class semiring_0 = semiring + comm_monoid_add + mult_zero 
38 

29904  39 
class semiring_0_cancel = semiring + cancel_comm_monoid_add 
25186  40 
begin 
14504  41 

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

44 
fix a :: 'a 
63588  45 
have "0 * a + 0 * a = 0 * a + 0" 
46 
by (simp add: distrib_right [symmetric]) 

47 
then show "0 * a = 0" 

48 
by (simp only: add_left_cancel) 

49 
have "a * 0 + a * 0 = a * 0 + 0" 

50 
by (simp add: distrib_left [symmetric]) 

51 
then show "a * 0 = 0" 

52 
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 
63588  64 
show "(a + b) * c = a * c + b * c" 
65 
by (simp add: distrib) 

66 
have "a * (b + c) = (b + c) * a" 

67 
by (simp add: ac_simps) 

68 
also have "\<dots> = b * a + c * a" 

69 
by (simp only: distrib) 

70 
also have "\<dots> = a * b + a * c" 

71 
by (simp add: ac_simps) 

72 
finally show "a * (b + c) = a * b + a * c" 

73 
by blast 

14504  74 
qed 
75 

25152  76 
end 
14504  77 

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

80 

27516  81 
subclass semiring_0 .. 
25152  82 

83 
end 

14504  84 

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

27516  88 
subclass semiring_0_cancel .. 
14940  89 

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

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

91 

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

93 

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

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

63325  99 
by (rule not_sym) (rule zero_neq_one) 
26193  100 

54225  101 
definition of_bool :: "bool \<Rightarrow> 'a" 
63325  102 
where "of_bool p = (if p then 1 else 0)" 
54225  103 

104 
lemma of_bool_eq [simp, code]: 

105 
"of_bool False = 0" 

106 
"of_bool True = 1" 

107 
by (simp_all add: of_bool_def) 

108 

63325  109 
lemma of_bool_eq_iff: "of_bool p = of_bool q \<longleftrightarrow> p = q" 
54225  110 
by (simp add: of_bool_def) 
111 

63325  112 
lemma split_of_bool [split]: "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)" 
55187  113 
by (cases p) simp_all 
114 

63325  115 
lemma split_of_bool_asm: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)" 
55187  116 
by (cases p) simp_all 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

117 

24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

119 

22390  120 
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66810
diff
changeset

121 
begin 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66810
diff
changeset

122 

212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66810
diff
changeset

123 
lemma (in semiring_1) of_bool_conj: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66810
diff
changeset

124 
"of_bool (P \<and> Q) = of_bool P * of_bool Q" 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66810
diff
changeset

125 
by auto 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66810
diff
changeset

126 

212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66810
diff
changeset

127 
end 
14504  128 

60758  129 
text \<open>Abstract divisibility\<close> 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

130 

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

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

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

133 

63325  134 
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) 
135 
where "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

136 

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

137 
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

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

139 

68251  140 
lemma dvdE [elim]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

142 

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

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

144 

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

145 
context comm_monoid_mult 
25152  146 
begin 
14738  147 

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

148 
subclass dvd . 
25152  149 

63325  150 
lemma dvd_refl [simp]: "a dvd a" 
28559  151 
proof 
152 
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

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

154 

62349
7c23469b5118
cleansed junkproducing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62347
diff
changeset

155 
lemma dvd_trans [trans]: 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

156 
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

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

158 
proof  
63588  159 
from assms obtain v where "b = a * v" 
160 
by (auto elim!: dvdE) 

161 
moreover from assms obtain w where "c = b * w" 

162 
by (auto elim!: dvdE) 

163 
ultimately have "c = a * (v * w)" 

164 
by (simp add: mult.assoc) 

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

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

167 

63325  168 
lemma subset_divisors_dvd: "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b" 
62366  169 
by (auto simp add: subset_iff intro: dvd_trans) 
170 

63325  171 
lemma strict_subset_divisors_dvd: "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a" 
62366  172 
by (auto simp add: subset_iff intro: dvd_trans) 
173 

63325  174 
lemma one_dvd [simp]: "1 dvd a" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

175 
by (auto intro!: dvdI) 
28559  176 

63325  177 
lemma dvd_mult [simp]: "a dvd c \<Longrightarrow> a dvd (b * c)" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

178 
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

179 

63325  180 
lemma dvd_mult2 [simp]: "a dvd b \<Longrightarrow> a dvd (b * c)" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

181 
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

182 

63325  183 
lemma dvd_triv_right [simp]: "a dvd b * a" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

184 
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

185 

63325  186 
lemma dvd_triv_left [simp]: "a dvd a * b" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

187 
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

188 

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

189 
lemma mult_dvd_mono: 
30042  190 
assumes "a dvd b" 
191 
and "c dvd d" 

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

192 
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

193 
proof  
60758  194 
from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 
195 
moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" .. 

63588  196 
ultimately have "b * d = (a * c) * (b' * d')" 
197 
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

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

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

200 

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

202 
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

203 

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

205 
using dvd_mult_left [of b a c] by (simp add: ac_simps) 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

206 

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

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

208 

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

209 
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

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

211 

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

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

213 

63325  214 
lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

215 
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

216 

63325  217 
lemma dvd_0_right [iff]: "a dvd 0" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
59000
diff
changeset

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

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

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

221 

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

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

224 

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

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

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

227 
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

228 
proof  
60758  229 
from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 
230 
moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" .. 

63588  231 
ultimately have "b + c = a * (b' + c')" 
232 
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

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

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

235 

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

237 

29904  238 
class semiring_1_cancel = semiring + cancel_comm_monoid_add 
239 
+ zero_neq_one + monoid_mult 

25267  240 
begin 
14940  241 

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

243 

27516  244 
subclass semiring_1 .. 
25267  245 

246 
end 

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

247 

63325  248 
class comm_semiring_1_cancel = 
249 
comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult + 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

250 
assumes right_diff_distrib' [algebra_simps]: "a * (b  c) = a * b  a * c" 
25267  251 
begin 
14738  252 

27516  253 
subclass semiring_1_cancel .. 
254 
subclass comm_semiring_0_cancel .. 

255 
subclass comm_semiring_1 .. 

25267  256 

63325  257 
lemma left_diff_distrib' [algebra_simps]: "(b  c) * a = b * a  c * a" 
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

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

259 

63325  260 
lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b" 
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

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

262 
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

263 
proof 
63325  264 
assume ?Q 
265 
then show ?P by simp 

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

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

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

268 
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

269 
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

270 
then have "b = a * d  a * c" by simp 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

272 
then show ?Q .. 
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 
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

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

276 

63325  277 
lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \<longleftrightarrow> a dvd b" 
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

278 
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

279 

63325  280 
lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \<longleftrightarrow> a dvd b" 
59816
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 

63325  283 
lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \<longleftrightarrow> a dvd b" 
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

284 
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

285 

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

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

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

288 
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

289 
proof 
63325  290 
assume ?P 
291 
then obtain d where "b + c = a * d" .. 

60758  292 
moreover from \<open>a dvd b\<close> obtain e where "b = a * e" .. 
59816
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 
63325  299 
assume ?Q 
300 
with assms show ?P by simp 

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

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

302 

63325  303 
lemma dvd_add_left_iff: "a dvd c \<Longrightarrow> a dvd b + c \<longleftrightarrow> a dvd b" 
304 
using dvd_add_right_iff [of a c b] by (simp add: ac_simps) 

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

305 

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

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

307 

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

27516  311 
subclass semiring_0_cancel .. 
25152  312 

60758  313 
text \<open>Distribution rules\<close> 
25152  314 

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

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

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

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

63325  321 
text \<open>Extract signs from products\<close> 
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
52435
diff
changeset

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

323 
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

324 

25152  325 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
63325  326 
by simp 
25152  327 

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

63325  329 
by simp 
29667  330 

63325  331 
lemma right_diff_distrib [algebra_simps]: "a * (b  c) = a * b  a * c" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

332 
using distrib_left [of a b "c "] by simp 
29667  333 

63325  334 
lemma left_diff_distrib [algebra_simps]: "(a  b) * c = a * c  b * c" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

335 
using distrib_right [of a " b" c] by simp 
25152  336 

63325  337 
lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  338 

63325  339 
lemma eq_add_iff1: "a * e + c = b * e + d \<longleftrightarrow> (a  b) * e + c = d" 
340 
by (simp add: algebra_simps) 

25230  341 

63325  342 
lemma eq_add_iff2: "a * e + c = b * e + d \<longleftrightarrow> c = (b  a) * e + d" 
343 
by (simp add: algebra_simps) 

25230  344 

25152  345 
end 
346 

63325  347 
lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  348 

22390  349 
class comm_ring = comm_semiring + ab_group_add 
25267  350 
begin 
14738  351 

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

353 
subclass comm_semiring_0_cancel .. 
25267  354 

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

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

357 

25267  358 
end 
14738  359 

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

362 

27516  363 
subclass semiring_1_cancel .. 
25267  364 

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

366 
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

367 

25267  368 
end 
25152  369 

22390  370 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
25267  371 
begin 
14738  372 

27516  373 
subclass ring_1 .. 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

375 
by unfold_locales (simp add: algebra_simps) 
58647  376 

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

377 
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

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

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

380 
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

381 
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

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

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

384 
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

385 
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

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

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

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

392 
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

393 
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

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

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

396 
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

397 
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

398 
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

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

400 

63325  401 
lemma dvd_diff [simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y  z)" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54225
diff
changeset

402 
using dvd_add [of x y " z"] by simp 
29409  403 

25267  404 
end 
25152  405 

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

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

407 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
25230  408 
begin 
409 

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

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

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

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

413 
proof (rule classical) 
63325  414 
assume "\<not> ?thesis" 
59833
ab828c2c5d67
clarified no_zero_devisors: makes only sense in a semiring;
haftmann
parents:
59832
diff
changeset

415 
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

416 
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

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

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

419 

63325  420 
lemma mult_eq_0_iff [simp]: "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 
25230  421 
proof (cases "a = 0 \<or> b = 0") 
63325  422 
case False 
423 
then have "a \<noteq> 0" and "b \<noteq> 0" by auto 

25230  424 
then show ?thesis using no_zero_divisors by simp 
425 
next 

63325  426 
case True 
427 
then show ?thesis by auto 

25230  428 
qed 
429 

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

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

431 

62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

432 
class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

433 

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

434 
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

435 
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

436 
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

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

438 

63325  439 
lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

441 

63325  442 
lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

444 

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

446 

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

447 
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

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

449 

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

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

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

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

453 
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

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

455 
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

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

457 
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

458 
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

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

460 
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

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

462 
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

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

464 

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

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

466 

23544  467 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  468 
begin 
469 

62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

470 
subclass semiring_1_no_zero_divisors .. 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

471 

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

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

474 
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

475 
by (simp add: algebra_simps) 
63325  476 
then have "x * x = 1 \<longleftrightarrow> (x  1) * (x + 1) = 0" 
36821
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

477 
by simp 
63325  478 
then show ?thesis 
36821
9207505d1ee5
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
huffman
parents:
36719
diff
changeset

479 
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

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

481 

63325  482 
lemma mult_cancel_right1 [simp]: "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1" 
483 
using mult_cancel_right [of 1 c b] by auto 

26274  484 

63325  485 
lemma mult_cancel_right2 [simp]: "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1" 
486 
using mult_cancel_right [of a c 1] by simp 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

487 

63325  488 
lemma mult_cancel_left1 [simp]: "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1" 
489 
using mult_cancel_left [of c 1 b] by force 

26274  490 

63325  491 
lemma mult_cancel_left2 [simp]: "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1" 
492 
using mult_cancel_left [of c a 1] by simp 

26274  493 

494 
end 

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

495 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

496 
class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

497 
begin 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

498 

b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

499 
subclass semiring_1_no_zero_divisors .. 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

500 

b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62390
diff
changeset

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

502 

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

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

505 

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

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

507 

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

509 

63325  510 
lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b" 
29981
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

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

512 
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

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

514 
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

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

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

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

518 

63325  519 
lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b" 
29981
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

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

521 
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

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

523 
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

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

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

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

527 

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

528 
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

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

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

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

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

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

534 
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

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

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

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

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

539 

25186  540 
end 
25152  541 

64290  542 
class idom_abs_sgn = idom + abs + sgn + 
543 
assumes sgn_mult_abs: "sgn a * \<bar>a\<bar> = a" 

544 
and sgn_sgn [simp]: "sgn (sgn a) = sgn a" 

545 
and abs_abs [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" 

546 
and abs_0 [simp]: "\<bar>0\<bar> = 0" 

547 
and sgn_0 [simp]: "sgn 0 = 0" 

548 
and sgn_1 [simp]: "sgn 1 = 1" 

549 
and sgn_minus_1: "sgn ( 1) =  1" 

550 
and sgn_mult: "sgn (a * b) = sgn a * sgn b" 

551 
begin 

552 

553 
lemma sgn_eq_0_iff: 

554 
"sgn a = 0 \<longleftrightarrow> a = 0" 

555 
proof  

556 
{ assume "sgn a = 0" 

557 
then have "sgn a * \<bar>a\<bar> = 0" 

558 
by simp 

559 
then have "a = 0" 

560 
by (simp add: sgn_mult_abs) 

561 
} then show ?thesis 

562 
by auto 

563 
qed 

564 

565 
lemma abs_eq_0_iff: 

566 
"\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" 

567 
proof  

568 
{ assume "\<bar>a\<bar> = 0" 

569 
then have "sgn a * \<bar>a\<bar> = 0" 

570 
by simp 

571 
then have "a = 0" 

572 
by (simp add: sgn_mult_abs) 

573 
} then show ?thesis 

574 
by auto 

575 
qed 

576 

577 
lemma abs_mult_sgn: 

578 
"\<bar>a\<bar> * sgn a = a" 

579 
using sgn_mult_abs [of a] by (simp add: ac_simps) 

580 

581 
lemma abs_1 [simp]: 

582 
"\<bar>1\<bar> = 1" 

583 
using sgn_mult_abs [of 1] by simp 

584 

585 
lemma sgn_abs [simp]: 

586 
"\<bar>sgn a\<bar> = of_bool (a \<noteq> 0)" 

587 
using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\<bar>sgn a\<bar>" 1] 

588 
by (auto simp add: sgn_eq_0_iff) 

589 

590 
lemma abs_sgn [simp]: 

591 
"sgn \<bar>a\<bar> = of_bool (a \<noteq> 0)" 

592 
using sgn_mult_abs [of "\<bar>a\<bar>"] mult_cancel_right [of "sgn \<bar>a\<bar>" "\<bar>a\<bar>" 1] 

593 
by (auto simp add: abs_eq_0_iff) 

594 

595 
lemma abs_mult: 

596 
"\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 

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

598 
case True 

599 
then show ?thesis 

600 
by auto 

601 
next 

602 
case False 

603 
then have *: "sgn (a * b) \<noteq> 0" 

604 
by (simp add: sgn_eq_0_iff) 

605 
from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b] 

606 
have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * sgn a * \<bar>b\<bar> * sgn b" 

607 
by (simp add: ac_simps) 

608 
then have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * \<bar>b\<bar> * sgn (a * b)" 

609 
by (simp add: sgn_mult ac_simps) 

610 
with * show ?thesis 

611 
by simp 

612 
qed 

613 

614 
lemma sgn_minus [simp]: 

615 
"sgn ( a) =  sgn a" 

616 
proof  

617 
from sgn_minus_1 have "sgn ( 1 * a) =  1 * sgn a" 

618 
by (simp only: sgn_mult) 

619 
then show ?thesis 

620 
by simp 

621 
qed 

622 

623 
lemma abs_minus [simp]: 

624 
"\<bar> a\<bar> = \<bar>a\<bar>" 

625 
proof  

626 
have [simp]: "\<bar> 1\<bar> = 1" 

627 
using sgn_mult_abs [of " 1"] by simp 

628 
then have "\<bar> 1 * a\<bar> = 1 * \<bar>a\<bar>" 

629 
by (simp only: abs_mult) 

630 
then show ?thesis 

631 
by simp 

632 
qed 

633 

634 
end 

635 

60758  636 
text \<open> 
35302  637 
The theory of partially ordered rings is taken from the books: 
63325  638 
\<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979 
639 
\<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963 

640 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

641 
Most of the used notions can also be looked up in 
63680  642 
\<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al. 
63325  643 
\<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer 
60758  644 
\<close> 
35302  645 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

646 
text \<open>Syntactic division operator\<close> 
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

647 

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

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

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

650 

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

652 

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

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

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

655 

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

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

657 
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

658 
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

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

660 

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

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

662 

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

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

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

665 

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

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

667 
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

668 
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

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

670 

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

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

672 

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

674 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

675 
text \<open>Algebraic classes with division\<close> 
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63947
diff
changeset

676 

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

677 
class semidom_divide = semidom + divide + 
64240  678 
assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a" 
679 
assumes div_by_0 [simp]: "a div 0 = 0" 

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

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

681 

64240  682 
lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b" 
683 
using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps) 

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

684 

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

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

686 
proof 
63325  687 
show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c 
688 
proof (cases "c = 0") 

689 
case True 

690 
then show ?thesis by simp 

691 
next 

692 
case False 

63588  693 
have "a = b" if "a * c = b * c" 
694 
proof  

695 
from that have "a * c div c = b * c div c" 

63325  696 
by simp 
63588  697 
with False show ?thesis 
63325  698 
by simp 
63588  699 
qed 
63325  700 
then show ?thesis by auto 
701 
qed 

702 
show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" for a b c 

703 
using * [of a c b] by (simp add: ac_simps) 

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

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

705 

63325  706 
lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1" 
64240  707 
using nonzero_mult_div_cancel_left [of a 1] by simp 
60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60429
diff
changeset

708 

64240  709 
lemma div_0 [simp]: "0 div a = 0" 
60570  710 
proof (cases "a = 0") 
63325  711 
case True 
712 
then show ?thesis by simp 

60570  713 
next 
63325  714 
case False 
715 
then have "a * 0 div a = 0" 

64240  716 
by (rule nonzero_mult_div_cancel_left) 
60570  717 
then show ?thesis by simp 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62366
diff
changeset

718 
qed 
60570  719 

64240  720 
lemma div_by_1 [simp]: "a div 1 = a" 
721 
using nonzero_mult_div_cancel_left [of 1 a] by simp 

60690  722 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

723 
lemma dvd_div_eq_0_iff: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

724 
assumes "b dvd a" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

725 
shows "a div b = 0 \<longleftrightarrow> a = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

726 
using assms by (elim dvdE, cases "b = 0") simp_all 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

727 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

728 
lemma dvd_div_eq_cancel: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

729 
"a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

730 
by (elim dvdE, cases "c = 0") simp_all 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

731 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

732 
lemma dvd_div_eq_iff: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

733 
"c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

734 
by (elim dvdE, cases "c = 0") simp_all 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

735 

60867  736 
end 
737 

738 
class idom_divide = idom + semidom_divide 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

739 
begin 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

740 

64592
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

741 
lemma dvd_neg_div: 
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

742 
assumes "b dvd a" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

743 
shows " a div b =  (a div b)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

744 
proof (cases "b = 0") 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

745 
case True 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

746 
then show ?thesis by simp 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

747 
next 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

748 
case False 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

749 
from assms obtain c where "a = b * c" .. 
64592
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

750 
then have " a div b = (b *  c) div b" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

751 
by simp 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

752 
from False also have "\<dots> =  c" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

753 
by (rule nonzero_mult_div_cancel_left) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

754 
with False \<open>a = b * c\<close> show ?thesis 
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

755 
by simp 
64592
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

756 
qed 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

757 

7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

758 
lemma dvd_div_neg: 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

759 
assumes "b dvd a" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

760 
shows "a div  b =  (a div b)" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

761 
proof (cases "b = 0") 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

762 
case True 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

763 
then show ?thesis by simp 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

764 
next 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

765 
case False 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

766 
then have " b \<noteq> 0" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

767 
by simp 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

768 
from assms obtain c where "a = b * c" .. 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

769 
then have "a div  b = ( b *  c) div  b" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

770 
by simp 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

771 
from \<open> b \<noteq> 0\<close> also have "\<dots> =  c" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

772 
by (rule nonzero_mult_div_cancel_left) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

773 
with False \<open>a = b * c\<close> show ?thesis 
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

774 
by simp 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

775 
qed 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

776 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

777 
end 
60867  778 

779 
class algebraic_semidom = semidom_divide 

780 
begin 

781 

782 
text \<open> 

783 
Class @{class algebraic_semidom} enriches a integral domain 

784 
by notions from algebra, like units in a ring. 

785 
It is a separate class to avoid spoiling fields with notions 

786 
which are degenerated there. 

787 
\<close> 

788 

60690  789 
lemma dvd_times_left_cancel_iff [simp]: 
790 
assumes "a \<noteq> 0" 

63588  791 
shows "a * b dvd a * c \<longleftrightarrow> b dvd c" 
792 
(is "?lhs \<longleftrightarrow> ?rhs") 

60690  793 
proof 
63588  794 
assume ?lhs 
63325  795 
then obtain d where "a * c = a * b * d" .. 
60690  796 
with assms have "c = b * d" by (simp add: ac_simps) 
63588  797 
then show ?rhs .. 
60690  798 
next 
63588  799 
assume ?rhs 
63325  800 
then obtain d where "c = b * d" .. 
60690  801 
then have "a * c = a * b * d" by (simp add: ac_simps) 
63588  802 
then show ?lhs .. 
60690  803 
qed 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62366
diff
changeset

804 

60690  805 
lemma dvd_times_right_cancel_iff [simp]: 
806 
assumes "a \<noteq> 0" 

63588  807 
shows "b * a dvd c * a \<longleftrightarrow> b dvd c" 
63325  808 
using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps) 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62366
diff
changeset

809 

60690  810 
lemma div_dvd_iff_mult: 
811 
assumes "b \<noteq> 0" and "b dvd a" 

812 
shows "a div b dvd c \<longleftrightarrow> a dvd c * b" 

813 
proof  

814 
from \<open>b dvd a\<close> obtain d where "a = b * d" .. 

815 
with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps) 

816 
qed 

817 

818 
lemma dvd_div_iff_mult: 

819 
assumes "c \<noteq> 0" and "c dvd b" 

820 
shows "a dvd b div c \<longleftrightarrow> a * c dvd b" 

821 
proof  

822 
from \<open>c dvd b\<close> obtain d where "b = c * d" .. 

823 
with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a]) 

824 
qed 

825 

60867  826 
lemma div_dvd_div [simp]: 
827 
assumes "a dvd b" and "a dvd c" 

828 
shows "b div a dvd c div a \<longleftrightarrow> b dvd c" 

829 
proof (cases "a = 0") 

63325  830 
case True 
831 
with assms show ?thesis by simp 

60867  832 
next 
833 
case False 

834 
moreover from assms obtain k l where "b = a * k" and "c = a * l" 

835 
by (auto elim!: dvdE) 

836 
ultimately show ?thesis by simp 

837 
qed 

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

838 

60867  839 
lemma div_add [simp]: 
840 
assumes "c dvd a" and "c dvd b" 

841 
shows "(a + b) div c = a div c + b div c" 

842 
proof (cases "c = 0") 

63325  843 
case True 
844 
then show ?thesis by simp 

60867  845 
next 
846 
case False 

847 
moreover from assms obtain k l where "a = c * k" and "b = c * l" 

848 
by (auto elim!: dvdE) 

849 
moreover have "c * k + c * l = c * (k + l)" 

850 
by (simp add: algebra_simps) 

851 
ultimately show ?thesis 

852 
by simp 

853 
qed 

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

854 

60867  855 
lemma div_mult_div_if_dvd: 
856 
assumes "b dvd a" and "d dvd c" 

857 
shows "(a div b) * (c div d) = (a * c) div (b * d)" 

858 
proof (cases "b = 0 \<or> c = 0") 

63325  859 
case True 
860 
with assms show ?thesis by auto 

60867  861 
next 
862 
case False 

863 
moreover from assms obtain k l where "a = b * k" and "c = d * l" 

864 
by (auto elim!: dvdE) 

865 
moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)" 

866 
by (simp add: ac_simps) 

867 
ultimately show ?thesis by simp 

868 
qed 

869 

870 
lemma dvd_div_eq_mult: 

871 
assumes "a \<noteq> 0" and "a dvd b" 

872 
shows "b div a = c \<longleftrightarrow> b = c * a" 

63588  873 
(is "?lhs \<longleftrightarrow> ?rhs") 
60867  874 
proof 
63588  875 
assume ?rhs 
876 
then show ?lhs by (simp add: assms) 

60867  877 
next 
63588  878 
assume ?lhs 
60867  879 
then have "b div a * a = c * a" by simp 
63325  880 
moreover from assms have "b div a * a = b" 
60867  881 
by (auto elim!: dvdE simp add: ac_simps) 
63588  882 
ultimately show ?rhs by simp 
60867  883 
qed 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

884 

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

886 
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

887 

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

889 
using dvd_div_mult_self [of a b] by (simp add: ac_simps) 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

890 

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

891 
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

892 
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

893 
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

894 
proof (cases "c = 0") 
63325  895 
case True 
896 
then show ?thesis by simp 

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

897 
next 
63325  898 
case False 
899 
from assms obtain d where "b = c * d" .. 

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

900 
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

901 
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

902 
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

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

904 

63325  905 
lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c" 
906 
using div_mult_swap [of c b a] by (simp add: ac_simps) 

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

907 

60570  908 
lemma dvd_div_mult2_eq: 
909 
assumes "b * c dvd a" 

910 
shows "a div (b * c) = a div b div c" 

63325  911 
proof  
912 
from assms obtain k where "a = b * c * k" .. 

60570  913 
then show ?thesis 
914 
by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps) 

915 
qed 

916 

60867  917 
lemma dvd_div_div_eq_mult: 
918 
assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d" 

63588  919 
shows "b div a = d div c \<longleftrightarrow> b * c = a * d" 
920 
(is "?lhs \<longleftrightarrow> ?rhs") 

60867  921 
proof  
922 
from assms have "a * c \<noteq> 0" by simp 

63588  923 
then have "?lhs \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)" 
60867  924 
by simp 
925 
also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a" 

926 
by (simp add: ac_simps) 

927 
also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a" 

928 
using assms by (simp add: div_mult_swap) 

63588  929 
also have "\<dots> \<longleftrightarrow> ?rhs" 
60867  930 
using assms by (simp add: ac_simps) 
931 
finally show ?thesis . 

932 
qed 

933 

63359  934 
lemma dvd_mult_imp_div: 
935 
assumes "a * c dvd b" 

936 
shows "a dvd b div c" 

937 
proof (cases "c = 0") 

938 
case True then show ?thesis by simp 

939 
next 

940 
case False 

941 
from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" .. 

63588  942 
with False show ?thesis 
943 
by (simp add: mult.commute [of a] mult.assoc) 

63359  944 
qed 
945 

64592
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

946 
lemma div_div_eq_right: 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

947 
assumes "c dvd b" "b dvd a" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

948 
shows "a div (b div c) = a div b * c" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

949 
proof (cases "c = 0 \<or> b = 0") 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

950 
case True 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

951 
then show ?thesis 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

952 
by auto 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

953 
next 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

954 
case False 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

955 
from assms obtain r s where "b = c * r" and "a = c * r * s" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

956 
by (blast elim: dvdE) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

957 
moreover with False have "r \<noteq> 0" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

958 
by auto 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

959 
ultimately show ?thesis using False 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

960 
by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c]) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

961 
qed 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

962 

7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

963 
lemma div_div_div_same: 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

964 
assumes "d dvd b" "b dvd a" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

965 
shows "(a div d) div (b div d) = a div b" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

966 
proof (cases "b = 0 \<or> d = 0") 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

967 
case True 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

968 
with assms show ?thesis 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

969 
by auto 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

970 
next 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

971 
case False 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

972 
from assms obtain r s 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

973 
where "a = d * r * s" and "b = d * r" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

974 
by (blast elim: dvdE) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

975 
with False show ?thesis 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

976 
by simp (simp add: ac_simps) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

977 
qed 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64591
diff
changeset

978 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

979 

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

980 
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

981 

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

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

984 

63325  985 
lemma not_is_unit_0 [simp]: "\<not> is_unit 0" 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

986 
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

987 

63325  988 
lemma unit_imp_dvd [dest]: "is_unit b \<Longrightarrow> b dvd a" 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

989 
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

990 

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

991 
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

992 
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

993 
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

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

995 
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

996 
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

997 
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

998 
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

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

1000 

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

1002 
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

1003 

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

1004 
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

1005 
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

1006 
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

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

1008 
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

1009 
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

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

1011 

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

1012 
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

1013 
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

1014 
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

1015 
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

1016 
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

1017 
proof (rule that) 
63040  1018 
define b where "b = 1 div a" 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

1019 
then show "1 div a = b" by simp 
63325  1020 
from assms b_def show "is_unit b" by simp 
1021 
with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto 

1022 
from assms b_def show "a * b = 1" by simp 

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

1023 
then have "1 = a * b" .. 
60758  1024 
with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp 
63325  1025 
from assms have "a dvd c" .. 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

1026 
then obtain d where "c = a * d" .. 
60758  1027 
with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b" 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

1028 
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

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

1030 

63325  1031 
lemma unit_prod [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

1032 
by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

1033 

63325  1034 
lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" 
62366  1035 
by (auto dest: dvd_mult_left dvd_mult_right) 
1036 

63325  1037 
lemma unit_div [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)" 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

1038 
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

1039 

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

1040 
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

1041 
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

1042 
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

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

1044 
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

1045 
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

1046 
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

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

1048 
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

1049 
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

1050 
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

1051 
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

1052 
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

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

1054 

63924  1055 
lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c" 
1056 
using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps) 

1057 

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

1058 
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

1059 
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

1060 
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

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

1062 
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

1063 
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

1064 
by (subst mult_assoc [symmetric]) simp 
63325  1065 
also from assms have "b * (1 div b) = 1" 
1066 
by (rule is_unitE) simp 

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

1067 
finally have "c * b dvd c" by simp 
60758  1068 
with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans) 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

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

1070 
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

1071 
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

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

1073 

63924  1074 
lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c" 
1075 
using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps) 

1076 

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

1078 
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

1079 

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

1081 
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

1082 

63924  1083 
lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff' 
1084 
dvd_mult_unit_iff dvd_mult_unit_iff' 

1085 
div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *) 

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

1086 

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

1088 
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

1089 

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

1091 
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

1092 

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

1094 
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

1095 

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

1097 
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

1098 

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

1100 
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

1101 

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

1103 
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

1104 

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

1106 
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

1107 

63325  1108 
lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c" 
1109 
using mult_cancel_left [of a b c] by auto 

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

1110 

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

1112 
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

1113 

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

1114 
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

1115 
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

1116 
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

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

1118 
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

1119 
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

1120 
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

1121 
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

1122 
qed 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

1123 

60570  1124 
lemma is_unit_div_mult2_eq: 
1125 
assumes "is_unit b" and "is_unit c" 

1126 
shows "a div (b * c) = a div b div c" 

1127 
proof  

63325  1128 
from assms have "is_unit (b * c)" 
1129 
by (simp add: unit_prod) 

60570  1130 
then have "b * c dvd a" 
1131 
by (rule unit_imp_dvd) 

1132 
then show ?thesis 

1133 
by (rule dvd_div_mult2_eq) 

1134 
qed 

1135 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

1137 
dvd_div_unit_iff unit_div_mult_swap unit_div_commute 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60529
diff
changeset

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

1139 
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

1140 

64240  1141 
lemma is_unit_div_mult_cancel_left: 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1142 
assumes "a \<noteq> 0" and "is_unit b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1143 
shows "a div (a * b) = 1 div b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1144 
proof  
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1145 
from assms have "a div (a * b) = a div a div b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1146 
by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1147 
with assms show ?thesis by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1148 
qed 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1149 

64240  1150 
lemma is_unit_div_mult_cancel_right: 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1151 
assumes "a \<noteq> 0" and "is_unit b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1152 
shows "a div (b * a) = 1 div b" 
64240  1153 
using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps) 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1154 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1155 
lemma unit_div_eq_0_iff: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1156 
assumes "is_unit b" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1157 
shows "a div b = 0 \<longleftrightarrow> a = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1158 
by (rule dvd_div_eq_0_iff) (insert assms, auto) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1159 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1160 
lemma div_mult_unit2: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1161 
"is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1162 
by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64290
diff
changeset

1163 

67051  1164 

1165 
text \<open>Coprimality\<close> 

1166 

1167 
definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

1168 
where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)" 

1169 

1170 
lemma coprimeI: 

1171 
assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c" 

1172 
shows "coprime a b" 

1173 
using assms by (auto simp: coprime_def) 

1174 

1175 
lemma not_coprimeI: 

1176 
assumes "c dvd a" and "c dvd b" and "\<not> is_unit c" 

1177 
shows "\<not> coprime a b" 

1178 
using assms by (auto simp: coprime_def) 

1179 

1180 
lemma coprime_common_divisor: 

1181 
"is_unit c" if "coprime a b" and "c dvd a" and "c dvd b" 

1182 
using that by (auto simp: coprime_def) 

1183 

1184 
lemma not_coprimeE: 

1185 
assumes "\<not> coprime a b" 

1186 
obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c" 

1187 
using assms by (auto simp: coprime_def) 

1188 

1189 
lemma coprime_imp_coprime: 

1190 
"coprime a b" if "coprime c d" 

1191 
and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c" 

1192 
and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d" 

1193 
proof (rule coprimeI) 

1194 
fix e 

1195 
assume "e dvd a" and "e dvd b" 

1196 
with that have "e dvd c" and "e dvd d" 

1197 
by (auto intro: dvd_trans) 

1198 
with \<open>coprime c d\<close> show "is_unit e" 

1199 
by (rule coprime_common_divisor) 

1200 
qed 

1201 

1202 
lemma coprime_divisors: 

1203 
"coprime a b" if "a dvd c" "b dvd d" and "coprime c d" 

1204 
using \<open>coprime c d\<close> proof (rule coprime_imp_coprime) 

1205 
fix e 

1206 
assume "e dvd a" then show "e dvd c" 

1207 
using \<open>a dvd c\<close> by (rule dvd_trans) 

1208 
assume "e dvd b" then show "e dvd d" 

1209 
using \<open>b dvd d\<close> by (rule dvd_trans) 

1210 
qed 

1211 

1212 
lemma coprime_self [simp]: 

1213 
"coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q") 

1214 
proof 

1215 
assume ?P 

1216 
then show ?Q 

1217 
by (rule coprime_common_divisor) simp_all 

1218 
next 

1219 
assume ?Q 

1220 
show ?P 

1221 
by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>) 

1222 
qed 

1223 

1224 
lemma coprime_commute [ac_simps]: 

1225 
"coprime b a \<longleftrightarrow> coprime a b" 

1226 
unfolding coprime_def by auto 

1227 

1228 
lemma is_unit_left_imp_coprime: 

1229 
"coprime a b" if "is_unit a" 

1230 
proof (rule coprimeI) 

1231 
fix c 

1232 
assume "c dvd a" 

1233 
with that show "is_unit c" 

1234 
by (auto intro: dvd_unit_imp_unit) 

1235 
qed 

1236 

1237 
lemma is_unit_right_imp_coprime: 

1238 
"coprime a b" if "is_unit b" 

1239 
using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps) 

1240 

1241 
lemma coprime_1_left [simp]: 

1242 
"coprime 1 a" 

1243 
by (rule coprimeI) 

1244 

1245 
lemma coprime_1_right [simp]: 

1246 
"coprime a 1" 

1247 
by (rule coprimeI) 

1248 

1249 
lemma coprime_0_left_iff [simp]: 

1250 
"coprime 0 a \<longleftrightarrow> is_unit a" 

1251 
by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a]) 

1252 

1253 
lemma coprime_0_right_iff [simp]: 

1254 
"coprime a 0 \<longleftrightarrow> is_unit a" 

1255 
using coprime_0_left_iff [of a] by (simp add: ac_simps) 

1256 

1257 
lemma coprime_mult_self_left_iff [simp]: 

1258 
"coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b" 

1259 
by (auto intro: coprime_common_divisor) 

1260 
(rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+ 

1261 

1262 
lemma coprime_mult_self_right_iff [simp]: 

1263 
"coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b" 

1264 
using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps) 

1265 

67234
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1266 
lemma coprime_absorb_left: 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1267 
assumes "x dvd y" 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1268 
shows "coprime x y \<longleftrightarrow> is_unit x" 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1269 
using assms coprime_common_divisor is_unit_left_imp_coprime by auto 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1270 

ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1271 
lemma coprime_absorb_right: 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1272 
assumes "y dvd x" 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1273 
shows "coprime x y \<longleftrightarrow> is_unit y" 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1274 
using assms coprime_common_divisor is_unit_right_imp_coprime by auto 
ab10ea1d6fd0
Some lemmas on complex numbers and coprimality
eberlm <eberlm@in.tum.de>
parents:
67226
diff
changeset

1275 

60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1276 
end 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1277 

64848
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1278 
class unit_factor = 
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1279 
fixes unit_factor :: "'a \<Rightarrow> 'a" 
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1280 

c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1281 
class semidom_divide_unit_factor = semidom_divide + unit_factor + 
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1282 
assumes unit_factor_0 [simp]: "unit_factor 0 = 0" 
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1283 
and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a" 
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1284 
and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1" 
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1285 
and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" 
67226  1286 
\<comment> \<open>This finegrained hierarchy will later on allow lean normalization of polynomials\<close> 
64848
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1287 

c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64713
diff
changeset

1288 
class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor + 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1289 
fixes normalize :: "'a \<Rightarrow> 'a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1290 
assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" 
63588  1291 
and normalize_0 [simp]: "normalize 0 = 0" 
60685 