--- a/src/HOL/Algebra/abstract/Ideal.ML Thu Aug 03 14:53:57 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,328 +0,0 @@
-(*
- Ideals for commutative rings
- $Id$
- Author: Clemens Ballarin, started 24 September 1999
-*)
-
-(* is_ideal *)
-
-Goalw [thm "is_ideal_def"]
- "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \
-\ !! a. a:I ==> - a : I; 0 : I; \
-\ !! a r. a:I ==> a * r : I |] ==> is_ideal I";
-by Auto_tac;
-qed "is_idealI";
-
-Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I; b:I |] ==> a + b : I";
-by (Fast_tac 1);
-qed "is_ideal_add";
-
-Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> - a : I";
-by (Fast_tac 1);
-qed "is_ideal_uminus";
-
-Goalw [thm "is_ideal_def"] "[| is_ideal I |] ==> 0 : I";
-by (Fast_tac 1);
-qed "is_ideal_zero";
-
-Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> a * r : I";
-by (Fast_tac 1);
-qed "is_ideal_mult";
-
-Goalw [dvd_def, thm "is_ideal_def"] "[| a dvd b; is_ideal I; a:I |] ==> b:I";
-by (Fast_tac 1);
-qed "is_ideal_dvd";
-
-Goalw [thm "is_ideal_def"] "is_ideal (UNIV::('a::ring) set)";
-by Auto_tac;
-qed "UNIV_is_ideal";
-
-Goalw [thm "is_ideal_def"] "is_ideal {0::'a::ring}";
-by Auto_tac;
-qed "zero_is_ideal";
-
-Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult,
- UNIV_is_ideal, zero_is_ideal];
-
-Goal "is_ideal {x::'a::ring. a dvd x}";
-by (rtac is_idealI 1);
-by Auto_tac;
-qed "is_ideal_1";
-
-Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}";
-by (rtac is_idealI 1);
-(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *)
-by (Clarify_tac 1);
-by (Clarify_tac 2);
-by (Clarify_tac 3);
-by (Clarify_tac 4);
-by (res_inst_tac [("x", "u+ua")] exI 1);
-by (res_inst_tac [("x", "v+va")] exI 1);
-by (res_inst_tac [("x", "-u")] exI 2);
-by (res_inst_tac [("x", "-v")] exI 2);
-by (res_inst_tac [("x", "0")] exI 3);
-by (res_inst_tac [("x", "0")] exI 3);
-by (res_inst_tac [("x", "u * r")] exI 4);
-by (res_inst_tac [("x", "v * r")] exI 4);
-by (REPEAT (Simp_tac 1));
-qed "is_ideal_2";
-
-(* ideal_of *)
-
-Goalw [thm "is_ideal_def", thm "ideal_of_def"] "is_ideal (ideal_of S)";
-by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *)
-qed "ideal_of_is_ideal";
-
-Goalw [thm "ideal_of_def"] "a:S ==> a : (ideal_of S)";
-by Auto_tac;
-qed "generator_in_ideal";
-
-Goalw [thm "ideal_of_def"] "ideal_of {1::'a::ring} = UNIV";
-by (force_tac (claset() addDs [is_ideal_mult],
- simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1);
- (* FIXME: Zumkeller's order raises Domain exn *)
-qed "ideal_of_one_eq";
-
-Goalw [thm "ideal_of_def"] "ideal_of {} = {0::'a::ring}";
-by (rtac subset_antisym 1);
-by (rtac subsetI 1);
-by (dtac InterD 1);
-by (assume_tac 2);
-by (auto_tac (claset(), simpset() addsimps [is_ideal_zero]));
-qed "ideal_of_empty_eq";
-
-Goalw [thm "ideal_of_def"] "ideal_of {a} = {x::'a::ring. a dvd x}";
-by (rtac subset_antisym 1);
-by (rtac subsetI 1);
-by (dtac InterD 1);
-by (assume_tac 2);
-by (auto_tac (claset() addIs [is_ideal_1], simpset()));
-by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1);
-qed "pideal_structure";
-
-Goalw [thm "ideal_of_def"]
- "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}";
-by (rtac subset_antisym 1);
-by (rtac subsetI 1);
-by (dtac InterD 1);
-by (assume_tac 2);
-by (auto_tac (claset() addIs [is_ideal_2],
- simpset() delsimprocs [ring_simproc]));
-(* FIXME: Zumkeller's order *)
-by (res_inst_tac [("x", "1")] exI 1);
-by (res_inst_tac [("x", "0")] exI 1);
-by (res_inst_tac [("x", "0")] exI 2);
-by (res_inst_tac [("x", "1")] exI 2);
-by (Simp_tac 1);
-by (Simp_tac 1);
-qed "ideal_of_2_structure";
-
-Goalw [thm "ideal_of_def"] "A <= B ==> ideal_of A <= ideal_of B";
-by Auto_tac;
-qed "ideal_of_mono";
-
-Goal "ideal_of {0::'a::ring} = {0}";
-by (simp_tac (simpset() addsimps [pideal_structure]) 1);
-by (rtac subset_antisym 1);
-by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
-qed "ideal_of_zero_eq";
-
-Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
-by (auto_tac (claset(),
- simpset() addsimps [pideal_structure, is_ideal_dvd]));
-qed "element_generates_subideal";
-
-(* is_pideal *)
-
-Goalw [thm "is_pideal_def"] "is_pideal (I::('a::ring) set) ==> is_ideal I";
-by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1);
-qed "is_pideal_imp_is_ideal";
-
-Goalw [thm "is_pideal_def"] "is_pideal (ideal_of {a::'a::ring})";
-by (Fast_tac 1);
-qed "pideal_is_pideal";
-
-Goalw [thm "is_pideal_def"] "is_pideal I ==> EX a. I = ideal_of {a}";
-by (assume_tac 1);
-qed "is_pidealD";
-
-(* Ideals and divisibility *)
-
-Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
-by (auto_tac (claset() addIs [dvd_trans_ring],
- simpset() addsimps [pideal_structure]));
-qed "dvd_imp_subideal";
-
-Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a";
-by (auto_tac (claset() addSDs [subsetD],
- simpset() addsimps [pideal_structure]));
-qed "subideal_imp_dvd";
-
-Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)";
-by (rtac iffI 1);
-by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1));
-qed "subideal_is_dvd";
-
-Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b";
-by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
-by (etac conjE 1);
-by (dres_inst_tac [("c", "a")] subsetD 1);
-by (auto_tac (claset() addIs [dvd_trans_ring],
- simpset()));
-qed "psubideal_not_dvd";
-
-Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
-by (rtac psubsetI 1);
-by (etac dvd_imp_subideal 1);
-by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1);
-qed "not_dvd_psubideal_singleton";
-
-Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)";
-by (rtac iffI 1);
-by (REPEAT (ares_tac
- [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
-by (etac conjE 1);
-by (REPEAT (ares_tac [not_dvd_psubideal_singleton] 1));
-qed "psubideal_is_dvd";
-
-Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}";
-by (rtac subset_antisym 1);
-by (REPEAT (ares_tac [dvd_imp_subideal] 1));
-qed "assoc_pideal_eq";
-
-AddIffs [subideal_is_dvd, psubideal_is_dvd];
-
-Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})";
-by (rtac is_ideal_dvd 1);
-by (assume_tac 1);
-by (rtac ideal_of_is_ideal 1);
-by (rtac generator_in_ideal 1);
-by (Simp_tac 1);
-qed "dvd_imp_in_pideal";
-
-Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b";
-by (full_simp_tac (simpset() addsimps [pideal_structure]) 1);
-qed "in_pideal_imp_dvd";
-
-Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}";
-by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1);
-by (etac contrapos_pp 1);
-by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
-by (rtac in_pideal_imp_dvd 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("x", "0")] exI 1);
-by (res_inst_tac [("x", "1")] exI 1);
-by (Simp_tac 1);
-qed "not_dvd_psubideal";
-
-Goalw [thm "irred_def"]
- "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I";
-by (dtac is_pidealD 1);
-by (etac exE 1);
-by (Clarify_tac 1);
-by (eres_inst_tac [("x", "aa")] allE 1);
-by (Clarify_tac 1);
-by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1);
-by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq]));
-qed "irred_imp_max_ideal";
-
-(* Pid are factorial *)
-
-(* Divisor chain condition *)
-(* proofs not finished *)
-
-Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)";
-by (induct_tac "m" 1);
-by (Blast_tac 1);
-(* induction step *)
-by (rename_tac "m" 1);
-by (case_tac "n <= m" 1);
-by Auto_tac;
-by (subgoal_tac "n = Suc m" 1);
-by (arith_tac 2);
-by (Force_tac 1);
-qed_spec_mp "subset_chain_lemma";
-
-Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \
-\ ==> is_ideal (Union (I`UNIV))";
-by (rtac is_idealI 1);
-by Auto_tac;
-by (res_inst_tac [("x", "max x xa")] exI 1);
-by (rtac is_ideal_add 1);
-by (Asm_simp_tac 1);
-by (rtac subset_chain_lemma 1);
-by (assume_tac 1);
-by (rtac conjI 1);
-by (assume_tac 2);
-by (arith_tac 1);
-by (rtac subset_chain_lemma 1);
-by (assume_tac 1);
-by (rtac conjI 1);
-by (assume_tac 2);
-by (arith_tac 1);
-by (res_inst_tac [("x", "x")] exI 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("x", "x")] exI 1);
-by (Asm_simp_tac 1);
-qed "chain_is_ideal";
-
-(*
-Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
-\ EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}";
-
-Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}";
-by (simp_tac (simpset()
- addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain]
- delsimps [psubideal_is_dvd]) 1);
-*)
-
-(* Primeness condition *)
-
-Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)";
-by (rtac conjI 1);
-by (rtac conjI 2);
-by (Clarify_tac 3);
-by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")]
- irred_imp_max_ideal 3);
-by (auto_tac (claset() addIs [ideal_of_is_ideal, thm "pid_ax"],
- simpset() addsimps [thm "irred_def", not_dvd_psubideal, thm "pid_ax"]));
-by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
-by (Clarify_tac 1);
-by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [r_distr]) 1);
-by (etac subst 1);
-by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]
- delsimprocs [ring_simproc]) 1);
-qed "pid_irred_imp_prime";
-
-(* Fields are Pid *)
-
-Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV";
-by (rtac subset_antisym 1);
-by (Simp_tac 1);
-by (rtac subset_trans 1);
-by (rtac dvd_imp_subideal 2);
-by (rtac (thm "field_ax") 2);
-by (assume_tac 2);
-by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
-qed "field_pideal_univ";
-
-Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I";
-by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1);
-qed "proper_ideal";
-
-Goalw [thm "is_pideal_def"] "is_ideal (I::('a::field) set) ==> is_pideal I";
-by (case_tac "I = {0}" 1);
-by (res_inst_tac [("x", "0")] exI 1);
-by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1);
-(* case "I ~= {0}" *)
-by (ftac proper_ideal 1);
-by (assume_tac 1);
-by (dtac psubset_imp_ex_mem 1);
-by (etac exE 1);
-by (res_inst_tac [("x", "b")] exI 1);
-by (cut_inst_tac [("a", "b")] element_generates_subideal 1);
- by (assume_tac 1); by (Blast_tac 1);
-by (auto_tac (claset(), simpset() addsimps [field_pideal_univ]));
-qed "field_pid";
-