src/HOL/Algebra/abstract/Ring.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 14738 83f1a514dcb4
permissions -rw-r--r--
Constant "If" is now local
paulson@7998
     1
(*
paulson@7998
     2
    Abstract class ring (commutative, with 1)
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 9 December 1996
paulson@7998
     5
*)
paulson@7998
     6
ballarin@13735
     7
(*
obua@14738
     8
val a_assoc = thm "semigroup_add.add_assoc";
obua@14738
     9
val l_zero = thm "comm_monoid_add.add_0";
obua@14738
    10
val a_comm = thm "ab_semigroup_add.add_commute";
wenzelm@11778
    11
paulson@7998
    12
section "Rings";
paulson@7998
    13
paulson@7998
    14
fun make_left_commute assoc commute s =
paulson@7998
    15
  [rtac (commute RS trans) 1, rtac (assoc RS trans) 1,
paulson@7998
    16
   rtac (commute RS arg_cong) 1];
paulson@7998
    17
paulson@7998
    18
(* addition *)
paulson@7998
    19
paulson@7998
    20
qed_goal "a_lcomm" Ring.thy "!!a::'a::ring. a+(b+c) = b+(a+c)"
paulson@7998
    21
  (make_left_commute a_assoc a_comm);
paulson@7998
    22
paulson@7998
    23
val a_ac = [a_assoc, a_comm, a_lcomm];
paulson@7998
    24
ballarin@11093
    25
Goal "!!a::'a::ring. a + 0 = a";
paulson@9390
    26
by (rtac (a_comm RS trans) 1);
paulson@9390
    27
by (rtac l_zero 1);
paulson@9390
    28
qed "r_zero";
paulson@7998
    29
ballarin@11093
    30
Goal "!!a::'a::ring. a + (-a) = 0";
paulson@9390
    31
by (rtac (a_comm RS trans) 1);
paulson@9390
    32
by (rtac l_neg 1);
paulson@9390
    33
qed "r_neg";
paulson@7998
    34
paulson@7998
    35
Goal "!! a::'a::ring. a + b = a + c ==> b = c";
paulson@7998
    36
by (rtac box_equals 1);
paulson@7998
    37
by (rtac l_zero 2);
paulson@7998
    38
by (rtac l_zero 2);
paulson@7998
    39
by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1);
paulson@7998
    40
by (asm_simp_tac (simpset() addsimps [a_assoc]) 1);
paulson@7998
    41
qed "a_lcancel";
paulson@7998
    42
paulson@7998
    43
Goal "!! a::'a::ring. b + a = c + a ==> b = c";
paulson@7998
    44
by (rtac a_lcancel 1);
paulson@7998
    45
by (asm_simp_tac (simpset() addsimps a_ac) 1);
paulson@7998
    46
qed "a_rcancel";
paulson@7998
    47
paulson@7998
    48
Goal "!! a::'a::ring. (a + b = a + c) = (b = c)";
paulson@7998
    49
by (auto_tac (claset() addSDs [a_lcancel], simpset()));
paulson@7998
    50
qed "a_lcancel_eq";
paulson@7998
    51
paulson@7998
    52
Goal "!! a::'a::ring. (b + a = c + a) = (b = c)";
paulson@7998
    53
by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1);
paulson@7998
    54
qed "a_rcancel_eq";
paulson@7998
    55
paulson@7998
    56
Addsimps [a_lcancel_eq, a_rcancel_eq];
paulson@7998
    57
paulson@7998
    58
Goal "!!a::'a::ring. -(-a) = a";
paulson@7998
    59
by (rtac a_lcancel 1);
paulson@7998
    60
by (rtac (r_neg RS trans) 1);
paulson@7998
    61
by (rtac (l_neg RS sym) 1);
paulson@7998
    62
qed "minus_minus";
paulson@7998
    63
ballarin@11093
    64
Goal "- 0 = (0::'a::ring)";
paulson@7998
    65
by (rtac a_lcancel 1);
paulson@7998
    66
by (rtac (r_neg RS trans) 1);
paulson@7998
    67
by (rtac (l_zero RS sym) 1);
paulson@7998
    68
qed "minus0";
paulson@7998
    69
paulson@7998
    70
Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)";
paulson@7998
    71
by (res_inst_tac [("a", "a+b")] a_lcancel 1);
paulson@7998
    72
by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1);
paulson@7998
    73
qed "minus_add";
paulson@7998
    74
paulson@7998
    75
(* multiplication *)
paulson@7998
    76
paulson@7998
    77
qed_goal "m_lcomm" Ring.thy "!!a::'a::ring. a*(b*c) = b*(a*c)"
paulson@7998
    78
  (make_left_commute m_assoc m_comm);
paulson@7998
    79
paulson@7998
    80
val m_ac = [m_assoc, m_comm, m_lcomm];
paulson@7998
    81
ballarin@13735
    82
Goal "!!a::'a::ring. a * 1 = a";
paulson@9390
    83
by (rtac (m_comm RS trans) 1);
paulson@9390
    84
by (rtac l_one 1);
paulson@9390
    85
qed "r_one";
paulson@7998
    86
paulson@7998
    87
(* distributive and derived *)
paulson@7998
    88
paulson@7998
    89
Goal "!!a::'a::ring. a * (b + c) = a * b + a * c";
paulson@7998
    90
by (rtac (m_comm RS trans) 1);
paulson@7998
    91
by (rtac (l_distr RS trans) 1);
paulson@7998
    92
by (simp_tac (simpset() addsimps [m_comm]) 1);
paulson@7998
    93
qed "r_distr";
paulson@7998
    94
paulson@7998
    95
val m_distr = m_ac @ [l_distr, r_distr];
paulson@7998
    96
paulson@7998
    97
(* the following two proofs can be found in
paulson@7998
    98
   Jacobson, Basic Algebra I, pp. 88-89 *)
paulson@7998
    99
ballarin@11093
   100
Goal "!!a::'a::ring. 0 * a = 0";
paulson@7998
   101
by (rtac a_lcancel 1);
paulson@7998
   102
by (rtac (l_distr RS sym RS trans) 1);
paulson@7998
   103
by (simp_tac (simpset() addsimps [r_zero]) 1);
paulson@7998
   104
qed "l_null";
paulson@7998
   105
ballarin@11093
   106
Goal "!!a::'a::ring. a * 0 = 0";
paulson@9390
   107
by (rtac (m_comm RS trans) 1);
paulson@9390
   108
by (rtac l_null 1);
paulson@9390
   109
qed "r_null";
paulson@7998
   110
paulson@7998
   111
Goal "!!a::'a::ring. (-a) * b = - (a * b)";
paulson@7998
   112
by (rtac a_lcancel 1);
paulson@7998
   113
by (rtac (r_neg RS sym RSN (2, trans)) 1);
paulson@7998
   114
by (rtac (l_distr RS sym RS trans) 1);
paulson@7998
   115
by (simp_tac (simpset() addsimps [l_null, r_neg]) 1);
paulson@7998
   116
qed "l_minus";
paulson@7998
   117
paulson@7998
   118
Goal "!!a::'a::ring. a * (-b) = - (a * b)";
paulson@7998
   119
by (rtac a_lcancel 1);
paulson@7998
   120
by (rtac (r_neg RS sym RSN (2, trans)) 1);
paulson@7998
   121
by (rtac (r_distr RS sym RS trans) 1);
paulson@7998
   122
by (simp_tac (simpset() addsimps [r_null, r_neg]) 1);
paulson@7998
   123
qed "r_minus";
paulson@7998
   124
paulson@7998
   125
val m_minus = [l_minus, r_minus];
paulson@7998
   126
paulson@7998
   127
Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, 
ballarin@11093
   128
	  l_one, r_one, l_null, r_null];
paulson@7998
   129
paulson@7998
   130
(* further rules *)
paulson@7998
   131
ballarin@11093
   132
Goal "!!a::'a::ring. -a = 0 ==> a = 0";
paulson@7998
   133
by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1);
paulson@7998
   134
by (Asm_simp_tac 1);
paulson@7998
   135
qed "uminus_monom";
paulson@7998
   136
ballarin@11093
   137
Goal "!!a::'a::ring. a ~= 0 ==> -a ~= 0";
paulson@10198
   138
by (blast_tac (claset() addIs [uminus_monom]) 1); 
paulson@7998
   139
qed "uminus_monom_neq";
paulson@7998
   140
ballarin@11093
   141
Goal "!!a::'a::ring. a * b ~= 0 ==> a ~= 0";
paulson@10198
   142
by Auto_tac;  
paulson@7998
   143
qed "l_nullD";
paulson@7998
   144
ballarin@11093
   145
Goal "!!a::'a::ring. a * b ~= 0 ==> b ~= 0";
paulson@10198
   146
by Auto_tac;  
paulson@7998
   147
qed "r_nullD";
paulson@7998
   148
ballarin@11093
   149
(* reflection between a = b and a -- b = 0 *)
paulson@7998
   150
ballarin@11093
   151
Goal "!!a::'a::ring. a = b ==> a + (-b) = 0";
paulson@7998
   152
by (Asm_simp_tac 1);
paulson@7998
   153
qed "eq_imp_diff_zero";
paulson@7998
   154
ballarin@11093
   155
Goal "!!a::'a::ring. a + (-b) = 0 ==> a = b";
paulson@7998
   156
by (res_inst_tac [("a", "-b")] a_rcancel 1);
paulson@7998
   157
by (Asm_simp_tac 1);
paulson@7998
   158
qed "diff_zero_imp_eq";
paulson@7998
   159
paulson@7998
   160
(* this could be a rewrite rule, but won't terminate
paulson@7998
   161
   ==> make it a simproc?
ballarin@11093
   162
Goal "!!a::'a::ring. (a = b) = (a -- b = 0)";
paulson@7998
   163
*)
paulson@7998
   164
ballarin@13735
   165
*)
ballarin@13735
   166
paulson@7998
   167
(* Power *)
paulson@7998
   168
ballarin@13735
   169
Goal "!!a::'a::ring. a ^ 0 = 1";
ballarin@13735
   170
by (simp_tac (simpset() addsimps [power_def]) 1);
paulson@7998
   171
qed "power_0";
paulson@7998
   172
paulson@7998
   173
Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
ballarin@13735
   174
by (simp_tac (simpset() addsimps [power_def]) 1);
paulson@7998
   175
qed "power_Suc";
paulson@7998
   176
paulson@7998
   177
Addsimps [power_0, power_Suc];
paulson@7998
   178
ballarin@13735
   179
Goal "1 ^ n = (1::'a::ring)";
paulson@8707
   180
by (induct_tac "n" 1);
paulson@8707
   181
by Auto_tac;
paulson@7998
   182
qed "power_one";
paulson@7998
   183
ballarin@11093
   184
Goal "!!n. n ~= 0 ==> 0 ^ n = (0::'a::ring)";
paulson@7998
   185
by (etac rev_mp 1);
paulson@8707
   186
by (induct_tac "n" 1);
paulson@8707
   187
by Auto_tac;
paulson@7998
   188
qed "power_zero";
paulson@7998
   189
paulson@7998
   190
Addsimps [power_zero, power_one];
paulson@7998
   191
paulson@7998
   192
Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
paulson@8707
   193
by (induct_tac "m" 1);
paulson@7998
   194
by (Simp_tac 1);
ballarin@13735
   195
by (Asm_simp_tac 1);
paulson@7998
   196
qed "power_mult";
paulson@7998
   197
paulson@7998
   198
(* Divisibility *)
paulson@7998
   199
section "Divisibility";
paulson@7998
   200
ballarin@11093
   201
Goalw [dvd_def] "!! a::'a::ring. a dvd 0";
ballarin@11093
   202
by (res_inst_tac [("x", "0")] exI 1);
paulson@7998
   203
by (Simp_tac 1);
paulson@7998
   204
qed "dvd_zero_right";
paulson@7998
   205
ballarin@11093
   206
Goalw [dvd_def] "!! a::'a::ring. 0 dvd a ==> a = 0";
paulson@7998
   207
by Auto_tac;
paulson@7998
   208
qed "dvd_zero_left";
paulson@7998
   209
paulson@7998
   210
Goalw [dvd_def] "!! a::'a::ring. a dvd a";
ballarin@13735
   211
by (res_inst_tac [("x", "1")] exI 1);
paulson@7998
   212
by (Simp_tac 1);
paulson@7998
   213
qed "dvd_refl_ring";
paulson@7998
   214
paulson@7998
   215
Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
paulson@7998
   216
by (Step_tac 1);
paulson@7998
   217
by (res_inst_tac [("x", "k * ka")] exI 1);
ballarin@13735
   218
by (Asm_simp_tac 1);
paulson@7998
   219
qed "dvd_trans_ring";
paulson@7998
   220
paulson@7998
   221
Addsimps [dvd_zero_right, dvd_refl_ring];
paulson@7998
   222
paulson@7998
   223
Goalw [dvd_def]
ballarin@13735
   224
  "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1";
paulson@7998
   225
by (Clarify_tac 1);
paulson@7998
   226
by (res_inst_tac [("x", "k * ka")] exI 1);
ballarin@13735
   227
by (Asm_full_simp_tac 1);
paulson@7998
   228
qed "unit_mult";
paulson@7998
   229
ballarin@13735
   230
Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1";
paulson@7998
   231
by (induct_tac "n" 1);
paulson@7998
   232
by (Simp_tac 1);
paulson@7998
   233
by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);
paulson@7998
   234
qed "unit_power";
paulson@7998
   235
paulson@7998
   236
Goalw [dvd_def]
nipkow@10789
   237
  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c";
paulson@7998
   238
by (Clarify_tac 1);
paulson@7998
   239
by (res_inst_tac [("x", "k + ka")] exI 1);
paulson@7998
   240
by (simp_tac (simpset() addsimps [r_distr]) 1);
paulson@7998
   241
qed "dvd_add_right";
paulson@7998
   242
paulson@7998
   243
Goalw [dvd_def]
nipkow@10789
   244
  "!! a::'a::ring. a dvd b ==> a dvd -b";
paulson@7998
   245
by (Clarify_tac 1);
paulson@7998
   246
by (res_inst_tac [("x", "-k")] exI 1);
paulson@7998
   247
by (simp_tac (simpset() addsimps [r_minus]) 1);
paulson@7998
   248
qed "dvd_uminus_right";
paulson@7998
   249
paulson@7998
   250
Goalw [dvd_def]
nipkow@10789
   251
  "!! a::'a::ring. a dvd b ==> a dvd c*b";
paulson@7998
   252
by (Clarify_tac 1);
paulson@7998
   253
by (res_inst_tac [("x", "c * k")] exI 1);
ballarin@13735
   254
by (Simp_tac 1);
paulson@7998
   255
qed "dvd_l_mult_right";
paulson@7998
   256
paulson@7998
   257
Goalw [dvd_def]
nipkow@10789
   258
  "!! a::'a::ring. a dvd b ==> a dvd b*c";
paulson@7998
   259
by (Clarify_tac 1);
paulson@7998
   260
by (res_inst_tac [("x", "k * c")] exI 1);
ballarin@13735
   261
by (Simp_tac 1);
paulson@7998
   262
qed "dvd_r_mult_right";
paulson@7998
   263
paulson@7998
   264
Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];
paulson@7998
   265
paulson@7998
   266
(* Inverse of multiplication *)
paulson@7998
   267
paulson@7998
   268
section "inverse";
paulson@7998
   269
ballarin@13735
   270
Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y";
paulson@7998
   271
by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);
ballarin@13735
   272
by (Simp_tac 1);
paulson@7998
   273
by Auto_tac;
paulson@7998
   274
qed "inverse_unique";
paulson@7998
   275
ballarin@13735
   276
Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1";
ballarin@13783
   277
by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def]
ballarin@13783
   278
  delsimprocs [ring_simproc]) 1);
paulson@7998
   279
by (Clarify_tac 1);
ballarin@13735
   280
by (rtac theI 1);
ballarin@13735
   281
by (atac 1);
ballarin@13735
   282
by (rtac inverse_unique 1);
ballarin@13735
   283
by (atac 1);
ballarin@13735
   284
by (atac 1);
paulson@7998
   285
qed "r_inverse_ring";
paulson@7998
   286
ballarin@13735
   287
Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1";
ballarin@13735
   288
by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
paulson@7998
   289
qed "l_inverse_ring";
paulson@7998
   290
paulson@7998
   291
(* Integral domain *)
paulson@7998
   292
ballarin@13735
   293
(*
paulson@7998
   294
section "Integral domains";
paulson@7998
   295
ballarin@13735
   296
Goal "0 ~= (1::'a::domain)";
ballarin@11093
   297
by (rtac not_sym 1);
ballarin@11093
   298
by (rtac one_not_zero 1);
ballarin@11093
   299
qed "zero_not_one";
ballarin@11093
   300
ballarin@13735
   301
Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0";
ballarin@11093
   302
by (auto_tac (claset() addDs [dvd_zero_left],
ballarin@11093
   303
  simpset() addsimps [one_not_zero] ));
ballarin@11093
   304
qed "unit_imp_nonzero";
ballarin@11093
   305
ballarin@11093
   306
Goal "[| a * b = 0; a ~= 0 |] ==> (b::'a::domain) = 0";
paulson@7998
   307
by (dtac integral 1);
paulson@7998
   308
by (Fast_tac 1);
paulson@7998
   309
qed "r_integral";
paulson@7998
   310
ballarin@11093
   311
Goal "[| a * b = 0; b ~= 0 |] ==> (a::'a::domain) = 0";
paulson@7998
   312
by (dtac integral 1);
paulson@7998
   313
by (Fast_tac 1);
paulson@7998
   314
qed "l_integral";
paulson@7998
   315
ballarin@11093
   316
Goal "!! a::'a::domain. [| a ~= 0; b ~= 0 |] ==> a * b ~= 0";
paulson@10230
   317
by (blast_tac (claset() addIs [l_integral]) 1); 
paulson@7998
   318
qed "not_integral";
paulson@7998
   319
ballarin@11093
   320
Addsimps [not_integral, one_not_zero, zero_not_one];
paulson@7998
   321
ballarin@13735
   322
Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1";
ballarin@13735
   323
by (res_inst_tac [("a", "- 1")] a_lcancel 1);
paulson@7998
   324
by (Simp_tac 1);
paulson@7998
   325
by (rtac l_integral 1);
paulson@7998
   326
by (assume_tac 2);
paulson@7998
   327
by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);
paulson@7998
   328
qed "l_one_integral";
paulson@7998
   329
ballarin@13735
   330
Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1";
ballarin@13735
   331
by (res_inst_tac [("a", "- 1")] a_rcancel 1);
paulson@7998
   332
by (Simp_tac 1);
paulson@7998
   333
by (rtac r_integral 1);
paulson@7998
   334
by (assume_tac 2);
paulson@7998
   335
by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1);
paulson@7998
   336
qed "r_one_integral";
paulson@7998
   337
paulson@7998
   338
(* cancellation laws for multiplication *)
paulson@7998
   339
ballarin@11093
   340
Goal "!! a::'a::domain. [| a ~= 0; a * b = a * c |] ==> b = c";
paulson@7998
   341
by (rtac diff_zero_imp_eq 1);
paulson@7998
   342
by (dtac eq_imp_diff_zero 1);
paulson@7998
   343
by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1);
paulson@7998
   344
by (fast_tac (claset() addIs [l_integral]) 1);
paulson@7998
   345
qed "m_lcancel";
paulson@7998
   346
ballarin@11093
   347
Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c";
paulson@7998
   348
by (rtac m_lcancel 1);
paulson@7998
   349
by (assume_tac 1);
ballarin@13735
   350
by (Asm_full_simp_tac 1);
paulson@7998
   351
qed "m_rcancel";
paulson@7998
   352
ballarin@11093
   353
Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)";
paulson@7998
   354
by (auto_tac (claset() addDs [m_lcancel], simpset()));
paulson@7998
   355
qed "m_lcancel_eq";
paulson@7998
   356
ballarin@11093
   357
Goal "!! a::'a::domain. a ~= 0 ==> (b * a = c * a) = (b = c)";
paulson@7998
   358
by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1);
paulson@7998
   359
qed "m_rcancel_eq";
paulson@7998
   360
paulson@7998
   361
Addsimps [m_lcancel_eq, m_rcancel_eq];
ballarin@13735
   362
*)
paulson@7998
   363
paulson@7998
   364
(* Fields *)
paulson@7998
   365
paulson@7998
   366
section "Fields";
paulson@7998
   367
ballarin@13735
   368
Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)";
ballarin@13735
   369
by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left],
ballarin@13735
   370
  simpset() addsimps [thm "field_one_not_zero"]));
paulson@7998
   371
qed "field_unit";
paulson@7998
   372
ballarin@13735
   373
(* required for instantiation of field < domain in file Field.thy *)
ballarin@13735
   374
paulson@7998
   375
Addsimps [field_unit];
paulson@7998
   376
ballarin@13735
   377
val field_one_not_zero = thm "field_one_not_zero";
ballarin@13735
   378
ballarin@13735
   379
Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1";
paulson@7998
   380
by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
paulson@7998
   381
qed "r_inverse";
paulson@7998
   382
ballarin@13735
   383
Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1";
paulson@7998
   384
by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);
paulson@7998
   385
qed "l_inverse";
paulson@7998
   386
paulson@7998
   387
Addsimps [l_inverse, r_inverse];
paulson@7998
   388
ballarin@11093
   389
(* fields are integral domains *)
paulson@7998
   390
ballarin@11093
   391
Goal "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0";
paulson@7998
   392
by (Step_tac 1);
paulson@7998
   393
by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
paulson@7998
   394
by (rtac refl 3);
ballarin@13735
   395
by (Simp_tac 2);
paulson@7998
   396
by Auto_tac;
paulson@7998
   397
qed "field_integral";
paulson@7998
   398
ballarin@11093
   399
(* fields are factorial domains *)
ballarin@11093
   400
ballarin@13735
   401
Goalw [thm "prime_def", thm "irred_def"]
ballarin@13735
   402
  "!! a::'a::field. irred a ==> prime a";
ballarin@13735
   403
by (blast_tac (claset() addIs [thm "field_ax"]) 1);
paulson@7998
   404
qed "field_fact_prime";