author  huffman 
Thu, 08 Jan 2009 10:43:09 0800  
changeset 29409  f0a8fe83bc07 
parent 29408  6d10cf26b5dc 
child 29461  7c1841a7bdf4 
permissions  rwrr 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

1 
(* Title: HOL/Ring_and_Field.thy 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

2 
ID: $Id$ 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

3 
Author: Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel, 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

4 
with contributions by Jeremy Avigad 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

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

6 

14738  7 
header {* (Ordered) Rings and Fields *} 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

8 

15229  9 
theory Ring_and_Field 
15140  10 
imports OrderedGroup 
15131  11 
begin 
14504  12 

14738  13 
text {* 
14 
The theory of partially ordered rings is taken from the books: 

15 
\begin{itemize} 

16 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 

17 
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 

18 
\end{itemize} 

19 
Most of the used notions can also be looked up in 

20 
\begin{itemize} 

14770  21 
\item \url{http://www.mathworld.com} by Eric Weisstein et. al. 
14738  22 
\item \emph{Algebra I} by van der Waerden, Springer. 
23 
\end{itemize} 

24 
*} 

14504  25 

22390  26 
class semiring = ab_semigroup_add + semigroup_mult + 
25062  27 
assumes left_distrib: "(a + b) * c = a * c + b * c" 
28 
assumes right_distrib: "a * (b + c) = a * b + a * c" 

25152  29 
begin 
30 

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

32 
lemma combine_common_factor: 

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

34 
by (simp add: left_distrib add_ac) 

35 

36 
end 

14504  37 

22390  38 
class mult_zero = times + zero + 
25062  39 
assumes mult_zero_left [simp]: "0 * a = 0" 
40 
assumes mult_zero_right [simp]: "a * 0 = 0" 

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

41 

22390  42 
class semiring_0 = semiring + comm_monoid_add + mult_zero 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

43 

22390  44 
class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add 
25186  45 
begin 
14504  46 

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

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

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

51 
by (simp add: left_distrib [symmetric]) 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

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

53 
by (simp only: add_left_cancel) 
25152  54 
next 
55 
fix a :: 'a 

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

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

57 
by (simp add: right_distrib [symmetric]) 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

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

59 
by (simp only: add_left_cancel) 
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

60 
qed 
14940  61 

25186  62 
end 
25152  63 

22390  64 
class comm_semiring = ab_semigroup_add + ab_semigroup_mult + 
25062  65 
assumes distrib: "(a + b) * c = a * c + b * c" 
25152  66 
begin 
14504  67 

25152  68 
subclass semiring 
28823  69 
proof 
14738  70 
fix a b c :: 'a 
71 
show "(a + b) * c = a * c + b * c" by (simp add: distrib) 

72 
have "a * (b + c) = (b + c) * a" by (simp add: mult_ac) 

73 
also have "... = b * a + c * a" by (simp only: distrib) 

74 
also have "... = a * b + a * c" by (simp add: mult_ac) 

75 
finally show "a * (b + c) = a * b + a * c" by blast 

14504  76 
qed 
77 

25152  78 
end 
14504  79 

25152  80 
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero 
81 
begin 

82 

27516  83 
subclass semiring_0 .. 
25152  84 

85 
end 

14504  86 

22390  87 
class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add 
25186  88 
begin 
14940  89 

27516  90 
subclass semiring_0_cancel .. 
14940  91 

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

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

93 

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

95 

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

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

101 
by (rule not_sym) (rule zero_neq_one) 

102 

103 
end 

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

104 

22390  105 
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 
14504  106 

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

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

108 

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

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

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

111 

28559  112 
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where 
113 
[code del]: "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

114 

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

115 
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

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

117 

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

118 
lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

120 

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

121 
end 
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 comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd 
22390  124 
(*previously almost_semiring*) 
25152  125 
begin 
14738  126 

27516  127 
subclass semiring_1 .. 
25152  128 

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

129 
lemma dvd_refl: "a dvd a" 
28559  130 
proof 
131 
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

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

133 

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

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

135 
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

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

137 
proof  
28559  138 
from assms obtain v where "b = a * v" by (auto elim!: dvdE) 
139 
moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE) 

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

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

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

143 

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

144 
lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0" 
28559  145 
by (auto intro: dvd_refl elim!: dvdE) 
146 

147 
lemma dvd_0_right [iff]: "a dvd 0" 

148 
proof 

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

149 
show "0 = a * 0" by simp 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

151 

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

152 
lemma one_dvd [simp]: "1 dvd a" 
28559  153 
by (auto intro!: dvdI) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

154 

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

155 
lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)" 
28559  156 
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

157 

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

158 
lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

159 
apply (subst mult_commute) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

160 
apply (erule dvd_mult) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

162 

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

163 
lemma dvd_triv_right [simp]: "a dvd b * a" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

165 

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

166 
lemma dvd_triv_left [simp]: "a dvd a * b" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

168 

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

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

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

171 
and "cd": "c dvd d" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

172 
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

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

174 
from ab obtain b' where "b = a * b'" .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

175 
moreover from "cd" obtain d' where "d = c * d'" .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

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

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

179 

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

180 
lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

181 
by (simp add: dvd_def mult_assoc, blast) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

182 

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

183 
lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

184 
unfolding mult_ac [of a] by (rule dvd_mult_left) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

185 

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

186 
lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

188 

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

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

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

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

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

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

194 
from ab obtain b' where "b = a * b'" .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

195 
moreover from ac obtain c' where "c = a * c'" .. 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

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

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

199 

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

201 

22390  202 
class no_zero_divisors = zero + times + 
25062  203 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
14504  204 

22390  205 
class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one 
206 
+ cancel_ab_semigroup_add + monoid_mult 

25267  207 
begin 
14940  208 

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

210 

27516  211 
subclass semiring_1 .. 
25267  212 

213 
end 

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

214 

22390  215 
class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult 
216 
+ zero_neq_one + cancel_ab_semigroup_add 

25267  217 
begin 
14738  218 

27516  219 
subclass semiring_1_cancel .. 
220 
subclass comm_semiring_0_cancel .. 

221 
subclass comm_semiring_1 .. 

25267  222 

223 
end 

25152  224 

22390  225 
class ring = semiring + ab_group_add 
25267  226 
begin 
25152  227 

27516  228 
subclass semiring_0_cancel .. 
25152  229 

230 
text {* Distribution rules *} 

231 

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

233 
by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 

234 

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

236 
by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 

237 

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

238 
text{*Extract signs from products*} 
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

239 
lemmas mult_minus_left [simp] = minus_mult_left [symmetric] 
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

240 
lemmas mult_minus_right [simp] = minus_mult_right [symmetric] 
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

241 

25152  242 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29407
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

243 
by simp 
25152  244 

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

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

246 
by simp 
25152  247 

248 
lemma right_diff_distrib: "a * (b  c) = a * b  a * c" 

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

249 
by (simp add: right_distrib diff_minus) 
25152  250 

251 
lemma left_diff_distrib: "(a  b) * c = a * c  b * c" 

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

252 
by (simp add: left_distrib diff_minus) 
25152  253 

254 
lemmas ring_distribs = 

255 
right_distrib left_distrib left_diff_distrib right_diff_distrib 

256 

25230  257 
lemmas ring_simps = 
258 
add_ac 

259 
add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 

260 
diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff 

261 
ring_distribs 

262 

263 
lemma eq_add_iff1: 

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

265 
by (simp add: ring_simps) 

266 

267 
lemma eq_add_iff2: 

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

269 
by (simp add: ring_simps) 

270 

25152  271 
end 
272 

273 
lemmas ring_distribs = 

274 
right_distrib left_distrib left_diff_distrib right_diff_distrib 

275 

22390  276 
class comm_ring = comm_semiring + ab_group_add 
25267  277 
begin 
14738  278 

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

280 
subclass comm_semiring_0_cancel .. 
25267  281 

282 
end 

14738  283 

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

286 

27516  287 
subclass semiring_1_cancel .. 
25267  288 

289 
end 

25152  290 

22390  291 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
292 
(*previously ring*) 

25267  293 
begin 
14738  294 

27516  295 
subclass ring_1 .. 
296 
subclass comm_semiring_1_cancel .. 

25267  297 

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

298 
lemma dvd_minus_iff: "x dvd  y \<longleftrightarrow> x dvd y" 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

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

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

301 
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

302 
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

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

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

305 
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

306 
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

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

308 

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

309 
lemma minus_dvd_iff: " x dvd y \<longleftrightarrow> x dvd y" 
6d10cf26b5dc
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman
parents:
29407
diff
changeset

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

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

312 
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

313 
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

314 
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

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

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

317 
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

318 
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

319 
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

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

321 

29409  322 
lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y  z)" 
323 
by (simp add: diff_minus dvd_add dvd_minus_iff) 

324 

25267  325 
end 
25152  326 

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

327 
class ring_no_zero_divisors = ring + no_zero_divisors 
25230  328 
begin 
329 

330 
lemma mult_eq_0_iff [simp]: 

331 
shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)" 

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

333 
case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto 

334 
then show ?thesis using no_zero_divisors by simp 

335 
next 

336 
case True then show ?thesis by auto 

337 
qed 

338 

26193  339 
text{*Cancellation of equalities with a common factor*} 
340 
lemma mult_cancel_right [simp, noatp]: 

341 
"a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" 

342 
proof  

343 
have "(a * c = b * c) = ((a  b) * c = 0)" 

344 
by (simp add: ring_distribs right_minus_eq) 

345 
thus ?thesis 

346 
by (simp add: disj_commute right_minus_eq) 

347 
qed 

348 

349 
lemma mult_cancel_left [simp, noatp]: 

350 
"c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" 

351 
proof  

352 
have "(c * a = c * b) = (c * (a  b) = 0)" 

353 
by (simp add: ring_distribs right_minus_eq) 

354 
thus ?thesis 

355 
by (simp add: right_minus_eq) 

356 
qed 

357 

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

359 

23544  360 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  361 
begin 
362 

363 
lemma mult_cancel_right1 [simp]: 

364 
"c = b * c \<longleftrightarrow> c = 0 \<or> b = 1" 

365 
by (insert mult_cancel_right [of 1 c b], force) 

366 

367 
lemma mult_cancel_right2 [simp]: 

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

369 
by (insert mult_cancel_right [of a c 1], simp) 

370 

371 
lemma mult_cancel_left1 [simp]: 

372 
"c = c * b \<longleftrightarrow> c = 0 \<or> b = 1" 

373 
by (insert mult_cancel_left [of c 1 b], force) 

374 

375 
lemma mult_cancel_left2 [simp]: 

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

377 
by (insert mult_cancel_left [of c a 1], simp) 

378 

379 
end 

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

380 

22390  381 
class idom = comm_ring_1 + no_zero_divisors 
25186  382 
begin 
14421
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14398
diff
changeset

383 

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

385 

25186  386 
end 
25152  387 

22390  388 
class division_ring = ring_1 + inverse + 
25062  389 
assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
390 
assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1" 

25186  391 
begin 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

392 

25186  393 
subclass ring_1_no_zero_divisors 
28823  394 
proof 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

395 
fix a b :: 'a 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

396 
assume a: "a \<noteq> 0" and b: "b \<noteq> 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

397 
show "a * b \<noteq> 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

398 
proof 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

399 
assume ab: "a * b = 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

400 
hence "0 = inverse a * (a * b) * inverse b" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

401 
by simp 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

402 
also have "\<dots> = (inverse a * a) * (b * inverse b)" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

403 
by (simp only: mult_assoc) 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

404 
also have "\<dots> = 1" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

405 
using a b by simp 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

406 
finally show False 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

407 
by simp 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

408 
qed 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

409 
qed 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

410 

26274  411 
lemma nonzero_imp_inverse_nonzero: 
412 
"a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0" 

413 
proof 

414 
assume ianz: "inverse a = 0" 

415 
assume "a \<noteq> 0" 

416 
hence "1 = a * inverse a" by simp 

417 
also have "... = 0" by (simp add: ianz) 

418 
finally have "1 = 0" . 

419 
thus False by (simp add: eq_commute) 

420 
qed 

421 

422 
lemma inverse_zero_imp_zero: 

423 
"inverse a = 0 \<Longrightarrow> a = 0" 

424 
apply (rule classical) 

425 
apply (drule nonzero_imp_inverse_nonzero) 

426 
apply auto 

427 
done 

428 

429 
lemma inverse_unique: 

430 
assumes ab: "a * b = 1" 

431 
shows "inverse a = b" 

432 
proof  

433 
have "a \<noteq> 0" using ab by (cases "a = 0") simp_all 

29406  434 
moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
435 
ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 

26274  436 
qed 
437 

29406  438 
lemma nonzero_inverse_minus_eq: 
439 
"a \<noteq> 0 \<Longrightarrow> inverse ( a) =  inverse a" 

440 
by (rule inverse_unique) simp 

441 

442 
lemma nonzero_inverse_inverse_eq: 

443 
"a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a" 

444 
by (rule inverse_unique) simp 

445 

446 
lemma nonzero_inverse_eq_imp_eq: 

447 
assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0" 

448 
shows "a = b" 

449 
proof  

450 
from `inverse a = inverse b` 

451 
have "inverse (inverse a) = inverse (inverse b)" 

452 
by (rule arg_cong) 

453 
with `a \<noteq> 0` and `b \<noteq> 0` show "a = b" 

454 
by (simp add: nonzero_inverse_inverse_eq) 

455 
qed 

456 

457 
lemma inverse_1 [simp]: "inverse 1 = 1" 

458 
by (rule inverse_unique) simp 

459 

26274  460 
lemma nonzero_inverse_mult_distrib: 
29406  461 
assumes "a \<noteq> 0" and "b \<noteq> 0" 
26274  462 
shows "inverse (a * b) = inverse b * inverse a" 
463 
proof  

29406  464 
have "a * (b * inverse b) * inverse a = 1" 
465 
using assms by simp 

466 
hence "a * b * (inverse b * inverse a) = 1" 

467 
by (simp only: mult_assoc) 

26274  468 
thus ?thesis 
29406  469 
by (rule inverse_unique) 
26274  470 
qed 
471 

472 
lemma division_ring_inverse_add: 

473 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b" 

474 
by (simp add: ring_simps mult_assoc) 

475 

476 
lemma division_ring_inverse_diff: 

477 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a  inverse b = inverse a * (b  a) * inverse b" 

478 
by (simp add: ring_simps mult_assoc) 

479 

25186  480 
end 
25152  481 

22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

482 
class field = comm_ring_1 + inverse + 
25062  483 
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
484 
assumes divide_inverse: "a / b = a * inverse b" 

25267  485 
begin 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

486 

25267  487 
subclass division_ring 
28823  488 
proof 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

489 
fix a :: 'a 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

490 
assume "a \<noteq> 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

491 
thus "inverse a * a = 1" by (rule field_inverse) 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

492 
thus "a * inverse a = 1" by (simp only: mult_commute) 
14738  493 
qed 
25230  494 

27516  495 
subclass idom .. 
25230  496 

497 
lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b" 

498 
proof 

499 
assume neq: "b \<noteq> 0" 

500 
{ 

501 
hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) 

502 
also assume "a / b = 1" 

503 
finally show "a = b" by simp 

504 
next 

505 
assume "a = b" 

506 
with neq show "a / b = 1" by (simp add: divide_inverse) 

507 
} 

508 
qed 

509 

510 
lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a" 

511 
by (simp add: divide_inverse) 

512 

513 
lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1" 

514 
by (simp add: divide_inverse) 

515 

516 
lemma divide_zero_left [simp]: "0 / a = 0" 

517 
by (simp add: divide_inverse) 

518 

519 
lemma inverse_eq_divide: "inverse a = 1 / a" 

520 
by (simp add: divide_inverse) 

521 

522 
lemma add_divide_distrib: "(a+b) / c = a/c + b/c" 

523 
by (simp add: divide_inverse ring_distribs) 

524 

525 
end 

526 

22390  527 
class division_by_zero = zero + inverse + 
25062  528 
assumes inverse_zero [simp]: "inverse 0 = 0" 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

529 

25230  530 
lemma divide_zero [simp]: 
531 
"a / 0 = (0::'a::{field,division_by_zero})" 

532 
by (simp add: divide_inverse) 

533 

534 
lemma divide_self_if [simp]: 

535 
"a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" 

28559  536 
by simp 
25230  537 

22390  538 
class mult_mono = times + zero + ord + 
25062  539 
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
540 
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

541 

22390  542 
class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
25230  543 
begin 
544 

545 
lemma mult_mono: 

546 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c 

547 
\<Longrightarrow> a * c \<le> b * d" 

548 
apply (erule mult_right_mono [THEN order_trans], assumption) 

549 
apply (erule mult_left_mono, assumption) 

550 
done 

551 

552 
lemma mult_mono': 

553 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c 

554 
\<Longrightarrow> a * c \<le> b * d" 

555 
apply (rule mult_mono) 

556 
apply (fast intro: order_trans)+ 

557 
done 

558 

559 
end 

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

560 

22390  561 
class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

562 
+ semiring + comm_monoid_add + cancel_ab_semigroup_add 
25267  563 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

564 

27516  565 
subclass semiring_0_cancel .. 
566 
subclass pordered_semiring .. 

23521  567 

25230  568 
lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b" 
569 
by (drule mult_left_mono [of zero b], auto) 

570 

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

572 
by (drule mult_left_mono [of b zero], auto) 

573 

574 
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 

575 
by (drule mult_right_mono [of b zero], auto) 

576 

26234  577 
lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0)  (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
25230  578 
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) 
579 

580 
end 

581 

582 
class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono 

25267  583 
begin 
25230  584 

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

586 

27516  587 
subclass pordered_comm_monoid_add .. 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

588 

25230  589 
lemma mult_left_less_imp_less: 
590 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

591 
by (force simp add: mult_left_mono not_le [symmetric]) 

592 

593 
lemma mult_right_less_imp_less: 

594 
"a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

595 
by (force simp add: mult_right_mono not_le [symmetric]) 

23521  596 

25186  597 
end 
25152  598 

22390  599 
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + 
25062  600 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
601 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

603 

27516  604 
subclass semiring_0_cancel .. 
14940  605 

25267  606 
subclass ordered_semiring 
28823  607 
proof 
23550  608 
fix a b c :: 'a 
609 
assume A: "a \<le> b" "0 \<le> c" 

610 
from A show "c * a \<le> c * b" 

25186  611 
unfolding le_less 
612 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  613 
from A show "a * c \<le> b * c" 
25152  614 
unfolding le_less 
25186  615 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  616 
qed 
617 

25230  618 
lemma mult_left_le_imp_le: 
619 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

620 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 

621 

622 
lemma mult_right_le_imp_le: 

623 
"a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

624 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 

625 

626 
lemma mult_pos_pos: 

627 
"0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b" 

628 
by (drule mult_strict_left_mono [of zero b], auto) 

629 

630 
lemma mult_pos_neg: 

631 
"0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0" 

632 
by (drule mult_strict_left_mono [of b zero], auto) 

633 

634 
lemma mult_pos_neg2: 

635 
"0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 

636 
by (drule mult_strict_right_mono [of b zero], auto) 

637 

638 
lemma zero_less_mult_pos: 

639 
"0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" 

640 
apply (cases "b\<le>0") 

641 
apply (auto simp add: le_less not_less) 

642 
apply (drule_tac mult_pos_neg [of a b]) 

643 
apply (auto dest: less_not_sym) 

644 
done 

645 

646 
lemma zero_less_mult_pos2: 

647 
"0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" 

648 
apply (cases "b\<le>0") 

649 
apply (auto simp add: le_less not_less) 

650 
apply (drule_tac mult_pos_neg2 [of a b]) 

651 
apply (auto dest: less_not_sym) 

652 
done 

653 

26193  654 
text{*Strict monotonicity in both arguments*} 
655 
lemma mult_strict_mono: 

656 
assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c" 

657 
shows "a * c < b * d" 

658 
using assms apply (cases "c=0") 

659 
apply (simp add: mult_pos_pos) 

660 
apply (erule mult_strict_right_mono [THEN less_trans]) 

661 
apply (force simp add: le_less) 

662 
apply (erule mult_strict_left_mono, assumption) 

663 
done 

664 

665 
text{*This weaker variant has more natural premises*} 

666 
lemma mult_strict_mono': 

667 
assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c" 

668 
shows "a * c < b * d" 

669 
by (rule mult_strict_mono) (insert assms, auto) 

670 

671 
lemma mult_less_le_imp_less: 

672 
assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c" 

673 
shows "a * c < b * d" 

674 
using assms apply (subgoal_tac "a * c < b * c") 

675 
apply (erule less_le_trans) 

676 
apply (erule mult_left_mono) 

677 
apply simp 

678 
apply (erule mult_strict_right_mono) 

679 
apply assumption 

680 
done 

681 

682 
lemma mult_le_less_imp_less: 

683 
assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c" 

684 
shows "a * c < b * d" 

685 
using assms apply (subgoal_tac "a * c \<le> b * c") 

686 
apply (erule le_less_trans) 

687 
apply (erule mult_strict_left_mono) 

688 
apply simp 

689 
apply (erule mult_right_mono) 

690 
apply simp 

691 
done 

692 

693 
lemma mult_less_imp_less_left: 

694 
assumes less: "c * a < c * b" and nonneg: "0 \<le> c" 

695 
shows "a < b" 

696 
proof (rule ccontr) 

697 
assume "\<not> a < b" 

698 
hence "b \<le> a" by (simp add: linorder_not_less) 

699 
hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono) 

700 
with this and less show False 

701 
by (simp add: not_less [symmetric]) 

702 
qed 

703 

704 
lemma mult_less_imp_less_right: 

705 
assumes less: "a * c < b * c" and nonneg: "0 \<le> c" 

706 
shows "a < b" 

707 
proof (rule ccontr) 

708 
assume "\<not> a < b" 

709 
hence "b \<le> a" by (simp add: linorder_not_less) 

710 
hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono) 

711 
with this and less show False 

712 
by (simp add: not_less [symmetric]) 

713 
qed 

714 

25230  715 
end 
716 

22390  717 
class mult_mono1 = times + zero + ord + 
25230  718 
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
14270  719 

22390  720 
class pordered_comm_semiring = comm_semiring_0 
721 
+ pordered_ab_semigroup_add + mult_mono1 

25186  722 
begin 
25152  723 

25267  724 
subclass pordered_semiring 
28823  725 
proof 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

726 
fix a b c :: 'a 
23550  727 
assume "a \<le> b" "0 \<le> c" 
25230  728 
thus "c * a \<le> c * b" by (rule mult_mono1) 
23550  729 
thus "a * c \<le> b * c" by (simp only: mult_commute) 
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
20633
diff
changeset

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

731 

25267  732 
end 
733 

734 
class pordered_cancel_comm_semiring = comm_semiring_0_cancel 

735 
+ pordered_ab_semigroup_add + mult_mono1 

736 
begin 

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

737 

27516  738 
subclass pordered_comm_semiring .. 
739 
subclass pordered_cancel_semiring .. 

25267  740 

741 
end 

742 

743 
class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add + 

26193  744 
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  745 
begin 
746 

747 
subclass ordered_semiring_strict 

28823  748 
proof 
23550  749 
fix a b c :: 'a 
750 
assume "a < b" "0 < c" 

26193  751 
thus "c * a < c * b" by (rule mult_strict_left_mono_comm) 
23550  752 
thus "a * c < b * c" by (simp only: mult_commute) 
753 
qed 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14270
diff
changeset

754 

25267  755 
subclass pordered_cancel_comm_semiring 
28823  756 
proof 
23550  757 
fix a b c :: 'a 
758 
assume "a \<le> b" "0 \<le> c" 

759 
thus "c * a \<le> c * b" 

25186  760 
unfolding le_less 
26193  761 
using mult_strict_left_mono by (cases "c = 0") auto 
23550  762 
qed 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14270
diff
changeset

763 

25267  764 
end 
25230  765 

25267  766 
class pordered_ring = ring + pordered_cancel_semiring 
767 
begin 

25230  768 

27516  769 
subclass pordered_ab_group_add .. 
14270  770 

25230  771 
lemmas ring_simps = ring_simps group_simps 
772 

773 
lemma less_add_iff1: 

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

775 
by (simp add: ring_simps) 

776 

777 
lemma less_add_iff2: 

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

779 
by (simp add: ring_simps) 

780 

781 
lemma le_add_iff1: 

782 
"a * e + c \<le> b * e + d \<longleftrightarrow> (a  b) * e + c \<le> d" 

783 
by (simp add: ring_simps) 

784 

785 
lemma le_add_iff2: 

786 
"a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b  a) * e + d" 

787 
by (simp add: ring_simps) 

788 

789 
lemma mult_left_mono_neg: 

790 
"b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b" 

791 
apply (drule mult_left_mono [of _ _ "uminus c"]) 

792 
apply (simp_all add: minus_mult_left [symmetric]) 

793 
done 

794 

795 
lemma mult_right_mono_neg: 

796 
"b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c" 

797 
apply (drule mult_right_mono [of _ _ "uminus c"]) 

798 
apply (simp_all add: minus_mult_right [symmetric]) 

799 
done 

800 

801 
lemma mult_nonpos_nonpos: 

802 
"a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b" 

803 
by (drule mult_right_mono_neg [of a zero b]) auto 

804 

805 
lemma split_mult_pos_le: 

806 
"(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b" 

807 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 

25186  808 

809 
end 

14270  810 

25762  811 
class abs_if = minus + uminus + ord + zero + abs + 
812 
assumes abs_if: "\<bar>a\<bar> = (if a < 0 then  a else a)" 

813 

814 
class sgn_if = minus + uminus + zero + one + ord + sgn + 

25186  815 
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else  1)" 
24506  816 

25564  817 
lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0" 
818 
by(simp add:sgn_if) 

819 

25230  820 
class ordered_ring = ring + ordered_semiring 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

821 
+ ordered_ab_group_add + abs_if 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

822 
begin 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

823 

27516  824 
subclass pordered_ring .. 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

825 

7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

826 
subclass pordered_ab_group_add_abs 
28823  827 
proof 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

828 
fix a b 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

829 
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

830 
by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

831 
(auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric] 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

832 
neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg, 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

833 
auto intro!: less_imp_le add_neg_neg) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

834 
qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

835 

7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

836 
end 
23521  837 

25230  838 
(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors. 
839 
Basically, ordered_ring + no_zero_divisors = ordered_ring_strict. 

840 
*) 

841 
class ordered_ring_strict = ring + ordered_semiring_strict 

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

842 
+ ordered_ab_group_add + abs_if 
25230  843 
begin 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

844 

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

846 

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

847 
lemma mult_strict_left_mono_neg: 
25230  848 
"b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b" 
849 
apply (drule mult_strict_left_mono [of _ _ "uminus c"]) 

850 
apply (simp_all add: minus_mult_left [symmetric]) 

851 
done 

14738  852 

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

853 
lemma mult_strict_right_mono_neg: 
25230  854 
"b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c" 
855 
apply (drule mult_strict_right_mono [of _ _ "uminus c"]) 

856 
apply (simp_all add: minus_mult_right [symmetric]) 

857 
done 

14738  858 

25230  859 
lemma mult_neg_neg: 
860 
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 

861 
by (drule mult_strict_right_mono_neg, auto) 

14738  862 

25917  863 
subclass ring_no_zero_divisors 
28823  864 
proof 
25917  865 
fix a b 
866 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

867 
assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff) 

868 
have "a * b < 0 \<or> 0 < a * b" 

869 
proof (cases "a < 0") 

870 
case True note A' = this 

871 
show ?thesis proof (cases "b < 0") 

872 
case True with A' 

873 
show ?thesis by (auto dest: mult_neg_neg) 

874 
next 

875 
case False with B have "0 < b" by auto 

876 
with A' show ?thesis by (auto dest: mult_strict_right_mono) 

877 
qed 

878 
next 

879 
case False with A have A': "0 < a" by auto 

880 
show ?thesis proof (cases "b < 0") 

881 
case True with A' 

882 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

883 
next 

884 
case False with B have "0 < b" by auto 

885 
with A' show ?thesis by (auto dest: mult_pos_pos) 

886 
qed 

887 
qed 

888 
then show "a * b \<noteq> 0" by (simp add: neq_iff) 

889 
qed 

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

890 

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

891 
lemma zero_less_mult_iff: 
25917  892 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
893 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

894 
apply (simp_all add: not_less le_less) 

895 
apply (erule disjE) apply assumption defer 

896 
apply (erule disjE) defer apply (drule sym) apply simp 

897 
apply (erule disjE) defer apply (drule sym) apply simp 

898 
apply (erule disjE) apply assumption apply (drule sym) apply simp 

899 
apply (drule sym) apply simp 

900 
apply (blast dest: zero_less_mult_pos) 

25230  901 
apply (blast dest: zero_less_mult_pos2) 
902 
done 

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

903 

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

904 
lemma zero_le_mult_iff: 
25917  905 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
906 
by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) 

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

907 

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

908 
lemma mult_less_0_iff: 
25917  909 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
910 
apply (insert zero_less_mult_iff [of "a" b]) 

911 
apply (force simp add: minus_mult_left[symmetric]) 

912 
done 

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

913 

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

914 
lemma mult_le_0_iff: 
25917  915 
"a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b" 
916 
apply (insert zero_le_mult_iff [of "a" b]) 

917 
apply (force simp add: minus_mult_left[symmetric]) 

918 
done 

919 

920 
lemma zero_le_square [simp]: "0 \<le> a * a" 

921 
by (simp add: zero_le_mult_iff linear) 

922 

923 
lemma not_square_less_zero [simp]: "\<not> (a * a < 0)" 

924 
by (simp add: not_less) 

925 

26193  926 
text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, 
927 
also with the relations @{text "\<le>"} and equality.*} 

928 

929 
text{*These ``disjunction'' versions produce two cases when the comparison is 

930 
an assumption, but effectively four when the comparison is a goal.*} 

931 

932 
lemma mult_less_cancel_right_disj: 

933 
"a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a" 

934 
apply (cases "c = 0") 

935 
apply (auto simp add: neq_iff mult_strict_right_mono 

936 
mult_strict_right_mono_neg) 

937 
apply (auto simp add: not_less 

938 
not_le [symmetric, of "a*c"] 

939 
not_le [symmetric, of a]) 

940 
apply (erule_tac [!] notE) 

941 
apply (auto simp add: less_imp_le mult_right_mono 

942 
mult_right_mono_neg) 

943 
done 

944 

945 
lemma mult_less_cancel_left_disj: 

946 
"c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a" 

947 
apply (cases "c = 0") 

948 
apply (auto simp add: neq_iff mult_strict_left_mono 

949 
mult_strict_left_mono_neg) 

950 
apply (auto simp add: not_less 

951 
not_le [symmetric, of "c*a"] 

952 
not_le [symmetric, of a]) 

953 
apply (erule_tac [!] notE) 

954 
apply (auto simp add: less_imp_le mult_left_mono 

955 
mult_left_mono_neg) 

956 
done 

957 

958 
text{*The ``conjunction of implication'' lemmas produce two cases when the 

959 
comparison is a goal, but give four when the comparison is an assumption.*} 

960 

961 
lemma mult_less_cancel_right: 

962 
"a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)" 

963 
using mult_less_cancel_right_disj [of a c b] by auto 

964 

965 
lemma mult_less_cancel_left: 

966 
"c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)" 

967 
using mult_less_cancel_left_disj [of c a b] by auto 

968 

969 
lemma mult_le_cancel_right: 

970 
"a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 

971 
by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 

972 

973 
lemma mult_le_cancel_left: 

974 
"c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 

975 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 

976 

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

978 

25230  979 
text{*This list of rewrites simplifies ring terms by multiplying 
980 
everything out and bringing sums and products into a canonical form 

981 
(by ordered rewriting). As a result it decides ring equalities but 

982 
also helps with inequalities. *} 

983 
lemmas ring_simps = group_simps ring_distribs 

984 

985 

986 
class pordered_comm_ring = comm_ring + pordered_comm_semiring 

25267  987 
begin 
25230  988 

27516  989 
subclass pordered_ring .. 
990 
subclass pordered_cancel_comm_semiring .. 

25230  991 

25267  992 
end 
25230  993 

994 
class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + 

995 
(*previously ordered_semiring*) 

996 
assumes zero_less_one [simp]: "0 < 1" 

997 
begin 

998 

999 
lemma pos_add_strict: 

1000 
shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" 

1001 
using add_strict_mono [of zero a b c] by simp 

1002 

26193  1003 
lemma zero_le_one [simp]: "0 \<le> 1" 
1004 
by (rule zero_less_one [THEN less_imp_le]) 

1005 

1006 
lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0" 

1007 
by (simp add: not_le) 

1008 

1009 
lemma not_one_less_zero [simp]: "\<not> 1 < 0" 

1010 
by (simp add: not_less) 

1011 

1012 
lemma less_1_mult: 

1013 
assumes "1 < m" and "1 < n" 

1014 
shows "1 < m * n" 

1015 
using assms mult_strict_mono [of 1 m 1 n] 

1016 
by (simp add: less_trans [OF zero_less_one]) 

1017 

25230  1018 
end 
1019 

26193  1020 
class ordered_idom = comm_ring_1 + 
1021 
ordered_comm_semiring_strict + ordered_ab_group_add + 

25230  1022 
abs_if + sgn_if 
1023 
(*previously ordered_ring*) 

25917  1024 
begin 
1025 

27516  1026 
subclass ordered_ring_strict .. 
1027 
subclass pordered_comm_ring .. 

1028 
subclass idom .. 

25917  1029 

1030 
subclass ordered_semidom 

28823  1031 
proof 
26193  1032 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
1033 
thus "0 < 1" by (simp add: le_less) 

25917  1034 
qed 
1035 

26193  1036 
lemma linorder_neqE_ordered_idom: 
1037 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 

1038 
using assms by (rule neqE) 

1039 

26274  1040 
text {* These cancellation simprules also produce two cases when the comparison is a goal. *} 
1041 

1042 
lemma mult_le_cancel_right1: 

1043 
"c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)" 

1044 
by (insert mult_le_cancel_right [of 1 c b], simp) 

1045 

1046 
lemma mult_le_cancel_right2: 

1047 
"a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)" 

1048 
by (insert mult_le_cancel_right [of a c 1], simp) 

1049 

1050 
lemma mult_le_cancel_left1: 

1051 
"c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)" 

1052 
by (insert mult_le_cancel_left [of c 1 b], simp) 

1053 

1054 
lemma mult_le_cancel_left2: 

1055 
"c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)" 

1056 
by (insert mult_le_cancel_left [of c a 1], simp) 

1057 

1058 
lemma mult_less_cancel_right1: 

1059 
"c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)" 

1060 
by (insert mult_less_cancel_right [of 1 c b], simp) 

1061 

1062 
lemma mult_less_cancel_right2: 

1063 
"a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)" 

1064 
by (insert mult_less_cancel_right [of a c 1], simp) 

1065 

1066 
lemma mult_less_cancel_left1: 

1067 
"c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)" 

1068 
by (insert mult_less_cancel_left [of c 1 b], simp) 

1069 

1070 
lemma mult_less_cancel_left2: 

1071 
"c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)" 

1072 
by (insert mult_less_cancel_left [of c a 1], simp) 

1073 

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

1074 
lemma sgn_sgn [simp]: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1075 
"sgn (sgn a) = sgn a" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

1077 

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

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

1079 
"sgn a = 0 \<longleftrightarrow> a = 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

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

1081 

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

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

1083 
"sgn a = 1 \<longleftrightarrow> a > 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1084 
unfolding sgn_if by (simp add: neg_equal_zero) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1085 

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

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

1087 
"sgn a =  1 \<longleftrightarrow> a < 0" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1088 
unfolding sgn_if by (auto simp add: equal_neg_zero) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1089 

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

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

1091 
"sgn (a * b) = sgn a * sgn b" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1092 
by (auto simp add: sgn_if zero_less_mult_iff) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1093 

25917  1094 
end 
25230  1095 

1096 
class ordered_field = field + ordered_idom 

1097 

26274  1098 
text {* Simprules for comparisons where common factors can be cancelled. *} 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1099 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1100 
lemmas mult_compare_simps = 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1101 
mult_le_cancel_right mult_le_cancel_left 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1102 
mult_le_cancel_right1 mult_le_cancel_right2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1103 
mult_le_cancel_left1 mult_le_cancel_left2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1104 
mult_less_cancel_right mult_less_cancel_left 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1105 
mult_less_cancel_right1 mult_less_cancel_right2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1106 
mult_less_cancel_left1 mult_less_cancel_left2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1107 
mult_cancel_right mult_cancel_left 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1108 
mult_cancel_right1 mult_cancel_right2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1109 
mult_cancel_left1 mult_cancel_left2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1110 

26274  1111 
 {* FIXME continue localization here *} 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1112 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1113 
lemma inverse_nonzero_iff_nonzero [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1114 
"(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))" 
26274  1115 
by (force dest: inverse_zero_imp_zero) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1116 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1117 
lemma inverse_minus_eq [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1118 
"inverse(a) = inverse(a::'a::{division_ring,division_by_zero})" 
14377  1119 
proof cases 
1120 
assume "a=0" thus ?thesis by (simp add: inverse_zero) 

1121 
next 

1122 
assume "a\<noteq>0" 

1123 
thus ?thesis by (simp add: nonzero_inverse_minus_eq) 

1124 
qed 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1125 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1126 
lemma inverse_eq_imp_eq: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1127 
"inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" 
21328  1128 
apply (cases "a=0  b=0") 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1129 
apply (force dest!: inverse_zero_imp_zero 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1130 
simp add: eq_commute [of "0::'a"]) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1131 
apply (force dest!: nonzero_inverse_eq_imp_eq) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1132 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1133 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1134 
lemma inverse_eq_iff_eq [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1135 
"(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))" 
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1136 
by (force dest!: inverse_eq_imp_eq) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1137 

14270  1138 
lemma inverse_inverse_eq [simp]: 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1139 
"inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" 
14270  1140 
proof cases 
1141 
assume "a=0" thus ?thesis by simp 

1142 
next 

1143 
assume "a\<noteq>0" 

1144 
thus ?thesis by (simp add: nonzero_inverse_inverse_eq) 

1145 
qed 

1146 

1147 
text{*This version builds in division by zero while also reorienting 

1148 
the righthand side.*} 

1149 
lemma inverse_mult_distrib [simp]: 

1150 
"inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" 

1151 
proof cases 

1152 
assume "a \<noteq> 0 & b \<noteq> 0" 

22993  1153 
thus ?thesis 
1154 
by (simp add: nonzero_inverse_mult_distrib mult_commute) 

14270  1155 
next 
1156 
assume "~ (a \<noteq> 0 & b \<noteq> 0)" 

22993  1157 
thus ?thesis 
1158 
by force 

14270  1159 
qed 
1160 

1161 
text{*There is no slick version using division by zero.*} 

1162 
lemma inverse_add: 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1163 
"[a \<noteq> 0; b \<noteq> 0] 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1164 
==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)" 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

1165 
by (simp add: division_ring_inverse_add mult_ac) 
14270  1166 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1167 
lemma inverse_divide [simp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1168 
"inverse (a/b) = b / (a::'a::{field,division_by_zero})" 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1169 
by (simp add: divide_inverse mult_commute) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1170 

23389  1171 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1172 
subsection {* Calculations with fractions *} 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1173 

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1174 
text{* There is a whole bunch of simprules just for class @{text 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1175 
field} but none for class @{text field} and @{text nonzero_divides} 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1176 
because the latter are covered by a simproc. *} 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1177 

24427  1178 
lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1179 
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)" 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1180 
proof  
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1181 
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" 
23482  1182 
by (simp add: divide_inverse nonzero_inverse_mult_distrib) 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1183 
also have "... = a * inverse b * (inverse c * c)" 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1184 
by (simp only: mult_ac) 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1185 
also have "... = a * inverse b" 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1186 
by simp 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1187 
finally show ?thesis 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1188 
by (simp add: divide_inverse) 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1189 
qed 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1190 

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1191 
lemma mult_divide_mult_cancel_left: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1192 
"c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" 
21328  1193 
apply (cases "b = 0") 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1194 
apply (simp_all add: nonzero_mult_divide_mult_cancel_left) 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1195 
done 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1196 

24427  1197 
lemma nonzero_mult_divide_mult_cancel_right [noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1198 
"[b\<noteq>0; c\<noteq>0] ==> (a*c) / (b*c) = a/(b::'a::field)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1199 
by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
14321  1200 

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1201 
lemma mult_divide_mult_cancel_right: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1202 
"c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})" 
21328  1203 
apply (cases "b = 0") 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1204 
apply (simp_all add: nonzero_mult_divide_mult_cancel_right) 
14321  1205 
done 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1206 

14284
f1abe67c448a
reorganisation of Real/RealArith0.ML; more `Isar scripts
paulson
parents:
14277
diff
changeset

1207 
lemma divide_1 [simp]: "a/1 = (a::'a::field)" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1208 
by (simp add: divide_inverse) 
14284
f1abe67c448a
reorganisation of Real/RealArith0.ML; more `Isar scripts
paulson
parents:
14277
diff
changeset

1209 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1210 
lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1211 
by (simp add: divide_inverse mult_assoc) 
14288  1212 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1213 
lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1214 
by (simp add: divide_inverse mult_ac) 
14288  1215 

23482  1216 
lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left 
1217 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset

1218 
lemma divide_divide_eq_right [simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1219 
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1220 
by (simp add: divide_inverse mult_ac) 
14288  1221 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset

1222 
lemma divide_divide_eq_left [simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1223 
"(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1224 
by (simp add: divide_inverse mult_assoc) 
14288  1225 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1226 
lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==> 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1227 
x / y + w / z = (x * z + w * y) / (y * z)" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1228 
apply (subgoal_tac "x / y = (x * z) / (y * z)") 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1229 
apply (erule ssubst) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1230 
apply (subgoal_tac "w / z = (w * y) / (y * z)") 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1231 
apply (erule ssubst) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1232 
apply (rule add_divide_distrib [THEN sym]) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1233 
apply (subst mult_commute) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1234 
apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym]) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1235 
apply assumption 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1236 
apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym]) 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1237 
apply assumption 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1238 
done 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

1239 

23389  1240 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1241 
subsubsection{*Special Cancellation Simprules for Division*} 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1242 

24427  1243 
lemma mult_divide_mult_cancel_left_if[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1244 
fixes c :: "'a :: {field,division_by_zero}" 
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1245 
shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1246 
by (simp add: mult_divide_mult_cancel_left) 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1247 

24427  1248 
lemma nonzero_mult_divide_cancel_right[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1249 
"b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1250 
using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1251 

24427  1252 
lemma nonzero_mult_divide_cancel_left[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1253 
"a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1254 
using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1255 

5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1256 

24427  1257 
lemma nonzero_divide_mult_cancel_right[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1258 
"\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1259 
using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1260 

24427  1261 
lemma nonzero_divide_mult_cancel_left[simp,noatp]: 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1262 
"\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)" 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1263 
using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1264 

5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1265 

24427  1266 
lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1267 
"[b\<noteq>0; c\<noteq>0] ==> (c*a) / (b*c) = a/(b::'a::field)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1268 
using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac) 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1269 

24427  1270 
lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]: 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

1271 
"[b\<noteq>0; c\<noteq>0] ==> (a*c) / (c*b) = a/(b::'a::field)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1272 
using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac) 
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

1273 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1274 

14293  1275 
subsection {* Division and Unary Minus *} 
1276 

1277 
lemma nonzero_minus_divide_left: "b \<noteq> 0 ==>  (a/b) = (a) / (b::'a::field)" 

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

1278 
by (simp add: divide_inverse) 
14293  1279 

1280 
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==>  (a/b) = a / (b::'a::field)" 

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

1281 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 
14293  1282 

1283 
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (a)/(b) = a / (b::'a::field)" 

1284 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 

1285 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

1286 
lemma minus_divide_left: " (a/b) = (a) / (b::'a::field)" 
29407
5ef7e97fd9e4
move lemmas mult_minus{left,right} inside class ring
huffman
parents:
29406
diff
changeset

1287 
by (simp add: divide_inverse) 
14293  1288 

1289 
lemma minus_divide_right: " (a/b) = a / (b::'a::{field,division_by_zero})" 

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

1290 
by (simp add: divide_inverse) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset
