author  hoelzl 
Wed, 10 Feb 2016 18:43:19 +0100  
changeset 62376  85f38d5f8807 
parent 62366  95c6cf433c91 
child 62377  ace69956d018 
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 
62366  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 

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

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

24 
by (simp add: distrib_right ac_simps) 
25152  25 

26 
end 

14504  27 

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

58195  31 
begin 
32 

33 
lemma mult_not_zero: 

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

35 
by auto 

36 

37 
end 

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

38 

58198  39 
class semiring_0 = semiring + comm_monoid_add + mult_zero 
40 

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

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

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

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

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

51 
have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric]) 
29667  52 
thus "a * 0 = 0" by (simp only: add_left_cancel) 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

53 
qed 
14940  54 

25186  55 
end 
25152  56 

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

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

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

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

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

25152  71 
end 
14504  72 

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

75 

27516  76 
subclass semiring_0 .. 
25152  77 

78 
end 

14504  79 

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

27516  83 
subclass semiring_0_cancel .. 
14940  84 

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

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

86 

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

88 

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

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

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

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

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

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

100 
lemma of_bool_eq [simp, code]: 

101 
"of_bool False = 0" 

102 
"of_bool True = 1" 

103 
by (simp_all add: of_bool_def) 

104 

105 
lemma of_bool_eq_iff: 

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

107 
by (simp add: of_bool_def) 

108 

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

111 
by (cases p) simp_all 

112 

113 
lemma split_of_bool_asm: 

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

115 
by (cases p) simp_all 

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

116 

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 
end 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

118 

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

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

122 

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

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

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

125 

50420  126 
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where 
37767  127 
"b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)" 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

128 

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

129 
lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

131 

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

132 
lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" 
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

133 
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

134 

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

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

136 

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

137 
context comm_monoid_mult 
25152  138 
begin 
14738  139 

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

140 
subclass dvd . 
25152  141 

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

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

143 
"a dvd a" 
28559  144 
proof 
145 
show "a = a * 1" by simp 

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

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

147 

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  
28559  152 
from assms obtain v where "b = a * v" by (auto elim!: dvdE) 
153 
moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE) 

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

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

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

157 

62366  158 
lemma subset_divisors_dvd: 
159 
"{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b" 

160 
by (auto simp add: subset_iff intro: dvd_trans) 

161 

162 
lemma strict_subset_divisors_dvd: 

163 
"{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a" 

164 
by (auto simp add: subset_iff intro: dvd_trans) 

165 

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

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

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

168 
by (auto intro!: dvdI) 
28559  169 

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

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

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

172 
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

173 

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

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

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

176 
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

177 

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

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

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

180 
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

181 

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

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

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

184 
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

185 

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

186 
lemma mult_dvd_mono: 
30042  187 
assumes "a dvd b" 
188 
and "c dvd d" 

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

189 
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

190 
proof  
60758  191 
from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 
192 
moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" .. 

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

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

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

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

196 

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

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

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

199 
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

200 

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

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

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

203 
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

204 

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

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

206 

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

207 
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

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

209 

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

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

211 

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

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

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

214 
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

215 

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

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

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

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

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

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

221 

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

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

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

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

225 

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

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

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

228 
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

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

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

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

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

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

235 

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

237 

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

25267  240 
begin 
14940  241 

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

243 

27516  244 
subclass semiring_1 .. 
25267  245 

246 
end 

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

247 

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

248 
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add + 
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

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

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

27516  253 
subclass semiring_1_cancel .. 
254 
subclass comm_semiring_0_cancel .. 

255 
subclass comm_semiring_1 .. 

25267  256 

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

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

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

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

260 

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

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

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

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

264 
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

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

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

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

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

269 
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

270 
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

271 
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

272 
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

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

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

275 
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

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

277 

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

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

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

280 
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

281 

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

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

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

284 
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

285 

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

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

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

288 
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

289 

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

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

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

292 
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

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

294 
assume ?P then obtain d where "b + c = a * d" .. 
60758  295 
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

296 
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

297 
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

298 
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

299 
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

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

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

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

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

304 

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

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

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

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

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

309 

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

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

311 

22390  312 
class ring = semiring + ab_group_add 
25267  313 
begin 
25152  314 

27516  315 
subclass semiring_0_cancel .. 
25152  316 

60758  317 
text \<open>Distribution rules\<close> 
25152  318 

319 
lemma minus_mult_left: " (a * b) =  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

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

322 
lemma minus_mult_right: " (a * b) = 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

323 
by (rule minus_unique) (simp add: distrib_left [symmetric]) 
25152  324 

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

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

327 
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

328 

25152  329 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  330 
by simp 
25152  331 

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

29667  333 
by simp 
334 

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

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

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

337 
using distrib_left [of a b "c "] by simp 
29667  338 

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

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

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

341 
using distrib_right [of a " b" c] by simp 
25152  342 

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

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

344 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  345 

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

29667  348 
by (simp add: algebra_simps) 
25230  349 

350 
lemma eq_add_iff2: 

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

29667  352 
by (simp add: algebra_simps) 
25230  353 

25152  354 
end 
355 

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

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

357 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  358 

22390  359 
class comm_ring = comm_semiring + ab_group_add 
25267  360 
begin 
14738  361 

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

363 
subclass comm_semiring_0_cancel .. 
25267  364 

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

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

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

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

368 

25267  369 
end 
14738  370 

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

373 

27516  374 
subclass semiring_1_cancel .. 
25267  375 

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

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

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

378 
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

379 

25267  380 
end 
25152  381 

22390  382 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
25267  383 
begin 
14738  384 

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

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

387 
by unfold_locales (simp add: algebra_simps) 
58647  388 

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

389 
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

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

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

392 
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

393 
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

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

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

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

397 
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

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

399 

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

400 
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

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

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

403 
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

404 
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

405 
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

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

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

408 
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

409 
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

410 
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

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

412 

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

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

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

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

25267  417 
end 
25152  418 

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

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

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

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

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

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

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

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

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

428 
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

429 
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

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

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

432 

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

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

437 
then show ?thesis using no_zero_divisors by simp 

438 
next 

439 
case True then show ?thesis by auto 

440 
qed 

441 

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

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

443 

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

444 
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

445 
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

446 
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

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

448 

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

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

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

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

452 

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

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

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

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

456 

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

458 

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

459 
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

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

461 

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

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

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

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

465 
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

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

467 
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

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

469 
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

470 
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

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

472 
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

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

474 
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

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

476 

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

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

478 

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

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

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

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

485 
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

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

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

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

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

490 
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

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

492 

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

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

497 
lemma mult_cancel_right2 [simp]: 

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

29667  499 
by (insert mult_cancel_right [of a c 1], 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

500 

26274  501 
lemma mult_cancel_left1 [simp]: 
502 
"c = c * b \<longleftrightarrow> c = 0 \<or> b = 1" 

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

505 
lemma mult_cancel_left2 [simp]: 

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

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

509 
end 

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

510 

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

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

512 

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

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

515 

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

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

517 

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

519 

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

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

521 
"a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

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

523 
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

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

525 
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

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

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

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

529 

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

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

531 
"c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b" 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29949
diff
changeset

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

533 
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

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

535 
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

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

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

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

539 

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

540 
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

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

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

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

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

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

546 
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

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

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

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

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

551 

25186  552 
end 
25152  553 

60758  554 
text \<open> 
35302  555 
The theory of partially ordered rings is taken from the books: 
556 
\begin{itemize} 

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

557 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
35302  558 
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 
559 
\end{itemize} 

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

560 
Most of the used notions can also be looked up in 
35302  561 
\begin{itemize} 
54703  562 
\item @{url "http://www.mathworld.com"} by Eric Weisstein et. al. 
35302  563 
\item \emph{Algebra I} by van der Waerden, Springer. 
564 
\end{itemize} 

60758  565 
\<close> 
35302  566 

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

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

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

569 

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

571 

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

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

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

574 

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

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

576 
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

577 
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

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

579 

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

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

581 

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

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

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

584 

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

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

586 
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

587 
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

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

589 

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

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

591 

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

593 

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

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

595 
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

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

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

598 

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

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

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

601 
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

602 

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

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

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

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

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

607 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

621 
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

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

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

624 

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

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

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

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

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

629 

60570  630 
lemma divide_zero_left [simp]: 
631 
"0 div a = 0" 

632 
proof (cases "a = 0") 

633 
case True then show ?thesis by simp 

634 
next 

635 
case False then have "a * 0 div a = 0" 

636 
by (rule nonzero_mult_divide_cancel_left) 

637 
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

638 
qed 
60570  639 

60690  640 
lemma divide_1 [simp]: 
641 
"a div 1 = a" 

642 
using nonzero_mult_divide_cancel_left [of 1 a] by simp 

643 

60867  644 
end 
645 

646 
class idom_divide = idom + semidom_divide 

647 

648 
class algebraic_semidom = semidom_divide 

649 
begin 

650 

651 
text \<open> 

652 
Class @{class algebraic_semidom} enriches a integral domain 

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

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

655 
which are degenerated there. 

656 
\<close> 

657 

60690  658 
lemma dvd_times_left_cancel_iff [simp]: 
659 
assumes "a \<noteq> 0" 

660 
shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q") 

661 
proof 

662 
assume ?P then obtain d where "a * c = a * b * d" .. 

663 
with assms have "c = b * d" by (simp add: ac_simps) 

664 
then show ?Q .. 

665 
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

666 
assume ?Q then obtain d where "c = b * d" .. 
60690  667 
then have "a * c = a * b * d" by (simp add: ac_simps) 
668 
then show ?P .. 

669 
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

670 

60690  671 
lemma dvd_times_right_cancel_iff [simp]: 
672 
assumes "a \<noteq> 0" 

673 
shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q") 

674 
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

675 

60690  676 
lemma div_dvd_iff_mult: 
677 
assumes "b \<noteq> 0" and "b dvd a" 

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

679 
proof  

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

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

682 
qed 

683 

684 
lemma dvd_div_iff_mult: 

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

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

687 
proof  

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

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

690 
qed 

691 

60867  692 
lemma div_dvd_div [simp]: 
693 
assumes "a dvd b" and "a dvd c" 

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

695 
proof (cases "a = 0") 

696 
case True with assms show ?thesis by simp 

697 
next 

698 
case False 

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

700 
by (auto elim!: dvdE) 

701 
ultimately show ?thesis by simp 

702 
qed 

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

703 

60867  704 
lemma div_add [simp]: 
705 
assumes "c dvd a" and "c dvd b" 

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

707 
proof (cases "c = 0") 

708 
case True then show ?thesis by simp 

709 
next 

710 
case False 

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

712 
by (auto elim!: dvdE) 

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

714 
by (simp add: algebra_simps) 

715 
ultimately show ?thesis 

716 
by simp 

717 
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

718 

60867  719 
lemma div_mult_div_if_dvd: 
720 
assumes "b dvd a" and "d dvd c" 

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

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

723 
case True with assms show ?thesis by auto 

724 
next 

725 
case False 

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

727 
by (auto elim!: dvdE) 

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

729 
by (simp add: ac_simps) 

730 
ultimately show ?thesis by simp 

731 
qed 

732 

733 
lemma dvd_div_eq_mult: 

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

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

736 
proof 

737 
assume "b = c * a" 

738 
then show "b div a = c" by (simp add: assms) 

739 
next 

740 
assume "b div a = c" 

741 
then have "b div a * a = c * a" by simp 

742 
moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b" 

743 
by (auto elim!: dvdE simp add: ac_simps) 

744 
ultimately show "b = c * a" by simp 

745 
qed 

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

746 

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 
lemma dvd_div_mult_self [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

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

749 
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

750 

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

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

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

753 
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

754 

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

755 
lemma div_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

756 
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

757 
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

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

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

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

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

762 
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

763 
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

764 
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

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

766 

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

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

768 
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

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

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

771 

60570  772 
lemma dvd_div_mult2_eq: 
773 
assumes "b * c dvd a" 

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

775 
using assms proof 

776 
fix k 

777 
assume "a = b * c * k" 

778 
then show ?thesis 

779 
by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps) 

780 
qed 

781 

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

784 
shows "b div a = d div c \<longleftrightarrow> b * c = a * d" (is "?P \<longleftrightarrow> ?Q") 

785 
proof  

786 
from assms have "a * c \<noteq> 0" by simp 

787 
then have "?P \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)" 

788 
by simp 

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

790 
by (simp add: ac_simps) 

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

792 
using assms by (simp add: div_mult_swap) 

793 
also have "\<dots> \<longleftrightarrow> ?Q" 

794 
using assms by (simp add: ac_simps) 

795 
finally show ?thesis . 

796 
qed 

797 

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

798 

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

799 
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

800 

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

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

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

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

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 not_is_unit_0 [simp]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

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

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

808 

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

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

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

811 
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

812 

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

813 
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

814 
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

815 
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

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

817 
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

818 
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

819 
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

820 
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

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

822 

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

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

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

825 
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

826 

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

827 
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

828 
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

829 
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

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

831 
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

832 
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

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

834 

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

835 
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

836 
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

837 
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

838 
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

839 
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

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

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

842 
then show "1 div a = b" by simp 
60758  843 
from b_def \<open>is_unit a\<close> show "is_unit b" by simp 
844 
from \<open>is_unit a\<close> and \<open>is_unit b\<close> show "a \<noteq> 0" and "b \<noteq> 0" by auto 

845 
from b_def \<open>is_unit a\<close> 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

846 
then have "1 = a * b" .. 
60758  847 
with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp 
848 
from \<open>is_unit a\<close> 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

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

851 
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

852 
qed 
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 unit_prod [intro]: 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

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

856 
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

857 

62366  858 
lemma is_unit_mult_iff: 
859 
"is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q") 

860 
by (auto dest: dvd_mult_left dvd_mult_right) 

861 

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

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

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

864 
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

865 

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

866 
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

867 
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

868 
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

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

870 
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

871 
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

872 
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

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

874 
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

875 
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

876 
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

877 
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

878 
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

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

880 

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

881 
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

882 
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

883 
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

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

885 
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

886 
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

887 
by (subst mult_assoc [symmetric]) simp 
60758  888 
also from \<open>is_unit b\<close> have "b * (1 div b) = 1" 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

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

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

892 
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

893 
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

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

895 

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

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

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

898 
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

899 

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

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

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

902 
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

903 

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

904 
lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff 
61799  905 
dvd_mult_unit_iff dvd_div_unit_iff \<comment> \<open>FIXME consider fact collection\<close> 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

906 

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

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

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

909 
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

910 

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

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

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

913 
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

914 

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

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

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

917 
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

918 

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

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

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

921 
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

922 

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

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

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

925 
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

926 

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

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

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

929 
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

930 

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

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

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

933 
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

934 

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

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

936 
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

937 
shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q") 
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

938 
using assms 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

939 

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

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

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

942 
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

943 

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

944 
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

945 
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

946 
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

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

948 
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

949 
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

950 
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

951 
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

952 
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

953 

60570  954 
lemma is_unit_div_mult2_eq: 
955 
assumes "is_unit b" and "is_unit c" 

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

957 
proof  

958 
from assms have "is_unit (b * c)" by (simp add: unit_prod) 

959 
then have "b * c dvd a" 

960 
by (rule unit_imp_dvd) 

961 
then show ?thesis 

962 
by (rule dvd_div_mult2_eq) 

963 
qed 

964 

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

965 
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

966 
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

967 
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

968 
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

969 

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

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

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

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

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

974 
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

975 
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

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

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

978 

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

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

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

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

982 
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

983 

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

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

985 

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

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

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

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

989 
assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

990 
assumes normalize_0 [simp]: "normalize 0 = 0" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

991 
and unit_factor_0 [simp]: "unit_factor 0 = 0" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

993 
"is_unit a \<Longrightarrow> normalize a = 1" 
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

994 
assumes unit_factor_is_unit [iff]: 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

995 
"a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

996 
assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

998 

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

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

1000 
Class @{class normalization_semidom} cultivates the idea that 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1001 
each integral domain can be split into equivalence classes 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1002 
whose representants are associated, i.e. divide each other. 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1003 
@{const normalize} specifies a canonical representant for each equivalence 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1004 
class. The rationale behind this is that it is easier to reason about equality 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1005 
than equivalences, hence we prefer to think about equality of normalized 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1006 
values rather than associated elements. 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

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

1008 

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

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

1010 
"a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1012 

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

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

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

1015 
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

1016 

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

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

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

1019 
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

1020 

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

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

1022 
"normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q") 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1024 
assume ?P 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1025 
moreover have "unit_factor a * normalize a = a" 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

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

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

1028 
assume ?Q then show ?P 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 

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

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

1032 
"unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q") 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1034 
assume ?P 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1035 
moreover have "unit_factor a * normalize a = a" 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

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

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

1038 
assume ?Q then show ?P by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1040 

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

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

1042 
assumes "is_unit a" 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

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

1044 
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

1045 
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

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

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

1048 

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

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

1050 
"unit_factor 1 = 1" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1052 

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

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

1054 
"normalize 1 = 1" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1056 

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

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

1058 
"normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q") 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1060 
assume ?Q then show ?P by (rule is_unit_normalize) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1062 
assume ?P 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1063 
then have "a \<noteq> 0" by auto 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1064 
from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

1068 
moreover have "is_unit (unit_factor a)" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1069 
using \<open>a \<noteq> 0\<close> by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1071 
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

1072 

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

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

1074 
"a div normalize a = unit_factor a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1077 
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

1078 
case False then have "normalize a \<noteq> 0" by simp 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1080 
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

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

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

1083 

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

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

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

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

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

1088 
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

1089 
case False 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

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

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

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

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

1094 

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

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

1096 
"normalize a div a = 1 div unit_factor a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

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

1101 
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

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

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

1104 
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

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

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

1107 

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

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

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

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

1111 

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

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

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

1114 
proof (cases "a = 0 \<or> b = 0") 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1115 
case True then show ?thesis by auto 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

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

1120 
also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps) 
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" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1126 
using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1128 
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

1129 

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

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

1131 
"unit_factor (unit_factor a) = unit_factor a" 
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 

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

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

1135 
"a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1136 
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

1137 

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

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

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

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

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

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

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

1144 
have "normalize a = normalize (unit_factor a * normalize a)" by simp 
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) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1147 
finally show ?thesis using False by simp_all 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1149 

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

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

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

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

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

1154 
from assms have "normalize a \<noteq> 0" by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1155 
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

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

1157 
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

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

1159 
with \<open>normalize a \<noteq> 0\<close> 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1162 
with \<open>normalize a \<noteq> 0\<close> 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1165 

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

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

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

1168 
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

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

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

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

1172 
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

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

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

1175 
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

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

1177 

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

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

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

1180 
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

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

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

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

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

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

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

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

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

1189 

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

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

1191 
"normalize a dvd b \<longleftrightarrow> a dvd b" 
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 

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

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

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

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

1202 
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

1203 
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

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

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

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

1207 

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

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

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

1210 
explicit normalisation instead. In theory we could define an abbreviation 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1211 
like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1212 
counterproductive without suggestive infix syntax, which we do not want 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1213 
to sacrifice for this purpose here. 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

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

1215 

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

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

1217 
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

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

1219 
proof (cases "a = 0 \<or> b = 0") 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1220 
case True 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" .. 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1225 
ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1226 
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

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

1228 
then have "is_unit c" and "is_unit d" by auto 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1229 
with a b show ?thesis by (simp add: normalize_mult is_unit_normalize) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

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

1231 

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

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

1233 
"normalize a = normalize b \<Longrightarrow> 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

1234 
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

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

1236 

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

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

1238 
"normalize a = normalize b \<Longrightarrow> 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

1239 
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

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

1241 

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

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

1243 
"normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b" 
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 

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

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

1247 
"normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q") 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

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

1249 
assume ?Q then show ?P by (auto intro!: associatedI) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

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

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

1252 
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

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

1254 
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

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

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

1257 
proof (cases "a = 0 \<or> b = 0") 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1258 
case True with \<open>?P\<close> show ?thesis by auto 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1259 
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

1260 
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

1261 
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

1262 
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

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

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

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

1266 

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

1267 
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

1268 
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

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

1270 
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

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

1272 
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

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

1274 
with \<open>normalize a = a\<close> have "a = normalize b" by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60685
diff
changeset

1275 
with \<open>normalize b = b\<close> show "a = b" by simp 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1277 

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

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

1279 

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

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

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

1282 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 
25230  1283 
begin 
1284 
