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. [| aI; bI |] ==> a + bI; !!a. aI ==> - aI; (0::'a) ∈ I;
     !!a r. aI ==> a * rI |]
  ==> is_ideal I

theorem is_ideal_add:

  [| is_ideal I; aI; bI |] ==> a + bI

theorem is_ideal_uminus:

  [| is_ideal I; aI |] ==> - aI

theorem is_ideal_zero:

  is_ideal I ==> (0::'a) ∈ I

theorem is_ideal_mult:

  [| is_ideal I; aI |] ==> a * rI

theorem is_ideal_dvd:

  [| a dvd b; is_ideal I; aI |] ==> bI

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:

  aS ==> 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:

  AB ==> ideal_of A ⊆ ideal_of B

theorem ideal_of_zero_eq:

  ideal_of {0::'a} = {0::'a}

theorem element_generates_subideal:

  [| is_ideal I; aI |] ==> 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 |] ==> xI

theorem subset_chain_lemma:

  [| ∀i. I iI (Suc i); nmaI n |] ==> aI m

theorem chain_is_ideal:

  [| ∀i. is_ideal (I i); ∀i. I iI (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