1 (* |
|
2 Title: The algebraic hierarchy of rings as axiomatic classes |
|
3 Id: $Id$ |
|
4 Author: Clemens Ballarin, started 9 December 1996 |
|
5 Copyright: Clemens Ballarin |
|
6 *) |
|
7 |
|
8 header {* The algebraic hierarchy of rings as axiomatic classes *} |
|
9 |
|
10 theory Ring imports Main |
|
11 uses ("order.ML") begin |
|
12 |
|
13 section {* Constants *} |
|
14 |
|
15 text {* Most constants are already declared by HOL. *} |
|
16 |
|
17 consts |
|
18 assoc :: "['a::times, 'a] => bool" (infixl 50) |
|
19 irred :: "'a::{zero, one, times} => bool" |
|
20 prime :: "'a::{zero, one, times} => bool" |
|
21 |
|
22 section {* Axioms *} |
|
23 |
|
24 subsection {* Ring axioms *} |
|
25 |
|
26 axclass ring < zero, one, plus, minus, times, inverse, power |
|
27 |
|
28 a_assoc: "(a + b) + c = a + (b + c)" |
|
29 l_zero: "0 + a = a" |
|
30 l_neg: "(-a) + a = 0" |
|
31 a_comm: "a + b = b + a" |
|
32 |
|
33 m_assoc: "(a * b) * c = a * (b * c)" |
|
34 l_one: "1 * a = a" |
|
35 |
|
36 l_distr: "(a + b) * c = a * c + b * c" |
|
37 |
|
38 m_comm: "a * b = b * a" |
|
39 |
|
40 -- {* Definition of derived operations *} |
|
41 |
|
42 minus_def: "a - b = a + (-b)" |
|
43 inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" |
|
44 divide_def: "a / b = a * inverse b" |
|
45 power_def: "a ^ n = nat_rec 1 (%u b. b * a) n" |
|
46 |
|
47 defs |
|
48 assoc_def: "a assoc b == a dvd b & b dvd a" |
|
49 irred_def: "irred a == a ~= 0 & ~ a dvd 1 |
|
50 & (ALL d. d dvd a --> d dvd 1 | a dvd d)" |
|
51 prime_def: "prime p == p ~= 0 & ~ p dvd 1 |
|
52 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)" |
|
53 |
|
54 subsection {* Integral domains *} |
|
55 |
|
56 axclass |
|
57 "domain" < ring |
|
58 |
|
59 one_not_zero: "1 ~= 0" |
|
60 integral: "a * b = 0 ==> a = 0 | b = 0" |
|
61 |
|
62 subsection {* Factorial domains *} |
|
63 |
|
64 axclass |
|
65 factorial < "domain" |
|
66 |
|
67 (* |
|
68 Proper definition using divisor chain condition currently not supported. |
|
69 factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}" |
|
70 *) |
|
71 factorial_divisor: "True" |
|
72 factorial_prime: "irred a ==> prime a" |
|
73 |
|
74 subsection {* Euclidean domains *} |
|
75 |
|
76 (* |
|
77 axclass |
|
78 euclidean < "domain" |
|
79 |
|
80 euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). |
|
81 a = b * q + r & e_size r < e_size b)" |
|
82 |
|
83 Nothing has been proved about Euclidean domains, yet. |
|
84 Design question: |
|
85 Fix quo, rem and e_size as constants that are axiomatised with |
|
86 euclidean_ax? |
|
87 - advantage: more pragmatic and easier to use |
|
88 - disadvantage: for every type, one definition of quo and rem will |
|
89 be fixed, users may want to use differing ones; |
|
90 also, it seems not possible to prove that fields are euclidean |
|
91 domains, because that would require generic (type-independent) |
|
92 definitions of quo and rem. |
|
93 *) |
|
94 |
|
95 subsection {* Fields *} |
|
96 |
|
97 axclass |
|
98 field < ring |
|
99 |
|
100 field_one_not_zero: "1 ~= 0" |
|
101 (* Avoid a common superclass as the first thing we will |
|
102 prove about fields is that they are domains. *) |
|
103 field_ax: "a ~= 0 ==> a dvd 1" |
|
104 |
|
105 section {* Basic facts *} |
|
106 |
|
107 subsection {* Normaliser for rings *} |
|
108 |
|
109 use "order.ML" |
|
110 |
|
111 method_setup ring = |
|
112 {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *} |
|
113 {* computes distributive normal form in rings *} |
|
114 |
|
115 |
|
116 subsection {* Rings and the summation operator *} |
|
117 |
|
118 (* Basic facts --- move to HOL!!! *) |
|
119 |
|
120 (* needed because natsum_cong (below) disables atMost_0 *) |
|
121 lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)" |
|
122 by simp |
|
123 (* |
|
124 lemma natsum_Suc [simp]: |
|
125 "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)" |
|
126 by (simp add: atMost_Suc) |
|
127 *) |
|
128 lemma natsum_Suc2: |
|
129 "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})" |
|
130 proof (induct n) |
|
131 case 0 show ?case by simp |
|
132 next |
|
133 case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) |
|
134 qed |
|
135 |
|
136 lemma natsum_cong [cong]: |
|
137 "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> |
|
138 setsum f {..j} = setsum g {..k}" |
|
139 by (induct j) auto |
|
140 |
|
141 lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)" |
|
142 by (induct n) simp_all |
|
143 |
|
144 lemma natsum_add [simp]: |
|
145 "!!f::nat=>'a::comm_monoid_add. |
|
146 setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" |
|
147 by (induct n) (simp_all add: add_ac) |
|
148 |
|
149 (* Facts specific to rings *) |
|
150 |
|
151 instance ring < comm_monoid_add |
|
152 proof |
|
153 fix x y z |
|
154 show "(x::'a::ring) + y = y + x" by (rule a_comm) |
|
155 show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc) |
|
156 show "0 + (x::'a::ring) = x" by (rule l_zero) |
|
157 qed |
|
158 |
|
159 ML {* |
|
160 local |
|
161 val lhss = |
|
162 ["t + u::'a::ring", |
|
163 "t - u::'a::ring", |
|
164 "t * u::'a::ring", |
|
165 "- t::'a::ring"]; |
|
166 fun proc ss t = |
|
167 let val rew = Goal.prove (Simplifier.the_context ss) [] [] |
|
168 (HOLogic.mk_Trueprop |
|
169 (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) |
|
170 (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) |
|
171 |> mk_meta_eq; |
|
172 val (t', u) = Logic.dest_equals (Thm.prop_of rew); |
|
173 in if t' aconv u |
|
174 then NONE |
|
175 else SOME rew |
|
176 end; |
|
177 in |
|
178 val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc); |
|
179 end; |
|
180 *} |
|
181 |
|
182 ML_setup {* Addsimprocs [ring_simproc] *} |
|
183 |
|
184 lemma natsum_ldistr: |
|
185 "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}" |
|
186 by (induct n) simp_all |
|
187 |
|
188 lemma natsum_rdistr: |
|
189 "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}" |
|
190 by (induct n) simp_all |
|
191 |
|
192 subsection {* Integral Domains *} |
|
193 |
|
194 declare one_not_zero [simp] |
|
195 |
|
196 lemma zero_not_one [simp]: |
|
197 "0 ~= (1::'a::domain)" |
|
198 by (rule not_sym) simp |
|
199 |
|
200 lemma integral_iff: (* not by default a simp rule! *) |
|
201 "(a * b = (0::'a::domain)) = (a = 0 | b = 0)" |
|
202 proof |
|
203 assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral) |
|
204 next |
|
205 assume "a = 0 | b = 0" then show "a * b = 0" by auto |
|
206 qed |
|
207 |
|
208 (* |
|
209 lemma "(a::'a::ring) - (a - b) = b" apply simp |
|
210 simproc seems to fail on this example (fixed with new term order) |
|
211 *) |
|
212 (* |
|
213 lemma bug: "(b::'a::ring) - (b - a) = a" by simp |
|
214 simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" |
|
215 *) |
|
216 lemma m_lcancel: |
|
217 assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)" |
|
218 proof |
|
219 assume eq: "a * b = a * c" |
|
220 then have "a * (b - c) = 0" by simp |
|
221 then have "a = 0 | (b - c) = 0" by (simp only: integral_iff) |
|
222 with prem have "b - c = 0" by auto |
|
223 then have "b = b - (b - c)" by simp |
|
224 also have "b - (b - c) = c" by simp |
|
225 finally show "b = c" . |
|
226 next |
|
227 assume "b = c" then show "a * b = a * c" by simp |
|
228 qed |
|
229 |
|
230 lemma m_rcancel: |
|
231 "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" |
|
232 by (simp add: m_lcancel) |
|
233 |
|
234 end |
|