src/HOL/Algebra/abstract/Ideal.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 13735 7de9342aca7a
child 17479 68a7acb5f22e
permissions -rw-r--r--
Constant "If" is now local
paulson@7998
     1
(*
paulson@7998
     2
    Ideals for commutative rings
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 24 September 1999
paulson@7998
     5
*)
paulson@7998
     6
paulson@7998
     7
Ideal = Ring +
paulson@7998
     8
paulson@7998
     9
consts
ballarin@13735
    10
  ideal_of	:: ('a::ring) set => 'a set
ballarin@13735
    11
  is_ideal	:: ('a::ring) set => bool
ballarin@13735
    12
  is_pideal	:: ('a::ring) set => bool
paulson@7998
    13
paulson@7998
    14
defs
paulson@7998
    15
  is_ideal_def	"is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
ballarin@11093
    16
                               (ALL a: I. - a : I) & 0 : I &
paulson@7998
    17
                               (ALL a: I. ALL r. a * r : I)"
paulson@7998
    18
  ideal_of_def	"ideal_of S == Inter {I. is_ideal I & S <= I}"
paulson@7998
    19
  is_pideal_def	"is_pideal I == (EX a. I = ideal_of {a})"
paulson@7998
    20
paulson@7998
    21
(* Principle ideal domains *)
paulson@7998
    22
paulson@7998
    23
axclass
paulson@7998
    24
  pid < domain
paulson@7998
    25
paulson@7998
    26
  pid_ax	"is_ideal I ==> is_pideal I"
paulson@7998
    27
paulson@7998
    28
end