author  wenzelm 
Mon, 15 Oct 2001 20:34:44 +0200  
changeset 11780  d17ee2241257 
parent 11701  3d51fbf81c17 
child 11914  bca734def300 
permissions  rwrr 
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 