src/HOL/Algebra/abstract/Ideal2.thy

Restructured algebra library, added ideals and quotient rings.

(*
    Ideals for commutative rings
    $Id$
    Author: Clemens Ballarin, started 24 September 1999
*)

theory Ideal2 imports Ring2 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