author | wenzelm |
Mon, 15 Oct 2001 20:34:44 +0200 | |
changeset 11780 | d17ee2241257 |
parent 11701 | 3d51fbf81c17 |
child 11914 | bca734def300 |
permissions | -rw-r--r-- |
10479 | 1 |
(* Title: HOL/Library/Ring_and_Field.thy |
2 |
ID: $Id$ |
|
10502 | 3 |
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen |
11780 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
10479 | 5 |
*) |
6 |
||
7 |
header {* |
|
10484 | 8 |
\title{Ring and field structures} |
10502 | 9 |
\author{Gertrud Bauer and Markus Wenzel} |
10479 | 10 |
*} |
11 |
||
12 |
theory Ring_and_Field = Main: |
|
13 |
||
10492 | 14 |
subsection {* Abstract algebraic structures *} |
10479 | 15 |
|
11099 | 16 |
axclass ring \<subseteq> zero, plus, minus, times, number |
10479 | 17 |
add_assoc: "(a + b) + c = a + (b + c)" |
18 |
add_commute: "a + b = b + a" |
|
10610 | 19 |
left_zero [simp]: "0 + a = a" |
20 |
left_minus [simp]: "- a + a = 0" |
|
10620 | 21 |
diff_minus: "a - b = a + (-b)" |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
22 |
zero_number: "0 = Numeral0" |
10479 | 23 |
|
24 |
mult_assoc: "(a * b) * c = a * (b * c)" |
|
25 |
mult_commute: "a * b = b * a" |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
26 |
left_one [simp]: "Numeral1 * a = a" |
10479 | 27 |
|
28 |
left_distrib: "(a + b) * c = a * c + b * c" |
|
29 |
||
11099 | 30 |
axclass ordered_ring \<subseteq> ring, linorder |
10492 | 31 |
add_left_mono: "a \<le> b ==> c + a \<le> c + b" |
32 |
mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b" |
|
33 |
abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)" |
|
10479 | 34 |
|
11099 | 35 |
axclass field \<subseteq> ring, inverse |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
36 |
left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = Numeral1" |
10620 | 37 |
divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b" |
10479 | 38 |
|
11099 | 39 |
axclass ordered_field \<subseteq> ordered_ring, field |
10488 | 40 |
|
11099 | 41 |
axclass division_by_zero \<subseteq> zero, inverse |
10620 | 42 |
inverse_zero: "inverse 0 = 0" |
43 |
divide_zero: "a / 0 = 0" |
|
44 |
||
10610 | 45 |
|
46 |
||
47 |
subsection {* Derived rules *} |
|
48 |
||
49 |
subsubsection {* Derived rules for addition *} |
|
50 |
||
51 |
lemma right_zero [simp]: "a + 0 = (a::'a::ring)" |
|
52 |
proof - |
|
53 |
have "a + 0 = 0 + a" by (simp only: add_commute) |
|
10622 | 54 |
also have "... = a" by simp |
10610 | 55 |
finally show ?thesis . |
56 |
qed |
|
57 |
||
58 |
lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ring))" |
|
59 |
proof - |
|
60 |
have "a + (b + c) = (a + b) + c" by (simp only: add_assoc) |
|
10622 | 61 |
also have "... = (b + a) + c" by (simp only: add_commute) |
10610 | 62 |
finally show ?thesis by (simp only: add_assoc) |
63 |
qed |
|
10544 | 64 |
|
10610 | 65 |
theorems ring_add_ac = add_assoc add_commute add_left_commute |
66 |
||
67 |
lemma right_minus [simp]: "a + -(a::'a::ring) = 0" |
|
68 |
proof - |
|
69 |
have "a + -a = -a + a" by (simp add: ring_add_ac) |
|
10622 | 70 |
also have "... = 0" by simp |
10610 | 71 |
finally show ?thesis . |
72 |
qed |
|
73 |
||
10620 | 74 |
lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))" |
10610 | 75 |
proof |
10620 | 76 |
have "a = a - b + b" by (simp add: diff_minus ring_add_ac) |
10610 | 77 |
also assume "a - b = 0" |
78 |
finally show "a = b" by simp |
|
10620 | 79 |
next |
80 |
assume "a = b" |
|
81 |
thus "a - b = 0" by (simp add: diff_minus) |
|
82 |
qed |
|
10610 | 83 |
|
84 |
lemma diff_self [simp]: "a - (a::'a::ring) = 0" |
|
10620 | 85 |
by (simp add: diff_minus) |
10610 | 86 |
|
87 |
||
88 |
subsubsection {* Derived rules for multiplication *} |
|
10544 | 89 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
90 |
lemma right_one [simp]: "a = a * (Numeral1::'a::field)" |
10610 | 91 |
proof - |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
92 |
have "a = Numeral1 * a" by simp |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
93 |
also have "... = a * Numeral1" by (simp add: mult_commute) |
10610 | 94 |
finally show ?thesis . |
95 |
qed |
|
96 |
||
97 |
lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))" |
|
98 |
proof - |
|
99 |
have "a * (b * c) = (a * b) * c" by (simp only: mult_assoc) |
|
10622 | 100 |
also have "... = (b * a) * c" by (simp only: mult_commute) |
10610 | 101 |
finally show ?thesis by (simp only: mult_assoc) |
102 |
qed |
|
103 |
||
104 |
theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute |
|
105 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
106 |
lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = Numeral1" |
10610 | 107 |
proof - |
108 |
have "a * inverse a = inverse a * a" by (simp add: ring_mult_ac) |
|
109 |
also assume "a \<noteq> 0" |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
110 |
hence "inverse a * a = Numeral1" by simp |
10610 | 111 |
finally show ?thesis . |
112 |
qed |
|
10492 | 113 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
114 |
lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = Numeral1) = (a = (b::'a::field))" |
10610 | 115 |
proof |
10620 | 116 |
assume neq: "b \<noteq> 0" |
117 |
{ |
|
118 |
hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
119 |
also assume "a / b = Numeral1" |
10620 | 120 |
finally show "a = b" by simp |
121 |
next |
|
122 |
assume "a = b" |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
123 |
with neq show "a / b = Numeral1" by (simp add: divide_inverse) |
10620 | 124 |
} |
125 |
qed |
|
10610 | 126 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11099
diff
changeset
|
127 |
lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = Numeral1" |
10620 | 128 |
by (simp add: divide_inverse) |
10610 | 129 |
|
130 |
||
131 |
subsubsection {* Distribution rules *} |
|
132 |
||
133 |
lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::ring)" |
|
134 |
proof - |
|
135 |
have "a * (b + c) = (b + c) * a" by (simp add: ring_mult_ac) |
|
10622 | 136 |
also have "... = b * a + c * a" by (simp only: left_distrib) |
137 |
also have "... = a * b + a * c" by (simp add: ring_mult_ac) |
|
10620 | 138 |
finally show ?thesis . |
10610 | 139 |
qed |
140 |
||
141 |
theorems ring_distrib = right_distrib left_distrib |
|
142 |
||
10484 | 143 |
end |