10 |
10 |
11 theory Ring_and_Field = Main: |
11 theory Ring_and_Field = Main: |
12 |
12 |
13 subsection {* Abstract algebraic structures *} |
13 subsection {* Abstract algebraic structures *} |
14 |
14 |
15 axclass ring < zero, plus, minus, times, number |
15 axclass ring \<subseteq> zero, plus, minus, times, number |
16 add_assoc: "(a + b) + c = a + (b + c)" |
16 add_assoc: "(a + b) + c = a + (b + c)" |
17 add_commute: "a + b = b + a" |
17 add_commute: "a + b = b + a" |
18 left_zero [simp]: "0 + a = a" |
18 left_zero [simp]: "0 + a = a" |
19 left_minus [simp]: "- a + a = 0" |
19 left_minus [simp]: "- a + a = 0" |
20 diff_minus: "a - b = a + (-b)" |
20 diff_minus: "a - b = a + (-b)" |
24 mult_commute: "a * b = b * a" |
24 mult_commute: "a * b = b * a" |
25 left_one [simp]: "#1 * a = a" |
25 left_one [simp]: "#1 * a = a" |
26 |
26 |
27 left_distrib: "(a + b) * c = a * c + b * c" |
27 left_distrib: "(a + b) * c = a * c + b * c" |
28 |
28 |
29 axclass ordered_ring < ring, linorder |
29 axclass ordered_ring \<subseteq> ring, linorder |
30 add_left_mono: "a \<le> b ==> c + a \<le> c + b" |
30 add_left_mono: "a \<le> b ==> c + a \<le> c + b" |
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 < 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 |
37 |
38 axclass ordered_field < ordered_ring, field |
38 axclass ordered_field \<subseteq> ordered_ring, field |
39 |
39 |
40 axclass division_by_zero < zero, inverse |
40 axclass division_by_zero \<subseteq> zero, inverse |
41 inverse_zero: "inverse 0 = 0" |
41 inverse_zero: "inverse 0 = 0" |
42 divide_zero: "a / 0 = 0" |
42 divide_zero: "a / 0 = 0" |
43 |
43 |
44 |
44 |
45 |
45 |