|
1 (* |
|
2 Abstract class ring (commutative, with 1) |
|
3 $Id$ |
|
4 Author: Clemens Ballarin, started 9 December 1996 |
|
5 *) |
|
6 |
|
7 Ring = Main + |
|
8 |
|
9 (* Syntactic class ring *) |
|
10 |
|
11 axclass |
|
12 ringS < plus, minus, times, power |
|
13 |
|
14 consts |
|
15 (* Basic rings *) |
|
16 "<0>" :: 'a::ringS ("<0>") |
|
17 "<1>" :: 'a::ringS ("<1>") |
|
18 "--" :: ['a, 'a] => 'a::ringS (infixl 65) |
|
19 |
|
20 (* Divisibility *) |
|
21 assoc :: ['a::times, 'a] => bool (infixl 70) |
|
22 irred :: 'a::ringS => bool |
|
23 prime :: 'a::ringS => bool |
|
24 |
|
25 (* Fields *) |
|
26 inverse :: 'a::ringS => 'a |
|
27 "'/'/" :: ['a, 'a] => 'a::ringS (infixl 70) |
|
28 |
|
29 translations |
|
30 "a -- b" == "a + (-b)" |
|
31 "a // b" == "a * inverse b" |
|
32 |
|
33 (* Class ring and ring axioms *) |
|
34 |
|
35 axclass |
|
36 ring < ringS |
|
37 |
|
38 a_assoc "(a + b) + c = a + (b + c)" |
|
39 l_zero "<0> + a = a" |
|
40 l_neg "(-a) + a = <0>" |
|
41 a_comm "a + b = b + a" |
|
42 |
|
43 m_assoc "(a * b) * c = a * (b * c)" |
|
44 l_one "<1> * a = a" |
|
45 |
|
46 l_distr "(a + b) * c = a * c + b * c" |
|
47 |
|
48 m_comm "a * b = b * a" |
|
49 |
|
50 one_not_zero "<1> ~= <0>" |
|
51 (* if <1> = <0>, then the ring has only one element! *) |
|
52 |
|
53 power_ax "a ^ n = nat_rec <1> (%u b. b * a) n" |
|
54 |
|
55 defs |
|
56 assoc_def "a assoc b == a dvd b & b dvd a" |
|
57 irred_def "irred a == a ~= <0> & ~ a dvd <1> |
|
58 & (ALL d. d dvd a --> d dvd <1> | a dvd d)" |
|
59 prime_def "prime p == p ~= <0> & ~ p dvd <1> |
|
60 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)" |
|
61 |
|
62 inverse_def "inverse a == if a dvd <1> then @x. a*x = <1> else <0>" |
|
63 |
|
64 (* Integral domains *) |
|
65 |
|
66 axclass |
|
67 domain < ring |
|
68 |
|
69 integral "a * b = <0> ==> a = <0> | b = <0>" |
|
70 |
|
71 (* Factorial domains *) |
|
72 |
|
73 axclass |
|
74 factorial < domain |
|
75 |
|
76 (* |
|
77 Proper definition using divisor chain condition currently not supported. |
|
78 factorial_divisor "wf {(a, b). a dvd b & ~ (b dvd a)}" |
|
79 *) |
|
80 factorial_divisor "True" |
|
81 factorial_prime "irred a ==> prime a" |
|
82 |
|
83 (* Euclidean domains *) |
|
84 |
|
85 (* |
|
86 axclass |
|
87 euclidean < domain |
|
88 |
|
89 euclidean_ax "b ~= <0> ==> Ex (% (q, r, e_size::('a::ringS)=>nat). |
|
90 a = b * q + r & e_size r < e_size b)" |
|
91 |
|
92 Nothing has been proved about euclidean domains, yet. |
|
93 Design question: |
|
94 Fix quo, rem and e_size as constants that are axiomatised with |
|
95 euclidean_ax? |
|
96 - advantage: more pragmatic and easier to use |
|
97 - disadvantage: for every type, one definition of quo and rem will |
|
98 be fixed, users may want to use differing ones; |
|
99 also, it seems not possible to prove that fields are euclidean |
|
100 domains, because that would require generic (type-independent) |
|
101 definitions of quo and rem. |
|
102 *) |
|
103 |
|
104 (* Fields *) |
|
105 |
|
106 axclass |
|
107 field < ring |
|
108 |
|
109 field_ax "a ~= <0> ==> a dvd <1>" |
|
110 |
|
111 end |