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