10479
|
1 |
(* Title: HOL/Library/Ring_and_Field.thy
|
|
2 |
ID: $Id$
|
10502
|
3 |
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
|
10479
|
4 |
*)
|
|
5 |
|
|
6 |
header {*
|
10484
|
7 |
\title{Ring and field structures}
|
10502
|
8 |
\author{Gertrud Bauer and Markus Wenzel}
|
10479
|
9 |
*}
|
|
10 |
|
|
11 |
theory Ring_and_Field = Main:
|
|
12 |
|
10492
|
13 |
subsection {* Abstract algebraic structures *}
|
10479
|
14 |
|
11099
|
15 |
axclass ring \<subseteq> zero, plus, minus, times, number
|
10479
|
16 |
add_assoc: "(a + b) + c = a + (b + c)"
|
|
17 |
add_commute: "a + b = b + a"
|
10610
|
18 |
left_zero [simp]: "0 + a = a"
|
|
19 |
left_minus [simp]: "- a + a = 0"
|
10620
|
20 |
diff_minus: "a - b = a + (-b)"
|
10484
|
21 |
zero_number: "0 = #0"
|
10479
|
22 |
|
|
23 |
mult_assoc: "(a * b) * c = a * (b * c)"
|
|
24 |
mult_commute: "a * b = b * a"
|
10610
|
25 |
left_one [simp]: "#1 * a = a"
|
10479
|
26 |
|
|
27 |
left_distrib: "(a + b) * c = a * c + b * c"
|
|
28 |
|
11099
|
29 |
axclass ordered_ring \<subseteq> ring, linorder
|
10492
|
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"
|
|
32 |
abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
|
10479
|
33 |
|
11099
|
34 |
axclass field \<subseteq> ring, inverse
|
10610
|
35 |
left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = #1"
|
10620
|
36 |
divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
|
10479
|
37 |
|
11099
|
38 |
axclass ordered_field \<subseteq> ordered_ring, field
|
10488
|
39 |
|
11099
|
40 |
axclass division_by_zero \<subseteq> zero, inverse
|
10620
|
41 |
inverse_zero: "inverse 0 = 0"
|
|
42 |
divide_zero: "a / 0 = 0"
|
|
43 |
|
10610
|
44 |
|
|
45 |
|
|
46 |
subsection {* Derived rules *}
|
|
47 |
|
|
48 |
subsubsection {* Derived rules for addition *}
|
|
49 |
|
|
50 |
lemma right_zero [simp]: "a + 0 = (a::'a::ring)"
|
|
51 |
proof -
|
|
52 |
have "a + 0 = 0 + a" by (simp only: add_commute)
|
10622
|
53 |
also have "... = a" by simp
|
10610
|
54 |
finally show ?thesis .
|
|
55 |
qed
|
|
56 |
|
|
57 |
lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ring))"
|
|
58 |
proof -
|
|
59 |
have "a + (b + c) = (a + b) + c" by (simp only: add_assoc)
|
10622
|
60 |
also have "... = (b + a) + c" by (simp only: add_commute)
|
10610
|
61 |
finally show ?thesis by (simp only: add_assoc)
|
|
62 |
qed
|
10544
|
63 |
|
10610
|
64 |
theorems ring_add_ac = add_assoc add_commute add_left_commute
|
|
65 |
|
|
66 |
lemma right_minus [simp]: "a + -(a::'a::ring) = 0"
|
|
67 |
proof -
|
|
68 |
have "a + -a = -a + a" by (simp add: ring_add_ac)
|
10622
|
69 |
also have "... = 0" by simp
|
10610
|
70 |
finally show ?thesis .
|
|
71 |
qed
|
|
72 |
|
10620
|
73 |
lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))"
|
10610
|
74 |
proof
|
10620
|
75 |
have "a = a - b + b" by (simp add: diff_minus ring_add_ac)
|
10610
|
76 |
also assume "a - b = 0"
|
|
77 |
finally show "a = b" by simp
|
10620
|
78 |
next
|
|
79 |
assume "a = b"
|
|
80 |
thus "a - b = 0" by (simp add: diff_minus)
|
|
81 |
qed
|
10610
|
82 |
|
|
83 |
lemma diff_self [simp]: "a - (a::'a::ring) = 0"
|
10620
|
84 |
by (simp add: diff_minus)
|
10610
|
85 |
|
|
86 |
|
|
87 |
subsubsection {* Derived rules for multiplication *}
|
10544
|
88 |
|
10622
|
89 |
lemma right_one [simp]: "a = a * (#1::'a::field)"
|
10610
|
90 |
proof -
|
|
91 |
have "a = #1 * a" by simp
|
10622
|
92 |
also have "... = a * #1" by (simp add: mult_commute)
|
10610
|
93 |
finally show ?thesis .
|
|
94 |
qed
|
|
95 |
|
|
96 |
lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))"
|
|
97 |
proof -
|
|
98 |
have "a * (b * c) = (a * b) * c" by (simp only: mult_assoc)
|
10622
|
99 |
also have "... = (b * a) * c" by (simp only: mult_commute)
|
10610
|
100 |
finally show ?thesis by (simp only: mult_assoc)
|
|
101 |
qed
|
|
102 |
|
|
103 |
theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute
|
|
104 |
|
10622
|
105 |
lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = #1"
|
10610
|
106 |
proof -
|
|
107 |
have "a * inverse a = inverse a * a" by (simp add: ring_mult_ac)
|
|
108 |
also assume "a \<noteq> 0"
|
|
109 |
hence "inverse a * a = #1" by simp
|
|
110 |
finally show ?thesis .
|
|
111 |
qed
|
10492
|
112 |
|
10622
|
113 |
lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = #1) = (a = (b::'a::field))"
|
10610
|
114 |
proof
|
10620
|
115 |
assume neq: "b \<noteq> 0"
|
|
116 |
{
|
|
117 |
hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac)
|
|
118 |
also assume "a / b = #1"
|
|
119 |
finally show "a = b" by simp
|
|
120 |
next
|
|
121 |
assume "a = b"
|
|
122 |
with neq show "a / b = #1" by (simp add: divide_inverse)
|
|
123 |
}
|
|
124 |
qed
|
10610
|
125 |
|
10622
|
126 |
lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = #1"
|
10620
|
127 |
by (simp add: divide_inverse)
|
10610
|
128 |
|
|
129 |
|
|
130 |
subsubsection {* Distribution rules *}
|
|
131 |
|
|
132 |
lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::ring)"
|
|
133 |
proof -
|
|
134 |
have "a * (b + c) = (b + c) * a" by (simp add: ring_mult_ac)
|
10622
|
135 |
also have "... = b * a + c * a" by (simp only: left_distrib)
|
|
136 |
also have "... = a * b + a * c" by (simp add: ring_mult_ac)
|
10620
|
137 |
finally show ?thesis .
|
10610
|
138 |
qed
|
|
139 |
|
|
140 |
theorems ring_distrib = right_distrib left_distrib
|
|
141 |
|
10484
|
142 |
end
|