wneuper/isa: src/HOL/Algebra/abstract/Ring.ML@83f1a514dcb4

     1 (*

     2     Abstract class ring (commutative, with 1)

     3     $Id$

     4     Author: Clemens Ballarin, started 9 December 1996

     5 *)

     7 (*

     8 val a_assoc = thm "semigroup_add.add_assoc";

     9 val l_zero = thm "comm_monoid_add.add_0";

    10 val a_comm = thm "ab_semigroup_add.add_commute";

    12 section "Rings";

    14 fun make_left_commute assoc commute s =

    15   [rtac (commute RS trans) 1, rtac (assoc RS trans) 1,

    16    rtac (commute RS arg_cong) 1];

    18 (* addition *)

    20 qed_goal "a_lcomm" Ring.thy "!!a::'a::ring. a+(b+c) = b+(a+c)"

    21   (make_left_commute a_assoc a_comm);

    23 val a_ac = [a_assoc, a_comm, a_lcomm];

    25 Goal "!!a::'a::ring. a + 0 = a";

    26 by (rtac (a_comm RS trans) 1);

    27 by (rtac l_zero 1);

    28 qed "r_zero";

    30 Goal "!!a::'a::ring. a + (-a) = 0";

    31 by (rtac (a_comm RS trans) 1);

    32 by (rtac l_neg 1);

    33 qed "r_neg";

    35 Goal "!! a::'a::ring. a + b = a + c ==> b = c";

    36 by (rtac box_equals 1);

    37 by (rtac l_zero 2);

    38 by (rtac l_zero 2);

    39 by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1);

    40 by (asm_simp_tac (simpset() addsimps [a_assoc]) 1);

    41 qed "a_lcancel";

    43 Goal "!! a::'a::ring. b + a = c + a ==> b = c";

    44 by (rtac a_lcancel 1);

    45 by (asm_simp_tac (simpset() addsimps a_ac) 1);

    46 qed "a_rcancel";

    48 Goal "!! a::'a::ring. (a + b = a + c) = (b = c)";

    49 by (auto_tac (claset() addSDs [a_lcancel], simpset()));

    50 qed "a_lcancel_eq";

    52 Goal "!! a::'a::ring. (b + a = c + a) = (b = c)";

    53 by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1);

    54 qed "a_rcancel_eq";

    56 Addsimps [a_lcancel_eq, a_rcancel_eq];

    58 Goal "!!a::'a::ring. -(-a) = a";

    59 by (rtac a_lcancel 1);

    60 by (rtac (r_neg RS trans) 1);

    61 by (rtac (l_neg RS sym) 1);

    62 qed "minus_minus";

    64 Goal "- 0 = (0::'a::ring)";

    65 by (rtac a_lcancel 1);

    66 by (rtac (r_neg RS trans) 1);

    67 by (rtac (l_zero RS sym) 1);

    68 qed "minus0";

    70 Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)";

    71 by (res_inst_tac [("a", "a+b")] a_lcancel 1);

    72 by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1);

    73 qed "minus_add";

    75 (* multiplication *)

    77 qed_goal "m_lcomm" Ring.thy "!!a::'a::ring. a*(b*c) = b*(a*c)"

    78   (make_left_commute m_assoc m_comm);

    80 val m_ac = [m_assoc, m_comm, m_lcomm];

    82 Goal "!!a::'a::ring. a * 1 = a";

    83 by (rtac (m_comm RS trans) 1);

    84 by (rtac l_one 1);

    85 qed "r_one";

    87 (* distributive and derived *)

    89 Goal "!!a::'a::ring. a * (b + c) = a * b + a * c";

    90 by (rtac (m_comm RS trans) 1);

    91 by (rtac (l_distr RS trans) 1);

    92 by (simp_tac (simpset() addsimps [m_comm]) 1);

    93 qed "r_distr";

    95 val m_distr = m_ac @ [l_distr, r_distr];

    97 (* the following two proofs can be found in

    98    Jacobson, Basic Algebra I, pp. 88-89 *)

   100 Goal "!!a::'a::ring. 0 * a = 0";

   101 by (rtac a_lcancel 1);

   102 by (rtac (l_distr RS sym RS trans) 1);

   103 by (simp_tac (simpset() addsimps [r_zero]) 1);

   104 qed "l_null";

   106 Goal "!!a::'a::ring. a * 0 = 0";

   107 by (rtac (m_comm RS trans) 1);

   108 by (rtac l_null 1);

   109 qed "r_null";

   111 Goal "!!a::'a::ring. (-a) * b = - (a * b)";

   112 by (rtac a_lcancel 1);

   113 by (rtac (r_neg RS sym RSN (2, trans)) 1);

   114 by (rtac (l_distr RS sym RS trans) 1);

   115 by (simp_tac (simpset() addsimps [l_null, r_neg]) 1);

   116 qed "l_minus";

   118 Goal "!!a::'a::ring. a * (-b) = - (a * b)";

   119 by (rtac a_lcancel 1);

   120 by (rtac (r_neg RS sym RSN (2, trans)) 1);

   121 by (rtac (r_distr RS sym RS trans) 1);

   122 by (simp_tac (simpset() addsimps [r_null, r_neg]) 1);

   123 qed "r_minus";

   125 val m_minus = [l_minus, r_minus];

   127 Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0,

   128 	  l_one, r_one, l_null, r_null];

   130 (* further rules *)

   132 Goal "!!a::'a::ring. -a = 0 ==> a = 0";

   133 by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1);

   134 by (Asm_simp_tac 1);

   135 qed "uminus_monom";

   137 Goal "!!a::'a::ring. a ~= 0 ==> -a ~= 0";

   138 by (blast_tac (claset() addIs [uminus_monom]) 1);

   139 qed "uminus_monom_neq";

   141 Goal "!!a::'a::ring. a * b ~= 0 ==> a ~= 0";

   142 by Auto_tac;

   143 qed "l_nullD";

   145 Goal "!!a::'a::ring. a * b ~= 0 ==> b ~= 0";

   146 by Auto_tac;

   147 qed "r_nullD";

   149 (* reflection between a = b and a -- b = 0 *)

   151 Goal "!!a::'a::ring. a = b ==> a + (-b) = 0";

   152 by (Asm_simp_tac 1);

   153 qed "eq_imp_diff_zero";

   155 Goal "!!a::'a::ring. a + (-b) = 0 ==> a = b";

   156 by (res_inst_tac [("a", "-b")] a_rcancel 1);

   157 by (Asm_simp_tac 1);

   158 qed "diff_zero_imp_eq";

   160 (* this could be a rewrite rule, but won't terminate

   161    ==> make it a simproc?

   162 Goal "!!a::'a::ring. (a = b) = (a -- b = 0)";

   163 *)

   165 *)

   167 (* Power *)

   169 Goal "!!a::'a::ring. a ^ 0 = 1";

   170 by (simp_tac (simpset() addsimps [power_def]) 1);

   171 qed "power_0";

   173 Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";

   174 by (simp_tac (simpset() addsimps [power_def]) 1);

   175 qed "power_Suc";

   177 Addsimps [power_0, power_Suc];

   179 Goal "1 ^ n = (1::'a::ring)";

   180 by (induct_tac "n" 1);

   181 by Auto_tac;

   182 qed "power_one";

   184 Goal "!!n. n ~= 0 ==> 0 ^ n = (0::'a::ring)";

   185 by (etac rev_mp 1);

   186 by (induct_tac "n" 1);

   187 by Auto_tac;

   188 qed "power_zero";

   190 Addsimps [power_zero, power_one];

   192 Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";

   193 by (induct_tac "m" 1);

   194 by (Simp_tac 1);

   195 by (Asm_simp_tac 1);

   196 qed "power_mult";

   198 (* Divisibility *)

   199 section "Divisibility";

   201 Goalw [dvd_def] "!! a::'a::ring. a dvd 0";

   202 by (res_inst_tac [("x", "0")] exI 1);

   203 by (Simp_tac 1);

   204 qed "dvd_zero_right";

   206 Goalw [dvd_def] "!! a::'a::ring. 0 dvd a ==> a = 0";

   207 by Auto_tac;

   208 qed "dvd_zero_left";

   210 Goalw [dvd_def] "!! a::'a::ring. a dvd a";

   211 by (res_inst_tac [("x", "1")] exI 1);

   212 by (Simp_tac 1);

   213 qed "dvd_refl_ring";

   215 Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";

   216 by (Step_tac 1);

   217 by (res_inst_tac [("x", "k * ka")] exI 1);

   218 by (Asm_simp_tac 1);

   219 qed "dvd_trans_ring";

   221 Addsimps [dvd_zero_right, dvd_refl_ring];

   223 Goalw [dvd_def]

   224   "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1";

   225 by (Clarify_tac 1);

   226 by (res_inst_tac [("x", "k * ka")] exI 1);

   227 by (Asm_full_simp_tac 1);

   228 qed "unit_mult";

   230 Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1";

   231 by (induct_tac "n" 1);

   232 by (Simp_tac 1);

   233 by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);

   234 qed "unit_power";

   236 Goalw [dvd_def]

   237   "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c";

   238 by (Clarify_tac 1);

   239 by (res_inst_tac [("x", "k + ka")] exI 1);

   240 by (simp_tac (simpset() addsimps [r_distr]) 1);

   241 qed "dvd_add_right";

   243 Goalw [dvd_def]

   244   "!! a::'a::ring. a dvd b ==> a dvd -b";

   245 by (Clarify_tac 1);

   246 by (res_inst_tac [("x", "-k")] exI 1);

   247 by (simp_tac (simpset() addsimps [r_minus]) 1);

   248 qed "dvd_uminus_right";

   250 Goalw [dvd_def]

   251   "!! a::'a::ring. a dvd b ==> a dvd c*b";

   252 by (Clarify_tac 1);

   253 by (res_inst_tac [("x", "c * k")] exI 1);

   254 by (Simp_tac 1);

   255 qed "dvd_l_mult_right";

   257 Goalw [dvd_def]

   258   "!! a::'a::ring. a dvd b ==> a dvd b*c";

   259 by (Clarify_tac 1);

   260 by (res_inst_tac [("x", "k * c")] exI 1);

   261 by (Simp_tac 1);

   262 qed "dvd_r_mult_right";

   264 Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];

   266 (* Inverse of multiplication *)

   268 section "inverse";

   270 Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y";

   271 by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);

   272 by (Simp_tac 1);

   273 by Auto_tac;

   274 qed "inverse_unique";

   276 Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1";

   277 by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def]

   278   delsimprocs [ring_simproc]) 1);

   279 by (Clarify_tac 1);

   280 by (rtac theI 1);

   281 by (atac 1);

   282 by (rtac inverse_unique 1);

   283 by (atac 1);

   284 by (atac 1);

   285 qed "r_inverse_ring";

   287 Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1";

   288 by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1);

   289 qed "l_inverse_ring";

   291 (* Integral domain *)

   293 (*

   294 section "Integral domains";

   296 Goal "0 ~= (1::'a::domain)";

   297 by (rtac not_sym 1);

   298 by (rtac one_not_zero 1);

   299 qed "zero_not_one";

   301 Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0";

   302 by (auto_tac (claset() addDs [dvd_zero_left],

   303   simpset() addsimps [one_not_zero] ));

   304 qed "unit_imp_nonzero";

   306 Goal "[| a * b = 0; a ~= 0 |] ==> (b::'a::domain) = 0";

   307 by (dtac integral 1);

   308 by (Fast_tac 1);

   309 qed "r_integral";

   311 Goal "[| a * b = 0; b ~= 0 |] ==> (a::'a::domain) = 0";

   312 by (dtac integral 1);

   313 by (Fast_tac 1);

   314 qed "l_integral";

   316 Goal "!! a::'a::domain. [| a ~= 0; b ~= 0 |] ==> a * b ~= 0";

   317 by (blast_tac (claset() addIs [l_integral]) 1);

   318 qed "not_integral";

   320 Addsimps [not_integral, one_not_zero, zero_not_one];

   322 Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1";

   323 by (res_inst_tac [("a", "- 1")] a_lcancel 1);

   324 by (Simp_tac 1);

   325 by (rtac l_integral 1);

   326 by (assume_tac 2);

   327 by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);

   328 qed "l_one_integral";

   330 Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1";

   331 by (res_inst_tac [("a", "- 1")] a_rcancel 1);

   332 by (Simp_tac 1);

   333 by (rtac r_integral 1);

   334 by (assume_tac 2);

   335 by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1);

   336 qed "r_one_integral";

   338 (* cancellation laws for multiplication *)

   340 Goal "!! a::'a::domain. [| a ~= 0; a * b = a * c |] ==> b = c";

   341 by (rtac diff_zero_imp_eq 1);

   342 by (dtac eq_imp_diff_zero 1);

   343 by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1);

   344 by (fast_tac (claset() addIs [l_integral]) 1);

   345 qed "m_lcancel";

   347 Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c";

   348 by (rtac m_lcancel 1);

   349 by (assume_tac 1);

   350 by (Asm_full_simp_tac 1);

   351 qed "m_rcancel";

   353 Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)";

   354 by (auto_tac (claset() addDs [m_lcancel], simpset()));

   355 qed "m_lcancel_eq";

   357 Goal "!! a::'a::domain. a ~= 0 ==> (b * a = c * a) = (b = c)";

   358 by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1);

   359 qed "m_rcancel_eq";

   361 Addsimps [m_lcancel_eq, m_rcancel_eq];

   362 *)

   364 (* Fields *)

   366 section "Fields";

   368 Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)";

   369 by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left],

   370   simpset() addsimps [thm "field_one_not_zero"]));

   371 qed "field_unit";

   373 (* required for instantiation of field < domain in file Field.thy *)

   375 Addsimps [field_unit];

   377 val field_one_not_zero = thm "field_one_not_zero";

   379 Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1";

   380 by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);

   381 qed "r_inverse";

   383 Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1";

   384 by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);

   385 qed "l_inverse";

   387 Addsimps [l_inverse, r_inverse];

   389 (* fields are integral domains *)

   391 Goal "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0";

   392 by (Step_tac 1);

   393 by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);

   394 by (rtac refl 3);

   395 by (Simp_tac 2);

   396 by Auto_tac;

   397 qed "field_integral";

   399 (* fields are factorial domains *)

   401 Goalw [thm "prime_def", thm "irred_def"]

   402   "!! a::'a::field. irred a ==> prime a";

   403 by (blast_tac (claset() addIs [thm "field_ax"]) 1);

   404 qed "field_fact_prime";

author	obua
	Tue, 11 May 2004 20:11:08 +0200
changeset 14738	83f1a514dcb4
parent 13783	3294f727e20d
permissions	-rw-r--r--