Up to index of Isabelle/HOL/HOL-Algebra
theory Ideal(* Ideals for commutative rings $Id: Ideal.thy,v 1.4 2005/09/17 18:49:14 wenzelm Exp $ Author: Clemens Ballarin, started 24 September 1999 *) theory Ideal imports Ring begin consts ideal_of :: "('a::ring) set => 'a set" is_ideal :: "('a::ring) set => bool" is_pideal :: "('a::ring) set => bool" defs is_ideal_def: "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)" ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}" is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})" text {* Principle ideal domains *} axclass pid < "domain" pid_ax: "is_ideal I ==> is_pideal I" end
theorem is_idealI:
[| !!a b. [| a ∈ I; b ∈ I |] ==> a + b ∈ I; !!a. a ∈ I ==> - a ∈ I; (0::'a) ∈ I; !!a r. a ∈ I ==> a * r ∈ I |] ==> is_ideal I
theorem is_ideal_add:
[| is_ideal I; a ∈ I; b ∈ I |] ==> a + b ∈ I
theorem is_ideal_uminus:
[| is_ideal I; a ∈ I |] ==> - a ∈ I
theorem is_ideal_zero:
is_ideal I ==> (0::'a) ∈ I
theorem is_ideal_mult:
[| is_ideal I; a ∈ I |] ==> a * r ∈ I
theorem is_ideal_dvd:
[| a dvd b; is_ideal I; a ∈ I |] ==> b ∈ I
theorem UNIV_is_ideal:
is_ideal UNIV
theorem zero_is_ideal:
is_ideal {0::'a}
theorem is_ideal_1:
is_ideal {x. a dvd x}
theorem is_ideal_2:
is_ideal {x. ∃u v. x = a * u + b * v}
theorem ideal_of_is_ideal:
is_ideal (ideal_of S)
theorem generator_in_ideal:
a ∈ S ==> a ∈ ideal_of S
theorem ideal_of_one_eq:
ideal_of {1::'a} = UNIV
theorem ideal_of_empty_eq:
ideal_of {} = {0::'a}
theorem pideal_structure:
ideal_of {a} = {x. a dvd x}
theorem ideal_of_2_structure:
ideal_of {a, b} = {x. ∃u v. x = a * u + b * v}
theorem ideal_of_mono:
A ⊆ B ==> ideal_of A ⊆ ideal_of B
theorem ideal_of_zero_eq:
ideal_of {0::'a} = {0::'a}
theorem element_generates_subideal:
[| is_ideal I; a ∈ I |] ==> ideal_of {a} ⊆ I
theorem is_pideal_imp_is_ideal:
is_pideal I ==> is_ideal I
theorem pideal_is_pideal:
is_pideal (ideal_of {a})
theorem is_pidealD:
is_pideal I ==> ∃a. I = ideal_of {a}
theorem dvd_imp_subideal:
b dvd a ==> ideal_of {a} ⊆ ideal_of {b}
theorem subideal_imp_dvd:
ideal_of {a} ⊆ ideal_of {b} ==> b dvd a
theorem subideal_is_dvd:
(ideal_of {a} ⊆ ideal_of {b}) = (b dvd a)
theorem psubideal_not_dvd:
ideal_of {a} ⊂ ideal_of {b} ==> ¬ a dvd b
theorem not_dvd_psubideal_singleton:
[| b dvd a; ¬ a dvd b |] ==> ideal_of {a} ⊂ ideal_of {b}
theorem psubideal_is_dvd:
(ideal_of {a} ⊂ ideal_of {b}) = (b dvd a ∧ ¬ a dvd b)
theorem assoc_pideal_eq:
[| a dvd b; b dvd a |] ==> ideal_of {a} = ideal_of {b}
theorem dvd_imp_in_pideal:
a dvd b ==> b ∈ ideal_of {a}
theorem in_pideal_imp_dvd:
b ∈ ideal_of {a} ==> a dvd b
theorem not_dvd_psubideal:
¬ a dvd b ==> ideal_of {a} ⊂ ideal_of {a, b}
theorem irred_imp_max_ideal:
[| irred a; is_pideal I; ideal_of {a} ⊂ I |] ==> x ∈ I
theorem subset_chain_lemma:
[| ∀i. I i ⊆ I (Suc i); n ≤ m ∧ a ∈ I n |] ==> a ∈ I m
theorem chain_is_ideal:
[| ∀i. is_ideal (I i); ∀i. I i ⊆ I (Suc i) |] ==> is_ideal (Union (range I))
theorem pid_irred_imp_prime:
irred a ==> prime a
theorem field_pideal_univ:
a ≠ (0::'a) ==> ideal_of {a} = UNIV
theorem proper_ideal:
[| is_ideal I; I ≠ {0::'a} |] ==> {0::'a} ⊂ I
theorem field_pid:
is_ideal I ==> is_pideal I