10479
|
1 |
(* Title: HOL/Library/Ring_and_Field.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gertrud Bauer, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {*
|
|
7 |
\title{Rings and Fields}
|
|
8 |
\author{Gertrud Bauer}
|
|
9 |
*}
|
|
10 |
|
|
11 |
theory Ring_and_Field = Main:
|
|
12 |
|
|
13 |
|
|
14 |
axclass ring < plus, minus, times, number
|
|
15 |
add_assoc: "(a + b) + c = a + (b + c)"
|
|
16 |
add_commute: "a + b = b + a"
|
|
17 |
left_zero: "#0 + a = a"
|
|
18 |
left_neg: "(- a) + a = #0"
|
|
19 |
minus_uminus: "a - b = a + (- b)"
|
|
20 |
|
|
21 |
mult_assoc: "(a * b) * c = a * (b * c)"
|
|
22 |
mult_commute: "a * b = b * a"
|
|
23 |
left_one: "#1 * a = a"
|
|
24 |
|
|
25 |
left_distrib: "(a + b) * c = a * c + b * c"
|
|
26 |
|
|
27 |
|
|
28 |
axclass field < ring, inverse
|
|
29 |
left_inverse: "a \<noteq> #0 \<Longrightarrow> inverse a * a = #1"
|
|
30 |
divides_inverse: "a / b = a * inverse b"
|
|
31 |
|
|
32 |
end |