isabelle: src/HOL/Algebra/abstract/Ideal.thy@fc385ce6187d (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Ideals for commutative rings
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 24 September 1999
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	7	theory Ideal imports Ring begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9	consts
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	10	ideal_of :: "('a::ring) set => 'a set"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	11	is_ideal :: "('a::ring) set => bool"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	12	is_pideal :: "('a::ring) set => bool"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14	defs
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	15	is_ideal_def: "is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	16	(ALL a: I. - a : I) & 0 : I &
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	17	(ALL a: I. ALL r. a * r : I)"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	18	ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	19	is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	20
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	21	text {* Principle ideal domains *}
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	22
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	23	axclass pid < "domain"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	24	pid_ax: "is_ideal I ==> is_pideal I"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	25
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	26	end

author	aspinall
	Fri, 30 Sep 2005 18:18:34 +0200
changeset 17740	fc385ce6187d
parent 17479	68a7acb5f22e
permissions	-rw-r--r--