31 mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b" |
31 mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b" |
32 abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)" |
32 abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)" |
33 |
33 |
34 axclass field \<subseteq> ring, inverse |
34 axclass field \<subseteq> ring, inverse |
35 left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1" |
35 left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1" |
36 divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b" |
36 divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b" |
|
37 zero_neq_one [simp]: "0 \<noteq> 1" |
37 |
38 |
38 axclass ordered_field \<subseteq> ordered_ring, field |
39 axclass ordered_field \<subseteq> ordered_ring, field |
39 |
40 |
40 axclass division_by_zero \<subseteq> zero, inverse |
41 axclass division_by_zero \<subseteq> zero, inverse |
41 inverse_zero: "inverse 0 = 0" |
42 inverse_zero: "inverse 0 = 0" |
42 divide_zero: "a / 0 = 0" |
43 divide_zero: "a / 0 = 0" |
43 |
44 |
44 |
45 |
45 |
46 |
46 subsection {* Derived rules *} |
47 subsection {* Derived rules for addition *} |
47 |
|
48 subsubsection {* Derived rules for addition *} |
|
49 |
48 |
50 lemma right_zero [simp]: "a + 0 = (a::'a::ring)" |
49 lemma right_zero [simp]: "a + 0 = (a::'a::ring)" |
51 proof - |
50 proof - |
52 have "a + 0 = 0 + a" by (simp only: add_commute) |
51 have "a + 0 = 0 + a" by (simp only: add_commute) |
53 also have "... = a" by simp |
52 also have "... = a" by simp |
260 |
259 |
261 lemma mult_strict_right_mono: |
260 lemma mult_strict_right_mono: |
262 "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_ring)" |
261 "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_ring)" |
263 by (simp add: mult_commute [of _ c] mult_strict_left_mono) |
262 by (simp add: mult_commute [of _ c] mult_strict_left_mono) |
264 |
263 |
265 lemma mult_neg_left_mono: |
264 lemma mult_left_mono: "[|a \<le> b; 0 < c|] ==> c * a \<le> c * (b::'a::ordered_ring)" |
|
265 by (force simp add: mult_strict_left_mono order_le_less) |
|
266 |
|
267 lemma mult_right_mono: "[|a \<le> b; 0 < c|] ==> a*c \<le> b * (c::'a::ordered_ring)" |
|
268 by (force simp add: mult_strict_right_mono order_le_less) |
|
269 |
|
270 lemma mult_strict_left_mono_neg: |
266 "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)" |
271 "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)" |
267 apply (drule mult_strict_left_mono [of _ _ "-c"]) |
272 apply (drule mult_strict_left_mono [of _ _ "-c"]) |
268 apply (simp_all add: minus_mult_left [symmetric]) |
273 apply (simp_all add: minus_mult_left [symmetric]) |
269 done |
274 done |
270 |
275 |
271 |
276 lemma mult_strict_right_mono_neg: |
272 subsubsection{* Products of Signs *} |
277 "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring)" |
|
278 apply (drule mult_strict_right_mono [of _ _ "-c"]) |
|
279 apply (simp_all add: minus_mult_right [symmetric]) |
|
280 done |
|
281 |
|
282 lemma mult_left_mono_neg: |
|
283 "[|b \<le> a; c < 0|] ==> c * a \<le> c * (b::'a::ordered_ring)" |
|
284 by (force simp add: mult_strict_left_mono_neg order_le_less) |
|
285 |
|
286 lemma mult_right_mono_neg: |
|
287 "[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)" |
|
288 by (force simp add: mult_strict_right_mono_neg order_le_less) |
|
289 |
|
290 |
|
291 subsection{* Products of Signs *} |
273 |
292 |
274 lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b" |
293 lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b" |
275 by (drule mult_strict_left_mono [of 0 b], auto) |
294 by (drule mult_strict_left_mono [of 0 b], auto) |
276 |
295 |
277 lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0" |
296 lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0" |
278 by (drule mult_strict_left_mono [of b 0], auto) |
297 by (drule mult_strict_left_mono [of b 0], auto) |
279 |
298 |
|
299 lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b" |
|
300 by (drule mult_strict_right_mono_neg, auto) |
|
301 |
|
302 lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_ring)" |
|
303 apply (case_tac "b\<le>0") |
|
304 apply (auto simp add: order_le_less linorder_not_less) |
|
305 apply (drule_tac mult_pos_neg [of a b]) |
|
306 apply (auto dest: order_less_not_sym) |
|
307 done |
|
308 |
|
309 lemma zero_less_mult_iff: |
|
310 "((0::'a::ordered_ring) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)" |
|
311 apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg) |
|
312 apply (blast dest: zero_less_mult_pos) |
|
313 apply (simp add: mult_commute [of a b]) |
|
314 apply (blast dest: zero_less_mult_pos) |
|
315 done |
|
316 |
|
317 |
|
318 lemma mult_eq_0_iff [iff]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)" |
|
319 apply (case_tac "a < 0") |
|
320 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff) |
|
321 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+ |
|
322 done |
|
323 |
|
324 lemma zero_le_mult_iff: |
|
325 "((0::'a::ordered_ring) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)" |
|
326 by (auto simp add: order_le_less linorder_not_less zero_less_mult_iff) |
|
327 |
|
328 lemma mult_less_0_iff: |
|
329 "(a*b < (0::'a::ordered_ring)) = (0 < a & b < 0 | a < 0 & 0 < b)" |
|
330 apply (insert zero_less_mult_iff [of "-a" b]) |
|
331 apply (force simp add: minus_mult_left[symmetric]) |
|
332 done |
|
333 |
|
334 lemma mult_le_0_iff: |
|
335 "(a*b \<le> (0::'a::ordered_ring)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)" |
|
336 apply (insert zero_le_mult_iff [of "-a" b]) |
|
337 apply (force simp add: minus_mult_left[symmetric]) |
|
338 done |
|
339 |
|
340 lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a" |
|
341 by (simp add: zero_le_mult_iff linorder_linear) |
|
342 |
|
343 |
|
344 subsection {* Absolute Value *} |
|
345 |
|
346 text{*But is it really better than just rewriting with @{text abs_if}?*} |
|
347 lemma abs_split: |
|
348 "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))" |
|
349 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) |
|
350 |
|
351 lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)" |
|
352 by (simp add: abs_if) |
|
353 |
|
354 lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)" |
|
355 apply (case_tac "x=0 | y=0", force) |
|
356 apply (auto elim: order_less_asym |
|
357 simp add: abs_if mult_less_0_iff linorder_neq_iff |
|
358 minus_mult_left [symmetric] minus_mult_right [symmetric]) |
|
359 done |
|
360 |
|
361 lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::'a::ordered_ring))" |
|
362 by (simp add: abs_if) |
|
363 |
|
364 lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))" |
|
365 by (simp add: abs_if linorder_neq_iff) |
|
366 |
|
367 |
|
368 subsection {* Fields *} |
|
369 |
|
370 lemma zero_less_one: "(0::'a::ordered_field) < 1" |
|
371 apply (insert zero_le_square [of 1]) |
|
372 apply (simp add: order_less_le) |
|
373 done |
|
374 |
|
375 |
280 end |
376 end |