author  haftmann 
Sun, 16 Oct 2016 09:31:03 +0200  
changeset 64239  de5cd9217d4c 
parent 64164  38c407446400 
child 64240  eabf80376aab 
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 
14504  121 

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

123 

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

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

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

126 

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

129 

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

130 
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

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

132 

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

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

134 
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

135 

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

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

137 

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

138 
context comm_monoid_mult 
25152  139 
begin 
14738  140 

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

141 
subclass dvd . 
25152  142 

63325  143 
lemma dvd_refl [simp]: "a dvd a" 
28559  144 
proof 
145 
show "a = a * 1" by simp 

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

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

147 

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

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

149 
assumes "a dvd b" and "b dvd c" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

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

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

155 
by (auto elim!: dvdE) 

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

157 
by (simp add: mult.assoc) 

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

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

160 

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

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

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

168 
by (auto intro!: dvdI) 
28559  169 

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

171 
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

172 

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

174 
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

175 

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

177 
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

178 

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

180 
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

181 

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

182 
lemma mult_dvd_mono: 
30042  183 
assumes "a dvd b" 
184 
and "c dvd d" 

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

185 
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

186 
proof  
60758  187 
from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 
188 
moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" .. 

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

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

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

193 

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

195 
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

196 

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

198 
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

199 

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

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

201 

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

202 
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

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

204 

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

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

206 

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

208 
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

209 

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

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

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

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

214 

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

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

217 

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

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

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

220 
shows "a dvd (b + c)" 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

221 
proof  
60758  222 
from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 
223 
moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" .. 

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

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

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

228 

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

230 

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

25267  233 
begin 
14940  234 

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

236 

27516  237 
subclass semiring_1 .. 
25267  238 

239 
end 

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

240 

63325  241 
class comm_semiring_1_cancel = 
242 
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

243 
assumes right_diff_distrib' [algebra_simps]: "a * (b  c) = a * b  a * c" 
25267  244 
begin 
14738  245 

27516  246 
subclass semiring_1_cancel .. 
247 
subclass comm_semiring_0_cancel .. 

248 
subclass comm_semiring_1 .. 

25267  249 

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

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

252 

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

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

255 
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

256 
proof 
63325  257 
assume ?Q 
258 
then show ?P by simp 

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

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

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

261 
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

262 
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

263 
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

264 
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

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

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

267 
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

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

269 

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

271 
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

272 

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

274 
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

275 

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

277 
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

278 

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

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

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

281 
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

282 
proof 
63325  283 
assume ?P 
284 
then obtain d where "b + c = a * d" .. 

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

286 
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

287 
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

288 
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

289 
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

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

291 
next 
63325  292 
assume ?Q 
293 
with assms show ?P by simp 

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

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

295 

63325  296 
lemma dvd_add_left_iff: "a dvd c \<Longrightarrow> a dvd b + c \<longleftrightarrow> a dvd b" 
297 
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

298 

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

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

300 

22390  301 
class ring = semiring + ab_group_add 
25267  302 
begin 
25152  303 

27516  304 
subclass semiring_0_cancel .. 
25152  305 

60758  306 
text \<open>Distribution rules\<close> 
25152  307 

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

63325  309 
by (rule minus_unique) (simp add: distrib_right [symmetric]) 
25152  310 

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

63325  312 
by (rule minus_unique) (simp add: distrib_left [symmetric]) 
25152  313 

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

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

316 
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

317 

25152  318 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
63325  319 
by simp 
25152  320 

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

63325  322 
by simp 
29667  323 

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

325 
using distrib_left [of a b "c "] by simp 
29667  326 

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

328 
using distrib_right [of a " b" c] by simp 
25152  329 

63325  330 
lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  331 

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

25230  334 

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

25230  337 

25152  338 
end 
339 

63325  340 
lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  341 

22390  342 
class comm_ring = comm_semiring + ab_group_add 
25267  343 
begin 
14738  344 

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

346 
subclass comm_semiring_0_cancel .. 
25267  347 

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

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

350 

25267  351 
end 
14738  352 

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

355 

27516  356 
subclass semiring_1_cancel .. 
25267  357 

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

359 
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

360 

25267  361 
end 
25152  362 

22390  363 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
25267  364 
begin 
14738  365 

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

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

368 
by unfold_locales (simp add: algebra_simps) 
58647  369 

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

370 
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

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

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

373 
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

374 
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

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

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

377 
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

378 
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

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

380 

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

381 
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

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

385 
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

386 
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

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

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

389 
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

390 
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

391 
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

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

393 

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

395 
using dvd_add [of x y " z"] by simp 
29409  396 

25267  397 
end 
25152  398 

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

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

400 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
25230  401 
begin 
402 

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

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

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

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

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

408 
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

409 
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

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

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

412 

63325  413 
lemma mult_eq_0_iff [simp]: "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 
25230  414 
proof (cases "a = 0 \<or> b = 0") 
63325  415 
case False 
416 
then have "a \<noteq> 0" and "b \<noteq> 0" by auto 

25230  417 
then show ?thesis using no_zero_divisors by simp 
418 
next 

63325  419 
case True 
420 
then show ?thesis by auto 

25230  421 
qed 
422 

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

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

424 

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

425 
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

426 

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

427 
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

428 
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

429 
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

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

431 

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

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

434 

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

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

437 

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

439 

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

440 
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

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

442 

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

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

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

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

446 
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

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

448 
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

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

450 
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

451 
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

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

453 
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

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

455 
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

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

457 

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

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

459 

23544  460 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  461 
begin 
462 

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

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

464 

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

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

467 
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

468 
by (simp add: algebra_simps) 
63325  469 
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

470 
by simp 
63325  471 
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

472 
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

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

474 

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

26274  477 

63325  478 
lemma mult_cancel_right2 [simp]: "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1" 
479 
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

480 

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

26274  483 

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

26274  486 

487 
end 

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

488 

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

489 
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

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

491 

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

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

493 

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

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

495 

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

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

498 

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

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

500 

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

502 

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

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

505 
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

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

507 
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

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

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

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

511 

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

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

514 
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

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

516 
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

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

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

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

520 

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

521 
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

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

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

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

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

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

527 
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

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

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

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

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

532 

25186  533 
end 
25152  534 

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

539 

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

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

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

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

546 

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

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

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

549 

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

551 

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

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

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

554 

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

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

556 
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

557 
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

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

559 

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

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

561 

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

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

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

564 

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

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

566 
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

567 
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

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

569 

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

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

571 

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

573 

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

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

575 

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

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

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

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

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

580 

63325  581 
lemma nonzero_mult_divide_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b" 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

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

583 

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

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

585 
proof 
63325  586 
show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c 
587 
proof (cases "c = 0") 

588 
case True 

589 
then show ?thesis by simp 

590 
next 

591 
case False 

63588  592 
have "a = b" if "a * c = b * c" 
593 
proof  

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

63325  595 
by simp 
63588  596 
with False show ?thesis 
63325  597 
by simp 
63588  598 
qed 
63325  599 
then show ?thesis by auto 
600 
qed 

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

602 
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

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

604 

63325  605 
lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1" 
606 
using nonzero_mult_divide_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

607 

63325  608 
lemma divide_zero_left [simp]: "0 div a = 0" 
60570  609 
proof (cases "a = 0") 
63325  610 
case True 
611 
then show ?thesis by simp 

60570  612 
next 
63325  613 
case False 
614 
then have "a * 0 div a = 0" 

60570  615 
by (rule nonzero_mult_divide_cancel_left) 
616 
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

617 
qed 
60570  618 

63325  619 
lemma divide_1 [simp]: "a div 1 = a" 
60690  620 
using nonzero_mult_divide_cancel_left [of 1 a] by simp 
621 

60867  622 
end 
623 

624 
class idom_divide = idom + semidom_divide 

625 

626 
class algebraic_semidom = semidom_divide 

627 
begin 

628 

629 
text \<open> 

630 
Class @{class algebraic_semidom} enriches a integral domain 

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

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

633 
which are degenerated there. 

634 
\<close> 

635 

60690  636 
lemma dvd_times_left_cancel_iff [simp]: 
637 
assumes "a \<noteq> 0" 

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

60690  640 
proof 
63588  641 
assume ?lhs 
63325  642 
then obtain d where "a * c = a * b * d" .. 
60690  643 
with assms have "c = b * d" by (simp add: ac_simps) 
63588  644 
then show ?rhs .. 
60690  645 
next 
63588  646 
assume ?rhs 
63325  647 
then obtain d where "c = b * d" .. 
60690  648 
then have "a * c = a * b * d" by (simp add: ac_simps) 
63588  649 
then show ?lhs .. 
60690  650 
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

651 

60690  652 
lemma dvd_times_right_cancel_iff [simp]: 
653 
assumes "a \<noteq> 0" 

63588  654 
shows "b * a dvd c * a \<longleftrightarrow> b dvd c" 
63325  655 
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

656 

60690  657 
lemma div_dvd_iff_mult: 
658 
assumes "b \<noteq> 0" and "b dvd a" 

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

660 
proof  

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

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

663 
qed 

664 

665 
lemma dvd_div_iff_mult: 

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

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

668 
proof  

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

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

671 
qed 

672 

60867  673 
lemma div_dvd_div [simp]: 
674 
assumes "a dvd b" and "a dvd c" 

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

676 
proof (cases "a = 0") 

63325  677 
case True 
678 
with assms show ?thesis by simp 

60867  679 
next 
680 
case False 

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

682 
by (auto elim!: dvdE) 

683 
ultimately show ?thesis by simp 

684 
qed 

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

685 

60867  686 
lemma div_add [simp]: 
687 
assumes "c dvd a" and "c dvd b" 

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

689 
proof (cases "c = 0") 

63325  690 
case True 
691 
then show ?thesis by simp 

60867  692 
next 
693 
case False 

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

695 
by (auto elim!: dvdE) 

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

697 
by (simp add: algebra_simps) 

698 
ultimately show ?thesis 

699 
by simp 

700 
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

701 

60867  702 
lemma div_mult_div_if_dvd: 
703 
assumes "b dvd a" and "d dvd c" 

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

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

63325  706 
case True 
707 
with assms show ?thesis by auto 

60867  708 
next 
709 
case False 

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

711 
by (auto elim!: dvdE) 

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

713 
by (simp add: ac_simps) 

714 
ultimately show ?thesis by simp 

715 
qed 

716 

717 
lemma dvd_div_eq_mult: 

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

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

63588  720 
(is "?lhs \<longleftrightarrow> ?rhs") 
60867  721 
proof 
63588  722 
assume ?rhs 
723 
then show ?lhs by (simp add: assms) 

60867  724 
next 
63588  725 
assume ?lhs 
60867  726 
then have "b div a * a = c * a" by simp 
63325  727 
moreover from assms have "b div a * a = b" 
60867  728 
by (auto elim!: dvdE simp add: ac_simps) 
63588  729 
ultimately show ?rhs by simp 
60867  730 
qed 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

731 

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

733 
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

734 

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

736 
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

737 

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

738 
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

739 
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

740 
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

741 
proof (cases "c = 0") 
63325  742 
case True 
743 
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

744 
next 
63325  745 
case False 
746 
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

747 
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

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

749 
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

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

751 

63325  752 
lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c" 
753 
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

754 

60570  755 
lemma dvd_div_mult2_eq: 
756 
assumes "b * c dvd a" 

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

63325  758 
proof  
759 
from assms obtain k where "a = b * c * k" .. 

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

762 
qed 

763 

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

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

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

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

773 
by (simp add: ac_simps) 

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

775 
using assms by (simp add: div_mult_swap) 

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

779 
qed 

780 

63359  781 
lemma dvd_mult_imp_div: 
782 
assumes "a * c dvd b" 

783 
shows "a dvd b div c" 

784 
proof (cases "c = 0") 

785 
case True then show ?thesis by simp 

786 
next 

787 
case False 

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

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

63359  791 
qed 
792 

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

793 

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

794 
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

795 

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

796 
abbreviation is_unit :: "'a \<Rightarrow> bool" 
63325  797 
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

798 

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

800 
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

801 

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

803 
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

804 

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

805 
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

806 
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

807 
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

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

809 
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

810 
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

811 
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

812 
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

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

814 

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

816 
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

817 

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

818 
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

819 
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

820 
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

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

822 
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

823 
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

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

825 

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

826 
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

827 
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

828 
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

829 
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

830 
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

831 
proof (rule that) 
63040  832 
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

833 
then show "1 div a = b" by simp 
63325  834 
from assms b_def show "is_unit b" by simp 
835 
with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto 

836 
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

837 
then have "1 = a * b" .. 
60758  838 
with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp 
63325  839 
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

840 
then obtain d where "c = a * d" .. 
60758  841 
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

842 
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

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

844 

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

846 
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

847 

63325  848 
lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" 
62366  849 
by (auto dest: dvd_mult_left dvd_mult_right) 
850 

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

852 
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

853 

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

854 
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

855 
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

856 
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

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

858 
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

859 
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

860 
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

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

862 
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

863 
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

864 
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

865 
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

866 
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

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

868 

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

871 

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

872 
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

873 
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

874 
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

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

876 
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

877 
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

878 
by (subst mult_assoc [symmetric]) simp 
63325  879 
also from assms have "b * (1 div b) = 1" 
880 
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

881 
finally have "c * b dvd c" by simp 
60758  882 
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

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

884 
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

885 
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

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

887 

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

890 

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

892 
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

893 

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

895 
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

896 

63924  897 
lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff' 
898 
dvd_mult_unit_iff dvd_mult_unit_iff' 

899 
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

900 

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

902 
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

903 

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

905 
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

906 

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

908 
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

909 

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

911 
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

912 

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

914 
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

915 

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

917 
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

918 

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

920 
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

921 

63325  922 
lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c" 
923 
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

924 

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

926 
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

927 

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

928 
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

929 
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

930 
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

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

932 
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

933 
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

934 
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

935 
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

936 
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

937 

60570  938 
lemma is_unit_div_mult2_eq: 
939 
assumes "is_unit b" and "is_unit c" 

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

941 
proof  

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

60570  944 
then have "b * c dvd a" 
945 
by (rule unit_imp_dvd) 

946 
then show ?thesis 

947 
by (rule dvd_div_mult2_eq) 

948 
qed 

949 

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

950 
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

951 
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

952 
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

953 
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

954 

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

955 
lemma is_unit_divide_mult_cancel_left: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

959 
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

960 
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

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

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

963 

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

964 
lemma is_unit_divide_mult_cancel_right: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

967 
using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

968 

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

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

970 

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

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

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

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

974 
assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" 
63588  975 
and normalize_0 [simp]: "normalize 0 = 0" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

976 
and unit_factor_0 [simp]: "unit_factor 0 = 0" 
63588  977 
and is_unit_normalize: "is_unit a \<Longrightarrow> normalize a = 1" 
978 
and unit_factor_is_unit [iff]: "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)" 

979 
and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" 

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

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

981 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

982 
text \<open> 
63588  983 
Class @{class normalization_semidom} cultivates the idea that each integral 
984 
domain can be split into equivalence classes whose representants are 

985 
associated, i.e. divide each other. @{const normalize} specifies a canonical 

986 
representant for each equivalence class. The rationale behind this is that 

987 
it is easier to reason about equality than equivalences, hence we prefer to 

988 
think about equality of normalized values rather than associated elements. 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

989 
\<close> 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

990 

63325  991 
lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

992 
by (rule unit_imp_dvd) simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

993 

63325  994 
lemma unit_factor_self [simp]: "unit_factor a dvd a" 
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

995 
by (cases "a = 0") simp_all 
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

996 

63325  997 
lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

998 
using unit_factor_mult_normalize [of a] by (simp add: ac_simps) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

999 

63325  1000 
lemma normalize_eq_0_iff [simp]: "normalize a = 0 \<longleftrightarrow> a = 0" 
63588  1001 
(is "?lhs \<longleftrightarrow> ?rhs") 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1002 
proof 
63588  1003 
assume ?lhs 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1004 
moreover have "unit_factor a * normalize a = a" by simp 
63588  1005 
ultimately show ?rhs by simp 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1006 
next 
63588  1007 
assume ?rhs 
1008 
then show ?lhs by simp 

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

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

1010 

63325  1011 
lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \<longleftrightarrow> a = 0" 
63588  1012 
(is "?lhs \<longleftrightarrow> ?rhs") 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1013 
proof 
63588  1014 
assume ?lhs 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1015 
moreover have "unit_factor a * normalize a = a" by simp 
63588  1016 
ultimately show ?rhs by simp 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1017 
next 
63588  1018 
assume ?rhs 
1019 
then show ?lhs by simp 

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

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

1021 

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

1022 
lemma is_unit_unit_factor: 
63325  1023 
assumes "is_unit a" 
1024 
shows "unit_factor a = a" 

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

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

1026 
from assms have "normalize a = 1" by (rule is_unit_normalize) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1027 
moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" . 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1030 

63325  1031 
lemma unit_factor_1 [simp]: "unit_factor 1 = 1" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1032 
by (rule is_unit_unit_factor) simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1033 

63325  1034 
lemma normalize_1 [simp]: "normalize 1 = 1" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1035 
by (rule is_unit_normalize) simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1036 

63325  1037 
lemma normalize_1_iff: "normalize a = 1 \<longleftrightarrow> is_unit a" 
63588  1038 
(is "?lhs \<longleftrightarrow> ?rhs") 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1039 
proof 
63588  1040 
assume ?rhs 
1041 
then show ?lhs by (rule is_unit_normalize) 

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

1042 
next 
63588  1043 
assume ?lhs 
1044 
then have "unit_factor a * normalize a = unit_factor a * 1" 

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

1045 
by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1046 
then have "unit_factor a = a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1047 
by simp 
63588  1048 
moreover 
1049 
from \<open>?lhs\<close> have "a \<noteq> 0" by auto 

1050 
then have "is_unit (unit_factor a)" by simp 

1051 
ultimately show ?rhs by simp 

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

1052 
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

1053 

63325  1054 
lemma div_normalize [simp]: "a div normalize a = unit_factor a" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1055 
proof (cases "a = 0") 
63325  1056 
case True 
1057 
then show ?thesis by simp 

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

1058 
next 
63325  1059 
case False 
1060 
then have "normalize a \<noteq> 0" by simp 

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

1061 
with nonzero_mult_divide_cancel_right 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1062 
have "unit_factor a * normalize a div normalize a = unit_factor a" by blast 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1065 

63325  1066 
lemma div_unit_factor [simp]: "a div unit_factor a = normalize a" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1067 
proof (cases "a = 0") 
63325  1068 
case True 
1069 
then show ?thesis by simp 

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

1070 
next 
63325  1071 
case False 
1072 
then have "unit_factor a \<noteq> 0" by simp 

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

1073 
with nonzero_mult_divide_cancel_left 
63588  1074 
have "unit_factor a * normalize a div unit_factor a = normalize a" 
1075 
by blast 

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

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

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

1078 

63325  1079 
lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1080 
proof (cases "a = 0") 
63325  1081 
case True 
1082 
then show ?thesis by simp 

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

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

1084 
case False 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1085 
have "normalize a div a = normalize a div (unit_factor a * normalize a)" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1086 
by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1087 
also have "\<dots> = 1 div unit_factor a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1088 
using False by (subst is_unit_divide_mult_cancel_right) simp_all 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1089 
finally show ?thesis . 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1091 

63325  1092 
lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1093 
by (cases "b = 0") simp_all 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1094 

63947  1095 
lemma inv_unit_factor_eq_0_iff [simp]: 
1096 
"1 div unit_factor a = 0 \<longleftrightarrow> a = 0" 

1097 
(is "?lhs \<longleftrightarrow> ?rhs") 

1098 
proof 

1099 
assume ?lhs 

1100 
then have "a * (1 div unit_factor a) = a * 0" 

1101 
by simp 

1102 
then show ?rhs 

1103 
by simp 

1104 
next 

1105 
assume ?rhs 

1106 
then show ?lhs by simp 

1107 
qed 

1108 

63325  1109 
lemma normalize_mult: "normalize (a * b) = normalize a * normalize b" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1110 
proof (cases "a = 0 \<or> b = 0") 
63325  1111 
case True 
1112 
then show ?thesis by auto 

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

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

1114 
case False 
63588  1115 
have "unit_factor (a * b) * normalize (a * b) = a * b" 
1116 
by (rule unit_factor_mult_normalize) 

63325  1117 
then have "normalize (a * b) = a * b div unit_factor (a * b)" 
1118 
by simp 

1119 
also have "\<dots> = a * b div unit_factor (b * a)" 

1120 
by (simp add: ac_simps) 

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

1121 
also have "\<dots> = a * b div unit_factor b div unit_factor a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1122 
using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1123 
also have "\<dots> = a * (b div unit_factor b) div unit_factor a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1124 
using False by (subst unit_div_mult_swap) simp_all 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1125 
also have "\<dots> = normalize a * normalize b" 
63325  1126 
using False 
1127 
by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) 

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

1128 
finally show ?thesis . 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1129 
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

1130 

63325  1131 
lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1132 
by (cases "a = 0") (auto intro: is_unit_unit_factor) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1133 

63325  1134 
lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1135 
by (rule is_unit_normalize) 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

1136 

63325  1137 
lemma normalize_idem [simp]: "normalize (normalize a) = normalize a" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1138 
proof (cases "a = 0") 
63325  1139 
case True 
1140 
then show ?thesis by simp 

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

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

1142 
case False 
63325  1143 
have "normalize a = normalize (unit_factor a * normalize a)" 
1144 
by simp 

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

1145 
also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1146 
by (simp only: normalize_mult) 
63325  1147 
finally show ?thesis 
1148 
using False by simp_all 

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

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

1150 

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

1151 
lemma unit_factor_normalize [simp]: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1153 
shows "unit_factor (normalize a) = 1" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1154 
proof  
63325  1155 
from assms have *: "normalize a \<noteq> 0" 
1156 
by simp 

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

1157 
have "unit_factor (normalize a) * normalize (normalize a) = normalize a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1158 
by (simp only: unit_factor_mult_normalize) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1159 
then have "unit_factor (normalize a) * normalize a = normalize a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1160 
by simp 
63325  1161 
with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1162 
by simp 
63325  1163 
with * show ?thesis 
1164 
by simp 

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

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

1166 

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

1167 
lemma dvd_unit_factor_div: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1168 
assumes "b dvd a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

1172 
by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1174 
by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1175 
then show ?thesis 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1176 
by (cases "b = 0") (simp_all add: unit_factor_mult) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1178 

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

1179 
lemma dvd_normalize_div: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1180 
assumes "b dvd a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

1184 
by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1186 
by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1187 
then show ?thesis 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1188 
by (cases "b = 0") (simp_all add: normalize_mult) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1190 

63325  1191 
lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1193 
have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1194 
using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b] 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1195 
by (cases "a = 0") simp_all 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1198 

63325  1199 
lemma dvd_normalize_iff [simp]: "a dvd normalize b \<longleftrightarrow> a dvd b" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1201 
have "a dvd normalize b \<longleftrightarrow> a dvd normalize b * unit_factor b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1202 
using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"] 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1203 
by (cases "b = 0") simp_all 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1206 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1207 
text \<open> 
63588  1208 
We avoid an explicit definition of associated elements but prefer explicit 
1209 
normalisation instead. In theory we could define an abbreviation like @{prop 

1210 
"associated a b \<longleftrightarrow> normalize a = normalize b"} but this is counterproductive 

1211 
without suggestive infix syntax, which we do not want to sacrifice for this 

1212 
purpose here. 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1213 
\<close> 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1214 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1215 
lemma associatedI: 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1216 
assumes "a dvd b" and "b dvd a" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1217 
shows "normalize a = normalize b" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1218 
proof (cases "a = 0 \<or> b = 0") 
63325  1219 
case True 
1220 
with assms show ?thesis by auto 

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

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

1222 
case False 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1223 
from \<open>a dvd b\<close> obtain c where b: "b = a * c" .. 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1224 
moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" .. 
63325  1225 
ultimately have "b * 1 = b * (c * d)" 
1226 
by (simp add: ac_simps) 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1227 
with False have "1 = c * d" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1228 
unfolding mult_cancel_left by simp 
63325  1229 
then have "is_unit c" and "is_unit d" 
1230 
by auto 

1231 
with a b show ?thesis 

1232 
by (simp add: normalize_mult is_unit_normalize) 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1233 
qed 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1234 

63325  1235 
lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1236 
using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric] 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1237 
by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1238 

63325  1239 
lemma associatedD2: "normalize a = normalize b \<Longrightarrow> b dvd a" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1240 
using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric] 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1241 
by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1242 

63325  1243 
lemma associated_unit: "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1244 
using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1245 

63325  1246 
lemma associated_iff_dvd: "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" 
63588  1247 
(is "?lhs \<longleftrightarrow> ?rhs") 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1248 
proof 
63588  1249 
assume ?rhs 
1250 
then show ?lhs by (auto intro!: associatedI) 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1251 
next 
63588  1252 
assume ?lhs 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1253 
then have "unit_factor a * normalize a = unit_factor a * normalize b" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1254 
by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1255 
then have *: "normalize b * unit_factor a = a" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1256 
by (simp add: ac_simps) 
63588  1257 
show ?rhs 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1258 
proof (cases "a = 0 \<or> b = 0") 
63325  1259 
case True 
63588  1260 
with \<open>?lhs\<close> show ?thesis by auto 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1262 
case False 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1263 
then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1264 
by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

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

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

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

1268 

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

1269 
lemma associated_eqI: 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1270 
assumes "a dvd b" and "b dvd a" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1271 
assumes "normalize a = a" and "normalize b = b" 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1272 
shows "a = b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1273 
proof  
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1274 
from assms have "normalize a = normalize b" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1275 
unfolding associated_iff_dvd by simp 
63588  1276 
with \<open>normalize a = a\<close> have "a = normalize b" 
1277 
by simp 

