src/HOL/Algebra/Ring.thy
changeset 27717 21bbd410ba04
parent 27714 27b4d7c01f8b
child 27933 4b867f6a65d3
     1.1 --- a/src/HOL/Algebra/Ring.thy	Fri Aug 01 17:41:37 2008 +0200
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Fri Aug 01 18:10:52 2008 +0200
     1.3 @@ -9,7 +9,9 @@
     1.4  uses ("ringsimp.ML") begin
     1.5  
     1.6  
     1.7 -section {* Abelian Groups *}
     1.8 +section {* The Algebraic Hierarchy of Rings *}
     1.9 +
    1.10 +subsection {* Abelian Groups *}
    1.11  
    1.12  record 'a ring = "'a monoid" +
    1.13    zero :: 'a ("\<zero>\<index>")
    1.14 @@ -341,9 +343,7 @@
    1.15  *)
    1.16  
    1.17  
    1.18 -section {* The Algebraic Hierarchy of Rings *}
    1.19 -
    1.20 -subsection {* Basic Definitions *}
    1.21 +subsection {* Rings: Basic Definitions *}
    1.22  
    1.23  locale ring = abelian_group R + monoid R +
    1.24    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.25 @@ -554,13 +554,13 @@
    1.26        show "\<one> = \<zero>" by simp
    1.27  qed
    1.28  
    1.29 -lemma (in ring) one_zero:
    1.30 +lemma (in ring) carrier_one_zero:
    1.31    shows "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
    1.32    by (rule, erule one_zeroI, erule one_zeroD)
    1.33  
    1.34 -lemma (in ring) one_not_zero:
    1.35 +lemma (in ring) carrier_one_not_zero:
    1.36    shows "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
    1.37 -  by (simp add: one_zero)
    1.38 +  by (simp add: carrier_one_zero)
    1.39  
    1.40  text {* Two examples for use of method algebra *}
    1.41  
    1.42 @@ -588,7 +588,7 @@
    1.43  
    1.44  subsubsection {* Sums over Finite Sets *}
    1.45  
    1.46 -lemma (in cring) finsum_ldistr:
    1.47 +lemma (in ring) finsum_ldistr:
    1.48    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    1.49     finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
    1.50  proof (induct set: finite)
    1.51 @@ -597,7 +597,7 @@
    1.52    case (insert x F) then show ?case by (simp add: Pi_def l_distr)
    1.53  qed
    1.54  
    1.55 -lemma (in cring) finsum_rdistr:
    1.56 +lemma (in ring) finsum_rdistr:
    1.57    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    1.58     a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
    1.59  proof (induct set: finite)