src/HOL/Algebra/abstract/Ideal2.ML

dvd_def now with object equality

(*
    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 [thm "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 [thm "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 [thm "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";