1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Algebra/abstract/Ring.ML Fri Nov 05 11:14:26 1999 +0100
1.3 @@ -0,0 +1,396 @@
1.4 +(*
1.5 + Abstract class ring (commutative, with 1)
1.6 + $Id$
1.7 + Author: Clemens Ballarin, started 9 December 1996
1.8 +*)
1.9 +
1.10 +open Ring;
1.11 +
1.12 +Blast.overloaded ("Divides.op dvd", domain_type);
1.13 +
1.14 +section "Rings";
1.15 +
1.16 +fun make_left_commute assoc commute s =
1.17 + [rtac (commute RS trans) 1, rtac (assoc RS trans) 1,
1.18 + rtac (commute RS arg_cong) 1];
1.19 +
1.20 +(* addition *)
1.21 +
1.22 +qed_goal "a_lcomm" Ring.thy "!!a::'a::ring. a+(b+c) = b+(a+c)"
1.23 + (make_left_commute a_assoc a_comm);
1.24 +
1.25 +val a_ac = [a_assoc, a_comm, a_lcomm];
1.26 +
1.27 +qed_goal "r_zero" Ring.thy "!!a::'a::ring. a + <0> = a"
1.28 + (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
1.29 +
1.30 +qed_goal "r_neg" Ring.thy "!!a::'a::ring. a + (-a) = <0>"
1.31 + (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
1.32 +
1.33 +Goal "!! a::'a::ring. a + b = a + c ==> b = c";
1.34 +by (rtac box_equals 1);
1.35 +by (rtac l_zero 2);
1.36 +by (rtac l_zero 2);
1.37 +by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1);
1.38 +by (asm_simp_tac (simpset() addsimps [a_assoc]) 1);
1.39 +qed "a_lcancel";
1.40 +
1.41 +Goal "!! a::'a::ring. b + a = c + a ==> b = c";
1.42 +by (rtac a_lcancel 1);
1.43 +by (asm_simp_tac (simpset() addsimps a_ac) 1);
1.44 +qed "a_rcancel";
1.45 +
1.46 +Goal "!! a::'a::ring. (a + b = a + c) = (b = c)";
1.47 +by (auto_tac (claset() addSDs [a_lcancel], simpset()));
1.48 +qed "a_lcancel_eq";
1.49 +
1.50 +Goal "!! a::'a::ring. (b + a = c + a) = (b = c)";
1.51 +by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1);
1.52 +qed "a_rcancel_eq";
1.53 +
1.54 +Addsimps [a_lcancel_eq, a_rcancel_eq];
1.55 +
1.56 +Goal "!!a::'a::ring. -(-a) = a";
1.57 +by (rtac a_lcancel 1);
1.58 +by (rtac (r_neg RS trans) 1);
1.59 +by (rtac (l_neg RS sym) 1);
1.60 +qed "minus_minus";
1.61 +
1.62 +Goal "- <0> = (<0>::'a::ring)";
1.63 +by (rtac a_lcancel 1);
1.64 +by (rtac (r_neg RS trans) 1);
1.65 +by (rtac (l_zero RS sym) 1);
1.66 +qed "minus0";
1.67 +
1.68 +Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)";
1.69 +by (res_inst_tac [("a", "a+b")] a_lcancel 1);
1.70 +by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1);
1.71 +qed "minus_add";
1.72 +
1.73 +(* multiplication *)
1.74 +
1.75 +qed_goal "m_lcomm" Ring.thy "!!a::'a::ring. a*(b*c) = b*(a*c)"
1.76 + (make_left_commute m_assoc m_comm);
1.77 +
1.78 +val m_ac = [m_assoc, m_comm, m_lcomm];
1.79 +
1.80 +qed_goal "r_one" Ring.thy "!!a::'a::ring. a * <1> = a"
1.81 + (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
1.82 +
1.83 +(* distributive and derived *)
1.84 +
1.85 +Goal "!!a::'a::ring. a * (b + c) = a * b + a * c";
1.86 +by (rtac (m_comm RS trans) 1);
1.87 +by (rtac (l_distr RS trans) 1);
1.88 +by (simp_tac (simpset() addsimps [m_comm]) 1);
1.89 +qed "r_distr";
1.90 +
1.91 +val m_distr = m_ac @ [l_distr, r_distr];
1.92 +
1.93 +(* the following two proofs can be found in
1.94 + Jacobson, Basic Algebra I, pp. 88-89 *)
1.95 +
1.96 +Goal "!!a::'a::ring. <0> * a = <0>";
1.97 +by (rtac a_lcancel 1);
1.98 +by (rtac (l_distr RS sym RS trans) 1);
1.99 +by (simp_tac (simpset() addsimps [r_zero]) 1);
1.100 +qed "l_null";
1.101 +
1.102 +qed_goal "r_null" Ring.thy "!!a::'a::ring. a * <0> = <0>"
1.103 + (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
1.104 +
1.105 +Goal "!!a::'a::ring. (-a) * b = - (a * b)";
1.106 +by (rtac a_lcancel 1);
1.107 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
1.108 +by (rtac (l_distr RS sym RS trans) 1);
1.109 +by (simp_tac (simpset() addsimps [l_null, r_neg]) 1);
1.110 +qed "l_minus";
1.111 +
1.112 +Goal "!!a::'a::ring. a * (-b) = - (a * b)";
1.113 +by (rtac a_lcancel 1);
1.114 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
1.115 +by (rtac (r_distr RS sym RS trans) 1);
1.116 +by (simp_tac (simpset() addsimps [r_null, r_neg]) 1);
1.117 +qed "r_minus";
1.118 +
1.119 +val m_minus = [l_minus, r_minus];
1.120 +
1.121 +(* one and zero are distinct *)
1.122 +
1.123 +qed_goal "zero_not_one" Ring.thy "<0> ~= (<1>::'a::ring)"
1.124 + (fn _ => [rtac not_sym 1, rtac one_not_zero 1]);
1.125 +
1.126 +Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0,
1.127 + l_one, r_one, l_null, r_null,
1.128 + one_not_zero, zero_not_one];
1.129 +
1.130 +(* further rules *)
1.131 +
1.132 +Goal "!!a::'a::ring. -a = <0> ==> a = <0>";
1.133 +by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1);
1.134 +by (Asm_simp_tac 1);
1.135 +qed "uminus_monom";
1.136 +
1.137 +Goal "!!a::'a::ring. a ~= <0> ==> -a ~= <0>";
1.138 +by (etac contrapos 1);
1.139 +by (rtac uminus_monom 1);
1.140 +by (assume_tac 1);
1.141 +qed "uminus_monom_neq";
1.142 +
1.143 +Goal "!!a::'a::ring. a * b ~= <0> ==> a ~= <0>";
1.144 +by (etac contrapos 1);
1.145 +by (Asm_simp_tac 1);
1.146 +qed "l_nullD";
1.147 +
1.148 +Goal "!!a::'a::ring. a * b ~= <0> ==> b ~= <0>";
1.149 +by (etac contrapos 1);
1.150 +by (Asm_simp_tac 1);
1.151 +qed "r_nullD";
1.152 +
1.153 +(* reflection between a = b and a -- b = <0> *)
1.154 +
1.155 +Goal "!!a::'a::ring. a = b ==> a + (-b) = <0>";
1.156 +by (Asm_simp_tac 1);
1.157 +qed "eq_imp_diff_zero";
1.158 +
1.159 +Goal "!!a::'a::ring. a + (-b) = <0> ==> a = b";
1.160 +by (res_inst_tac [("a", "-b")] a_rcancel 1);
1.161 +by (Asm_simp_tac 1);
1.162 +qed "diff_zero_imp_eq";
1.163 +
1.164 +(* this could be a rewrite rule, but won't terminate
1.165 + ==> make it a simproc?
1.166 +Goal "!!a::'a::ring. (a = b) = (a -- b = <0>)";
1.167 +*)
1.168 +
1.169 +(* Power *)
1.170 +
1.171 +Goal "!!a::'a::ring. a ^ 0 = <1>";
1.172 +by (simp_tac (simpset() addsimps [power_ax]) 1);
1.173 +qed "power_0";
1.174 +
1.175 +Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
1.176 +by (simp_tac (simpset() addsimps [power_ax]) 1);
1.177 +qed "power_Suc";
1.178 +
1.179 +Addsimps [power_0, power_Suc];
1.180 +
1.181 +Goal "<1> ^ n = (<1>::'a::ring)";
1.182 +by (nat_ind_tac "n" 1);
1.183 +by (Simp_tac 1);
1.184 +by (Asm_simp_tac 1);
1.185 +qed "power_one";
1.186 +
1.187 +Goal "!!n. n ~= 0 ==> <0> ^ n = (<0>::'a::ring)";
1.188 +by (etac rev_mp 1);
1.189 +by (nat_ind_tac "n" 1);
1.190 +by (Simp_tac 1);
1.191 +by (Simp_tac 1);
1.192 +qed "power_zero";
1.193 +
1.194 +Addsimps [power_zero, power_one];
1.195 +
1.196 +Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
1.197 +by (nat_ind_tac "m" 1);
1.198 +by (Simp_tac 1);
1.199 +by (asm_simp_tac (simpset() addsimps m_ac) 1);
1.200 +qed "power_mult";
1.201 +
1.202 +(* Divisibility *)
1.203 +section "Divisibility";
1.204 +
1.205 +Goalw [dvd_def] "!! a::'a::ring. a dvd <0>";
1.206 +by (res_inst_tac [("x", "<0>")] exI 1);
1.207 +by (Simp_tac 1);
1.208 +qed "dvd_zero_right";
1.209 +
1.210 +Goalw [dvd_def] "!! a::'a::ring. <0> dvd a ==> a = <0>";
1.211 +by Auto_tac;
1.212 +qed "dvd_zero_left";
1.213 +
1.214 +Goalw [dvd_def] "!! a::'a::ring. a dvd a";
1.215 +by (res_inst_tac [("x", "<1>")] exI 1);
1.216 +by (Simp_tac 1);
1.217 +qed "dvd_refl_ring";
1.218 +
1.219 +Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
1.220 +by (Step_tac 1);
1.221 +by (res_inst_tac [("x", "k * ka")] exI 1);
1.222 +by (simp_tac (simpset() addsimps m_ac) 1);
1.223 +qed "dvd_trans_ring";
1.224 +
1.225 +Addsimps [dvd_zero_right, dvd_refl_ring];
1.226 +
1.227 +Goal "!! a::'a::ring. a dvd <1> ==> a ~= <0>";
1.228 +by (auto_tac (claset() addDs [dvd_zero_left], simpset()));
1.229 +qed "unit_imp_nonzero";
1.230 +
1.231 +Goalw [dvd_def]
1.232 + "!!a::'a::ring. [| a dvd <1>; b dvd <1> |] ==> a * b dvd <1>";
1.233 +by (Clarify_tac 1);
1.234 +by (res_inst_tac [("x", "k * ka")] exI 1);
1.235 +by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
1.236 +qed "unit_mult";
1.237 +
1.238 +Goal "!!a::'a::ring. a dvd <1> ==> a^n dvd <1>";
1.239 +by (induct_tac "n" 1);
1.240 +by (Simp_tac 1);
1.241 +by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);
1.242 +qed "unit_power";
1.243 +
1.244 +Goalw [dvd_def]
1.245 + "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd (b + c)";
1.246 +by (Clarify_tac 1);
1.247 +by (res_inst_tac [("x", "k + ka")] exI 1);
1.248 +by (simp_tac (simpset() addsimps [r_distr]) 1);
1.249 +qed "dvd_add_right";
1.250 +
1.251 +Goalw [dvd_def]
1.252 + "!! a::'a::ring. a dvd b ==> a dvd (-b)";
1.253 +by (Clarify_tac 1);
1.254 +by (res_inst_tac [("x", "-k")] exI 1);
1.255 +by (simp_tac (simpset() addsimps [r_minus]) 1);
1.256 +qed "dvd_uminus_right";
1.257 +
1.258 +Goalw [dvd_def]
1.259 + "!! a::'a::ring. a dvd b ==> a dvd (c * b)";
1.260 +by (Clarify_tac 1);
1.261 +by (res_inst_tac [("x", "c * k")] exI 1);
1.262 +by (simp_tac (simpset() addsimps m_ac) 1);
1.263 +qed "dvd_l_mult_right";
1.264 +
1.265 +Goalw [dvd_def]
1.266 + "!! a::'a::ring. a dvd b ==> a dvd (b * c)";
1.267 +by (Clarify_tac 1);
1.268 +by (res_inst_tac [("x", "k * c")] exI 1);
1.269 +by (simp_tac (simpset() addsimps m_ac) 1);
1.270 +qed "dvd_r_mult_right";
1.271 +
1.272 +Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];
1.273 +
1.274 +(* Inverse of multiplication *)
1.275 +
1.276 +section "inverse";
1.277 +
1.278 +Goal "!! a::'a::ring. [| a * x = <1>; a * y = <1> |] ==> x = y";
1.279 +by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);
1.280 +by (simp_tac (simpset() addsimps m_ac) 1);
1.281 +by Auto_tac;
1.282 +qed "inverse_unique";
1.283 +
1.284 +Goalw [inverse_def, dvd_def]
1.285 + "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
1.286 +by (Asm_simp_tac 1);
1.287 +by (Clarify_tac 1);
1.288 +by (rtac selectI 1);
1.289 +by (rtac sym 1);
1.290 +by (assume_tac 1);
1.291 +qed "r_inverse_ring";
1.292 +
1.293 +Goal "!! a::'a::ring. a dvd <1> ==> inverse a * a= <1>";
1.294 +by (asm_simp_tac (simpset() addsimps r_inverse_ring::m_ac) 1);
1.295 +qed "l_inverse_ring";
1.296 +
1.297 +(* Integral domain *)
1.298 +
1.299 +section "Integral domains";
1.300 +
1.301 +Goal
1.302 + "!! a. [| a * b = <0>; a ~= <0> |] ==> (b::'a::domain) = <0>";
1.303 +by (dtac integral 1);
1.304 +by (Fast_tac 1);
1.305 +qed "r_integral";
1.306 +
1.307 +Goal
1.308 + "!! a. [| a * b = <0>; b ~= <0> |] ==> (a::'a::domain) = <0>";
1.309 +by (dtac integral 1);
1.310 +by (Fast_tac 1);
1.311 +qed "l_integral";
1.312 +
1.313 +Goal
1.314 + "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
1.315 +by (etac contrapos 1);
1.316 +by (rtac l_integral 1);
1.317 +by (assume_tac 1);
1.318 +by (assume_tac 1);
1.319 +qed "not_integral";
1.320 +
1.321 +Addsimps [not_integral];
1.322 +
1.323 +Goal "!! a::'a::domain. [| a * x = x; x ~= <0> |] ==> a = <1>";
1.324 +by (res_inst_tac [("a", "- <1>")] a_lcancel 1);
1.325 +by (Simp_tac 1);
1.326 +by (rtac l_integral 1);
1.327 +by (assume_tac 2);
1.328 +by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);
1.329 +qed "l_one_integral";
1.330 +
1.331 +Goal "!! a::'a::domain. [| x * a = x; x ~= <0> |] ==> a = <1>";
1.332 +by (res_inst_tac [("a", "- <1>")] a_rcancel 1);
1.333 +by (Simp_tac 1);
1.334 +by (rtac r_integral 1);
1.335 +by (assume_tac 2);
1.336 +by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1);
1.337 +qed "r_one_integral";
1.338 +
1.339 +(* cancellation laws for multiplication *)
1.340 +
1.341 +Goal "!! a::'a::domain. [| a ~= <0>; a * b = a * c |] ==> b = c";
1.342 +by (rtac diff_zero_imp_eq 1);
1.343 +by (dtac eq_imp_diff_zero 1);
1.344 +by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1);
1.345 +by (fast_tac (claset() addIs [l_integral]) 1);
1.346 +qed "m_lcancel";
1.347 +
1.348 +Goal "!! a::'a::domain. [| a ~= <0>; b * a = c * a |] ==> b = c";
1.349 +by (rtac m_lcancel 1);
1.350 +by (assume_tac 1);
1.351 +by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
1.352 +qed "m_rcancel";
1.353 +
1.354 +Goal "!! a::'a::domain. a ~= <0> ==> (a * b = a * c) = (b = c)";
1.355 +by (auto_tac (claset() addDs [m_lcancel], simpset()));
1.356 +qed "m_lcancel_eq";
1.357 +
1.358 +Goal "!! a::'a::domain. a ~= <0> ==> (b * a = c * a) = (b = c)";
1.359 +by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1);
1.360 +qed "m_rcancel_eq";
1.361 +
1.362 +Addsimps [m_lcancel_eq, m_rcancel_eq];
1.363 +
1.364 +(* Fields *)
1.365 +
1.366 +section "Fields";
1.367 +
1.368 +Goal "!! a::'a::field. a dvd <1> = (a ~= <0>)";
1.369 +by (blast_tac (claset() addDs [field_ax, unit_imp_nonzero]) 1);
1.370 +qed "field_unit";
1.371 +
1.372 +Addsimps [field_unit];
1.373 +
1.374 +Goal "!! a::'a::field. a ~= <0> ==> a * inverse a = <1>";
1.375 +by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
1.376 +qed "r_inverse";
1.377 +
1.378 +Goal "!! a::'a::field. a ~= <0> ==> inverse a * a= <1>";
1.379 +by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);
1.380 +qed "l_inverse";
1.381 +
1.382 +Addsimps [l_inverse, r_inverse];
1.383 +
1.384 +(* fields are factorial domains *)
1.385 +
1.386 +Goal "!! a::'a::field. a * b = <0> ==> a = <0> | b = <0>";
1.387 +by (Step_tac 1);
1.388 +by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
1.389 +by (rtac refl 3);
1.390 +by (simp_tac (simpset() addsimps m_ac) 2);
1.391 +by Auto_tac;
1.392 +qed "field_integral";
1.393 +
1.394 +Goalw [prime_def, irred_def] "!! a::'a::field. irred a ==> prime a";
1.395 +by (blast_tac (claset() addIs [field_ax]) 1);
1.396 +qed "field_fact_prime";
1.397 +
1.398 +
1.399 +