14 |
14 |
15 axclass ring < zero, plus, minus, times, number |
15 axclass ring < 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: "0 + a = a" |
18 left_zero: "0 + a = a" |
19 left_minus: "(-a) + a = 0" |
19 right_minus: "a + - a = 0" |
20 diff_minus: "a - b = a + (-b)" |
20 diff_minus: "a - b = a + (-b)" |
21 zero_number: "0 = #0" |
21 zero_number: "0 = #0" |
22 |
22 |
23 mult_assoc: "(a * b) * c = a * (b * c)" |
23 mult_assoc: "(a * b) * c = a * (b * c)" |
24 mult_commute: "a * b = b * a" |
24 mult_commute: "a * b = b * a" |
35 left_inverse: "a \<noteq> 0 ==> inverse a * a = #1" |
35 left_inverse: "a \<noteq> 0 ==> inverse a * a = #1" |
36 divides_inverse: "b \<noteq> 0 ==> a / b = a * inverse b" |
36 divides_inverse: "b \<noteq> 0 ==> a / b = a * inverse b" |
37 |
37 |
38 axclass ordered_field < ordered_ring, field |
38 axclass ordered_field < ordered_ring, field |
39 |
39 |
|
40 subsection {* simplification rules *} |
|
41 |
|
42 lemma left_minus [simp]: "- (a::'a::field) + a = 0" |
|
43 by (simp only: add_commute right_minus) |
|
44 |
|
45 lemma diff_self [simp]: "a - (a::'a::field) = 0" |
|
46 by (simp only: diff_minus right_minus) |
40 |
47 |
41 subsection {* The ordered ring of integers *} |
48 subsection {* The ordered ring of integers *} |
42 |
49 |
43 instance int :: ordered_ring |
50 instance int :: ordered_ring |
44 proof |
51 proof |
45 fix i j k :: int |
52 fix i j k :: int |
46 show "(i + j) + k = i + (j + k)" by simp |
53 show "(i + j) + k = i + (j + k)" by simp |
47 show "i + j = j + i" by simp |
54 show "i + j = j + i" by simp |
48 show "0 + i = i" by simp |
55 show "0 + i = i" by simp |
49 show "(-i) + i = 0" by simp |
56 show "i + - i = 0" by simp |
50 show "i - j = i + (-j)" by simp |
57 show "i - j = i + (-j)" by simp |
51 show "(i * j) * k = i * (j * k)" by simp |
58 show "(i * j) * k = i * (j * k)" by simp |
52 show "i * j = j * i" by simp |
59 show "i * j = j * i" by simp |
53 show "#1 * i = i" by simp |
60 show "#1 * i = i" by simp |
54 show "0 = (#0::int)" by simp |
61 show "0 = (#0::int)" by simp |