author  haftmann 
Wed, 08 Jul 2015 14:01:34 +0200  
changeset 60685  cb21b7022b00 
parent 60615  e5fa1d5d3952 
child 60688  01488b559910 
permissions  rwrr 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

1 
(* Title: HOL/Rings.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

2 
Author: Gertrud Bauer 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

3 
Author: Steven Obua 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

4 
Author: Tobias Nipkow 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

5 
Author: Lawrence C Paulson 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

6 
Author: Markus Wenzel 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

7 
Author: Jeremy Avigad 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

8 
*) 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

9 

58889  10 
section {* Rings *} 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

11 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

12 
theory Rings 
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

13 
imports Groups 
15131  14 
begin 
14504  15 

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

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

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

21 
text{*For the @{text combine_numerals} simproc*} 

22 
lemma combine_common_factor: 

23 
"a * e + (b * e + c) = (a + b) * e + c" 

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

24 
by (simp add: distrib_right ac_simps) 
25152  25 

26 
end 

14504  27 

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

58195  31 
begin 
32 

33 
lemma mult_not_zero: 

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

35 
by auto 

36 

37 
end 

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

38 

58198  39 
class semiring_0 = semiring + comm_monoid_add + mult_zero 
40 

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

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

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

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

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

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

53 
qed 
14940  54 

25186  55 
end 
25152  56 

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

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

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

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

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

25152  71 
end 
14504  72 

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

75 

27516  76 
subclass semiring_0 .. 
25152  77 

78 
end 

14504  79 

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

27516  83 
subclass semiring_0_cancel .. 
14940  84 

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

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

86 

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

88 

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

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

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

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

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 

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

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

122 

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

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

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

125 

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

128 

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

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

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

131 

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

132 
lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" 
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  
30042  183 
from `a dvd b` obtain b' where "b = a * b'" .. 
184 
moreover from `c dvd d` obtain d' where "d = c * d'" .. 

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

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

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

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

188 

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

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

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

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

192 

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

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

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

195 
using dvd_mult_left [of b a c] by (simp add: ac_simps) 
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  
29925  222 
from `a dvd b` obtain b' where "b = a * b'" .. 
223 
moreover from `a dvd c` obtain c' where "c = a * c'" .. 

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

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

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

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

227 

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

229 

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

25267  232 
begin 
14940  233 

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

235 

27516  236 
subclass semiring_1 .. 
25267  237 

238 
end 

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

239 

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" .. 
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
59557
diff
changeset

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

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 

309 
text {* Distribution rules *} 

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 

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

317 
text{*Extract signs from products*} 
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 

35302  546 
text {* 
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} 

557 
*} 

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 

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

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

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 

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

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

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 

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

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

633 

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

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

635 

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

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

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

638 

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

639 
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

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

641 
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

642 

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

643 
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

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

645 
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

646 

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

647 
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

648 
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

649 
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

650 
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

651 
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

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

653 
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

654 
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

655 
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

656 
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

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

658 

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

659 
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

660 
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

661 
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

662 
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

663 

60570  664 
lemma dvd_div_mult2_eq: 
665 
assumes "b * c dvd a" 

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

667 
using assms proof 

668 
fix k 

669 
assume "a = b * c * k" 

670 
then show ?thesis 

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

672 
qed 

673 

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

674 

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

675 
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

676 

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

677 
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

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

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

680 

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

681 
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

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

683 
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

684 

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

685 
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

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

687 
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

688 

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

689 
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

690 
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

691 
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

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

693 
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

694 
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

695 
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

696 
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

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

698 

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

699 
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

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

701 
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

702 

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

703 
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

704 
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

705 
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

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

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

708 
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

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

710 

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

711 
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

712 
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

713 
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

714 
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

715 
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

716 
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

717 
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

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

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

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

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

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

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

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

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

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

727 
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

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

729 

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

730 
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

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

732 
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

733 

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

734 
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

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

736 
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

737 

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

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

739 
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

740 
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

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

742 
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

743 
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

744 
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

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

746 
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

747 
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

748 
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

749 
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

750 
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

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

752 

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

753 
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

754 
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

755 
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

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

757 
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

758 
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

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

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

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

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

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

764 
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

765 
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

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

767 

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

768 
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

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

770 
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

771 

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

772 
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

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

774 
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

775 

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

776 
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

777 
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

778 

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

779 
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

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

781 
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

782 

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

783 
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

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

785 
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

786 

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

787 
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

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

789 
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

790 

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

791 
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

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

793 
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

794 

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

795 
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

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

797 
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

798 

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

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

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

801 
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

802 

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

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

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

805 
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

806 

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

807 
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

808 
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

809 
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

810 
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

811 

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

812 
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

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

814 
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

815 

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

816 
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

817 
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

818 
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

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

820 
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

821 
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

822 
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

823 
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

824 
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

825 

60570  826 
lemma is_unit_div_mult2_eq: 
827 
assumes "is_unit b" and "is_unit c" 

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

829 
proof  

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

831 
then have "b * c dvd a" 

832 
by (rule unit_imp_dvd) 

833 
then show ?thesis 

834 
by (rule dvd_div_mult2_eq) 

835 
qed 

836 

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

837 

60529  838 
text \<open>Associated elements in a ring  an equivalence relation induced 
839 
by the quasiorder divisibility.\<close> 

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

840 

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

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

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

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

844 

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

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

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

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

848 

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

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

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

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

852 

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

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

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

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

856 

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

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

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

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

860 

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

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

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

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

864 

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

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

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

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

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

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

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

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

873 

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

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

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

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

877 

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

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

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

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

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

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

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

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

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

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

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

888 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

903 
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

904 

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

905 
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

906 
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

907 
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

908 
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

909 

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

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

911 

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

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

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

914 

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

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

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

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

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

919 
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

920 
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

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

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

923 

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

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

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

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

927 
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

928 

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

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

930 

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

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

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

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

934 
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

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

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

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

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

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

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

941 
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

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

943 

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

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

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

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

947 

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

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

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

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

951 

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

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

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

954 
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

955 

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

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

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

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

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

960 
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

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

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

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

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

965 

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

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

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

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

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

970 
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

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

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

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

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

975 

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

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

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

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

979 
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

980 
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

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

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

983 

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

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

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

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

987 

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

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

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

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

991 

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

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

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

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

995 
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

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

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

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

999 
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

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

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

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

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

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

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

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

1007 

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

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

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

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

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

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

1013 
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

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

1015 
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

1016 
then show ?thesis 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 div_unit_factor [simp]: 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

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

1024 
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

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

1026 
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

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

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

1029 

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

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

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

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

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

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

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

1036 
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

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

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

1039 
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

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

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

1042 

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

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

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

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

1046 

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

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

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

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

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

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

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

1053 
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

1054 
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

1055 
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

1056 
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

1057 
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

1058 
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

1059 
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

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

1061 
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

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

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

1064 

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

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

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

1067 
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

1068 

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

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

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

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

1072 

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

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

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

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

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

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

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

1079 
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

1080 
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

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

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

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

1084 

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

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

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

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

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

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

1090 
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

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

1092 
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

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

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

1095 
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

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

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

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

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

1100 

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

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

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

1103 
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

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

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

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

1107 
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

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

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

1110 
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

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

1112 

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

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

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

1115 
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

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

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

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

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

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

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

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

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

1124 

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

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

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

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

1128 
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

1129 
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

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

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

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

1133 

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

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

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

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

1137 
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

1138 
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

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

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

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

1142 

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

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

1144 
"associated (normalize a) b \<longleftrightarrow> associated a b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1145 
by (auto simp add: associated_def) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1146 

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

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

1148 
"associated a (normalize b) \<longleftrightarrow> associated a b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1149 
by (auto simp add: associated_def) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1150 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1164 
assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

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

1169 
by (simp add: unit_div_commute unit_div_mult_swap [symmetric]) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1170 
with * show ?P 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

1171 
by (rule is_unit_associatedI) 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1174 

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

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

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

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

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

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

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

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

1182 
case False with assms have "b \<noteq> 0" by auto 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

1185 
moreover from assms have "normalize a = normalize b" 
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60615
diff
changeset

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

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

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

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

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

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

1192 

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

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

1194 

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

1195 
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

1196 
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

1197 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 
25230  1198 
begin 
1199 

1200 
lemma mult_mono: 

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

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

1204 
done 

1205 

1206 
lemma mult_mono': 

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

1207 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 
25230  1208 
apply (rule mult_mono) 
1209 
apply (fast intro: order_trans)+ 

1210 
done 

1211 

1212 
end 

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

1213 

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

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

1216 

27516  1217 
subclass semiring_0_cancel .. 
23521  1218 

56536  1219 
lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1220 
using mult_left_mono [of 0 b a] by simp 
25230  1221 

1222 
lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0" 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1223 
using mult_left_mono [of b 0 a] by simp 
30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1224 

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

1225 
lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1226 
using mult_right_mono [of a 0 b] by simp 
30692
44ea10bc07a7
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
huffman
parents:
30650
diff
changeset

1227 

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

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

1229 
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1230 
by (drule mult_right_mono [of b 0], auto) 
25230  1231 

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

1232 
lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0)  (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
29667  1233 
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) 
25230  1234 

1235 
end 

1236 

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

1237 
class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add 
25267  1238 
begin 
25230  1239 

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

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

1241 

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

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

1243 

25230  1244 
lemma mult_left_less_imp_less: 
1245 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  1246 
by (force simp add: mult_left_mono not_le [symmetric]) 
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

1247 

25230  1248 
lemma mult_right_less_imp_less: 
1249 
"a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  1250 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  1251 

25186  1252 
end 
25152  1253 

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

1254 
class linordered_semiring_1 = linordered_semiring + semiring_1 
36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1255 
begin 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1256 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1257 
lemma convex_bound_le: 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1258 
assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1259 
shows "u * x + v * y \<le> a" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1260 
proof 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1261 
from assms have "u * x + v * y \<le> u * a + v * a" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

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

1263 
thus ?thesis using assms unfolding distrib_right[symmetric] by simp 
36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1264 
qed 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

1265 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36348
diff
changeset

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

1267 

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

1268 
class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + 
25062  1269 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
1270 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

1272 

27516  1273 
subclass semiring_0_cancel .. 
14940  1274 

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

1275 
subclass linordered_semiring 
28823  1276 
proof 
23550  1277 
fix a b c :: 'a 
1278 
assume A: "a \<le> b" "0 \<le> c" 

d4f1d6ef119c
convert instance proofs to Isar style
huffman 