# Theory Ideal2

Up to index of Isabelle/HOL/HOL-Algebra

theory Ideal2
imports Ring2
`(*  Author: Clemens Ballarin, started 24 September 1999Ideals for commutative rings.*)theory Ideal2imports Ring2begindefinition  is_ideal :: "('a::ring) set => bool" where  "is_ideal I <-> (ALL a: I. ALL b: I. a + b : I) &                           (ALL a: I. - a : I) & 0 : I &                           (ALL a: I. ALL r. a * r : I)"definition  ideal_of :: "('a::ring) set => 'a set" where  "ideal_of S = Inter {I. is_ideal I & S <= I}"definition  is_pideal :: "('a::ring) set => bool" where  "is_pideal I <-> (EX a. I = ideal_of {a})"text {* Principle ideal domains *}class pid =  assumes pid_ax: "is_ideal (I :: ('a::domain) set) ==> is_pideal I"(* is_ideal *)lemma is_idealI:  "!! 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"  unfolding is_ideal_def by blastlemma is_ideal_add [simp]: "[| is_ideal I; a:I; b:I |] ==> a + b : I"  unfolding is_ideal_def by blastlemma is_ideal_uminus [simp]: "[| is_ideal I; a:I |] ==> - a : I"  unfolding is_ideal_def by blastlemma is_ideal_zero [simp]: "[| is_ideal I |] ==> 0 : I"  unfolding is_ideal_def by blastlemma is_ideal_mult [simp]: "[| is_ideal I; a:I |] ==> a * r : I"  unfolding is_ideal_def by blastlemma is_ideal_dvd: "[| a dvd b; is_ideal I; a:I |] ==> b:I"  unfolding is_ideal_def dvd_def by blastlemma UNIV_is_ideal [simp]: "is_ideal (UNIV::('a::ring) set)"  unfolding is_ideal_def by blastlemma zero_is_ideal [simp]: "is_ideal {0::'a::ring}"  unfolding is_ideal_def by autolemma is_ideal_1: "is_ideal {x::'a::ring. a dvd x}"  apply (rule is_idealI)  apply auto  donelemma is_ideal_2: "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"  apply (rule is_idealI)  apply auto     apply (rule_tac x = "u+ua" in exI)     apply (rule_tac x = "v+va" in exI)     apply (rule_tac [2] x = "-u" in exI)     apply (rule_tac [2] x = "-v" in exI)     apply (rule_tac [3] x = "0" in exI)     apply (rule_tac [3] x = "0" in exI)     apply (rule_tac [4] x = "u * r" in exI)     apply (rule_tac [4] x = "v * r" in exI)  apply simp_all  done(* ideal_of *)lemma ideal_of_is_ideal: "is_ideal (ideal_of S)"  unfolding is_ideal_def ideal_of_def by blastlemma generator_in_ideal: "a:S ==> a : (ideal_of S)"  unfolding ideal_of_def by blastlemma ideal_of_one_eq: "ideal_of {1::'a::ring} = UNIV"  apply (unfold ideal_of_def)  apply (force dest: is_ideal_mult simp add: l_one)  donelemma ideal_of_empty_eq: "ideal_of {} = {0::'a::ring}"  apply (unfold ideal_of_def)  apply (rule subset_antisym)   apply (rule subsetI)   apply (drule InterD)    prefer 2 apply assumption   apply (auto simp add: is_ideal_zero)  donelemma pideal_structure: "ideal_of {a} = {x::'a::ring. a dvd x}"  apply (unfold ideal_of_def)  apply (rule subset_antisym)   apply (rule subsetI)   apply (drule InterD)    prefer 2 apply assumption   apply (auto intro: is_ideal_1)  apply (simp add: is_ideal_dvd)  donelemma ideal_of_2_structure:    "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"  apply (unfold ideal_of_def)  apply (rule subset_antisym)   apply (rule subsetI)   apply (drule InterD)    prefer 2 apply assumption   using [[simproc del: ring]]   apply (auto intro: is_ideal_2)   using [[simproc ring]]   apply (rule_tac x = "1" in exI)   apply (rule_tac x = "0" in exI)   apply (rule_tac [2] x = "0" in exI)   apply (rule_tac [2] x = "1" in exI)   apply simp  apply simp  donelemma ideal_of_mono: "A <= B ==> ideal_of A <= ideal_of B"  unfolding ideal_of_def by blastlemma ideal_of_zero_eq: "ideal_of {0::'a::ring} = {0}"  apply (simp add: pideal_structure)  apply (rule subset_antisym)   apply (auto intro: "dvd_zero_left")  donelemma element_generates_subideal: "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"  apply (auto simp add: pideal_structure is_ideal_dvd)  done(* is_pideal *)lemma is_pideal_imp_is_ideal: "is_pideal (I::('a::ring) set) ==> is_ideal I"  unfolding is_pideal_def by (fast intro: ideal_of_is_ideal)lemma pideal_is_pideal: "is_pideal (ideal_of {a::'a::ring})"  unfolding is_pideal_def by blastlemma is_pidealD: "is_pideal I ==> EX a. I = ideal_of {a}"  unfolding is_pideal_def .(* Ideals and divisibility *)lemma dvd_imp_subideal: "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"  by (auto intro: dvd_trans_ring simp add: pideal_structure)lemma subideal_imp_dvd: "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"  by (auto dest!: subsetD simp add: pideal_structure)lemma psubideal_not_dvd: "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"  apply (simp add: psubset_eq pideal_structure)  apply (erule conjE)  apply (drule_tac c = "a" in subsetD)   apply (auto intro: dvd_trans_ring)  donelemma not_dvd_psubideal_singleton:    "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"  apply (rule psubsetI)   apply (erule dvd_imp_subideal)  apply (blast intro: dvd_imp_subideal subideal_imp_dvd)  donelemma subideal_is_dvd [iff]: "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"  apply (rule iffI)   apply (assumption | rule subideal_imp_dvd dvd_imp_subideal)+  donelemma psubideal_is_dvd [iff]: "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"  apply (rule iffI)  apply (assumption | rule conjI psubideal_not_dvd psubset_imp_subset [THEN subideal_imp_dvd])+  apply (erule conjE)  apply (assumption | rule not_dvd_psubideal_singleton)+  donelemma assoc_pideal_eq: "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"  apply (rule subset_antisym)  apply (assumption | rule dvd_imp_subideal)+  donelemma dvd_imp_in_pideal: "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"  apply (rule is_ideal_dvd)    apply assumption   apply (rule ideal_of_is_ideal)  apply (rule generator_in_ideal)  apply simp  donelemma in_pideal_imp_dvd: "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"  by (simp add: pideal_structure)lemma not_dvd_psubideal: "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"  apply (simp add: psubset_eq ideal_of_mono)  apply (erule contrapos_pp)  apply (simp add: ideal_of_2_structure)  apply (rule in_pideal_imp_dvd)  apply simp  apply (rule_tac x = "0" in exI)  apply (rule_tac x = "1" in exI)  apply simp  donelemma irred_imp_max_ideal:    "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"  apply (unfold irred_def)  apply (drule is_pidealD)  apply (erule exE)  apply clarify  apply (erule_tac x = "aa" in allE)  apply clarify  apply (drule_tac a = "1" in dvd_imp_subideal)  apply (auto simp add: ideal_of_one_eq)  done(* Pid are factorial *)(* Divisor chain condition *)(* proofs not finished *)lemma subset_chain_lemma [rule_format (no_asm)]:  "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"  apply (induct_tac m)   apply blast  (* induction step *)   apply (rename_tac m)   apply (case_tac "n <= m")    apply auto  apply (subgoal_tac "n = Suc m")   prefer 2   apply arith  apply force  donelemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]    ==> is_ideal (Union (I`UNIV))"  apply (rule is_idealI)     apply auto    apply (rule_tac x = "max x xa" in exI)    apply (rule is_ideal_add)      apply simp     apply (rule subset_chain_lemma)      apply assumption     apply (rule conjI)      prefer 2      apply assumption     apply arith    apply (rule subset_chain_lemma)    apply assumption   apply (rule conjI)     prefer 2     apply assumption    apply arith   apply (rule_tac x = "x" in exI)   apply simp   apply (rule_tac x = "x" in exI)   apply simp   done(* Primeness condition *)lemma pid_irred_imp_prime: "irred a ==> prime (a::'a::pid)"  apply (unfold prime_def)  apply (rule conjI)   apply (rule_tac [2] conjI)    apply (tactic "clarify_tac @{context} 3")    apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)      apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)  apply (simp add: ideal_of_2_structure)  apply clarify  apply (drule_tac f = "op* aa" in arg_cong)  apply (simp add: r_distr)  apply (erule subst)  using [[simproc del: ring]]  apply (simp add: m_assoc [symmetric])  done(* Fields are Pid *)lemma field_pideal_univ: "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"  apply (rule subset_antisym)   apply simp  apply (rule subset_trans)   prefer 2   apply (rule dvd_imp_subideal)   apply (rule field_ax)   apply assumption  apply (simp add: ideal_of_one_eq)  donelemma proper_ideal: "[| is_ideal I; I ~= {0} |] ==> {0} < I"  by (simp add: psubset_eq not_sym is_ideal_zero)lemma field_pid: "is_ideal (I::('a::field) set) ==> is_pideal I"  apply (unfold is_pideal_def)  apply (case_tac "I = {0}")   apply (rule_tac x = "0" in exI)  apply (simp add: ideal_of_zero_eq)  (* case "I ~= {0}" *)  apply (frule proper_ideal)   apply assumption  apply (drule psubset_imp_ex_mem)  apply (erule exE)  apply (rule_tac x = b in exI)  apply (cut_tac a = b in element_generates_subideal)    apply assumption   apply blast  apply (auto simp add: field_pideal_univ)  doneend`