author haftmann Tue Oct 23 11:48:08 2007 +0200 (2007-10-23) changeset 25152 bfde2f8c0f63 parent 25151 9374a0df240c child 25153 af3c7e99fed0
partially localized
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Oct 23 10:53:15 2007 +0200
1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Oct 23 11:48:08 2007 +0200
1.3 @@ -26,6 +26,14 @@
1.4  class semiring = ab_semigroup_add + semigroup_mult +
1.5    assumes left_distrib: "(a + b) * c = a * c + b * c"
1.6    assumes right_distrib: "a * (b + c) = a * b + a * c"
1.7 +begin
1.8 +
1.9 +text{*For the @{text combine_numerals} simproc*}
1.10 +lemma combine_common_factor:
1.11 +  "a * e + (b * e + c) = (a + b) * e + c"
1.13 +
1.14 +end
1.15
1.16  class mult_zero = times + zero +
1.17    assumes mult_zero_left [simp]: "0 * a = 0"
1.18 @@ -42,18 +50,35 @@
1.19      by (simp add: left_distrib [symmetric])
1.20    thus "0 * a = 0"
1.22 -
1.23 +next
1.24 +  fix a :: 'a
1.25    have "a * 0 + a * 0 = a * 0 + 0"
1.26      by (simp add: right_distrib [symmetric])
1.27    thus "a * 0 = 0"
1.29  qed
1.30
1.31 +interpretation semiring_0_cancel \<subseteq> semiring_0
1.32 +proof unfold_locales
1.33 +  fix a :: 'a
1.34 +  have "plus (times zero a) (times zero a) = plus (times zero a) zero"
1.35 +    by (simp add: left_distrib [symmetric])
1.36 +  thus "times zero a = zero"
1.37 +    by (simp only: add_left_cancel)
1.38 +next
1.39 +  fix a :: 'a
1.40 +  have "plus (times a zero) (times a zero) = plus (times a zero) zero"
1.41 +    by (simp add: right_distrib [symmetric])
1.42 +  thus "times a zero = zero"
1.43 +    by (simp only: add_left_cancel)
1.44 +qed
1.45 +
1.46  class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
1.47    assumes distrib: "(a + b) * c = a * c + b * c"
1.48 +begin
1.49
1.50 -instance comm_semiring \<subseteq> semiring
1.51 -proof
1.52 +subclass semiring
1.53 +proof unfold_locales
1.54    fix a b c :: 'a
1.55    show "(a + b) * c = a * c + b * c" by (simp add: distrib)
1.56    have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
1.57 @@ -62,15 +87,20 @@
1.58    finally show "a * (b + c) = a * b + a * c" by blast
1.59  qed
1.60
1.61 -class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
1.62 +end
1.63
1.64 -instance comm_semiring_0 \<subseteq> semiring_0 ..
1.65 +class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
1.66 +begin
1.67 +
1.68 +subclass semiring_0 by unfold_locales
1.69 +
1.70 +end
1.71
1.73
1.74  instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
1.75
1.76 -instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
1.77 +interpretation comm_semiring_0_cancel \<subseteq> semiring_0_cancel by unfold_locales
1.78
1.79  class zero_neq_one = zero + one +
1.80    assumes zero_neq_one [simp]: "0 \<noteq> 1"
1.81 @@ -79,8 +109,11 @@
1.82
1.83  class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
1.84    (*previously almost_semiring*)
1.85 +begin
1.86
1.87 -instance comm_semiring_1 \<subseteq> semiring_1 ..
1.88 +subclass semiring_1 by unfold_locales
1.89 +
1.90 +end
1.91
1.92  class no_zero_divisors = zero + times +
1.93    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
1.94 @@ -90,38 +123,95 @@
1.95
1.96  instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
1.97
1.98 -instance semiring_1_cancel \<subseteq> semiring_1 ..
1.99 +interpretation semiring_1_cancel \<subseteq> semiring_0_cancel by unfold_locales
1.100 +
1.101 +subclass (in semiring_1_cancel) semiring_1 by unfold_locales
1.102
1.103  class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
1.105
1.106  instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
1.107
1.108 -instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
1.109 +interpretation comm_semiring_1_cancel \<subseteq> semiring_1_cancel by unfold_locales
1.110 +
1.111 +subclass (in comm_semiring_1_cancel) comm_semiring_0_cancel by unfold_locales
1.112
1.113  instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
1.114
1.115 +interpretation comm_semiring_1_cancel \<subseteq> comm_semiring_1 by unfold_locales
1.116 +
1.117  class ring = semiring + ab_group_add
1.118
1.119  instance ring \<subseteq> semiring_0_cancel ..
1.120
1.121 +interpretation ring \<subseteq> semiring_0_cancel by unfold_locales
1.122 +
1.123 +context ring
1.124 +begin
1.125 +
1.126 +text {* Distribution rules *}
1.127 +
1.128 +lemma minus_mult_left: "- (a * b) = - a * b"
1.129 +  by (rule equals_zero_I) (simp add: left_distrib [symmetric])
1.130 +
1.131 +lemma minus_mult_right: "- (a * b) = a * - b"
1.132 +  by (rule equals_zero_I) (simp add: right_distrib [symmetric])
1.133 +
1.134 +lemma minus_mult_minus [simp]: "- a * - b = a * b"
1.135 +  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
1.136 +
1.137 +lemma minus_mult_commute: "- a * b = a * - b"
1.138 +  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
1.139 +
1.140 +lemma right_diff_distrib: "a * (b - c) = a * b - a * c"
1.141 +  by (simp add: right_distrib diff_minus
1.142 +    minus_mult_left [symmetric] minus_mult_right [symmetric])
1.143 +
1.144 +lemma left_diff_distrib: "(a - b) * c = a * c - b * c"
1.145 +  by (simp add: left_distrib diff_minus
1.146 +    minus_mult_left [symmetric] minus_mult_right [symmetric])
1.147 +
1.148 +lemmas ring_distribs =
1.149 +  right_distrib left_distrib left_diff_distrib right_diff_distrib
1.150 +
1.151 +end
1.152 +
1.153 +lemmas ring_distribs =
1.154 +  right_distrib left_distrib left_diff_distrib right_diff_distrib
1.155 +
1.156 +text{*This list of rewrites simplifies ring terms by multiplying
1.157 +everything out and bringing sums and products into a canonical form
1.158 +(by ordered rewriting). As a result it decides ring equalities but
1.159 +also helps with inequalities. *}
1.160 +lemmas ring_simps = group_simps ring_distribs
1.161 +
1.162  class comm_ring = comm_semiring + ab_group_add
1.163
1.164  instance comm_ring \<subseteq> ring ..
1.165
1.166 -instance comm_ring \<subseteq> comm_semiring_0_cancel ..
1.167 +interpretation comm_ring \<subseteq> ring by unfold_locales
1.168 +
1.169 +instance comm_ring \<subseteq> comm_semiring_0 ..
1.170 +
1.171 +interpretation comm_ring \<subseteq> comm_semiring_0 by unfold_locales
1.172
1.173  class ring_1 = ring + zero_neq_one + monoid_mult
1.174
1.175  instance ring_1 \<subseteq> semiring_1_cancel ..
1.176
1.177 +interpretation ring_1 \<subseteq> semiring_1_cancel by unfold_locales
1.178 +
1.179  class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
1.180    (*previously ring*)
1.181
1.182  instance comm_ring_1 \<subseteq> ring_1 ..
1.183
1.184 +interpretation comm_ring_1 \<subseteq> ring_1 by unfold_locales
1.185 +
1.186  instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
1.187
1.188 +interpretation comm_ring_1 \<subseteq> comm_semiring_1_cancel by unfold_locales
1.189 +
1.190  class ring_no_zero_divisors = ring + no_zero_divisors
1.191
1.192  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
1.193 @@ -130,6 +220,8 @@
1.194
1.195  instance idom \<subseteq> ring_1_no_zero_divisors ..
1.196
1.197 +interpretation idom \<subseteq> ring_1_no_zero_divisors by unfold_locales
1.198 +
1.199  class division_ring = ring_1 + inverse +
1.200    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
1.201    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
1.202 @@ -152,6 +244,24 @@
1.203    qed
1.204  qed
1.205
1.206 +interpretation division_ring \<subseteq> ring_1_no_zero_divisors
1.207 +proof unfold_locales
1.208 +  fix a b :: 'a
1.209 +  assume a: "a \<noteq> zero" and b: "b \<noteq> zero"
1.210 +  show "times a b \<noteq> zero"
1.211 +  proof
1.212 +    assume ab: "times a b = zero"
1.213 +    hence "zero = times (times (inverse a) (times a b)) (inverse b)"
1.214 +      by simp
1.215 +    also have "\<dots> = times (times (inverse a) a) (times b (inverse b))"
1.216 +      by (simp only: mult_assoc)
1.217 +    also have "\<dots> = one"
1.218 +      using a b by simp
1.219 +    finally show False
1.220 +      by simp
1.221 +  qed
1.222 +qed
1.223 +
1.224  class field = comm_ring_1 + inverse +
1.225    assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
1.226    assumes divide_inverse: "a / b = a * inverse b"
1.227 @@ -164,52 +274,19 @@
1.228    thus "a * inverse a = 1" by (simp only: mult_commute)
1.229  qed
1.230
1.231 -instance field \<subseteq> idom ..
1.232 +interpretation field \<subseteq> division_ring
1.233 +proof unfold_locales
1.234 +  fix a :: 'a
1.235 +  assume "a \<noteq> zero"
1.236 +  thus "times (inverse a) a = one" by (rule field_inverse)
1.237 +  thus "times a (inverse a) = one" by (simp only: mult_commute)
1.238 +qed
1.239 +
1.240 +subclass (in field) idom by unfold_locales
1.241
1.242  class division_by_zero = zero + inverse +
1.243    assumes inverse_zero [simp]: "inverse 0 = 0"
1.244
1.245 -
1.246 -subsection {* Distribution rules *}
1.247 -
1.248 -text{*For the @{text combine_numerals} simproc*}
1.249 -lemma combine_common_factor:
1.250 -     "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
1.252 -
1.253 -lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
1.254 -apply (rule equals_zero_I)
1.255 -apply (simp add: left_distrib [symmetric])
1.256 -done
1.257 -
1.258 -lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"
1.259 -apply (rule equals_zero_I)
1.260 -apply (simp add: right_distrib [symmetric])
1.261 -done
1.262 -
1.263 -lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"
1.264 -  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
1.265 -
1.266 -lemma minus_mult_commute: "(- a) * b = a * (- b::'a::ring)"
1.267 -  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
1.268 -
1.269 -lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
1.270 -by (simp add: right_distrib diff_minus
1.271 -              minus_mult_left [symmetric] minus_mult_right [symmetric])
1.272 -
1.273 -lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)"
1.274 -by (simp add: left_distrib diff_minus
1.275 -              minus_mult_left [symmetric] minus_mult_right [symmetric])
1.276 -
1.277 -lemmas ring_distribs =
1.278 -  right_distrib left_distrib left_diff_distrib right_diff_distrib
1.279 -
1.280 -text{*This list of rewrites simplifies ring terms by multiplying
1.281 -everything out and bringing sums and products into a canonical form
1.282 -(by ordered rewriting). As a result it decides ring equalities but
1.283 -also helps with inequalities. *}
1.284 -lemmas ring_simps = group_simps ring_distribs
1.285 -
1.286  class mult_mono = times + zero + ord +
1.287    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1.288    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
1.289 @@ -221,18 +298,24 @@
1.290
1.291  instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
1.292
1.293 -instance pordered_cancel_semiring \<subseteq> pordered_semiring ..
1.294 +interpretation pordered_cancel_semiring \<subseteq> semiring_0_cancel by unfold_locales
1.295 +
1.296 +subclass (in pordered_cancel_semiring) pordered_semiring by unfold_locales
1.297
1.299
1.300  instance ordered_semiring \<subseteq> pordered_cancel_semiring ..
1.301
1.302 +interpretation ordered_semiring \<subseteq> pordered_cancel_semiring by unfold_locales
1.303 +
1.305    assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
1.306    assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
1.307
1.308  instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
1.309
1.310 +interpretation ordered_semiring_strict \<subseteq> semiring_0_cancel by unfold_locales
1.311 +
1.312  instance ordered_semiring_strict \<subseteq> ordered_semiring
1.313  proof
1.314    fix a b c :: 'a
1.315 @@ -245,6 +328,18 @@
1.316      using mult_strict_right_mono by auto
1.317  qed
1.318
1.319 +interpretation ordered_semiring_strict \<subseteq> ordered_semiring
1.320 +proof unfold_locales
1.321 +  fix a b c :: 'a
1.322 +  assume A: "less_eq a b" "less_eq zero c"
1.323 +  from A show "less_eq (times c a) (times c b)"
1.324 +    unfolding le_less
1.325 +    using mult_strict_left_mono by (cases "c = zero") auto
1.326 +  from A show "less_eq (times a c) (times b c)"
1.327 +    unfolding le_less
1.328 +    using mult_strict_right_mono by (cases "c = zero") auto
1.329 +qed
1.330 +
1.331  class mult_mono1 = times + zero + ord +
1.332    assumes mult_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1.333
1.334 @@ -253,7 +348,9 @@
1.335
1.336  class pordered_cancel_comm_semiring = comm_semiring_0_cancel