7998
|
1 |
(*
|
13735
|
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
|
7998
|
6 |
*)
|
|
7 |
|
13735
|
8 |
header {* The algebraic hierarchy of rings as axiomatic classes *}
|
7998
|
9 |
|
13735
|
10 |
theory Ring = Main
|
|
11 |
files ("order.ML"):
|
7998
|
12 |
|
13735
|
13 |
section {* Constants *}
|
|
14 |
|
|
15 |
text {* Most constants are already declared by HOL. *}
|
7998
|
16 |
|
|
17 |
consts
|
13735
|
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"
|
7998
|
35 |
|
13735
|
36 |
l_distr: "(a + b) * c = a * c + b * c"
|
|
37 |
|
|
38 |
m_comm: "a * b = b * a"
|
|
39 |
|
|
40 |
-- {* Definition of derived operations *}
|
7998
|
41 |
|
13735
|
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"
|
7998
|
46 |
|
13735
|
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 *}
|
7998
|
55 |
|
|
56 |
axclass
|
13735
|
57 |
"domain" < ring
|
7998
|
58 |
|
13735
|
59 |
one_not_zero: "1 ~= 0"
|
|
60 |
integral: "a * b = 0 ==> a = 0 | b = 0"
|
7998
|
61 |
|
13735
|
62 |
subsection {* Factorial domains *}
|
7998
|
63 |
|
|
64 |
axclass
|
13735
|
65 |
factorial < "domain"
|
7998
|
66 |
|
|
67 |
(*
|
|
68 |
Proper definition using divisor chain condition currently not supported.
|
13735
|
69 |
factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}"
|
7998
|
70 |
*)
|
13735
|
71 |
factorial_divisor: "True"
|
|
72 |
factorial_prime: "irred a ==> prime a"
|
7998
|
73 |
|
13735
|
74 |
subsection {* Euclidean domains *}
|
7998
|
75 |
|
|
76 |
(*
|
|
77 |
axclass
|
13735
|
78 |
euclidean < "domain"
|
7998
|
79 |
|
13735
|
80 |
euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
|
7998
|
81 |
a = b * q + r & e_size r < e_size b)"
|
|
82 |
|
13735
|
83 |
Nothing has been proved about Euclidean domains, yet.
|
7998
|
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 |
|
13735
|
95 |
subsection {* Fields *}
|
7998
|
96 |
|
|
97 |
axclass
|
|
98 |
field < ring
|
|
99 |
|
13735
|
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 |
lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
|
|
121 |
by simp
|
|
122 |
|
|
123 |
lemma natsum_Suc [simp]:
|
|
124 |
"setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
|
|
125 |
by (simp add: atMost_Suc)
|
|
126 |
|
|
127 |
lemma natsum_Suc2:
|
|
128 |
"setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
|
|
129 |
proof (induct n)
|
|
130 |
case 0 show ?case by simp
|
|
131 |
next
|
14439
|
132 |
case Suc thus ?case by (simp add: plus_ac0.assoc)
|
13735
|
133 |
qed
|
|
134 |
|
|
135 |
lemma natsum_cong [cong]:
|
|
136 |
"!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
|
|
137 |
setsum f {..j} = setsum g {..k}"
|
|
138 |
by (induct j) auto
|
|
139 |
|
|
140 |
lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
|
|
141 |
by (induct n) simp_all
|
|
142 |
|
|
143 |
lemma natsum_add [simp]:
|
|
144 |
"!!f::nat=>'a::plus_ac0.
|
|
145 |
setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
|
|
146 |
by (induct n) (simp_all add: plus_ac0)
|
|
147 |
|
|
148 |
(* Facts specific to rings *)
|
|
149 |
|
|
150 |
instance ring < plus_ac0
|
|
151 |
proof
|
|
152 |
fix x y z
|
|
153 |
show "(x::'a::ring) + y = y + x" by (rule a_comm)
|
|
154 |
show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
|
|
155 |
show "0 + (x::'a::ring) = x" by (rule l_zero)
|
|
156 |
qed
|
|
157 |
|
|
158 |
ML {*
|
|
159 |
local
|
|
160 |
val lhss =
|
|
161 |
[read_cterm (sign_of (the_context ()))
|
|
162 |
("?t + ?u::'a::ring", TVar (("'z", 0), [])),
|
|
163 |
read_cterm (sign_of (the_context ()))
|
|
164 |
("?t - ?u::'a::ring", TVar (("'z", 0), [])),
|
|
165 |
read_cterm (sign_of (the_context ()))
|
|
166 |
("?t * ?u::'a::ring", TVar (("'z", 0), [])),
|
|
167 |
read_cterm (sign_of (the_context ()))
|
|
168 |
("- ?t::'a::ring", TVar (("'z", 0), []))
|
|
169 |
];
|
|
170 |
fun proc sg _ t =
|
|
171 |
let val rew = Tactic.prove sg [] []
|
|
172 |
(HOLogic.mk_Trueprop
|
|
173 |
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
|
|
174 |
(fn _ => simp_tac ring_ss 1)
|
|
175 |
|> mk_meta_eq;
|
|
176 |
val (t', u) = Logic.dest_equals (Thm.prop_of rew);
|
|
177 |
in if t' aconv u
|
|
178 |
then None
|
|
179 |
else Some rew
|
|
180 |
end;
|
|
181 |
in
|
|
182 |
val ring_simproc = mk_simproc "ring" lhss proc;
|
|
183 |
end;
|
|
184 |
*}
|
|
185 |
|
|
186 |
ML_setup {* Addsimprocs [ring_simproc] *}
|
|
187 |
|
|
188 |
lemma natsum_ldistr:
|
|
189 |
"!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
|
|
190 |
by (induct n) simp_all
|
|
191 |
|
|
192 |
lemma natsum_rdistr:
|
|
193 |
"!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
|
|
194 |
by (induct n) simp_all
|
|
195 |
|
|
196 |
subsection {* Integral Domains *}
|
|
197 |
|
|
198 |
declare one_not_zero [simp]
|
|
199 |
|
|
200 |
lemma zero_not_one [simp]:
|
|
201 |
"0 ~= (1::'a::domain)"
|
|
202 |
by (rule not_sym) simp
|
|
203 |
|
|
204 |
lemma integral_iff: (* not by default a simp rule! *)
|
|
205 |
"(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
|
|
206 |
proof
|
|
207 |
assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
|
|
208 |
next
|
|
209 |
assume "a = 0 | b = 0" then show "a * b = 0" by auto
|
|
210 |
qed
|
|
211 |
|
|
212 |
(*
|
|
213 |
lemma "(a::'a::ring) - (a - b) = b" apply simp
|
13783
|
214 |
simproc seems to fail on this example (fixed with new term order)
|
13735
|
215 |
*)
|
13783
|
216 |
(*
|
13735
|
217 |
lemma bug: "(b::'a::ring) - (b - a) = a" by simp
|
13783
|
218 |
simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
|
|
219 |
*)
|
13735
|
220 |
lemma m_lcancel:
|
|
221 |
assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
|
|
222 |
proof
|
|
223 |
assume eq: "a * b = a * c"
|
|
224 |
then have "a * (b - c) = 0" by simp
|
|
225 |
then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
|
|
226 |
with prem have "b - c = 0" by auto
|
|
227 |
then have "b = b - (b - c)" by simp
|
13783
|
228 |
also have "b - (b - c) = c" by simp
|
13735
|
229 |
finally show "b = c" .
|
|
230 |
next
|
|
231 |
assume "b = c" then show "a * b = a * c" by simp
|
|
232 |
qed
|
|
233 |
|
|
234 |
lemma m_rcancel:
|
|
235 |
"(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
|
|
236 |
by (simp add: m_lcancel)
|
7998
|
237 |
|
|
238 |
end
|