src/HOL/GroupTheory/Ring.thy

HOL-Algebra partially ported to Isar.

(*  Title:      HOL/GroupTheory/Ring
    ID:         $Id$
    Author:     Florian Kammueller, with new proofs by L C Paulson

*)

header{*Ring Theory*}

theory Ring = Bij + Coset:


subsection{*Definition of a Ring*}

record 'a ring  = "'a group" +
  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>\<index>" 70)

record 'a unit_ring  = "'a ring" +
  one :: 'a    ("\<one>\<index>")


text{*Abbrevations for the left and right distributive laws*}
constdefs
  distrib_l :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
    "distrib_l A f g ==
       (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f x (g y z) = g (f x y) (f x z)))"

  distrib_r       :: "['a set, ['a, 'a] => 'a, ['a, 'a] => 'a] => bool"
    "distrib_r A f g == 
       (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (f (g y z) x = g (f y x) (f z x)))"


locale ring = abelian_group R +
  assumes prod_funcset: "prod R \<in> carrier R \<rightarrow> carrier R \<rightarrow> carrier R"
      and prod_assoc:   
            "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|] 
             ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
      and left:  "distrib_l (carrier R) (prod R) (sum R)"
      and right: "distrib_r (carrier R) (prod R) (sum R)"

constdefs
  Ring :: "('a,'b) ring_scheme set"
   "Ring == Collect ring"


lemma ring_is_abelian_group: "ring(R) ==> abelian_group(R)"
by (simp add: ring_def abelian_group_def)

text{*Construction of a ring from a semigroup and an Abelian group*}
lemma ringI:
     "[|abelian_group R; 
        semigroup(|carrier = carrier R, sum = prod R|);
        distrib_l (carrier R) (prod R) (sum R);
        distrib_r (carrier R) (prod R) (sum R)|] ==> ring R"
by (simp add: abelian_group_def ring_def ring_axioms_def semigroup_def) 

lemma (in ring) prod_closed [simp]:
     "[| x \<in> carrier R; y \<in> carrier R |] ==>  x \<cdot> y \<in> carrier R"
apply (insert prod_funcset) 
apply (blast dest: funcset_mem) 
done

declare ring.prod_closed [simp]

lemma (in ring) sum_closed:
     "[| x \<in> carrier R; y \<in> carrier R |] ==>  x \<oplus> y \<in> carrier R"
by simp 

declare ring.sum_closed [simp]

lemma (in ring) distrib_left:
     "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]  
      ==> x \<cdot> (y \<oplus> z) = (x \<cdot> y) \<oplus> (x \<cdot> z)"
apply (insert left) 
apply (simp add: distrib_l_def)
done

lemma (in ring) distrib_right:
     "[|x \<in> carrier R; y \<in> carrier R; z \<in> carrier R|]  
      ==> (y \<oplus> z) \<cdot> x = (y \<cdot> x) \<oplus> (z \<cdot> x)"
apply (insert right) 
apply (simp add: distrib_r_def)
done

lemma (in ring) prod_zero_left: "x \<in> carrier R ==> \<zero> \<cdot> x = \<zero>"
by (simp add: idempotent_imp_zero distrib_right [symmetric])

lemma (in ring) prod_zero_right: "x \<in> carrier R ==> x \<cdot> \<zero> = \<zero>"
by (simp add: idempotent_imp_zero distrib_left [symmetric])

lemma (in ring) prod_minus_left:
     "[|x \<in> carrier R; y \<in> carrier R|]  
      ==> (\<ominus>x) \<cdot> y = \<ominus> (x \<cdot> y)"
by (simp add: minus_unique prod_zero_left distrib_right [symmetric]) 

lemma (in ring) prod_minus_right:
     "[|x \<in> carrier R; y \<in> carrier R|]  
      ==> x \<cdot> (\<ominus>y) = \<ominus> (x \<cdot> y)"
by (simp add: minus_unique prod_zero_right distrib_left [symmetric]) 


subsection {*Example: The Ring of Integers*}

constdefs
 integers :: "int ring"
  "integers == (|carrier = UNIV, 
                 sum = op +,
                 gminus = (%x. -x),
                 zero = 0::int,
                 prod = op *|)"

theorem ring_integers: "ring (integers)"
by (simp add: integers_def ring_def ring_axioms_def 
              distrib_l_def distrib_r_def 
              zadd_zmult_distrib zadd_zmult_distrib2 
              abelian_group_axioms_def group_axioms_def semigroup_def) 


subsection {*Ring Homomorphisms*}

constdefs
 ring_hom :: "[('a,'c)ring_scheme, ('b,'d)ring_scheme] => ('a => 'b)set"
  "ring_hom R R' ==
   {h. h \<in> carrier R -> carrier R' & 
       (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(sum R x y) = sum R' (h x) (h y)) &
       (\<forall>x \<in> carrier R. \<forall>y \<in> carrier R. h(prod R x y) = prod R' (h x) (h y))}"

 ring_auto :: "('a,'b)ring_scheme => ('a => 'a)set"
  "ring_auto R == ring_hom R R \<inter> Bij(carrier R)"

  RingAutoGroup :: "[('a,'c) ring_scheme] => ('a=>'a) group"
  "RingAutoGroup R == BijGroup (carrier R) (|carrier := ring_auto R |)"


lemma ring_hom_subset_hom: "ring_hom R R' <= hom R R'"
by (force simp add: ring_hom_def hom_def)

subsection{*The Ring Automorphisms From a Group*}

lemma id_in_ring_auto: "ring R ==> (%x: carrier R. x) \<in> ring_auto R"
by (simp add: ring_auto_def ring_hom_def restrictI ring.axioms id_Bij) 

lemma restrict_Inv_ring_hom:
      "[|ring R; h \<in> ring_hom R R; h \<in> Bij (carrier R)|]
       ==> restrict (Inv (carrier R) h) (carrier R) \<in> ring_hom R R"
by (simp add: ring.axioms group.axioms 
              ring_hom_def Bij_Inv_mem restrictI 
              semigroup.sum_funcset ring.prod_funcset Bij_Inv_lemma)

text{*Ring automorphisms are a subgroup of the group of bijections over the 
   ring's carrier, and thus a group*}
lemma subgroup_ring_auto:
      "ring R ==> subgroup (ring_auto R) (BijGroup (carrier R))"
apply (rule group.subgroupI) 
    apply (rule group_BijGroup) 
   apply (force simp add: ring_auto_def BijGroup_def) 
  apply (blast dest: id_in_ring_auto) 
 apply (simp add: ring_auto_def BijGroup_def restrict_Inv_Bij
                  restrict_Inv_ring_hom) 
apply (simp add: ring_auto_def BijGroup_def compose_Bij)
apply (simp add: ring_hom_def compose_def Pi_def)
done

lemma ring_auto: "ring R ==> group (RingAutoGroup R)"
apply (drule subgroup_ring_auto) 
apply (simp add: subgroup_def RingAutoGroup_def) 
done


subsection{*A Locale for a Pair of Rings and a Homomorphism*}

locale ring_homomorphism = ring R + ring R' +
  fixes h
  assumes homh: "h \<in> ring_hom R R'"

lemma ring_hom_sum:
     "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|] 
      ==> h(sum R x y) = sum R' (h x) (h y)"
by (simp add: ring_hom_def) 

lemma ring_hom_prod:
     "[|h \<in> ring_hom R R'; x \<in> carrier R; y \<in> carrier R|] 
      ==> h(prod R x y) = prod R' (h x) (h y)"
by (simp add: ring_hom_def) 

lemma ring_hom_closed:
     "[|h \<in> ring_hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'"
by (auto simp add: ring_hom_def funcset_mem)

lemma (in ring_homomorphism) ring_hom_sum [simp]:
     "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)"
by (simp add: ring_hom_sum [OF homh])

lemma (in ring_homomorphism) ring_hom_prod [simp]:
     "[|x \<in> carrier R; y \<in> carrier R|] ==> h (x \<cdot>\<^sub>1 y) = (h x) \<cdot>\<^sub>2 (h y)"
by (simp add: ring_hom_prod [OF homh])

lemma (in ring_homomorphism) group_homomorphism: "group_homomorphism R R' h"
by (simp add: group_homomorphism_def group_homomorphism_axioms_def
              prems homh ring_hom_subset_hom [THEN subsetD])

lemma (in ring_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier R'"
by (simp add: ring_hom_closed [OF homh]) 

lemma (in ring_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2"
by (rule group_homomorphism.hom_zero [OF group_homomorphism]) 

lemma (in ring_homomorphism) hom_minus_closed [simp]:
     "x \<in> carrier R ==> h (\<ominus>x) \<in> carrier R'"
by (rule group_homomorphism.hom_minus_closed [OF group_homomorphism]) 

lemma (in ring_homomorphism) hom_minus [simp]:
     "x \<in> carrier R ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)"
by (rule group_homomorphism.hom_minus [OF group_homomorphism]) 


text{*Needed because the standard theorem @{text "ring_homomorphism.intro"} 
is unnatural.*}
lemma ring_homomorphismI:
    "[|ring R; ring R'; h \<in> ring_hom R R'|] ==> ring_homomorphism R R' h"
by (simp add: ring_def ring_homomorphism_def ring_homomorphism_axioms_def)

end