author  haftmann 
Thu, 06 Aug 2015 23:56:48 +0200  
changeset 60867  86e7560e07d0 
parent 60758  d8d85a8172b5 
child 61649  268d88ec9087 
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 
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

13 
imports Groups 
15131  14 
begin 
14504  15 

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

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

18 
assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c" 
25152  19 
begin 
20 

60758  21 
text\<open>For the @{text combine_numerals} 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 

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

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

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

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

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

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

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

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

157 

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

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

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

160 
by (auto intro!: dvdI) 
28559  161 

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

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

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

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

165 

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

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

167 
"a dvd b \<Longrightarrow> a dvd (b * c)" 
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

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

169 

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

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

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

172 
by (rule dvd_mult) (rule dvd_refl) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

173 

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

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

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

176 
by (rule dvd_mult2) (rule dvd_refl) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

177 

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

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

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

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

182 
proof  
60758  183 
from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 
184 
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

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

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

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

188 

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

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

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

191 
by (simp add: dvd_def mult.assoc) blast 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

192 

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

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

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

195 
using dvd_mult_left [of b a c] by (simp add: ac_simps) 
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

196 

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

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

198 

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

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

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

201 

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

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

203 

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

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

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

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

207 

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

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

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

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

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

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

213 

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

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

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

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

217 

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

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

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

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

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

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

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

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

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

227 

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

229 

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

25267  232 
begin 
14940  233 

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

235 

27516  236 
subclass semiring_1 .. 
25267  237 

238 
end 

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

239 

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

240 
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

241 
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

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

27516  245 
subclass semiring_1_cancel .. 
246 
subclass comm_semiring_0_cancel .. 

247 
subclass comm_semiring_1 .. 

25267  248 

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

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

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

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

252 

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

253 
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

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

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

256 
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

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

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

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

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

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

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

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

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

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

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

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

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

269 

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

270 
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

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

272 
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

273 

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

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

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

276 
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

277 

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

278 
lemma dvd_add_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 + 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_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

281 

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

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

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

284 
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

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

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

288 
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

289 
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

290 
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

291 
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

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

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

294 
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

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

296 

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

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

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

299 
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

300 
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

301 

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

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

303 

22390  304 
class ring = semiring + ab_group_add 
25267  305 
begin 
25152  306 

27516  307 
subclass semiring_0_cancel .. 
25152  308 

60758  309 
text \<open>Distribution rules\<close> 
25152  310 

311 
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

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

314 
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

315 
by (rule minus_unique) (simp add: distrib_left [symmetric]) 
25152  316 

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

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

319 
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

320 

25152  321 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  322 
by simp 
25152  323 

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

29667  325 
by simp 
326 

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

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

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

329 
using distrib_left [of a b "c "] by simp 
29667  330 

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

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

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

333 
using distrib_right [of a " b" c] by simp 
25152  334 

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

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

336 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  337 

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

29667  340 
by (simp add: algebra_simps) 
25230  341 

342 
lemma eq_add_iff2: 

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

29667  344 
by (simp add: algebra_simps) 
25230  345 

25152  346 
end 
347 

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

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

349 
distrib_left distrib_right left_diff_distrib right_diff_distrib 
25152  350 

22390  351 
class comm_ring = comm_semiring + ab_group_add 
25267  352 
begin 
14738  353 

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

355 
subclass comm_semiring_0_cancel .. 
25267  356 

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

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

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

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

360 

25267  361 
end 
14738  362 

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

365 

27516  366 
subclass semiring_1_cancel .. 
25267  367 

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

368 
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

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

370 
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

371 

25267  372 
end 
25152  373 

22390  374 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
25267  375 
begin 
14738  376 

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

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

379 
by unfold_locales (simp add: algebra_simps) 
58647  380 

29465
b2cfb5d0a59e
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
huffman
parents:
29461
diff
changeset

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

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

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

384 
then have "x dvd  1 *  y" by (rule dvd_mult) 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

385 
then show "x dvd y" by simp 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

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

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

388 
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

389 
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

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

391 

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

392 
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

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

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

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

396 
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

397 
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

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

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

400 
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

401 
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

402 
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

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

404 

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

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

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

407 
using dvd_add [of x y " z"] by simp 
29409  408 

25267  409 
end 
25152  410 

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

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

412 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
25230  413 
begin 
414 

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

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

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

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

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

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

420 
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

421 
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

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

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

424 

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

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

429 
then show ?thesis using no_zero_divisors by simp 

430 
next 

431 
case True then show ?thesis by auto 

432 
qed 

433 

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

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

435 

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

436 
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

437 
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

438 
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

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

440 

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

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

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

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

444 

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

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

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

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

448 

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

450 

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

451 
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

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

453 

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

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

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

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

457 
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

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

459 
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

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

461 
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

462 
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

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

464 
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

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

466 
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

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

468 

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

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

470 

23544  471 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  472 
begin 
473 

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

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

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

477 
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

478 
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

479 
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

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

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

482 
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

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

484 

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

29667  487 
by (insert mult_cancel_right [of 1 c b], force) 
26274  488 

489 
lemma mult_cancel_right2 [simp]: 

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

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

492 

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

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

497 
lemma mult_cancel_left2 [simp]: 

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

29667  499 
by (insert mult_cancel_left [of c a 1], simp) 
26274  500 

501 
end 

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

502 

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

503 
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

504 

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

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

507 

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

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

509 

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

511 

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

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

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

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

515 
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

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

517 
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

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

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

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

521 

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

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

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

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

525 
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

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

527 
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

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

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

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

531 

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

532 
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

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

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

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

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

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

538 
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

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

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

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

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

543 

25186  544 
end 
25152  545 

60758  546 
text \<open> 
35302  547 
The theory of partially ordered rings is taken from the books: 
548 
\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

549 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
35302  550 
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 
551 
\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

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

60758  557 
\<close> 
35302  558 

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

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

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

561 

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

563 

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

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

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

566 

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

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

568 
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

569 
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

570 
by (rule distrib_left distrib_right)+ 
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 
end 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

573 

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

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

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

576 

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

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

578 
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

579 
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

580 
by (rule left_diff_distrib right_diff_distrib)+ 
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 
end 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

583 

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

585 

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

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

587 
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

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

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

590 

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

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

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

593 
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

594 

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

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

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

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

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

599 
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

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

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

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

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

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

605 
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

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

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

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

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

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

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

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

613 
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

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

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

616 

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

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

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

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

620 
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

621 

60570  622 
lemma divide_zero_left [simp]: 
623 
"0 div a = 0" 

624 
proof (cases "a = 0") 

625 
case True then show ?thesis by simp 

626 
next 

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

628 
by (rule nonzero_mult_divide_cancel_left) 

629 
then show ?thesis by simp 

630 
qed 

631 

60690  632 
lemma divide_1 [simp]: 
633 
"a div 1 = a" 

634 
using nonzero_mult_divide_cancel_left [of 1 a] by simp 

635 

60867  636 
end 
637 

638 
class idom_divide = idom + semidom_divide 

639 

640 
class algebraic_semidom = semidom_divide 

641 
begin 

642 

643 
text \<open> 

644 
Class @{class algebraic_semidom} enriches a integral domain 

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

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

647 
which are degenerated there. 

648 
\<close> 

649 

60690  650 
lemma dvd_times_left_cancel_iff [simp]: 
651 
assumes "a \<noteq> 0" 

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

653 
proof 

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

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

656 
then show ?Q .. 

657 
next 

658 
assume ?Q then obtain d where "c = b * d" .. 

659 
then have "a * c = a * b * d" by (simp add: ac_simps) 

660 
then show ?P .. 

661 
qed 

662 

663 
lemma dvd_times_right_cancel_iff [simp]: 

664 
assumes "a \<noteq> 0" 

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

666 
using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps) 

667 

668 
lemma div_dvd_iff_mult: 

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

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

671 
proof  

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

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

674 
qed 

675 

676 
lemma dvd_div_iff_mult: 

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

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

679 
proof  

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

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

682 
qed 

683 

60867  684 
lemma div_dvd_div [simp]: 
685 
assumes "a dvd b" and "a dvd c" 

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

687 
proof (cases "a = 0") 

688 
case True with assms show ?thesis by simp 

689 
next 

690 
case False 

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

692 
by (auto elim!: dvdE) 

693 
ultimately show ?thesis by simp 

694 
qed 

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

695 

60867  696 
lemma div_add [simp]: 
697 
assumes "c dvd a" and "c dvd b" 

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

699 
proof (cases "c = 0") 

700 
case True then show ?thesis by simp 

701 
next 

702 
case False 

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

704 
by (auto elim!: dvdE) 

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

706 
by (simp add: algebra_simps) 

707 
ultimately show ?thesis 

708 
by simp 

709 
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

710 

60867  711 
lemma div_mult_div_if_dvd: 
712 
assumes "b dvd a" and "d dvd c" 

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

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

715 
case True with assms show ?thesis by auto 

716 
next 

717 
case False 

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

719 
by (auto elim!: dvdE) 

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

721 
by (simp add: ac_simps) 

722 
ultimately show ?thesis by simp 

723 
qed 

724 

725 
lemma dvd_div_eq_mult: 

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

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

728 
proof 

729 
assume "b = c * a" 

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

731 
next 

732 
assume "b div a = c" 

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

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

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

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

737 
qed 

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

738 

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

739 
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

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

741 
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

742 

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

743 
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

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

745 
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

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

748 
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

749 
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

750 
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

751 
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

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

753 
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

754 
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

755 
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

756 
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

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

758 

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

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

760 
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

761 
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

762 
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

763 

60570  764 
lemma dvd_div_mult2_eq: 
765 
assumes "b * c dvd a" 

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

767 
using assms proof 

768 
fix k 

769 
assume "a = b * c * k" 

770 
then show ?thesis 

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

772 
qed 

773 

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

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

777 
proof  

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

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

780 
by simp 

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

782 
by (simp add: ac_simps) 

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

784 
using assms by (simp add: div_mult_swap) 

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

786 
using assms by (simp add: ac_simps) 

787 
finally show ?thesis . 

788 
qed 

789 

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

790 

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

791 
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

792 

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

793 
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

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

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

796 

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

797 
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

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

799 
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

800 

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

801 
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

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

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

804 

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

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

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

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

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

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

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

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

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

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

814 

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

815 
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

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

817 
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

818 

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

819 
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

820 
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

821 
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

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

823 
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

824 
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

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

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

830 
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

831 
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

832 
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

833 
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

834 
then show "1 div a = b" by simp 
60758  835 
from b_def \<open>is_unit a\<close> show "is_unit b" by simp 
836 
from \<open>is_unit a\<close> and \<open>is_unit b\<close> show "a \<noteq> 0" and "b \<noteq> 0" by auto 

837 
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

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

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

843 
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

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

845 

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

846 
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

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

848 
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

849 

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

850 
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

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

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

853 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

868 

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

869 
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

870 
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

871 
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

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

873 
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

874 
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

875 
by (subst mult_assoc [symmetric]) simp 
60758  876 
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

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

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

880 
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

881 
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

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

883 

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

884 
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

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

886 
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

887 

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

888 
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

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

890 
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

891 

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

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

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

894 

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

895 
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

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

897 
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

898 

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

899 
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

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

901 
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

902 

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

903 
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

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

905 
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

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

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

909 
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

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

913 
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

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

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

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

918 

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

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

921 
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

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

924 
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

925 
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

926 
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

927 

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

928 
lemma unit_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

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

930 
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

931 

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

932 
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

933 
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

934 
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

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

936 
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

937 
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

938 
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

939 
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

940 
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

941 

60570  942 
lemma is_unit_div_mult2_eq: 
943 
assumes "is_unit b" and "is_unit c" 

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

945 
proof  

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

947 
then have "b * c dvd a" 

948 
by (rule unit_imp_dvd) 

949 
then show ?thesis 

950 
by (rule dvd_div_mult2_eq) 

951 
qed 

952 

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

954 
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

955 
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

956 
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

957 

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

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

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

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

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

962 
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

963 
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

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

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

966 

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

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

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

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

970 
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

971 

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

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

973 

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

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

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

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

977 
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

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

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

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

981 
"is_unit a \<Longrightarrow> normalize a = 1" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

984 
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

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

986 

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

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

988 
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

989 
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

990 
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

991 
@{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

992 
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

993 
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

994 
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

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

996 

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

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

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

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

1000 

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

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

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

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

1004 

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

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

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

1007 
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

1008 

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

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

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

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

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

1013 
moreover have "unit_factor a * normalize a = a" by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

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

1018 

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

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

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

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

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

1023 
moreover have "unit_factor a * normalize a = a" by simp 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

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

1028 

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

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

1030 
assumes "is_unit a" shows "unit_factor a = a" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1032 
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

1033 
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

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

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

1036 

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

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

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

1039 
by (rule is_unit_unit_factor) simp 
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 normalize_1 [simp]: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1044 

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

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

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

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

1048 
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

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

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

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

1052 
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

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

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

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

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

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

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

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

1060 

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

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

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

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

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

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

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

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

1068 
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

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

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

1071 

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

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

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

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

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

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

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

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

1079 
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

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

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

1082 

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

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

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

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

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

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

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

1089 
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

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

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

1092 
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

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

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

1095 

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

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

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

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

1099 

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

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

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

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

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

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

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

1106 
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

1107 
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

1108 
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

1109 
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

1110 
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

1111 
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

1112 
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

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

1114 
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

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

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

1117 

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

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

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

1120 
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

1121 

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

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

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

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

1125 

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

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

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

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

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

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

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

1132 
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

1133 
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

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

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

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

1137 

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

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

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

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

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

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

1143 
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

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

1145 
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

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

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

1148 
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

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

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

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

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

1153 

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

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

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

1156 
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

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

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

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

1160 
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

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

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

1163 
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

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_normalize_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 "normalize (a div b) = normalize a div normalize 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 "normalize a = normalize (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: normalize_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 normalize_dvd_iff [simp]: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1181 
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

1182 
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

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

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

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

1186 

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

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

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

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

1190 
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

1191 
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

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

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

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

1195 

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

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

1197 
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

1198 
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

1199 
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

1200 
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

1201 
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

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

1203 

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

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

1205 
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

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

1207 
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

1208 
case True with assms show ?thesis by auto 
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

1210 
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

1211 
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

1212 
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

1213 
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

1214 
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

1215 
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

1216 
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

1217 
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

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

1219 

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

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

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

1222 
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

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

1224 

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

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

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

1227 
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

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

1229 

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

1230 
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

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

1232 
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

1233 

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

1234 
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

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

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

1237 
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

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

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

1240 
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

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

1242 
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

1243 
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

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

1245 
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

1246 
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

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

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

1249 
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

1250 
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

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

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

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

1254 

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

1255 
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

1256 
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

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

1258 
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

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

1260 
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

1261 
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

1262 
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

1263 
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

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

1265 

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

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

1267 

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

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

1269 
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

1270 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 
25230  1271 
begin 
1272 

1273 
lemma mult_mono: 

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

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

1277 
done 

1278 

1279 
lemma mult_mono': 

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

1280 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 
25230  1281 
apply (rule mult_mono) 
1282 
apply (fast intro: order_trans)+ 

1283 
done 

1284 

1285 
end 

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

1286 

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

1287 
class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add 
25267  1288 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
& 