1 (* Title: HOL/Algebra/abstract/Ring2.thy
2 Author: Clemens Ballarin
4 The algebraic hierarchy of rings as axiomatic classes.
7 header {* The algebraic hierarchy of rings as type classes *}
13 subsection {* Ring axioms *}
15 class ring = zero + one + plus + minus + uminus + times + inverse + power + Ring_and_Field.dvd +
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"
21 assumes m_assoc: "(a * b) * c = a * (b * c)"
22 and l_one: "1 * a = a"
24 assumes l_distr: "(a + b) * c = a * c + b * c"
26 assumes m_comm: "a * b = b * a"
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"
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"
38 definition irred :: "'a \<Rightarrow> bool" where
39 irred_def: "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1
40 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
42 definition prime :: "'a \<Rightarrow> bool" where
43 prime_def: "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1
44 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
49 subsection {* Integral domains *}
51 class "domain" = ring +
52 assumes one_not_zero: "1 ~= 0"
53 and integral: "a * b = 0 ==> a = 0 | b = 0"
55 subsection {* Factorial domains *}
57 class factorial = "domain" +
59 Proper definition using divisor chain condition currently not supported.
60 factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}"
62 (*assumes factorial_divisor: "True"*)
63 assumes factorial_prime: "irred a ==> prime a"
66 subsection {* Euclidean domains *}
72 euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
73 a = b * q + r & e_size r < e_size b)"
75 Nothing has been proved about Euclidean domains, yet.
77 Fix quo, rem and e_size as constants that are axiomatised with
79 - advantage: more pragmatic and easier to use
80 - disadvantage: for every type, one definition of quo and rem will
81 be fixed, users may want to use differing ones;
82 also, it seems not possible to prove that fields are euclidean
83 domains, because that would require generic (type-independent)
84 definitions of quo and rem.
87 subsection {* Fields *}
90 assumes field_one_not_zero: "1 ~= 0"
91 (* Avoid a common superclass as the first thing we will
92 prove about fields is that they are domains. *)
93 and field_ax: "a ~= 0 ==> a dvd 1"
96 section {* Basic facts *}
98 subsection {* Normaliser for rings *}
100 (* derived rewrite rules *)
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])
108 lemma r_zero: "(a::'a::ring) + 0 = a"
109 apply (rule a_comm [THEN trans])
113 lemma r_neg: "(a::'a::ring) + (-a) = 0"
114 apply (rule a_comm [THEN trans])
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)
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)
131 lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c"
132 apply (rule box_equals)
137 apply (rule_tac a1 = a in l_neg [THEN subst])
138 apply (simp add: a_assoc)
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)
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])
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])
159 (* derived rules for multiplication *)
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])
167 lemma r_one: "(a::'a::ring) * 1 = a"
168 apply (rule m_comm [THEN trans])
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)
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)
186 lemma r_null: "(a::'a::ring) * 0 = 0"
187 apply (rule m_comm [THEN trans])
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)
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)
205 (*** Term order for commutative rings ***)
208 fun ring_ord (Const (a, _)) =
209 find_index (fn a' => a = a')
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}]
214 fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
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 *)
225 {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
226 {* computes distributive normal form in rings *}
229 subsection {* Rings and the summation operator *}
231 (* Basic facts --- move to HOL!!! *)
233 (* needed because natsum_cong (below) disables atMost_0 *)
234 lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
237 lemma natsum_Suc [simp]:
238 "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
239 by (simp add: atMost_Suc)
242 "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
244 case 0 show ?case by simp
246 case Suc thus ?case by (simp add: add_assoc)
249 lemma natsum_cong [cong]:
250 "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
251 setsum f {..j} = setsum g {..k}"
254 lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
255 by (induct n) simp_all
257 lemma natsum_add [simp]:
258 "!!f::nat=>'a::comm_monoid_add.
259 setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
260 by (induct n) (simp_all add: add_ac)
262 (* Facts specific to rings *)
264 subclass (in ring) comm_monoid_add
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)
280 let val rew = Goal.prove (Simplifier.the_context ss) [] []
282 (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
283 (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
285 val (t', u) = Logic.dest_equals (Thm.prop_of rew);
291 val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
295 ML {* Addsimprocs [ring_simproc] *}
298 "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
299 by (induct n) simp_all
302 "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
303 by (induct n) simp_all
305 subsection {* Integral Domains *}
307 declare one_not_zero [simp]
309 lemma zero_not_one [simp]:
310 "0 ~= (1::'a::domain)"
311 by (rule not_sym) simp
313 lemma integral_iff: (* not by default a simp rule! *)
314 "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
316 assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
318 assume "a = 0 | b = 0" then show "a * b = 0" by auto
322 lemma "(a::'a::ring) - (a - b) = b" apply simp
323 simproc seems to fail on this example (fixed with new term order)
326 lemma bug: "(b::'a::ring) - (b - a) = a" by simp
327 simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
330 assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
332 assume eq: "a * b = a * c"
333 then have "a * (b - c) = 0" by simp
334 then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
335 with prem have "b - c = 0" by auto
336 then have "b = b - (b - c)" by simp
337 also have "b - (b - c) = c" by simp
338 finally show "b = c" .
340 assume "b = c" then show "a * b = a * c" by simp
344 "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
345 by (simp add: m_lcancel)
347 declare power_Suc [simp]
349 lemma power_one [simp]:
350 "1 ^ n = (1::'a::ring)" by (induct n) simp_all
352 lemma power_zero [simp]:
353 "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all
355 lemma power_mult [simp]:
356 "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
357 by (induct m) simp_all
360 section "Divisibility"
362 lemma dvd_zero_right [simp]:
363 "(a::'a::ring) dvd 0"
365 show "0 = a * 0" by simp
369 "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp
371 lemma dvd_refl_ring [simp]:
372 "(a::'a::ring) dvd a"
374 show "a = a * 1" by simp
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"
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
392 "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
393 apply (unfold dvd_def)
395 apply (rule_tac x = "k * ka" in exI)
399 lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"
402 apply (simp add: unit_mult)
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)
409 apply (rule_tac x = "k + ka" in exI)
410 apply (simp add: r_distr)
413 lemma dvd_uminus_right [simp]:
414 "!! a::'a::ring. a dvd b ==> a dvd -b"
415 apply (unfold dvd_def)
417 apply (rule_tac x = "-k" in exI)
418 apply (simp add: r_minus)
421 lemma dvd_l_mult_right [simp]:
422 "!! a::'a::ring. a dvd b ==> a dvd c*b"
423 apply (unfold dvd_def)
425 apply (rule_tac x = "c * k" in exI)
429 lemma dvd_r_mult_right [simp]:
430 "!! a::'a::ring. a dvd b ==> a dvd b*c"
431 apply (unfold dvd_def)
433 apply (rule_tac x = "k * c" in exI)
438 (* Inverse of multiplication *)
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))
448 lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
449 apply (unfold inverse_def dvd_def)
450 apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
454 apply (rule inverse_unique)
459 lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1"
460 by (simp add: r_inverse_ring)
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)
470 lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"
471 by (simp add: r_inverse_ring)
473 lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"
474 by (simp add: l_inverse_ring)
477 (* fields are integral domains *)
479 lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
480 apply (tactic "step_tac @{claset} 1")
481 apply (rule_tac a = " (a*b) * inverse b" in box_equals)
482 apply (rule_tac [3] refl)
484 apply (simp (no_asm))
489 (* fields are factorial domains *)
491 lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a"
492 unfolding prime_def irred_def by (blast intro: field_ax)