src/HOL/Algebra/abstract/Ideal.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 13735 7de9342aca7a
child 17479 68a7acb5f22e
permissions -rw-r--r--
Constant "If" is now local
paulson@7998
     1
(*
paulson@7998
     2
    Ideals for commutative rings
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 24 September 1999
paulson@7998
     5
*)
paulson@7998
     6
paulson@7998
     7
(* is_ideal *)
paulson@7998
     8
paulson@7998
     9
Goalw [is_ideal_def]
paulson@7998
    10
  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \
ballarin@11093
    11
\     !! a. a:I ==> - a : I; 0 : I; \
paulson@7998
    12
\     !! a r. a:I ==> a * r : I |] ==> is_ideal I";
paulson@7998
    13
by Auto_tac;
paulson@7998
    14
qed "is_idealI";
paulson@7998
    15
paulson@7998
    16
Goalw [is_ideal_def] "[| is_ideal I; a:I; b:I |] ==> a + b : I";
paulson@7998
    17
by (Fast_tac 1);
paulson@7998
    18
qed "is_ideal_add";
paulson@7998
    19
paulson@7998
    20
Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> - a : I";
paulson@7998
    21
by (Fast_tac 1);
paulson@7998
    22
qed "is_ideal_uminus";
paulson@7998
    23
ballarin@11093
    24
Goalw [is_ideal_def] "[| is_ideal I |] ==> 0 : I";
paulson@7998
    25
by (Fast_tac 1);
paulson@7998
    26
qed "is_ideal_zero";
paulson@7998
    27
paulson@7998
    28
Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> a * r : I";
paulson@7998
    29
by (Fast_tac 1);
paulson@7998
    30
qed "is_ideal_mult";
paulson@7998
    31
paulson@7998
    32
Goalw [dvd_def, is_ideal_def] "[| a dvd b; is_ideal I; a:I |] ==> b:I";
paulson@7998
    33
by (Fast_tac 1);
paulson@7998
    34
qed "is_ideal_dvd";
paulson@7998
    35
paulson@7998
    36
Goalw [is_ideal_def] "is_ideal (UNIV::('a::ring) set)";
paulson@7998
    37
by Auto_tac;
paulson@7998
    38
qed "UNIV_is_ideal";
paulson@7998
    39
ballarin@11093
    40
Goalw [is_ideal_def] "is_ideal {0::'a::ring}";
paulson@7998
    41
by Auto_tac;
paulson@7998
    42
qed "zero_is_ideal";
paulson@7998
    43
paulson@7998
    44
Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult,
paulson@7998
    45
  UNIV_is_ideal, zero_is_ideal];
paulson@7998
    46
paulson@7998
    47
Goal "is_ideal {x::'a::ring. a dvd x}";
paulson@7998
    48
by (rtac is_idealI 1);
paulson@7998
    49
by Auto_tac;
paulson@7998
    50
qed "is_ideal_1";
paulson@7998
    51
paulson@7998
    52
Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}";
paulson@7998
    53
by (rtac is_idealI 1);
ballarin@13735
    54
(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *)
ballarin@13735
    55
by (Clarify_tac 1);
ballarin@13735
    56
by (Clarify_tac 2);
ballarin@13735
    57
by (Clarify_tac 3);
ballarin@13735
    58
by (Clarify_tac 4);
paulson@7998
    59
by (res_inst_tac [("x", "u+ua")] exI 1);
paulson@7998
    60
by (res_inst_tac [("x", "v+va")] exI 1);
paulson@7998
    61
by (res_inst_tac [("x", "-u")] exI 2);
paulson@7998
    62
by (res_inst_tac [("x", "-v")] exI 2);
ballarin@11093
    63
by (res_inst_tac [("x", "0")] exI 3);
ballarin@11093
    64
by (res_inst_tac [("x", "0")] exI 3);
paulson@7998
    65
by (res_inst_tac [("x", "u * r")] exI 4);
paulson@7998
    66
by (res_inst_tac [("x", "v * r")] exI 4);
ballarin@13735
    67
by (REPEAT (Simp_tac 1));
paulson@7998
    68
qed "is_ideal_2";
paulson@7998
    69
paulson@7998
    70
(* ideal_of *)
paulson@7998
    71
paulson@7998
    72
Goalw [is_ideal_def, ideal_of_def] "is_ideal (ideal_of S)";
paulson@7998
    73
by (Blast_tac 1);  (* Here, blast_tac is much superior to fast_tac! *)
paulson@7998
    74
qed "ideal_of_is_ideal";
paulson@7998
    75
paulson@7998
    76
Goalw [ideal_of_def] "a:S ==> a : (ideal_of S)";
paulson@7998
    77
by Auto_tac;
paulson@7998
    78
qed "generator_in_ideal";
paulson@7998
    79
ballarin@13735
    80
Goalw [ideal_of_def] "ideal_of {1::'a::ring} = UNIV";
ballarin@13735
    81
by (force_tac (claset() addDs [is_ideal_mult], 
ballarin@13735
    82
  simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1);
ballarin@13735
    83
  (* FIXME: Zumkeller's order raises Domain exn *)
paulson@7998
    84
qed "ideal_of_one_eq";
paulson@7998
    85
ballarin@11093
    86
Goalw [ideal_of_def] "ideal_of {} = {0::'a::ring}";
paulson@7998
    87
by (rtac subset_antisym 1);
paulson@7998
    88
by (rtac subsetI 1);
paulson@7998
    89
by (dtac InterD 1);
paulson@7998
    90
by (assume_tac 2);
paulson@7998
    91
by (auto_tac (claset(), simpset() addsimps [is_ideal_zero]));
paulson@7998
    92
qed "ideal_of_empty_eq";
paulson@7998
    93
paulson@7998
    94
Goalw [ideal_of_def] "ideal_of {a} = {x::'a::ring. a dvd x}";
paulson@7998
    95
by (rtac subset_antisym 1);
paulson@7998
    96
by (rtac subsetI 1);
paulson@7998
    97
by (dtac InterD 1);
paulson@7998
    98
by (assume_tac 2);
paulson@7998
    99
by (auto_tac (claset() addIs [is_ideal_1], simpset()));
paulson@7998
   100
by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1);
paulson@7998
   101
qed "pideal_structure";
paulson@7998
   102
paulson@7998
   103
Goalw [ideal_of_def]
paulson@7998
   104
  "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}";
paulson@7998
   105
by (rtac subset_antisym 1);
paulson@7998
   106
by (rtac subsetI 1);
paulson@7998
   107
by (dtac InterD 1);
paulson@7998
   108
by (assume_tac 2);
ballarin@13735
   109
by (auto_tac (claset() addIs [is_ideal_2],
ballarin@13735
   110
  simpset() delsimprocs [ring_simproc]));
ballarin@13735
   111
(* FIXME: Zumkeller's order *)
ballarin@13735
   112
by (res_inst_tac [("x", "1")] exI 1);
ballarin@11093
   113
by (res_inst_tac [("x", "0")] exI 1);
ballarin@11093
   114
by (res_inst_tac [("x", "0")] exI 2);
ballarin@13735
   115
by (res_inst_tac [("x", "1")] exI 2);
paulson@7998
   116
by (Simp_tac 1);
paulson@7998
   117
by (Simp_tac 1);
paulson@7998
   118
qed "ideal_of_2_structure";
paulson@7998
   119
paulson@7998
   120
Goalw [ideal_of_def] "A <= B ==> ideal_of A <= ideal_of B";
paulson@7998
   121
by Auto_tac;
paulson@7998
   122
qed "ideal_of_mono";
paulson@7998
   123
ballarin@11093
   124
Goal "ideal_of {0::'a::ring} = {0}";
paulson@7998
   125
by (simp_tac (simpset() addsimps [pideal_structure]) 1);
paulson@7998
   126
by (rtac subset_antisym 1);
paulson@7998
   127
by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
paulson@7998
   128
qed "ideal_of_zero_eq";
paulson@7998
   129
paulson@7998
   130
Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
paulson@7998
   131
by (auto_tac (claset(),
paulson@7998
   132
  simpset() addsimps [pideal_structure, is_ideal_dvd]));
paulson@7998
   133
qed "element_generates_subideal";
paulson@7998
   134
paulson@7998
   135
(* is_pideal *)
paulson@7998
   136
paulson@7998
   137
Goalw [is_pideal_def] "is_pideal (I::('a::ring) set) ==> is_ideal I";
paulson@7998
   138
by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1);
paulson@7998
   139
qed "is_pideal_imp_is_ideal";
paulson@7998
   140
paulson@7998
   141
Goalw [is_pideal_def] "is_pideal (ideal_of {a::'a::ring})";
paulson@7998
   142
by (Fast_tac 1);
paulson@7998
   143
qed "pideal_is_pideal";
paulson@7998
   144
paulson@7998
   145
Goalw [is_pideal_def] "is_pideal I ==> EX a. I = ideal_of {a}";
paulson@7998
   146
by (assume_tac 1);
paulson@7998
   147
qed "is_pidealD";
paulson@7998
   148
paulson@7998
   149
(* Ideals and divisibility *)
paulson@7998
   150
paulson@7998
   151
Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
paulson@7998
   152
by (auto_tac (claset() addIs [dvd_trans_ring],
paulson@7998
   153
  simpset() addsimps [pideal_structure]));
paulson@7998
   154
qed "dvd_imp_subideal";
paulson@7998
   155
paulson@7998
   156
Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a";
paulson@7998
   157
by (auto_tac (claset() addSDs [subsetD],
paulson@7998
   158
  simpset() addsimps [pideal_structure]));
paulson@7998
   159
qed "subideal_imp_dvd";
paulson@7998
   160
nipkow@10789
   161
Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)";
paulson@7998
   162
by (rtac iffI 1);
paulson@7998
   163
by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1));
paulson@7998
   164
qed "subideal_is_dvd";
paulson@7998
   165
nipkow@10789
   166
Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b";
paulson@7998
   167
by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
paulson@7998
   168
by (etac conjE 1);
paulson@7998
   169
by (dres_inst_tac [("c", "a")] subsetD 1);
paulson@7998
   170
by (auto_tac (claset() addIs [dvd_trans_ring],
paulson@7998
   171
  simpset()));
paulson@7998
   172
qed "psubideal_not_dvd";
paulson@7998
   173
nipkow@10789
   174
Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
paulson@7998
   175
by (rtac psubsetI 1);
paulson@10198
   176
by (etac dvd_imp_subideal 1);
paulson@10198
   177
by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); 
paulson@11384
   178
qed "not_dvd_psubideal_singleton";
paulson@7998
   179
nipkow@10789
   180
Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)";
paulson@7998
   181
by (rtac iffI 1);
paulson@7998
   182
by (REPEAT (ares_tac
paulson@7998
   183
  [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
paulson@7998
   184
by (etac conjE 1);
paulson@11384
   185
by (REPEAT (ares_tac [not_dvd_psubideal_singleton] 1));
paulson@7998
   186
qed "psubideal_is_dvd";
paulson@7998
   187
paulson@7998
   188
Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}";
paulson@7998
   189
by (rtac subset_antisym 1);
paulson@7998
   190
by (REPEAT (ares_tac [dvd_imp_subideal] 1));
paulson@7998
   191
qed "assoc_pideal_eq";
paulson@7998
   192
paulson@7998
   193
AddIffs [subideal_is_dvd, psubideal_is_dvd];
paulson@7998
   194
paulson@7998
   195
Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})";
paulson@7998
   196
by (rtac is_ideal_dvd 1);
paulson@7998
   197
by (assume_tac 1);
paulson@7998
   198
by (rtac ideal_of_is_ideal 1);
paulson@7998
   199
by (rtac generator_in_ideal 1);
paulson@7998
   200
by (Simp_tac 1);
paulson@7998
   201
qed "dvd_imp_in_pideal";
paulson@7998
   202
paulson@7998
   203
Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b";
paulson@7998
   204
by (full_simp_tac (simpset() addsimps [pideal_structure]) 1);
paulson@7998
   205
qed "in_pideal_imp_dvd";
paulson@7998
   206
paulson@7998
   207
Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}";
paulson@7998
   208
by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1);
paulson@10230
   209
by (etac contrapos_pp 1);
paulson@10230
   210
by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
paulson@7998
   211
by (rtac in_pideal_imp_dvd 1);
paulson@7998
   212
by (Asm_simp_tac 1);
ballarin@11093
   213
by (res_inst_tac [("x", "0")] exI 1);
ballarin@13735
   214
by (res_inst_tac [("x", "1")] exI 1);
paulson@7998
   215
by (Simp_tac 1);
paulson@7998
   216
qed "not_dvd_psubideal";
paulson@7998
   217
ballarin@13735
   218
Goalw [thm "irred_def"]
paulson@7998
   219
  "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I";
paulson@7998
   220
by (dtac is_pidealD 1);
paulson@7998
   221
by (etac exE 1);
paulson@7998
   222
by (Clarify_tac 1);
paulson@7998
   223
by (eres_inst_tac [("x", "aa")] allE 1);
paulson@7998
   224
by (Clarify_tac 1);
ballarin@13735
   225
by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1);
paulson@7998
   226
by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq]));
paulson@7998
   227
qed "irred_imp_max_ideal";
paulson@7998
   228
paulson@7998
   229
(* Pid are factorial *)
paulson@7998
   230
paulson@7998
   231
(* Divisor chain condition *)
paulson@7998
   232
(* proofs not finished *)
paulson@7998
   233
paulson@8707
   234
Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)";
paulson@8707
   235
by (induct_tac "m" 1);
paulson@7998
   236
by (Blast_tac 1);
paulson@7998
   237
(* induction step *)
paulson@8707
   238
by (rename_tac "m" 1);
paulson@7998
   239
by (case_tac "n <= m" 1);
paulson@7998
   240
by Auto_tac;
paulson@7998
   241
by (subgoal_tac "n = Suc m" 1);
paulson@8707
   242
by (arith_tac 2);
paulson@8707
   243
by (Force_tac 1);
paulson@8707
   244
qed_spec_mp "subset_chain_lemma";
paulson@7998
   245
paulson@8707
   246
Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \
nipkow@10833
   247
\     ==> is_ideal (Union (I`UNIV))";
paulson@7998
   248
by (rtac is_idealI 1);
paulson@7998
   249
by Auto_tac;
paulson@7998
   250
by (res_inst_tac [("x", "max x xa")] exI 1);
paulson@7998
   251
by (rtac is_ideal_add 1);
paulson@7998
   252
by (Asm_simp_tac 1);
paulson@8707
   253
by (rtac subset_chain_lemma 1);
paulson@7998
   254
by (assume_tac 1);
paulson@7998
   255
by (rtac conjI 1);
paulson@7998
   256
by (assume_tac 2);
paulson@7998
   257
by (arith_tac 1);
paulson@8707
   258
by (rtac subset_chain_lemma 1);
paulson@7998
   259
by (assume_tac 1);
paulson@7998
   260
by (rtac conjI 1);
paulson@7998
   261
by (assume_tac 2);
paulson@7998
   262
by (arith_tac 1);
paulson@7998
   263
by (res_inst_tac [("x", "x")] exI 1);
paulson@7998
   264
by (Asm_simp_tac 1);
paulson@7998
   265
by (res_inst_tac [("x", "x")] exI 1);
paulson@7998
   266
by (Asm_simp_tac 1);
paulson@7998
   267
qed "chain_is_ideal";
paulson@7998
   268
paulson@7998
   269
(*
paulson@7998
   270
Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
nipkow@10833
   271
\   EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}";
paulson@7998
   272
nipkow@10789
   273
Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}";
paulson@7998
   274
by (simp_tac (simpset()
paulson@7998
   275
  addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain]
paulson@7998
   276
  delsimps [psubideal_is_dvd]) 1);
paulson@7998
   277
*)
paulson@7998
   278
paulson@7998
   279
(* Primeness condition *)
paulson@7998
   280
ballarin@13735
   281
Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)";
paulson@7998
   282
by (rtac conjI 1);
paulson@7998
   283
by (rtac conjI 2);
paulson@7998
   284
by (Clarify_tac 3);
ballarin@13735
   285
by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")]
paulson@7998
   286
  irred_imp_max_ideal 3);
paulson@7998
   287
by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax],
ballarin@13735
   288
  simpset() addsimps [thm "irred_def", not_dvd_psubideal, pid_ax]));
paulson@7998
   289
by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
paulson@7998
   290
by (Clarify_tac 1);
paulson@7998
   291
by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
paulson@7998
   292
by (full_simp_tac (simpset() addsimps [r_distr]) 1);
ballarin@13735
   293
by (etac subst 1);
ballarin@13735
   294
by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]
ballarin@13735
   295
  delsimprocs [ring_simproc]) 1);
paulson@7998
   296
qed "pid_irred_imp_prime";
paulson@7998
   297
paulson@7998
   298
(* Fields are Pid *)
paulson@7998
   299
ballarin@11093
   300
Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV";
paulson@7998
   301
by (rtac subset_antisym 1);
paulson@7998
   302
by (Simp_tac 1);
paulson@7998
   303
by (rtac subset_trans 1);
paulson@7998
   304
by (rtac dvd_imp_subideal 2);
ballarin@13735
   305
by (rtac (thm "field_ax") 2);
paulson@7998
   306
by (assume_tac 2);
paulson@7998
   307
by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
paulson@7998
   308
qed "field_pideal_univ";
paulson@7998
   309
ballarin@11093
   310
Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I";
paulson@7998
   311
by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1);
paulson@7998
   312
qed "proper_ideal";
paulson@7998
   313
paulson@7998
   314
Goalw [is_pideal_def] "is_ideal (I::('a::field) set) ==> is_pideal I";
ballarin@11093
   315
by (case_tac "I = {0}" 1);
ballarin@11093
   316
by (res_inst_tac [("x", "0")] exI 1);
paulson@7998
   317
by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1);
ballarin@11093
   318
(* case "I ~= {0}" *)
paulson@7998
   319
by (ftac proper_ideal 1);
paulson@7998
   320
by (assume_tac 1);
paulson@7998
   321
by (dtac psubset_imp_ex_mem 1);
paulson@7998
   322
by (etac exE 1);
paulson@7998
   323
by (res_inst_tac [("x", "b")] exI 1);
paulson@7998
   324
by (cut_inst_tac [("a", "b")] element_generates_subideal 1);
paulson@7998
   325
  by (assume_tac 1); by (Blast_tac 1);
paulson@7998
   326
by (auto_tac (claset(), simpset() addsimps [field_pideal_univ]));
paulson@7998
   327
qed "field_pid";
paulson@7998
   328