author | nipkow |
Wed, 28 Jan 2009 16:57:36 +0100 | |
changeset 29669 | 2a580d9af918 |
parent 29665 | 2b956243d123 |
parent 29667 | 53103fc8ffa3 |
child 30510 | 4120fc59dd85 |
permissions | -rw-r--r-- |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27651
diff
changeset
|
1 |
(* Title: HOL/Algebra/abstract/Ring2.thy |
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27651
diff
changeset
|
2 |
Author: Clemens Ballarin |
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27651
diff
changeset
|
3 |
|
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27651
diff
changeset
|
4 |
The algebraic hierarchy of rings as axiomatic classes. |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
5 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
6 |
|
27542 | 7 |
header {* The algebraic hierarchy of rings as type classes *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
8 |
|
27542 | 9 |
theory Ring2 |
10 |
imports Main |
|
11 |
begin |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
12 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
13 |
subsection {* Ring axioms *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
14 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27542
diff
changeset
|
15 |
class ring = zero + one + plus + minus + uminus + times + inverse + power + Ring_and_Field.dvd + |
27542 | 16 |
assumes a_assoc: "(a + b) + c = a + (b + c)" |
17 |
and l_zero: "0 + a = a" |
|
18 |
and l_neg: "(-a) + a = 0" |
|
19 |
and a_comm: "a + b = b + a" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
20 |
|
27542 | 21 |
assumes m_assoc: "(a * b) * c = a * (b * c)" |
22 |
and l_one: "1 * a = a" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
23 |
|
27542 | 24 |
assumes l_distr: "(a + b) * c = a * c + b * c" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
25 |
|
27542 | 26 |
assumes m_comm: "a * b = b * a" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
27 |
|
27542 | 28 |
assumes minus_def: "a - b = a + (-b)" |
29 |
and inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" |
|
30 |
and divide_def: "a / b = a * inverse b" |
|
31 |
and power_0 [simp]: "a ^ 0 = 1" |
|
32 |
and power_Suc [simp]: "a ^ Suc n = a ^ n * a" |
|
33 |
begin |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
34 |
|
27542 | 35 |
definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where |
36 |
assoc_def: "a assoc b \<longleftrightarrow> a dvd b & b dvd a" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
37 |
|
27542 | 38 |
definition irred :: "'a \<Rightarrow> bool" where |
39 |
irred_def: "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
40 |
& (ALL d. d dvd a --> d dvd 1 | a dvd d)" |
27542 | 41 |
|
42 |
definition prime :: "'a \<Rightarrow> bool" where |
|
43 |
prime_def: "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
44 |
& (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
45 |
|
27542 | 46 |
end |
47 |
||
48 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
49 |
subsection {* Integral domains *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
50 |
|
27542 | 51 |
class "domain" = ring + |
52 |
assumes one_not_zero: "1 ~= 0" |
|
53 |
and integral: "a * b = 0 ==> a = 0 | b = 0" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
54 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
55 |
subsection {* Factorial domains *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
56 |
|
27542 | 57 |
class factorial = "domain" + |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
58 |
(* |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
59 |
Proper definition using divisor chain condition currently not supported. |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
60 |
factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
61 |
*) |
29665
2b956243d123
explicit check for exactly one type variable in class specification elements
haftmann
parents:
29269
diff
changeset
|
62 |
(*assumes factorial_divisor: "True"*) |
2b956243d123
explicit check for exactly one type variable in class specification elements
haftmann
parents:
29269
diff
changeset
|
63 |
assumes factorial_prime: "irred a ==> prime a" |
2b956243d123
explicit check for exactly one type variable in class specification elements
haftmann
parents:
29269
diff
changeset
|
64 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
65 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
66 |
subsection {* Euclidean domains *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
67 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
68 |
(* |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
69 |
axclass |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
70 |
euclidean < "domain" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
71 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
72 |
euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
73 |
a = b * q + r & e_size r < e_size b)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
74 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
75 |
Nothing has been proved about Euclidean domains, yet. |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
76 |
Design question: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
77 |
Fix quo, rem and e_size as constants that are axiomatised with |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
78 |
euclidean_ax? |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
79 |
- advantage: more pragmatic and easier to use |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
80 |
- disadvantage: for every type, one definition of quo and rem will |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
81 |
be fixed, users may want to use differing ones; |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
82 |
also, it seems not possible to prove that fields are euclidean |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
83 |
domains, because that would require generic (type-independent) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
84 |
definitions of quo and rem. |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
85 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
86 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
87 |
subsection {* Fields *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
88 |
|
27542 | 89 |
class field = ring + |
90 |
assumes field_one_not_zero: "1 ~= 0" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
91 |
(* Avoid a common superclass as the first thing we will |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
92 |
prove about fields is that they are domains. *) |
27542 | 93 |
and field_ax: "a ~= 0 ==> a dvd 1" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
94 |
|
21423 | 95 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
96 |
section {* Basic facts *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
97 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
98 |
subsection {* Normaliser for rings *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
99 |
|
21423 | 100 |
(* derived rewrite rules *) |
101 |
||
102 |
lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)" |
|
103 |
apply (rule a_comm [THEN trans]) |
|
104 |
apply (rule a_assoc [THEN trans]) |
|
105 |
apply (rule a_comm [THEN arg_cong]) |
|
106 |
done |
|
107 |
||
108 |
lemma r_zero: "(a::'a::ring) + 0 = a" |
|
109 |
apply (rule a_comm [THEN trans]) |
|
110 |
apply (rule l_zero) |
|
111 |
done |
|
112 |
||
113 |
lemma r_neg: "(a::'a::ring) + (-a) = 0" |
|
114 |
apply (rule a_comm [THEN trans]) |
|
115 |
apply (rule l_neg) |
|
116 |
done |
|
117 |
||
118 |
lemma r_neg2: "(a::'a::ring) + (-a + b) = b" |
|
119 |
apply (rule a_assoc [symmetric, THEN trans]) |
|
120 |
apply (simp add: r_neg l_zero) |
|
121 |
done |
|
122 |
||
123 |
lemma r_neg1: "-(a::'a::ring) + (a + b) = b" |
|
124 |
apply (rule a_assoc [symmetric, THEN trans]) |
|
125 |
apply (simp add: l_neg l_zero) |
|
126 |
done |
|
127 |
||
128 |
||
129 |
(* auxiliary *) |
|
130 |
||
131 |
lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c" |
|
132 |
apply (rule box_equals) |
|
133 |
prefer 2 |
|
134 |
apply (rule l_zero) |
|
135 |
prefer 2 |
|
136 |
apply (rule l_zero) |
|
137 |
apply (rule_tac a1 = a in l_neg [THEN subst]) |
|
138 |
apply (simp add: a_assoc) |
|
139 |
done |
|
140 |
||
141 |
lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)" |
|
142 |
apply (rule_tac a = "a + b" in a_lcancel) |
|
143 |
apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm) |
|
144 |
done |
|
145 |
||
146 |
lemma minus_minus: "-(-(a::'a::ring)) = a" |
|
147 |
apply (rule a_lcancel) |
|
148 |
apply (rule r_neg [THEN trans]) |
|
149 |
apply (rule l_neg [symmetric]) |
|
150 |
done |
|
151 |
||
152 |
lemma minus0: "- 0 = (0::'a::ring)" |
|
153 |
apply (rule a_lcancel) |
|
154 |
apply (rule r_neg [THEN trans]) |
|
155 |
apply (rule l_zero [symmetric]) |
|
156 |
done |
|
157 |
||
158 |
||
159 |
(* derived rules for multiplication *) |
|
160 |
||
161 |
lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)" |
|
162 |
apply (rule m_comm [THEN trans]) |
|
163 |
apply (rule m_assoc [THEN trans]) |
|
164 |
apply (rule m_comm [THEN arg_cong]) |
|
165 |
done |
|
166 |
||
167 |
lemma r_one: "(a::'a::ring) * 1 = a" |
|
168 |
apply (rule m_comm [THEN trans]) |
|
169 |
apply (rule l_one) |
|
170 |
done |
|
171 |
||
172 |
lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c" |
|
173 |
apply (rule m_comm [THEN trans]) |
|
174 |
apply (rule l_distr [THEN trans]) |
|
175 |
apply (simp add: m_comm) |
|
176 |
done |
|
177 |
||
178 |
||
179 |
(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *) |
|
180 |
lemma l_null: "0 * (a::'a::ring) = 0" |
|
181 |
apply (rule a_lcancel) |
|
182 |
apply (rule l_distr [symmetric, THEN trans]) |
|
183 |
apply (simp add: r_zero) |
|
184 |
done |
|
185 |
||
186 |
lemma r_null: "(a::'a::ring) * 0 = 0" |
|
187 |
apply (rule m_comm [THEN trans]) |
|
188 |
apply (rule l_null) |
|
189 |
done |
|
190 |
||
191 |
lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)" |
|
192 |
apply (rule a_lcancel) |
|
193 |
apply (rule r_neg [symmetric, THEN [2] trans]) |
|
194 |
apply (rule l_distr [symmetric, THEN trans]) |
|
195 |
apply (simp add: l_null r_neg) |
|
196 |
done |
|
197 |
||
198 |
lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)" |
|
199 |
apply (rule a_lcancel) |
|
200 |
apply (rule r_neg [symmetric, THEN [2] trans]) |
|
201 |
apply (rule r_distr [symmetric, THEN trans]) |
|
202 |
apply (simp add: r_null r_neg) |
|
203 |
done |
|
204 |
||
205 |
(*** Term order for commutative rings ***) |
|
206 |
||
207 |
ML {* |
|
208 |
fun ring_ord (Const (a, _)) = |
|
209 |
find_index (fn a' => a = a') |
|
22997 | 210 |
[@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus}, |
211 |
@{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}] |
|
21423 | 212 |
| ring_ord _ = ~1; |
213 |
||
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27651
diff
changeset
|
214 |
fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS); |
21423 | 215 |
|
216 |
val ring_ss = HOL_basic_ss settermless termless_ring addsimps |
|
217 |
[thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc", |
|
218 |
thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def", |
|
219 |
thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add", |
|
220 |
thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*) |
|
221 |
thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"]; |
|
222 |
*} (* Note: r_one is not necessary in ring_ss *) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
223 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
224 |
method_setup ring = |
21588 | 225 |
{* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
226 |
{* computes distributive normal form in rings *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
227 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
228 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
229 |
subsection {* Rings and the summation operator *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
230 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
(* Basic facts --- move to HOL!!! *) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
232 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
233 |
(* needed because natsum_cong (below) disables atMost_0 *) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
234 |
lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
235 |
by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
236 |
(* |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
237 |
lemma natsum_Suc [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
238 |
"setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
239 |
by (simp add: atMost_Suc) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
240 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
241 |
lemma natsum_Suc2: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
242 |
"setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
243 |
proof (induct n) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
244 |
case 0 show ?case by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
245 |
next |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
21588
diff
changeset
|
246 |
case Suc thus ?case by (simp add: add_assoc) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
247 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
248 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
249 |
lemma natsum_cong [cong]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
250 |
"!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
251 |
setsum f {..j} = setsum g {..k}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
252 |
by (induct j) auto |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
253 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
254 |
lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
255 |
by (induct n) simp_all |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
256 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
257 |
lemma natsum_add [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
258 |
"!!f::nat=>'a::comm_monoid_add. |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
259 |
setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
260 |
by (induct n) (simp_all add: add_ac) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
261 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
262 |
(* Facts specific to rings *) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
263 |
|
27542 | 264 |
subclass (in ring) comm_monoid_add |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
265 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
266 |
fix x y z |
27542 | 267 |
show "x + y = y + x" by (rule a_comm) |
268 |
show "(x + y) + z = x + (y + z)" by (rule a_assoc) |
|
269 |
show "0 + x = x" by (rule l_zero) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
270 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
271 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
272 |
ML {* |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
273 |
local |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
274 |
val lhss = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
275 |
["t + u::'a::ring", |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
276 |
"t - u::'a::ring", |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
277 |
"t * u::'a::ring", |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
278 |
"- t::'a::ring"]; |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
279 |
fun proc ss t = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
280 |
let val rew = Goal.prove (Simplifier.the_context ss) [] [] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
281 |
(HOLogic.mk_Trueprop |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
282 |
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
283 |
(fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
284 |
|> mk_meta_eq; |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
285 |
val (t', u) = Logic.dest_equals (Thm.prop_of rew); |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
286 |
in if t' aconv u |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
287 |
then NONE |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
288 |
else SOME rew |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
289 |
end; |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
290 |
in |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
291 |
val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc); |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
292 |
end; |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
293 |
*} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
294 |
|
26480 | 295 |
ML {* Addsimprocs [ring_simproc] *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
296 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
297 |
lemma natsum_ldistr: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
298 |
"!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
299 |
by (induct n) simp_all |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
300 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
301 |
lemma natsum_rdistr: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
302 |
"!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
303 |
by (induct n) simp_all |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
304 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
305 |
subsection {* Integral Domains *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
306 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
307 |
declare one_not_zero [simp] |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
308 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
309 |
lemma zero_not_one [simp]: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
310 |
"0 ~= (1::'a::domain)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
311 |
by (rule not_sym) simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
312 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
313 |
lemma integral_iff: (* not by default a simp rule! *) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
314 |
"(a * b = (0::'a::domain)) = (a = 0 | b = 0)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
315 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
316 |
assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
317 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
318 |
assume "a = 0 | b = 0" then show "a * b = 0" by auto |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
319 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
320 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
321 |
(* |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
322 |
lemma "(a::'a::ring) - (a - b) = b" apply simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
323 |
simproc seems to fail on this example (fixed with new term order) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
324 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
325 |
(* |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
326 |
lemma bug: "(b::'a::ring) - (b - a) = a" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
327 |
simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
328 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
329 |
lemma m_lcancel: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
330 |
assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
331 |
proof |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
332 |
assume eq: "a * b = a * c" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
333 |
then have "a * (b - c) = 0" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
334 |
then have "a = 0 | (b - c) = 0" by (simp only: integral_iff) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
335 |
with prem have "b - c = 0" by auto |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
336 |
then have "b = b - (b - c)" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
337 |
also have "b - (b - c) = c" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
338 |
finally show "b = c" . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
339 |
next |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
340 |
assume "b = c" then show "a * b = a * c" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
341 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
342 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
343 |
lemma m_rcancel: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
344 |
"(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
345 |
by (simp add: m_lcancel) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
346 |
|
27542 | 347 |
declare power_Suc [simp] |
21416 | 348 |
|
349 |
lemma power_one [simp]: |
|
350 |
"1 ^ n = (1::'a::ring)" by (induct n) simp_all |
|
351 |
||
352 |
lemma power_zero [simp]: |
|
353 |
"n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all |
|
354 |
||
355 |
lemma power_mult [simp]: |
|
356 |
"(a::'a::ring) ^ m * a ^ n = a ^ (m + n)" |
|
357 |
by (induct m) simp_all |
|
358 |
||
359 |
||
360 |
section "Divisibility" |
|
361 |
||
362 |
lemma dvd_zero_right [simp]: |
|
363 |
"(a::'a::ring) dvd 0" |
|
364 |
proof |
|
365 |
show "0 = a * 0" by simp |
|
366 |
qed |
|
367 |
||
368 |
lemma dvd_zero_left: |
|
369 |
"0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp |
|
370 |
||
371 |
lemma dvd_refl_ring [simp]: |
|
372 |
"(a::'a::ring) dvd a" |
|
373 |
proof |
|
374 |
show "a = a * 1" by simp |
|
375 |
qed |
|
376 |
||
377 |
lemma dvd_trans_ring: |
|
378 |
fixes a b c :: "'a::ring" |
|
379 |
assumes a_dvd_b: "a dvd b" |
|
380 |
and b_dvd_c: "b dvd c" |
|
381 |
shows "a dvd c" |
|
382 |
proof - |
|
383 |
from a_dvd_b obtain l where "b = a * l" using dvd_def by blast |
|
384 |
moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast |
|
385 |
ultimately have "c = a * (l * j)" by simp |
|
386 |
then have "\<exists>k. c = a * k" .. |
|
387 |
then show ?thesis using dvd_def by blast |
|
388 |
qed |
|
389 |
||
21423 | 390 |
|
391 |
lemma unit_mult: |
|
392 |
"!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1" |
|
393 |
apply (unfold dvd_def) |
|
394 |
apply clarify |
|
395 |
apply (rule_tac x = "k * ka" in exI) |
|
396 |
apply simp |
|
397 |
done |
|
398 |
||
399 |
lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1" |
|
400 |
apply (induct_tac n) |
|
401 |
apply simp |
|
402 |
apply (simp add: unit_mult) |
|
403 |
done |
|
404 |
||
405 |
lemma dvd_add_right [simp]: |
|
406 |
"!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c" |
|
407 |
apply (unfold dvd_def) |
|
408 |
apply clarify |
|
409 |
apply (rule_tac x = "k + ka" in exI) |
|
410 |
apply (simp add: r_distr) |
|
411 |
done |
|
412 |
||
413 |
lemma dvd_uminus_right [simp]: |
|
414 |
"!! a::'a::ring. a dvd b ==> a dvd -b" |
|
415 |
apply (unfold dvd_def) |
|
416 |
apply clarify |
|
417 |
apply (rule_tac x = "-k" in exI) |
|
418 |
apply (simp add: r_minus) |
|
419 |
done |
|
420 |
||
421 |
lemma dvd_l_mult_right [simp]: |
|
422 |
"!! a::'a::ring. a dvd b ==> a dvd c*b" |
|
423 |
apply (unfold dvd_def) |
|
424 |
apply clarify |
|
425 |
apply (rule_tac x = "c * k" in exI) |
|
426 |
apply simp |
|
427 |
done |
|
428 |
||
429 |
lemma dvd_r_mult_right [simp]: |
|
430 |
"!! a::'a::ring. a dvd b ==> a dvd b*c" |
|
431 |
apply (unfold dvd_def) |
|
432 |
apply clarify |
|
433 |
apply (rule_tac x = "k * c" in exI) |
|
434 |
apply simp |
|
435 |
done |
|
436 |
||
437 |
||
438 |
(* Inverse of multiplication *) |
|
439 |
||
440 |
section "inverse" |
|
441 |
||
442 |
lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y" |
|
443 |
apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals) |
|
444 |
apply (simp (no_asm)) |
|
445 |
apply auto |
|
446 |
done |
|
447 |
||
448 |
lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1" |
|
449 |
apply (unfold inverse_def dvd_def) |
|
26342 | 450 |
apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) |
21423 | 451 |
apply clarify |
452 |
apply (rule theI) |
|
453 |
apply assumption |
|
454 |
apply (rule inverse_unique) |
|
455 |
apply assumption |
|
456 |
apply assumption |
|
457 |
done |
|
458 |
||
459 |
lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1" |
|
460 |
by (simp add: r_inverse_ring) |
|
461 |
||
462 |
||
463 |
(* Fields *) |
|
464 |
||
465 |
section "Fields" |
|
466 |
||
467 |
lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)" |
|
468 |
by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero) |
|
469 |
||
470 |
lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1" |
|
471 |
by (simp add: r_inverse_ring) |
|
472 |
||
473 |
lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1" |
|
474 |
by (simp add: l_inverse_ring) |
|
475 |
||
476 |
||
477 |
(* fields are integral domains *) |
|
478 |
||
479 |
lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0" |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
22997
diff
changeset
|
480 |
apply (tactic "step_tac @{claset} 1") |
21423 | 481 |
apply (rule_tac a = " (a*b) * inverse b" in box_equals) |
482 |
apply (rule_tac [3] refl) |
|
483 |
prefer 2 |
|
484 |
apply (simp (no_asm)) |
|
485 |
apply auto |
|
486 |
done |
|
487 |
||
488 |
||
489 |
(* fields are factorial domains *) |
|
490 |
||
491 |
lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a" |
|
492 |
unfolding prime_def irred_def by (blast intro: field_ax) |
|
21416 | 493 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
494 |
end |