partially localized
authorhaftmann
Tue Oct 23 11:48:08 2007 +0200 (2007-10-23)
changeset 25152bfde2f8c0f63
parent 25151 9374a0df240c
child 25153 af3c7e99fed0
partially localized
src/HOL/Ring_and_Field.thy
     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.12 +  by (simp add: left_distrib add_ac)
    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.21      by (simp only: add_left_cancel)
    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.28      by (simp only: add_left_cancel)
    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.72  class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
    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.104    + zero_neq_one + cancel_ab_semigroup_add
   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.251 -by (simp add: left_distrib add_ac)
   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.298  class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   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.304  class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   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
   1.337    + pordered_ab_semigroup_add + mult_mono1
   1.338 -  
   1.339 +
   1.340 +-- {*FIXME: continue localization here*}
   1.341 +
   1.342  instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
   1.343  
   1.344  class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +