author  nipkow 
Sun, 15 Feb 2009 22:58:02 +0100  
changeset 29925  17d1e32ef867 
parent 29915  2146e512cec9 
child 29940  83b373f61d41 
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 + 
29667  27 
assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c" 
28 
assumes right_distrib[algebra_simps]: "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" 

29667  34 
by (simp add: left_distrib add_ac) 
25152  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 

29904  44 
class semiring_0_cancel = semiring + cancel_comm_monoid_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 
29667  50 
have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric]) 
51 
thus "0 * a = 0" by (simp only: add_left_cancel) 

25152  52 
next 
53 
fix a :: 'a 

29667  54 
have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric]) 
55 
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

56 
qed 
14940  57 

25186  58 
end 
25152  59 

22390  60 
class comm_semiring = ab_semigroup_add + ab_semigroup_mult + 
25062  61 
assumes distrib: "(a + b) * c = a * c + b * c" 
25152  62 
begin 
14504  63 

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

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

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

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

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

14504  72 
qed 
73 

25152  74 
end 
14504  75 

25152  76 
class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero 
77 
begin 

78 

27516  79 
subclass semiring_0 .. 
25152  80 

81 
end 

14504  82 

29904  83 
class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add 
25186  84 
begin 
14940  85 

27516  86 
subclass semiring_0_cancel .. 
14940  87 

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

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

89 

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

91 

22390  92 
class zero_neq_one = zero + one + 
25062  93 
assumes zero_neq_one [simp]: "0 \<noteq> 1" 
26193  94 
begin 
95 

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

29667  97 
by (rule not_sym) (rule zero_neq_one) 
26193  98 

99 
end 

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

100 

22390  101 
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 
14504  102 

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

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

104 

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

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

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

107 

28559  108 
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where 
109 
[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

110 

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

111 
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

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

113 

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

114 
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

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

116 

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

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

118 

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

119 
class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd 
22390  120 
(*previously almost_semiring*) 
25152  121 
begin 
14738  122 

27516  123 
subclass semiring_1 .. 
25152  124 

29925  125 
lemma dvd_refl[simp]: "a dvd a" 
28559  126 
proof 
127 
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

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

129 

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

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

131 
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

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

133 
proof  
28559  134 
from assms obtain v where "b = a * v" by (auto elim!: dvdE) 
135 
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

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

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

139 

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

140 
lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0" 
29667  141 
by (auto intro: dvd_refl elim!: dvdE) 
28559  142 

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

144 
proof 

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

145 
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

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 one_dvd [simp]: "1 dvd a" 
29667  149 
by (auto intro!: dvdI) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

150 

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

151 
lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)" 
29667  152 
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

153 

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

154 
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

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

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

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

158 

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

159 
lemma dvd_triv_right [simp]: "a dvd b * a" 
29667  160 
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

161 

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

162 
lemma dvd_triv_left [simp]: "a dvd a * b" 
29667  163 
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

164 

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

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

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

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

168 
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

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

170 
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

171 
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

172 
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

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

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

175 

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

176 
lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c" 
29667  177 
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

178 

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

179 
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

180 
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

181 

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

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

184 

29925  185 
lemma dvd_add[simp]: 
186 
assumes "a dvd b" and "a dvd c" 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

187 
proof  
29925  188 
from `a dvd b` obtain b' where "b = a * b'" .. 
189 
moreover from `a dvd c` obtain c' where "c = a * c'" .. 

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

190 
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

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

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

193 

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

195 

29925  196 

22390  197 
class no_zero_divisors = zero + times + 
25062  198 
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
14504  199 

29904  200 
class semiring_1_cancel = semiring + cancel_comm_monoid_add 
201 
+ zero_neq_one + monoid_mult 

25267  202 
begin 
14940  203 

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

205 

27516  206 
subclass semiring_1 .. 
25267  207 

208 
end 

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

209 

29904  210 
class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add 
211 
+ zero_neq_one + comm_monoid_mult 

25267  212 
begin 
14738  213 

27516  214 
subclass semiring_1_cancel .. 
215 
subclass comm_semiring_0_cancel .. 

216 
subclass comm_semiring_1 .. 

25267  217 

218 
end 

25152  219 

22390  220 
class ring = semiring + ab_group_add 
25267  221 
begin 
25152  222 

27516  223 
subclass semiring_0_cancel .. 
25152  224 

225 
text {* Distribution rules *} 

226 

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

29667  228 
by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 
25152  229 

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

29667  231 
by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
25152  232 

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

233 
text{*Extract signs from products*} 
29833  234 
lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric] 
235 
lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric] 

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

236 

25152  237 
lemma minus_mult_minus [simp]: " a *  b = a * b" 
29667  238 
by simp 
25152  239 

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

29667  241 
by simp 
242 

243 
lemma right_diff_distrib[algebra_simps]: "a * (b  c) = a * b  a * c" 

244 
by (simp add: right_distrib diff_minus) 

245 

246 
lemma left_diff_distrib[algebra_simps]: "(a  b) * c = a * c  b * c" 

247 
by (simp add: left_distrib diff_minus) 

25152  248 

29833  249 
lemmas ring_distribs[noatp] = 
25152  250 
right_distrib left_distrib left_diff_distrib right_diff_distrib 
251 

29667  252 
text{*Legacy  use @{text algebra_simps} *} 
29833  253 
lemmas ring_simps[noatp] = algebra_simps 
25230  254 

255 
lemma eq_add_iff1: 

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

29667  257 
by (simp add: algebra_simps) 
25230  258 

259 
lemma eq_add_iff2: 

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

29667  261 
by (simp add: algebra_simps) 
25230  262 

25152  263 
end 
264 

29833  265 
lemmas ring_distribs[noatp] = 
25152  266 
right_distrib left_distrib left_diff_distrib right_diff_distrib 
267 

22390  268 
class comm_ring = comm_semiring + ab_group_add 
25267  269 
begin 
14738  270 

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

272 
subclass comm_semiring_0_cancel .. 
25267  273 

274 
end 

14738  275 

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

278 

27516  279 
subclass semiring_1_cancel .. 
25267  280 

281 
end 

25152  282 

22390  283 
class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 
284 
(*previously ring*) 

25267  285 
begin 
14738  286 

27516  287 
subclass ring_1 .. 
288 
subclass comm_semiring_1_cancel .. 

25267  289 

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

290 
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

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

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

293 
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

294 
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

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

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

297 
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

298 
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

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

300 

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

301 
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

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

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

304 
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

305 
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

306 
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

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

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

309 
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

310 
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

311 
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

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

313 

29409  314 
lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y  z)" 
29667  315 
by (simp add: diff_minus dvd_add dvd_minus_iff) 
29409  316 

25267  317 
end 
25152  318 

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

319 
class ring_no_zero_divisors = ring + no_zero_divisors 
25230  320 
begin 
321 

322 
lemma mult_eq_0_iff [simp]: 

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

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

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

326 
then show ?thesis using no_zero_divisors by simp 

327 
next 

328 
case True then show ?thesis by auto 

329 
qed 

330 

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

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

334 
proof  

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

29667  336 
by (simp add: algebra_simps right_minus_eq) 
337 
thus ?thesis by (simp add: disj_commute right_minus_eq) 

26193  338 
qed 
339 

340 
lemma mult_cancel_left [simp, noatp]: 

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

342 
proof  

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

29667  344 
by (simp add: algebra_simps right_minus_eq) 
345 
thus ?thesis by (simp add: right_minus_eq) 

26193  346 
qed 
347 

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

349 

23544  350 
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 
26274  351 
begin 
352 

353 
lemma mult_cancel_right1 [simp]: 

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

29667  355 
by (insert mult_cancel_right [of 1 c b], force) 
26274  356 

357 
lemma mult_cancel_right2 [simp]: 

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

29667  359 
by (insert mult_cancel_right [of a c 1], simp) 
26274  360 

361 
lemma mult_cancel_left1 [simp]: 

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

29667  363 
by (insert mult_cancel_left [of c 1 b], force) 
26274  364 

365 
lemma mult_cancel_left2 [simp]: 

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

29667  367 
by (insert mult_cancel_left [of c a 1], simp) 
26274  368 

369 
end 

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

370 

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

373 

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

375 

29915
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

376 
lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a =  b)" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

377 
proof 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

378 
assume "a * a = b * b" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

379 
then have "(a  b) * (a + b) = 0" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

380 
by (simp add: algebra_simps) 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

381 
then show "a = b \<or> a =  b" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

382 
by (simp add: right_minus_eq eq_neg_iff_add_eq_0) 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

383 
next 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

384 
assume "a = b \<or> a =  b" 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

385 
then show "a * a = b * b" by auto 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

386 
qed 
2146e512cec9
generalize lemma fps_square_eq_iff, move to Ring_and_Field
huffman
parents:
29904
diff
changeset

387 

25186  388 
end 
25152  389 

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

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

394 

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

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

398 
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

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

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

401 
assume ab: "a * b = 0" 
29667  402 
hence "0 = inverse a * (a * b) * inverse b" by simp 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

403 
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

404 
by (simp only: mult_assoc) 
29667  405 
also have "\<dots> = 1" using a b by simp 
406 
finally show False by simp 

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

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

408 
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

409 

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

412 
proof 

413 
assume ianz: "inverse a = 0" 

414 
assume "a \<noteq> 0" 

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

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

417 
finally have "1 = 0" . 

418 
thus False by (simp add: eq_commute) 

419 
qed 

420 

421 
lemma inverse_zero_imp_zero: 

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

423 
apply (rule classical) 

424 
apply (drule nonzero_imp_inverse_nonzero) 

425 
apply auto 

426 
done 

427 

428 
lemma inverse_unique: 

429 
assumes ab: "a * b = 1" 

430 
shows "inverse a = b" 

431 
proof  

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

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

26274  435 
qed 
436 

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

29667  439 
by (rule inverse_unique) simp 
29406  440 

441 
lemma nonzero_inverse_inverse_eq: 

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

29667  443 
by (rule inverse_unique) simp 
29406  444 

445 
lemma nonzero_inverse_eq_imp_eq: 

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

447 
shows "a = b" 

448 
proof  

449 
from `inverse a = inverse b` 

29667  450 
have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) 
29406  451 
with `a \<noteq> 0` and `b \<noteq> 0` show "a = b" 
452 
by (simp add: nonzero_inverse_inverse_eq) 

453 
qed 

454 

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

29667  456 
by (rule inverse_unique) simp 
29406  457 

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

29667  462 
have "a * (b * inverse b) * inverse a = 1" using assms by simp 
463 
hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc) 

464 
thus ?thesis by (rule inverse_unique) 

26274  465 
qed 
466 

467 
lemma division_ring_inverse_add: 

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

29667  469 
by (simp add: algebra_simps) 
26274  470 

471 
lemma division_ring_inverse_diff: 

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

29667  473 
by (simp add: algebra_simps) 
26274  474 

25186  475 
end 
25152  476 

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

477 
class field = comm_ring_1 + inverse + 
25062  478 
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
479 
assumes divide_inverse: "a / b = a * inverse b" 

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

481 

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

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

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

486 
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

487 
thus "a * inverse a = 1" by (simp only: mult_commute) 
14738  488 
qed 
25230  489 

27516  490 
subclass idom .. 
25230  491 

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

493 
proof 

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

495 
{ 

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

497 
also assume "a / b = 1" 

498 
finally show "a = b" by simp 

499 
next 

500 
assume "a = b" 

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

502 
} 

503 
qed 

504 

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

29667  506 
by (simp add: divide_inverse) 
25230  507 

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

29667  509 
by (simp add: divide_inverse) 
25230  510 

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

29667  512 
by (simp add: divide_inverse) 
25230  513 

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

29667  515 
by (simp add: divide_inverse) 
25230  516 

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

29667  518 
by (simp add: divide_inverse algebra_simps) 
25230  519 

520 
end 

521 

22390  522 
class division_by_zero = zero + inverse + 
25062  523 
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

524 

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

29667  527 
by (simp add: divide_inverse) 
25230  528 

529 
lemma divide_self_if [simp]: 

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

29667  531 
by simp 
25230  532 

22390  533 
class mult_mono = times + zero + ord + 
25062  534 
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
535 
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

536 

22390  537 
class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
25230  538 
begin 
539 

540 
lemma mult_mono: 

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

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

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

544 
apply (erule mult_left_mono, assumption) 

545 
done 

546 

547 
lemma mult_mono': 

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

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

550 
apply (rule mult_mono) 

551 
apply (fast intro: order_trans)+ 

552 
done 

553 

554 
end 

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

555 

22390  556 
class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add 
29904  557 
+ semiring + cancel_comm_monoid_add 
25267  558 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

559 

27516  560 
subclass semiring_0_cancel .. 
561 
subclass pordered_semiring .. 

23521  562 

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

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

29667  567 
by (drule mult_left_mono [of b zero], auto) 
25230  568 

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

29667  570 
by (drule mult_right_mono [of b zero], auto) 
25230  571 

26234  572 
lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0)  (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
29667  573 
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) 
25230  574 

575 
end 

576 

577 
class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono 

25267  578 
begin 
25230  579 

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

581 

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

583 

25230  584 
lemma mult_left_less_imp_less: 
585 
"c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 

29667  586 
by (force simp add: mult_left_mono not_le [symmetric]) 
25230  587 

588 
lemma mult_right_less_imp_less: 

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

29667  590 
by (force simp add: mult_right_mono not_le [symmetric]) 
23521  591 

25186  592 
end 
25152  593 

22390  594 
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + 
25062  595 
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
596 
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 

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

598 

27516  599 
subclass semiring_0_cancel .. 
14940  600 

25267  601 
subclass ordered_semiring 
28823  602 
proof 
23550  603 
fix a b c :: 'a 
604 
assume A: "a \<le> b" "0 \<le> c" 

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

25186  606 
unfolding le_less 
607 
using mult_strict_left_mono by (cases "c = 0") auto 

23550  608 
from A show "a * c \<le> b * c" 
25152  609 
unfolding le_less 
25186  610 
using mult_strict_right_mono by (cases "c = 0") auto 
25152  611 
qed 
612 

25230  613 
lemma mult_left_le_imp_le: 
614 
"c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 

29667  615 
by (force simp add: mult_strict_left_mono _not_less [symmetric]) 
25230  616 

617 
lemma mult_right_le_imp_le: 

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

29667  619 
by (force simp add: mult_strict_right_mono not_less [symmetric]) 
25230  620 

621 
lemma mult_pos_pos: 

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

29667  623 
by (drule mult_strict_left_mono [of zero b], auto) 
25230  624 

625 
lemma mult_pos_neg: 

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

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

629 
lemma mult_pos_neg2: 

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

29667  631 
by (drule mult_strict_right_mono [of b zero], auto) 
25230  632 

633 
lemma zero_less_mult_pos: 

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

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

636 
apply (auto simp add: le_less not_less) 

637 
apply (drule_tac mult_pos_neg [of a b]) 

638 
apply (auto dest: less_not_sym) 

639 
done 

640 

641 
lemma zero_less_mult_pos2: 

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

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

644 
apply (auto simp add: le_less not_less) 

645 
apply (drule_tac mult_pos_neg2 [of a b]) 

646 
apply (auto dest: less_not_sym) 

647 
done 

648 

26193  649 
text{*Strict monotonicity in both arguments*} 
650 
lemma mult_strict_mono: 

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

652 
shows "a * c < b * d" 

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

654 
apply (simp add: mult_pos_pos) 

655 
apply (erule mult_strict_right_mono [THEN less_trans]) 

656 
apply (force simp add: le_less) 

657 
apply (erule mult_strict_left_mono, assumption) 

658 
done 

659 

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

661 
lemma mult_strict_mono': 

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

663 
shows "a * c < b * d" 

29667  664 
by (rule mult_strict_mono) (insert assms, auto) 
26193  665 

666 
lemma mult_less_le_imp_less: 

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

668 
shows "a * c < b * d" 

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

670 
apply (erule less_le_trans) 

671 
apply (erule mult_left_mono) 

672 
apply simp 

673 
apply (erule mult_strict_right_mono) 

674 
apply assumption 

675 
done 

676 

677 
lemma mult_le_less_imp_less: 

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

679 
shows "a * c < b * d" 

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

681 
apply (erule le_less_trans) 

682 
apply (erule mult_strict_left_mono) 

683 
apply simp 

684 
apply (erule mult_right_mono) 

685 
apply simp 

686 
done 

687 

688 
lemma mult_less_imp_less_left: 

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

690 
shows "a < b" 

691 
proof (rule ccontr) 

692 
assume "\<not> a < b" 

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

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

29667  695 
with this and less show False by (simp add: not_less [symmetric]) 
26193  696 
qed 
697 

698 
lemma mult_less_imp_less_right: 

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

700 
shows "a < b" 

701 
proof (rule ccontr) 

702 
assume "\<not> a < b" 

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

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

29667  705 
with this and less show False by (simp add: not_less [symmetric]) 
26193  706 
qed 
707 

25230  708 
end 
709 

22390  710 
class mult_mono1 = times + zero + ord + 
25230  711 
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 
14270  712 

22390  713 
class pordered_comm_semiring = comm_semiring_0 
714 
+ pordered_ab_semigroup_add + mult_mono1 

25186  715 
begin 
25152  716 

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

719 
fix a b c :: 'a 
23550  720 
assume "a \<le> b" "0 \<le> c" 
25230  721 
thus "c * a \<le> c * b" by (rule mult_mono1) 
23550  722 
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

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

724 

25267  725 
end 
726 

727 
class pordered_cancel_comm_semiring = comm_semiring_0_cancel 

728 
+ pordered_ab_semigroup_add + mult_mono1 

729 
begin 

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

730 

27516  731 
subclass pordered_comm_semiring .. 
732 
subclass pordered_cancel_semiring .. 

25267  733 

734 
end 

735 

736 
class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add + 

26193  737 
assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 
25267  738 
begin 
739 

740 
subclass ordered_semiring_strict 

28823  741 
proof 
23550  742 
fix a b c :: 'a 
743 
assume "a < b" "0 < c" 

26193  744 
thus "c * a < c * b" by (rule mult_strict_left_mono_comm) 
23550  745 
thus "a * c < b * c" by (simp only: mult_commute) 
746 
qed 

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

747 

25267  748 
subclass pordered_cancel_comm_semiring 
28823  749 
proof 
23550  750 
fix a b c :: 'a 
751 
assume "a \<le> b" "0 \<le> c" 

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

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

756 

25267  757 
end 
25230  758 

25267  759 
class pordered_ring = ring + pordered_cancel_semiring 
760 
begin 

25230  761 

27516  762 
subclass pordered_ab_group_add .. 
14270  763 

29667  764 
text{*Legacy  use @{text algebra_simps} *} 
29833  765 
lemmas ring_simps[noatp] = algebra_simps 
25230  766 

767 
lemma less_add_iff1: 

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

29667  769 
by (simp add: algebra_simps) 
25230  770 

771 
lemma less_add_iff2: 

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

29667  773 
by (simp add: algebra_simps) 
25230  774 

775 
lemma le_add_iff1: 

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

29667  777 
by (simp add: algebra_simps) 
25230  778 

779 
lemma le_add_iff2: 

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

29667  781 
by (simp add: algebra_simps) 
25230  782 

783 
lemma mult_left_mono_neg: 

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

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

786 
apply (simp_all add: minus_mult_left [symmetric]) 

787 
done 

788 

789 
lemma mult_right_mono_neg: 

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

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

792 
apply (simp_all add: minus_mult_right [symmetric]) 

793 
done 

794 

795 
lemma mult_nonpos_nonpos: 

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

29667  797 
by (drule mult_right_mono_neg [of a zero b]) auto 
25230  798 

799 
lemma split_mult_pos_le: 

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

29667  801 
by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) 
25186  802 

803 
end 

14270  804 

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

807 

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

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

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

813 

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

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

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

817 

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

819 

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

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

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

823 
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
29667  824 
by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos) 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

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

826 
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

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

828 
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

829 

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

830 
end 
23521  831 

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

834 
*) 

835 
class ordered_ring_strict = ring + ordered_semiring_strict 

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

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

838 

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

840 

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

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

844 
apply (simp_all add: minus_mult_left [symmetric]) 

845 
done 

14738  846 

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

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

850 
apply (simp_all add: minus_mult_right [symmetric]) 

851 
done 

14738  852 

25230  853 
lemma mult_neg_neg: 
854 
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 

29667  855 
by (drule mult_strict_right_mono_neg, auto) 
14738  856 

25917  857 
subclass ring_no_zero_divisors 
28823  858 
proof 
25917  859 
fix a b 
860 
assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 

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

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

863 
proof (cases "a < 0") 

864 
case True note A' = this 

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

866 
case True with A' 

867 
show ?thesis by (auto dest: mult_neg_neg) 

868 
next 

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

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

871 
qed 

872 
next 

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

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

875 
case True with A' 

876 
show ?thesis by (auto dest: mult_strict_right_mono_neg) 

877 
next 

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

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

880 
qed 

881 
qed 

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

883 
qed 

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

884 

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

885 
lemma zero_less_mult_iff: 
25917  886 
"0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
887 
apply (auto simp add: mult_pos_pos mult_neg_neg) 

888 
apply (simp_all add: not_less le_less) 

889 
apply (erule disjE) apply assumption defer 

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

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

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

893 
apply (drule sym) apply simp 

894 
apply (blast dest: zero_less_mult_pos) 

25230  895 
apply (blast dest: zero_less_mult_pos2) 
896 
done 

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

897 

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

898 
lemma zero_le_mult_iff: 
25917  899 
"0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
29667  900 
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

901 

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

902 
lemma mult_less_0_iff: 
25917  903 
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
904 
apply (insert zero_less_mult_iff [of "a" b]) 

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

906 
done 

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_le_0_iff: 
25917  909 
"a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b" 
910 
apply (insert zero_le_mult_iff [of "a" b]) 

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

912 
done 

913 

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

29667  915 
by (simp add: zero_le_mult_iff linear) 
25917  916 

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

29667  918 
by (simp add: not_less) 
25917  919 

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

922 

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

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

925 

926 
lemma mult_less_cancel_right_disj: 

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

928 
apply (cases "c = 0") 

929 
apply (auto simp add: neq_iff mult_strict_right_mono 

930 
mult_strict_right_mono_neg) 

931 
apply (auto simp add: not_less 

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

933 
not_le [symmetric, of a]) 

934 
apply (erule_tac [!] notE) 

935 
apply (auto simp add: less_imp_le mult_right_mono 

936 
mult_right_mono_neg) 

937 
done 

938 

939 
lemma mult_less_cancel_left_disj: 

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

941 
apply (cases "c = 0") 

942 
apply (auto simp add: neq_iff mult_strict_left_mono 

943 
mult_strict_left_mono_neg) 

944 
apply (auto simp add: not_less 

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

946 
not_le [symmetric, of a]) 

947 
apply (erule_tac [!] notE) 

948 
apply (auto simp add: less_imp_le mult_left_mono 

949 
mult_left_mono_neg) 

950 
done 

951 

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

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

954 

955 
lemma mult_less_cancel_right: 

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

957 
using mult_less_cancel_right_disj [of a c b] by auto 

958 

959 
lemma mult_less_cancel_left: 

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

961 
using mult_less_cancel_left_disj [of c a b] by auto 

962 

963 
lemma mult_le_cancel_right: 

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

29667  965 
by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 
26193  966 

967 
lemma mult_le_cancel_left: 

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

29667  969 
by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 
26193  970 

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

972 

29667  973 
text{*Legacy  use @{text algebra_simps} *} 
29833  974 
lemmas ring_simps[noatp] = algebra_simps 
25230  975 

976 

977 
class pordered_comm_ring = comm_ring + pordered_comm_semiring 

25267  978 
begin 
25230  979 

27516  980 
subclass pordered_ring .. 
981 
subclass pordered_cancel_comm_semiring .. 

25230  982 

25267  983 
end 
25230  984 

985 
class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict + 

986 
(*previously ordered_semiring*) 

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

988 
begin 

989 

990 
lemma pos_add_strict: 

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

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

993 

26193  994 
lemma zero_le_one [simp]: "0 \<le> 1" 
29667  995 
by (rule zero_less_one [THEN less_imp_le]) 
26193  996 

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

29667  998 
by (simp add: not_le) 
26193  999 

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

29667  1001 
by (simp add: not_less) 
26193  1002 

1003 
lemma less_1_mult: 

1004 
assumes "1 < m" and "1 < n" 

1005 
shows "1 < m * n" 

1006 
using assms mult_strict_mono [of 1 m 1 n] 

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

1008 

25230  1009 
end 
1010 

26193  1011 
class ordered_idom = comm_ring_1 + 
1012 
ordered_comm_semiring_strict + ordered_ab_group_add + 

25230  1013 
abs_if + sgn_if 
1014 
(*previously ordered_ring*) 

25917  1015 
begin 
1016 

27516  1017 
subclass ordered_ring_strict .. 
1018 
subclass pordered_comm_ring .. 

1019 
subclass idom .. 

25917  1020 

1021 
subclass ordered_semidom 

28823  1022 
proof 
26193  1023 
have "0 \<le> 1 * 1" by (rule zero_le_square) 
1024 
thus "0 < 1" by (simp add: le_less) 

25917  1025 
qed 
1026 

26193  1027 
lemma linorder_neqE_ordered_idom: 
1028 
assumes "x \<noteq> y" obtains "x < y"  "y < x" 

1029 
using assms by (rule neqE) 

1030 

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

1033 
lemma mult_le_cancel_right1: 

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

29667  1035 
by (insert mult_le_cancel_right [of 1 c b], simp) 
26274  1036 

1037 
lemma mult_le_cancel_right2: 

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

29667  1039 
by (insert mult_le_cancel_right [of a c 1], simp) 
26274  1040 

1041 
lemma mult_le_cancel_left1: 

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

29667  1043 
by (insert mult_le_cancel_left [of c 1 b], simp) 
26274  1044 

1045 
lemma mult_le_cancel_left2: 

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

29667  1047 
by (insert mult_le_cancel_left [of c a 1], simp) 
26274  1048 

1049 
lemma mult_less_cancel_right1: 

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

29667  1051 
by (insert mult_less_cancel_right [of 1 c b], simp) 
26274  1052 

1053 
lemma mult_less_cancel_right2: 

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

29667  1055 
by (insert mult_less_cancel_right [of a c 1], simp) 
26274  1056 

1057 
lemma mult_less_cancel_left1: 

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

29667  1059 
by (insert mult_less_cancel_left [of c 1 b], simp) 
26274  1060 

1061 
lemma mult_less_cancel_left2: 

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

29667  1063 
by (insert mult_less_cancel_left [of c a 1], simp) 
26274  1064 

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

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

1066 
"sgn (sgn a) = sgn a" 
29700  1067 
unfolding sgn_if by simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1068 

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

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

1070 
"sgn a = 0 \<longleftrightarrow> a = 0" 
29700  1071 
unfolding sgn_if by simp 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1072 

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

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

1074 
"sgn a = 1 \<longleftrightarrow> a > 0" 
29700  1075 
unfolding sgn_if by (simp add: neg_equal_zero) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1076 

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

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

1078 
"sgn a =  1 \<longleftrightarrow> a < 0" 
29700  1079 
unfolding sgn_if by (auto simp add: equal_neg_zero) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1080 

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

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

1082 
"sgn (a * b) = sgn a * sgn b" 
29667  1083 
by (auto simp add: sgn_if zero_less_mult_iff) 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27516
diff
changeset

1084 

29653  1085 
lemma abs_sgn: "abs k = k * sgn k" 
29700  1086 
unfolding sgn_if abs_if by auto 
1087 

1088 
(* The int instances are proved, these generic ones are tedious to prove here. 

1089 
And not very useful, as int seems to be the only instance. 

1090 
If needed, they should be proved later, when metis is available. 

1091 
lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k" 

1092 
proof 

1093 
have "\<forall>k.\<exists>ka.  (m * k) = m * ka" 

1094 
by(simp add: mult_minus_right[symmetric] del: mult_minus_right) 

1095 
moreover 

1096 
have "\<forall>k.\<exists>ka. m * k =  (m * ka)" 

1097 
by(auto intro!: minus_minus[symmetric] 

1098 
simp add: mult_minus_right[symmetric] simp del: mult_minus_right) 

1099 
ultimately show ?thesis by (auto simp: abs_if dvd_def) 

1100 
qed 

1101 

1102 
lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k" 

1103 
proof 

1104 
have "\<forall>k.\<exists>ka.  (m * k) = m * ka" 

1105 
by(simp add: mult_minus_right[symmetric] del: mult_minus_right) 

1106 
moreover 

1107 
have "\<forall>k.\<exists>ka.  (m * ka) = m * k" 

1108 
by(auto intro!: minus_minus 

1109 
simp add: mult_minus_right[symmetric] simp del: mult_minus_right) 

1110 
ultimately show ?thesis 

1111 
by (auto simp add:abs_if dvd_def minus_equation_iff[of k]) 

1112 
qed 

1113 
*) 

29653  1114 

25917  1115 
end 
25230  1116 

1117 
class ordered_field = field + ordered_idom 

1118 

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

1120 

29833  1121 
lemmas mult_compare_simps[noatp] = 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

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

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

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

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

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

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

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

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

1131 

26274  1132 
 {* FIXME continue localization here *} 
14268
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_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

1135 
"(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))" 
26274  1136 
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

1137 

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

1138 
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

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

1142 
next 

1143 
assume "a\<noteq>0" 

1144 
thus ?thesis by (simp add: nonzero_inverse_minus_eq) 

1145 
qed 

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

1146 

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

1147 
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

1148 
"inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" 
21328  1149 
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

1150 
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

1151 
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

1152 
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

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

1154 

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

1155 
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

1156 
"(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

1157 
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

1158 

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

1160 
"inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" 
14270  1161 
proof cases 
1162 
assume "a=0" thus ?thesis by simp 

1163 
next 

1164 
assume "a\<noteq>0" 

1165 
thus ?thesis by (simp add: nonzero_inverse_inverse_eq) 

1166 
qed 

1167 

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

1169 
the righthand side.*} 

1170 
lemma inverse_mult_distrib [simp]: 

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

1172 
proof cases 

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

29667  1174 
thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute) 
14270  1175 
next 
1176 
assume "~ (a \<noteq> 0 & b \<noteq> 0)" 

29667  1177 
thus ?thesis by force 
14270  1178 
qed 
1179 

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

1181 
lemma inverse_add: 

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

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

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

1184 
by (simp add: division_ring_inverse_add mult_ac) 
14270  1185 

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

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

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

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

1189 

23389  1190 

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

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

1192 

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

1193 
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

1194 
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

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

1196 

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

1198 
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

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

1200 
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" 
23482  1201 
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

1202 
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

1203 
by (simp only: mult_ac) 
29667  1204 
also have "... = a * inverse b" by simp 
1205 
finally show ?thesis by (simp add: divide_inverse) 

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

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

1207 

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

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

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

1211 
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

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

1213 

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

1215 
"[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

1216 
by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
14321  1217 

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

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

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

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

1223 

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

1224 
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

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

1226 

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

1227 
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

1228 
by (simp add: divide_inverse mult_assoc) 
14288  1229 

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

1230 
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

1231 
by (simp add: divide_inverse mult_ac) 
14288  1232 

29833  1233 
lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left 
23482  1234 

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

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

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

1237 
by (simp add: divide_inverse mult_ac) 
14288  1238 

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

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

1240 
"(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

1241 
by (simp add: divide_inverse mult_assoc) 
14288  1242 

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

1243 
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

1244 
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

1245 
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

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

1247 
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

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

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

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

1251 
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

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

1253 
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

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

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

1256 

23389  1257 

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

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

1259 

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

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

1262 
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

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

1264 

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

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

1267 
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

1268 

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

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

1271 
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

1272 

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

1273 

24427  1274 
lemma nonzero_divide_mult_cancel_right[simp,noatp]: 