# Theory Ideal

Up to index of Isabelle/HOL/HOL-Algebra

theory Ideal
imports Ring
uses [Ideal.ML]
begin

    (*
        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