author | haftmann |
Wed, 10 Feb 2010 08:49:26 +0100 | |
changeset 35084 | e25eedfc15ce |
parent 35050 | 9f841f20dca6 |
child 35090 | 88cc65ae046e |
permissions | -rw-r--r-- |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
1 |
(* Title: HOL/Fields.thy |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30961
diff
changeset
|
2 |
Author: Gertrud Bauer |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30961
diff
changeset
|
3 |
Author: Steven Obua |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30961
diff
changeset
|
4 |
Author: Tobias Nipkow |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30961
diff
changeset
|
5 |
Author: Lawrence C Paulson |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30961
diff
changeset
|
6 |
Author: Markus Wenzel |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30961
diff
changeset
|
7 |
Author: Jeremy Avigad |
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset
|
8 |
*) |
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset
|
9 |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
10 |
header {* Fields *} |
25152 | 11 |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
12 |
theory Fields |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
13 |
imports Rings |
25186 | 14 |
begin |
14421
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14398
diff
changeset
|
15 |
|
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset
|
16 |
class field = comm_ring_1 + inverse + |
35084 | 17 |
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" |
18 |
assumes field_divide_inverse: "a / b = a * inverse b" |
|
25267 | 19 |
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
|
20 |
|
25267 | 21 |
subclass division_ring |
28823 | 22 |
proof |
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset
|
23 |
fix a :: 'a |
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset
|
24 |
assume "a \<noteq> 0" |
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset
|
25 |
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
|
26 |
thus "a * inverse a = 1" by (simp only: mult_commute) |
35084 | 27 |
next |
28 |
fix a b :: 'a |
|
29 |
show "a / b = a * inverse b" by (rule field_divide_inverse) |
|
14738 | 30 |
qed |
25230 | 31 |
|
27516 | 32 |
subclass idom .. |
25230 | 33 |
|
34 |
lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b" |
|
35 |
proof |
|
36 |
assume neq: "b \<noteq> 0" |
|
37 |
{ |
|
38 |
hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) |
|
39 |
also assume "a / b = 1" |
|
40 |
finally show "a = b" by simp |
|
41 |
next |
|
42 |
assume "a = b" |
|
43 |
with neq show "a / b = 1" by (simp add: divide_inverse) |
|
44 |
} |
|
45 |
qed |
|
46 |
||
47 |
lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a" |
|
29667 | 48 |
by (simp add: divide_inverse) |
25230 | 49 |
|
50 |
lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1" |
|
29667 | 51 |
by (simp add: divide_inverse) |
25230 | 52 |
|
53 |
lemma divide_zero_left [simp]: "0 / a = 0" |
|
29667 | 54 |
by (simp add: divide_inverse) |
25230 | 55 |
|
56 |
lemma inverse_eq_divide: "inverse a = 1 / a" |
|
29667 | 57 |
by (simp add: divide_inverse) |
25230 | 58 |
|
59 |
lemma add_divide_distrib: "(a+b) / c = a/c + b/c" |
|
30630 | 60 |
by (simp add: divide_inverse algebra_simps) |
61 |
||
62 |
text{*There is no slick version using division by zero.*} |
|
63 |
lemma inverse_add: |
|
64 |
"[| a \<noteq> 0; b \<noteq> 0 |] |
|
65 |
==> inverse a + inverse b = (a + b) * inverse a * inverse b" |
|
66 |
by (simp add: division_ring_inverse_add mult_ac) |
|
67 |
||
68 |
lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]: |
|
69 |
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b" |
|
70 |
proof - |
|
71 |
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" |
|
72 |
by (simp add: divide_inverse nonzero_inverse_mult_distrib) |
|
73 |
also have "... = a * inverse b * (inverse c * c)" |
|
74 |
by (simp only: mult_ac) |
|
75 |
also have "... = a * inverse b" by simp |
|
76 |
finally show ?thesis by (simp add: divide_inverse) |
|
77 |
qed |
|
78 |
||
79 |
lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]: |
|
80 |
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b" |
|
81 |
by (simp add: mult_commute [of _ c]) |
|
82 |
||
83 |
lemma divide_1 [simp]: "a / 1 = a" |
|
84 |
by (simp add: divide_inverse) |
|
85 |
||
86 |
lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" |
|
87 |
by (simp add: divide_inverse mult_assoc) |
|
88 |
||
89 |
lemma times_divide_eq_left: "(b / c) * a = (b * a) / c" |
|
90 |
by (simp add: divide_inverse mult_ac) |
|
91 |
||
92 |
text {* These are later declared as simp rules. *} |
|
93 |
lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left |
|
94 |
||
95 |
lemma add_frac_eq: |
|
96 |
assumes "y \<noteq> 0" and "z \<noteq> 0" |
|
97 |
shows "x / y + w / z = (x * z + w * y) / (y * z)" |
|
98 |
proof - |
|
99 |
have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)" |
|
100 |
using assms by simp |
|
101 |
also have "\<dots> = (x * z + y * w) / (y * z)" |
|
102 |
by (simp only: add_divide_distrib) |
|
103 |
finally show ?thesis |
|
104 |
by (simp only: mult_commute) |
|
105 |
qed |
|
106 |
||
107 |
text{*Special Cancellation Simprules for Division*} |
|
108 |
||
109 |
lemma nonzero_mult_divide_cancel_right [simp, noatp]: |
|
110 |
"b \<noteq> 0 \<Longrightarrow> a * b / b = a" |
|
111 |
using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp |
|
112 |
||
113 |
lemma nonzero_mult_divide_cancel_left [simp, noatp]: |
|
114 |
"a \<noteq> 0 \<Longrightarrow> a * b / a = b" |
|
115 |
using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp |
|
116 |
||
117 |
lemma nonzero_divide_mult_cancel_right [simp, noatp]: |
|
118 |
"\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a" |
|
119 |
using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp |
|
120 |
||
121 |
lemma nonzero_divide_mult_cancel_left [simp, noatp]: |
|
122 |
"\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b" |
|
123 |
using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp |
|
124 |
||
125 |
lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]: |
|
126 |
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b" |
|
127 |
using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac) |
|
128 |
||
129 |
lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]: |
|
130 |
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b" |
|
131 |
using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac) |
|
132 |
||
133 |
lemma minus_divide_left: "- (a / b) = (-a) / b" |
|
134 |
by (simp add: divide_inverse) |
|
135 |
||
136 |
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)" |
|
137 |
by (simp add: divide_inverse nonzero_inverse_minus_eq) |
|
138 |
||
139 |
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b" |
|
140 |
by (simp add: divide_inverse nonzero_inverse_minus_eq) |
|
141 |
||
142 |
lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)" |
|
143 |
by (simp add: divide_inverse) |
|
144 |
||
145 |
lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" |
|
146 |
by (simp add: diff_minus add_divide_distrib) |
|
147 |
||
148 |
lemma add_divide_eq_iff: |
|
149 |
"z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z" |
|
150 |
by (simp add: add_divide_distrib) |
|
151 |
||
152 |
lemma divide_add_eq_iff: |
|
153 |
"z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z" |
|
154 |
by (simp add: add_divide_distrib) |
|
155 |
||
156 |
lemma diff_divide_eq_iff: |
|
157 |
"z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z" |
|
158 |
by (simp add: diff_divide_distrib) |
|
159 |
||
160 |
lemma divide_diff_eq_iff: |
|
161 |
"z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z" |
|
162 |
by (simp add: diff_divide_distrib) |
|
163 |
||
164 |
lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b" |
|
165 |
proof - |
|
166 |
assume [simp]: "c \<noteq> 0" |
|
167 |
have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp |
|
168 |
also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc) |
|
169 |
finally show ?thesis . |
|
170 |
qed |
|
171 |
||
172 |
lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c" |
|
173 |
proof - |
|
174 |
assume [simp]: "c \<noteq> 0" |
|
175 |
have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp |
|
176 |
also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) |
|
177 |
finally show ?thesis . |
|
178 |
qed |
|
179 |
||
180 |
lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a" |
|
181 |
by simp |
|
182 |
||
183 |
lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c" |
|
184 |
by (erule subst, simp) |
|
185 |
||
186 |
lemmas field_eq_simps[noatp] = algebra_simps |
|
187 |
(* pull / out*) |
|
188 |
add_divide_eq_iff divide_add_eq_iff |
|
189 |
diff_divide_eq_iff divide_diff_eq_iff |
|
190 |
(* multiply eqn *) |
|
191 |
nonzero_eq_divide_eq nonzero_divide_eq_eq |
|
192 |
(* is added later: |
|
193 |
times_divide_eq_left times_divide_eq_right |
|
194 |
*) |
|
195 |
||
196 |
text{*An example:*} |
|
197 |
lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1" |
|
198 |
apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0") |
|
199 |
apply(simp add:field_eq_simps) |
|
200 |
apply(simp) |
|
201 |
done |
|
202 |
||
203 |
lemma diff_frac_eq: |
|
204 |
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)" |
|
205 |
by (simp add: field_eq_simps times_divide_eq) |
|
206 |
||
207 |
lemma frac_eq_eq: |
|
208 |
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)" |
|
209 |
by (simp add: field_eq_simps times_divide_eq) |
|
25230 | 210 |
|
211 |
end |
|
212 |
||
22390 | 213 |
class division_by_zero = zero + inverse + |
25062 | 214 |
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
|
215 |
|
25230 | 216 |
lemma divide_zero [simp]: |
217 |
"a / 0 = (0::'a::{field,division_by_zero})" |
|
29667 | 218 |
by (simp add: divide_inverse) |
25230 | 219 |
|
220 |
lemma divide_self_if [simp]: |
|
221 |
"a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" |
|
29667 | 222 |
by simp |
25230 | 223 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
224 |
class linordered_field = field + linordered_idom |
25230 | 225 |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
226 |
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
|
227 |
"(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))" |
26274 | 228 |
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
|
229 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
230 |
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
|
231 |
"inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})" |
14377 | 232 |
proof cases |
233 |
assume "a=0" thus ?thesis by (simp add: inverse_zero) |
|
234 |
next |
|
235 |
assume "a\<noteq>0" |
|
236 |
thus ?thesis by (simp add: nonzero_inverse_minus_eq) |
|
237 |
qed |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
238 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
239 |
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
|
240 |
"inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" |
21328 | 241 |
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
|
242 |
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
|
243 |
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
|
244 |
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
|
245 |
done |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
246 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
247 |
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
|
248 |
"(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
|
249 |
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
|
250 |
|
14270 | 251 |
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
|
252 |
"inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" |
14270 | 253 |
proof cases |
254 |
assume "a=0" thus ?thesis by simp |
|
255 |
next |
|
256 |
assume "a\<noteq>0" |
|
257 |
thus ?thesis by (simp add: nonzero_inverse_inverse_eq) |
|
258 |
qed |
|
259 |
||
260 |
text{*This version builds in division by zero while also re-orienting |
|
261 |
the right-hand side.*} |
|
262 |
lemma inverse_mult_distrib [simp]: |
|
263 |
"inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" |
|
264 |
proof cases |
|
265 |
assume "a \<noteq> 0 & b \<noteq> 0" |
|
29667 | 266 |
thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute) |
14270 | 267 |
next |
268 |
assume "~ (a \<noteq> 0 & b \<noteq> 0)" |
|
29667 | 269 |
thus ?thesis by force |
14270 | 270 |
qed |
271 |
||
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
272 |
lemma inverse_divide [simp]: |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
273 |
"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
|
274 |
by (simp add: divide_inverse mult_commute) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
275 |
|
23389 | 276 |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
277 |
subsection {* Calculations with fractions *} |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
278 |
|
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
279 |
text{* There is a whole bunch of simp-rules just for class @{text |
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
280 |
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
|
281 |
because the latter are covered by a simproc. *} |
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
282 |
|
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
283 |
lemma mult_divide_mult_cancel_left: |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
284 |
"c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" |
21328 | 285 |
apply (cases "b = 0") |
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
286 |
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
|
287 |
done |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
288 |
|
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
289 |
lemma mult_divide_mult_cancel_right: |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
290 |
"c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})" |
21328 | 291 |
apply (cases "b = 0") |
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
292 |
apply (simp_all add: nonzero_mult_divide_mult_cancel_right) |
14321 | 293 |
done |
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
294 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
295 |
lemma divide_divide_eq_right [simp,noatp]: |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
296 |
"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
|
297 |
by (simp add: divide_inverse mult_ac) |
14288 | 298 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
299 |
lemma divide_divide_eq_left [simp,noatp]: |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
300 |
"(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
|
301 |
by (simp add: divide_inverse mult_assoc) |
14288 | 302 |
|
23389 | 303 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
304 |
subsubsection{*Special Cancellation Simprules for Division*} |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
305 |
|
24427 | 306 |
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
|
307 |
fixes c :: "'a :: {field,division_by_zero}" |
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
308 |
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
|
309 |
by (simp add: mult_divide_mult_cancel_left) |
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset
|
310 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
311 |
|
14293 | 312 |
subsection {* Division and Unary Minus *} |
313 |
||
314 |
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
|
315 |
by (simp add: divide_inverse) |
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset
|
316 |
|
30630 | 317 |
lemma divide_minus_right [simp, noatp]: |
318 |
"a / -(b::'a::{field,division_by_zero}) = -(a / b)" |
|
319 |
by (simp add: divide_inverse) |
|
320 |
||
321 |
lemma minus_divide_divide: |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
322 |
"(-a)/(-b) = a / (b::'a::{field,division_by_zero})" |
21328 | 323 |
apply (cases "b=0", simp) |
14293 | 324 |
apply (simp add: nonzero_minus_divide_divide) |
325 |
done |
|
326 |
||
23482 | 327 |
lemma eq_divide_eq: |
328 |
"((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)" |
|
30630 | 329 |
by (simp add: nonzero_eq_divide_eq) |
23482 | 330 |
|
331 |
lemma divide_eq_eq: |
|
332 |
"(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)" |
|
30630 | 333 |
by (force simp add: nonzero_divide_eq_eq) |
14293 | 334 |
|
23389 | 335 |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
336 |
subsection {* Ordered Fields *} |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
337 |
|
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
338 |
lemma positive_imp_inverse_positive: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
339 |
assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::linordered_field)" |
23482 | 340 |
proof - |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
341 |
have "0 < a * inverse a" |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
342 |
by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
343 |
thus "0 < inverse a" |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
344 |
by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff) |
23482 | 345 |
qed |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
346 |
|
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
347 |
lemma negative_imp_inverse_negative: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
348 |
"a < 0 ==> inverse a < (0::'a::linordered_field)" |
23482 | 349 |
by (insert positive_imp_inverse_positive [of "-a"], |
350 |
simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
351 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
352 |
lemma inverse_le_imp_le: |
23482 | 353 |
assumes invle: "inverse a \<le> inverse b" and apos: "0 < a" |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
354 |
shows "b \<le> (a::'a::linordered_field)" |
23482 | 355 |
proof (rule classical) |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
356 |
assume "~ b \<le> a" |
23482 | 357 |
hence "a < b" by (simp add: linorder_not_le) |
358 |
hence bpos: "0 < b" by (blast intro: apos order_less_trans) |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
359 |
hence "a * inverse a \<le> a * inverse b" |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
360 |
by (simp add: apos invle order_less_imp_le mult_left_mono) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
361 |
hence "(a * inverse a) * b \<le> (a * inverse b) * b" |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
362 |
by (simp add: bpos order_less_imp_le mult_right_mono) |
23482 | 363 |
thus "b \<le> a" by (simp add: mult_assoc apos bpos order_less_imp_not_eq2) |
364 |
qed |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
365 |
|
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
366 |
lemma inverse_positive_imp_positive: |
23482 | 367 |
assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0" |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
368 |
shows "0 < (a::'a::linordered_field)" |
23389 | 369 |
proof - |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
370 |
have "0 < inverse (inverse a)" |
23389 | 371 |
using inv_gt_0 by (rule positive_imp_inverse_positive) |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
372 |
thus "0 < a" |
23389 | 373 |
using nz by (simp add: nonzero_inverse_inverse_eq) |
374 |
qed |
|
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
375 |
|
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
376 |
lemma inverse_positive_iff_positive [simp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
377 |
"(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))" |
21328 | 378 |
apply (cases "a = 0", simp) |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
379 |
apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
380 |
done |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
381 |
|
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
382 |
lemma inverse_negative_imp_negative: |
23482 | 383 |
assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0" |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
384 |
shows "a < (0::'a::linordered_field)" |
23389 | 385 |
proof - |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
386 |
have "inverse (inverse a) < 0" |
23389 | 387 |
using inv_less_0 by (rule negative_imp_inverse_negative) |
23482 | 388 |
thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq) |
23389 | 389 |
qed |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
390 |
|
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
391 |
lemma inverse_negative_iff_negative [simp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
392 |
"(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))" |
21328 | 393 |
apply (cases "a = 0", simp) |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
394 |
apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
395 |
done |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
396 |
|
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
397 |
lemma inverse_nonnegative_iff_nonnegative [simp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
398 |
"(0 \<le> inverse a) = (0 \<le> (a::'a::{linordered_field,division_by_zero}))" |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
399 |
by (simp add: linorder_not_less [symmetric]) |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
400 |
|
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
401 |
lemma inverse_nonpositive_iff_nonpositive [simp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
402 |
"(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))" |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
403 |
by (simp add: linorder_not_less [symmetric]) |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
404 |
|
35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset
|
405 |
lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)" |
23406
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
406 |
proof |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
407 |
fix x::'a |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
408 |
have m1: "- (1::'a) < 0" by simp |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
409 |
from add_strict_right_mono[OF m1, where c=x] |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
410 |
have "(- 1) + x < x" by simp |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
411 |
thus "\<exists>y. y < x" by blast |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
412 |
qed |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
413 |
|
35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35032
diff
changeset
|
414 |
lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)" |
23406
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
415 |
proof |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
416 |
fix x::'a |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
417 |
have m1: " (1::'a) > 0" by simp |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
418 |
from add_strict_right_mono[OF m1, where c=x] |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
419 |
have "1 + x > x" by simp |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
420 |
thus "\<exists>y. y > x" by blast |
167b53019d6f
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
chaieb
parents:
23400
diff
changeset
|
421 |
qed |
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
422 |
|
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
423 |
subsection{*Anti-Monotonicity of @{term inverse}*} |
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
424 |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
425 |
lemma less_imp_inverse_less: |
23482 | 426 |
assumes less: "a < b" and apos: "0 < a" |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
427 |
shows "inverse b < inverse (a::'a::linordered_field)" |
23482 | 428 |
proof (rule ccontr) |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
429 |
assume "~ inverse b < inverse a" |
29667 | 430 |
hence "inverse a \<le> inverse b" by (simp add: linorder_not_less) |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
431 |
hence "~ (a < b)" |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
432 |
by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos]) |
29667 | 433 |
thus False by (rule notE [OF _ less]) |
23482 | 434 |
qed |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
435 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
436 |
lemma inverse_less_imp_less: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
437 |
"[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)" |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
438 |
apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"]) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
439 |
apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
440 |
done |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
441 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
442 |
text{*Both premises are essential. Consider -1 and 1.*} |
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
443 |
lemma inverse_less_iff_less [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
444 |
"[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
445 |
by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
446 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
447 |
lemma le_imp_inverse_le: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
448 |
"[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)" |
23482 | 449 |
by (force simp add: order_le_less less_imp_inverse_less) |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
450 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
451 |
lemma inverse_le_iff_le [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
452 |
"[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))" |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
453 |
by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
454 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
455 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
456 |
text{*These results refer to both operands being negative. The opposite-sign |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
457 |
case is trivial, since inverse preserves signs.*} |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
458 |
lemma inverse_le_imp_le_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
459 |
"[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::linordered_field)" |
23482 | 460 |
apply (rule classical) |
461 |
apply (subgoal_tac "a < 0") |
|
462 |
prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) |
|
463 |
apply (insert inverse_le_imp_le [of "-b" "-a"]) |
|
464 |
apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) |
|
465 |
done |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
466 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
467 |
lemma less_imp_inverse_less_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
468 |
"[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)" |
23482 | 469 |
apply (subgoal_tac "a < 0") |
470 |
prefer 2 apply (blast intro: order_less_trans) |
|
471 |
apply (insert less_imp_inverse_less [of "-b" "-a"]) |
|
472 |
apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) |
|
473 |
done |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
474 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
475 |
lemma inverse_less_imp_less_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
476 |
"[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)" |
23482 | 477 |
apply (rule classical) |
478 |
apply (subgoal_tac "a < 0") |
|
479 |
prefer 2 |
|
480 |
apply (force simp add: linorder_not_less intro: order_le_less_trans) |
|
481 |
apply (insert inverse_less_imp_less [of "-b" "-a"]) |
|
482 |
apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) |
|
483 |
done |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
484 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
485 |
lemma inverse_less_iff_less_neg [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
486 |
"[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" |
23482 | 487 |
apply (insert inverse_less_iff_less [of "-b" "-a"]) |
488 |
apply (simp del: inverse_less_iff_less |
|
489 |
add: order_less_imp_not_eq nonzero_inverse_minus_eq) |
|
490 |
done |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
491 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
492 |
lemma le_imp_inverse_le_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
493 |
"[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)" |
23482 | 494 |
by (force simp add: order_le_less less_imp_inverse_less_neg) |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
495 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
496 |
lemma inverse_le_iff_le_neg [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
497 |
"[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))" |
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset
|
498 |
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) |
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset
|
499 |
|
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset
|
500 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
501 |
subsection{*Inverses and the Number One*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
502 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
503 |
lemma one_less_inverse_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
504 |
"(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))" |
23482 | 505 |
proof cases |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
506 |
assume "0 < x" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
507 |
with inverse_less_iff_less [OF zero_less_one, of x] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
508 |
show ?thesis by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
509 |
next |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
510 |
assume notless: "~ (0 < x)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
511 |
have "~ (1 < inverse x)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
512 |
proof |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
513 |
assume "1 < inverse x" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
514 |
also with notless have "... \<le> 0" by (simp add: linorder_not_less) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
515 |
also have "... < 1" by (rule zero_less_one) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
516 |
finally show False by auto |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
517 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
518 |
with notless show ?thesis by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
519 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
520 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
521 |
lemma inverse_eq_1_iff [simp]: |
23482 | 522 |
"(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
523 |
by (insert inverse_eq_iff_eq [of x 1], simp) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
524 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
525 |
lemma one_le_inverse_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
526 |
"(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
527 |
by (force simp add: order_le_less one_less_inverse_iff zero_less_one |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
528 |
eq_commute [of 1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
529 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
530 |
lemma inverse_less_1_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
531 |
"(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{linordered_field,division_by_zero}))" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
532 |
by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
533 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
534 |
lemma inverse_le_1_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
535 |
"(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_by_zero}))" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
536 |
by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
537 |
|
23389 | 538 |
|
14288 | 539 |
subsection{*Simplification of Inequalities Involving Literal Divisors*} |
540 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
541 |
lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \<le> b/c) = (a*c \<le> b)" |
14288 | 542 |
proof - |
543 |
assume less: "0<c" |
|
544 |
hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)" |
|
545 |
by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) |
|
546 |
also have "... = (a*c \<le> b)" |
|
547 |
by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) |
|
548 |
finally show ?thesis . |
|
549 |
qed |
|
550 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
551 |
lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \<le> b/c) = (b \<le> a*c)" |
14288 | 552 |
proof - |
553 |
assume less: "c<0" |
|
554 |
hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)" |
|
555 |
by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) |
|
556 |
also have "... = (b \<le> a*c)" |
|
557 |
by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) |
|
558 |
finally show ?thesis . |
|
559 |
qed |
|
560 |
||
561 |
lemma le_divide_eq: |
|
562 |
"(a \<le> b/c) = |
|
563 |
(if 0 < c then a*c \<le> b |
|
564 |
else if c < 0 then b \<le> a*c |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
565 |
else a \<le> (0::'a::{linordered_field,division_by_zero}))" |
21328 | 566 |
apply (cases "c=0", simp) |
14288 | 567 |
apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) |
568 |
done |
|
569 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
570 |
lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \<le> a) = (b \<le> a*c)" |
14288 | 571 |
proof - |
572 |
assume less: "0<c" |
|
573 |
hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)" |
|
574 |
by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) |
|
575 |
also have "... = (b \<le> a*c)" |
|
576 |
by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) |
|
577 |
finally show ?thesis . |
|
578 |
qed |
|
579 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
580 |
lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \<le> a) = (a*c \<le> b)" |
14288 | 581 |
proof - |
582 |
assume less: "c<0" |
|
583 |
hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)" |
|
584 |
by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) |
|
585 |
also have "... = (a*c \<le> b)" |
|
586 |
by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) |
|
587 |
finally show ?thesis . |
|
588 |
qed |
|
589 |
||
590 |
lemma divide_le_eq: |
|
591 |
"(b/c \<le> a) = |
|
592 |
(if 0 < c then b \<le> a*c |
|
593 |
else if c < 0 then a*c \<le> b |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
594 |
else 0 \<le> (a::'a::{linordered_field,division_by_zero}))" |
21328 | 595 |
apply (cases "c=0", simp) |
14288 | 596 |
apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) |
597 |
done |
|
598 |
||
599 |
lemma pos_less_divide_eq: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
600 |
"0 < (c::'a::linordered_field) ==> (a < b/c) = (a*c < b)" |
14288 | 601 |
proof - |
602 |
assume less: "0<c" |
|
603 |
hence "(a < b/c) = (a*c < (b/c)*c)" |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
604 |
by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) |
14288 | 605 |
also have "... = (a*c < b)" |
606 |
by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) |
|
607 |
finally show ?thesis . |
|
608 |
qed |
|
609 |
||
610 |
lemma neg_less_divide_eq: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
611 |
"c < (0::'a::linordered_field) ==> (a < b/c) = (b < a*c)" |
14288 | 612 |
proof - |
613 |
assume less: "c<0" |
|
614 |
hence "(a < b/c) = ((b/c)*c < a*c)" |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
615 |
by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) |
14288 | 616 |
also have "... = (b < a*c)" |
617 |
by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) |
|
618 |
finally show ?thesis . |
|
619 |
qed |
|
620 |
||
621 |
lemma less_divide_eq: |
|
622 |
"(a < b/c) = |
|
623 |
(if 0 < c then a*c < b |
|
624 |
else if c < 0 then b < a*c |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
625 |
else a < (0::'a::{linordered_field,division_by_zero}))" |
21328 | 626 |
apply (cases "c=0", simp) |
14288 | 627 |
apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) |
628 |
done |
|
629 |
||
630 |
lemma pos_divide_less_eq: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
631 |
"0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)" |
14288 | 632 |
proof - |
633 |
assume less: "0<c" |
|
634 |
hence "(b/c < a) = ((b/c)*c < a*c)" |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
635 |
by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) |
14288 | 636 |
also have "... = (b < a*c)" |
637 |
by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) |
|
638 |
finally show ?thesis . |
|
639 |
qed |
|
640 |
||
641 |
lemma neg_divide_less_eq: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
642 |
"c < (0::'a::linordered_field) ==> (b/c < a) = (a*c < b)" |
14288 | 643 |
proof - |
644 |
assume less: "c<0" |
|
645 |
hence "(b/c < a) = (a*c < (b/c)*c)" |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
646 |
by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) |
14288 | 647 |
also have "... = (a*c < b)" |
648 |
by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) |
|
649 |
finally show ?thesis . |
|
650 |
qed |
|
651 |
||
652 |
lemma divide_less_eq: |
|
653 |
"(b/c < a) = |
|
654 |
(if 0 < c then b < a*c |
|
655 |
else if c < 0 then a*c < b |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
656 |
else 0 < (a::'a::{linordered_field,division_by_zero}))" |
21328 | 657 |
apply (cases "c=0", simp) |
14288 | 658 |
apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) |
659 |
done |
|
660 |
||
23482 | 661 |
|
662 |
subsection{*Field simplification*} |
|
663 |
||
29667 | 664 |
text{* Lemmas @{text field_simps} multiply with denominators in in(equations) |
665 |
if they can be proved to be non-zero (for equations) or positive/negative |
|
666 |
(for inequations). Can be too aggressive and is therefore separate from the |
|
667 |
more benign @{text algebra_simps}. *} |
|
14288 | 668 |
|
29833 | 669 |
lemmas field_simps[noatp] = field_eq_simps |
23482 | 670 |
(* multiply ineqn *) |
671 |
pos_divide_less_eq neg_divide_less_eq |
|
672 |
pos_less_divide_eq neg_less_divide_eq |
|
673 |
pos_divide_le_eq neg_divide_le_eq |
|
674 |
pos_le_divide_eq neg_le_divide_eq |
|
14288 | 675 |
|
23482 | 676 |
text{* Lemmas @{text sign_simps} is a first attempt to automate proofs |
23483 | 677 |
of positivity/negativity needed for @{text field_simps}. Have not added @{text |
23482 | 678 |
sign_simps} to @{text field_simps} because the former can lead to case |
679 |
explosions. *} |
|
14288 | 680 |
|
29833 | 681 |
lemmas sign_simps[noatp] = group_simps |
23482 | 682 |
zero_less_mult_iff mult_less_0_iff |
14288 | 683 |
|
23482 | 684 |
(* Only works once linear arithmetic is installed: |
685 |
text{*An example:*} |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
686 |
lemma fixes a b c d e f :: "'a::linordered_field" |
23482 | 687 |
shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow> |
688 |
((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < |
|
689 |
((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u" |
|
690 |
apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0") |
|
691 |
prefer 2 apply(simp add:sign_simps) |
|
692 |
apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0") |
|
693 |
prefer 2 apply(simp add:sign_simps) |
|
694 |
apply(simp add:field_simps) |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
695 |
done |
23482 | 696 |
*) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
697 |
|
23389 | 698 |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
699 |
subsection{*Division and Signs*} |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
700 |
|
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
701 |
lemma zero_less_divide_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
702 |
"((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
703 |
by (simp add: divide_inverse zero_less_mult_iff) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
704 |
|
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
705 |
lemma divide_less_0_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
706 |
"(a/b < (0::'a::{linordered_field,division_by_zero})) = |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
707 |
(0 < a & b < 0 | a < 0 & 0 < b)" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
708 |
by (simp add: divide_inverse mult_less_0_iff) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
709 |
|
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
710 |
lemma zero_le_divide_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
711 |
"((0::'a::{linordered_field,division_by_zero}) \<le> a/b) = |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
712 |
(0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
713 |
by (simp add: divide_inverse zero_le_mult_iff) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
714 |
|
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
715 |
lemma divide_le_0_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
716 |
"(a/b \<le> (0::'a::{linordered_field,division_by_zero})) = |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
717 |
(0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
718 |
by (simp add: divide_inverse mult_le_0_iff) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
719 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
720 |
lemma divide_eq_0_iff [simp,noatp]: |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
721 |
"(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" |
23482 | 722 |
by (simp add: divide_inverse) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
723 |
|
23482 | 724 |
lemma divide_pos_pos: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
725 |
"0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y" |
23482 | 726 |
by(simp add:field_simps) |
727 |
||
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
728 |
|
23482 | 729 |
lemma divide_nonneg_pos: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
730 |
"0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y" |
23482 | 731 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
732 |
|
23482 | 733 |
lemma divide_neg_pos: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
734 |
"(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0" |
23482 | 735 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
736 |
|
23482 | 737 |
lemma divide_nonpos_pos: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
738 |
"(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0" |
23482 | 739 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
740 |
|
23482 | 741 |
lemma divide_pos_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
742 |
"0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0" |
23482 | 743 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
744 |
|
23482 | 745 |
lemma divide_nonneg_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
746 |
"0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0" |
23482 | 747 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
748 |
|
23482 | 749 |
lemma divide_neg_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
750 |
"(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y" |
23482 | 751 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
752 |
|
23482 | 753 |
lemma divide_nonpos_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
754 |
"(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y" |
23482 | 755 |
by(simp add:field_simps) |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
756 |
|
23389 | 757 |
|
14288 | 758 |
subsection{*Cancellation Laws for Division*} |
759 |
||
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
760 |
lemma divide_cancel_right [simp,noatp]: |
14288 | 761 |
"(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))" |
23482 | 762 |
apply (cases "c=0", simp) |
23496 | 763 |
apply (simp add: divide_inverse) |
14288 | 764 |
done |
765 |
||
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
766 |
lemma divide_cancel_left [simp,noatp]: |
14288 | 767 |
"(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" |
23482 | 768 |
apply (cases "c=0", simp) |
23496 | 769 |
apply (simp add: divide_inverse) |
14288 | 770 |
done |
771 |
||
23389 | 772 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
773 |
subsection {* Division and the Number One *} |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
774 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
775 |
text{*Simplify expressions equated with 1*} |
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
776 |
lemma divide_eq_1_iff [simp,noatp]: |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
777 |
"(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))" |
23482 | 778 |
apply (cases "b=0", simp) |
779 |
apply (simp add: right_inverse_eq) |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
780 |
done |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
781 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
782 |
lemma one_eq_divide_iff [simp,noatp]: |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
783 |
"(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))" |
23482 | 784 |
by (simp add: eq_commute [of 1]) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
785 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
786 |
lemma zero_eq_1_divide_iff [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
787 |
"((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)" |
23482 | 788 |
apply (cases "a=0", simp) |
789 |
apply (auto simp add: nonzero_eq_divide_eq) |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
790 |
done |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
791 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
792 |
lemma one_divide_eq_0_iff [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
793 |
"(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)" |
23482 | 794 |
apply (cases "a=0", simp) |
795 |
apply (insert zero_neq_one [THEN not_sym]) |
|
796 |
apply (auto simp add: nonzero_divide_eq_eq) |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
797 |
done |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
798 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
799 |
text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*} |
18623 | 800 |
lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified] |
801 |
lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified] |
|
802 |
lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified] |
|
803 |
lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified] |
|
17085 | 804 |
|
29833 | 805 |
declare zero_less_divide_1_iff [simp,noatp] |
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
806 |
declare divide_less_0_1_iff [simp,noatp] |
29833 | 807 |
declare zero_le_divide_1_iff [simp,noatp] |
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
808 |
declare divide_le_0_1_iff [simp,noatp] |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
809 |
|
23389 | 810 |
|
14293 | 811 |
subsection {* Ordering Rules for Division *} |
812 |
||
813 |
lemma divide_strict_right_mono: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
814 |
"[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)" |
14293 | 815 |
by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono |
23482 | 816 |
positive_imp_inverse_positive) |
14293 | 817 |
|
818 |
lemma divide_right_mono: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
819 |
"[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_field,division_by_zero})" |
23482 | 820 |
by (force simp add: divide_strict_right_mono order_le_less) |
14293 | 821 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
822 |
lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
823 |
==> c <= 0 ==> b / c <= a / c" |
23482 | 824 |
apply (drule divide_right_mono [of _ _ "- c"]) |
825 |
apply auto |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
826 |
done |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
827 |
|
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
828 |
lemma divide_strict_right_mono_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
829 |
"[|b < a; c < 0|] ==> a / c < b / (c::'a::linordered_field)" |
23482 | 830 |
apply (drule divide_strict_right_mono [of _ _ "-c"], simp) |
831 |
apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
832 |
done |
14293 | 833 |
|
834 |
text{*The last premise ensures that @{term a} and @{term b} |
|
835 |
have the same sign*} |
|
836 |
lemma divide_strict_left_mono: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
837 |
"[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" |
23482 | 838 |
by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono) |
14293 | 839 |
|
840 |
lemma divide_left_mono: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
841 |
"[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::linordered_field)" |
23482 | 842 |
by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono) |
14293 | 843 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
844 |
lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
845 |
==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
846 |
apply (drule divide_left_mono [of _ _ "- c"]) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
847 |
apply (auto simp add: mult_commute) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
848 |
done |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
849 |
|
14293 | 850 |
lemma divide_strict_left_mono_neg: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
851 |
"[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" |
23482 | 852 |
by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg) |
853 |
||
14293 | 854 |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
855 |
text{*Simplify quotients that are compared with the value 1.*} |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
856 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
857 |
lemma le_divide_eq_1 [noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
858 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
859 |
shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
860 |
by (auto simp add: le_divide_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
861 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
862 |
lemma divide_le_eq_1 [noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
863 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
864 |
shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
865 |
by (auto simp add: divide_le_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
866 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
867 |
lemma less_divide_eq_1 [noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
868 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
869 |
shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
870 |
by (auto simp add: less_divide_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
871 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
872 |
lemma divide_less_eq_1 [noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
873 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
874 |
shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
875 |
by (auto simp add: divide_less_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
876 |
|
23389 | 877 |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
878 |
subsection{*Conditional Simplification Rules: No Case Splits*} |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
879 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
880 |
lemma le_divide_eq_1_pos [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
881 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
882 |
shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
883 |
by (auto simp add: le_divide_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
884 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
885 |
lemma le_divide_eq_1_neg [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
886 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
887 |
shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
888 |
by (auto simp add: le_divide_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
889 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
890 |
lemma divide_le_eq_1_pos [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
891 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
892 |
shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
893 |
by (auto simp add: divide_le_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
894 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
895 |
lemma divide_le_eq_1_neg [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
896 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
897 |
shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
898 |
by (auto simp add: divide_le_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
899 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
900 |
lemma less_divide_eq_1_pos [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
901 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
902 |
shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
903 |
by (auto simp add: less_divide_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
904 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
905 |
lemma less_divide_eq_1_neg [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
906 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
907 |
shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
908 |
by (auto simp add: less_divide_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
909 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
910 |
lemma divide_less_eq_1_pos [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
911 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
912 |
shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)" |
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
913 |
by (auto simp add: divide_less_eq) |
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
914 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
915 |
lemma divide_less_eq_1_neg [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
916 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
917 |
shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
918 |
by (auto simp add: divide_less_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
919 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
920 |
lemma eq_divide_eq_1 [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
921 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
922 |
shows "(1 = b/a) = ((a \<noteq> 0 & a = b))" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
923 |
by (auto simp add: eq_divide_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
924 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23879
diff
changeset
|
925 |
lemma divide_eq_eq_1 [simp,noatp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
926 |
fixes a :: "'a :: {linordered_field,division_by_zero}" |
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset
|
927 |
shows "(b/a = 1) = ((a \<noteq> 0 & a = b))" |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
928 |
by (auto simp add: divide_eq_eq) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
929 |
|
23389 | 930 |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
931 |
subsection {* Reasoning about inequalities with division *} |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
932 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
933 |
lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==> |
33319 | 934 |
x / y <= z" |
935 |
by (subst pos_divide_le_eq, assumption+) |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
936 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
937 |
lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==> |
23482 | 938 |
z <= x / y" |
939 |
by(simp add:field_simps) |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
940 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
941 |
lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==> |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
942 |
x / y < z" |
23482 | 943 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
944 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
945 |
lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==> |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
946 |
z < x / y" |
23482 | 947 |
by(simp add:field_simps) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
948 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
949 |
lemma frac_le: "(0::'a::linordered_field) <= x ==> |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
950 |
x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
951 |
apply (rule mult_imp_div_pos_le) |
25230 | 952 |
apply simp |
953 |
apply (subst times_divide_eq_left) |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
954 |
apply (rule mult_imp_le_div_pos, assumption) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
955 |
apply (rule mult_mono) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
956 |
apply simp_all |
14293 | 957 |
done |
958 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
959 |
lemma frac_less: "(0::'a::linordered_field) <= x ==> |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
960 |
x < y ==> 0 < w ==> w <= z ==> x / z < y / w" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
961 |
apply (rule mult_imp_div_pos_less) |
33319 | 962 |
apply simp |
963 |
apply (subst times_divide_eq_left) |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
964 |
apply (rule mult_imp_less_div_pos, assumption) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
965 |
apply (erule mult_less_le_imp_less) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
966 |
apply simp_all |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
967 |
done |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
968 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
969 |
lemma frac_less2: "(0::'a::linordered_field) < x ==> |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
970 |
x <= y ==> 0 < w ==> w < z ==> x / z < y / w" |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
971 |
apply (rule mult_imp_div_pos_less) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
972 |
apply simp_all |
33319 | 973 |
apply (subst times_divide_eq_left) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
974 |
apply (rule mult_imp_less_div_pos, assumption) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
975 |
apply (erule mult_le_less_imp_less) |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
976 |
apply simp_all |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
977 |
done |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
978 |
|
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
979 |
text{*It's not obvious whether these should be simprules or not. |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
980 |
Their effect is to gather terms into one big fraction, like |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
981 |
a*b*c / x*y*z. The rationale for that is unclear, but many proofs |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
982 |
seem to need them.*} |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
983 |
|
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
984 |
declare times_divide_eq [simp] |
14293 | 985 |
|
23389 | 986 |
|
14293 | 987 |
subsection {* Ordered Fields are Dense *} |
988 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
989 |
lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)" |
23482 | 990 |
by (simp add: field_simps zero_less_two) |
14293 | 991 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
992 |
lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b" |
23482 | 993 |
by (simp add: field_simps zero_less_two) |
14293 | 994 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
995 |
instance linordered_field < dense_linorder |
24422 | 996 |
proof |
997 |
fix x y :: 'a |
|
998 |
have "x < x + 1" by simp |
|
999 |
then show "\<exists>y. x < y" .. |
|
1000 |
have "x - 1 < x" by simp |
|
1001 |
then show "\<exists>y. y < x" .. |
|
1002 |
show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum) |
|
1003 |
qed |
|
14293 | 1004 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
1005 |
|
14293 | 1006 |
subsection {* Absolute Value *} |
1007 |
||
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1008 |
lemma nonzero_abs_inverse: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
1009 |
"a \<noteq> 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)" |
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1010 |
apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1011 |
negative_imp_inverse_negative) |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1012 |
apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1013 |
done |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1014 |
|
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1015 |
lemma abs_inverse [simp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
1016 |
"abs (inverse (a::'a::{linordered_field,division_by_zero})) = |
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1017 |
inverse (abs a)" |
21328 | 1018 |
apply (cases "a=0", simp) |
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1019 |
apply (simp add: nonzero_abs_inverse) |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1020 |
done |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1021 |
|
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1022 |
lemma nonzero_abs_divide: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
1023 |
"b \<noteq> 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b" |
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1024 |
by (simp add: divide_inverse abs_mult nonzero_abs_inverse) |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1025 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
1026 |
lemma abs_divide [simp]: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
1027 |
"abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b" |
21328 | 1028 |
apply (cases "b=0", simp) |
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1029 |
apply (simp add: nonzero_abs_divide) |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1030 |
done |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
1031 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34146
diff
changeset
|
1032 |
lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==> |
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset
|
1033 |
abs x / y = abs (x / y)" |
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset
|
1034 |
apply (subst abs_divide) |
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset
|
1035 |
apply (simp add: order_less_imp_le) |
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset
|
1036 |
done |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset
|
1037 |
|
33364 | 1038 |
code_modulename SML |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
1039 |
Fields Arith |
33364 | 1040 |
|
1041 |
code_modulename OCaml |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
1042 |
Fields Arith |
33364 | 1043 |
|
1044 |
code_modulename Haskell |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
1045 |
Fields Arith |
33364 | 1046 |
|
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset
|
1047 |
end |