src/HOL/Algebra/CRing.thy
changeset 14399 dc677b35e54f
parent 14286 0ae66ffb9784
child 14551 2cb6ff394bfb
     1.1 --- a/src/HOL/Algebra/CRing.thy	Thu Feb 19 15:57:34 2004 +0100
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Thu Feb 19 16:44:21 2004 +0100
     1.3 @@ -276,8 +276,8 @@
     1.4      simplified monoid_record_simps])
     1.5  
     1.6  lemma (in abelian_monoid) finsum_cong:
     1.7 -  "[| A = B;
     1.8 -      f : B -> carrier G = True; !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
     1.9 +  "[| A = B; f : B -> carrier G = True;
    1.10 +      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
    1.11    by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
    1.12      simplified monoid_record_simps]) auto
    1.13  
    1.14 @@ -289,9 +289,13 @@
    1.15  
    1.16  subsection {* Basic Definitions *}
    1.17  
    1.18 -locale cring = abelian_group R + comm_monoid R +
    1.19 +locale ring = abelian_group R + monoid R +
    1.20    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.21        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    1.22 +    and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.23 +      ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
    1.24 +
    1.25 +locale cring = ring + comm_monoid R
    1.26  
    1.27  locale "domain" = cring +
    1.28    assumes one_not_zero [simp]: "\<one> ~= \<zero>"
    1.29 @@ -300,18 +304,54 @@
    1.30  
    1.31  subsection {* Basic Facts of Rings *}
    1.32  
    1.33 +lemma ringI:
    1.34 +  includes struct R
    1.35 +  assumes abelian_group: "abelian_group R"
    1.36 +    and monoid: "monoid R"
    1.37 +    and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.38 +      ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
    1.39 +    and r_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.40 +      ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
    1.41 +  shows "ring R"
    1.42 +  by (auto intro: ring.intro
    1.43 +    abelian_group.axioms monoid.axioms ring_axioms.intro prems)
    1.44 +
    1.45 +lemma (in ring) is_abelian_group:
    1.46 +  "abelian_group R"
    1.47 +  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
    1.48 +
    1.49 +lemma (in ring) is_monoid:
    1.50 +  "monoid R"
    1.51 +  by (auto intro!: monoidI m_assoc)
    1.52 +
    1.53  lemma cringI:
    1.54 +  includes struct R
    1.55    assumes abelian_group: "abelian_group R"
    1.56      and comm_monoid: "comm_monoid R"
    1.57      and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.58        ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
    1.59    shows "cring R"
    1.60 -  by (auto intro: cring.intro
    1.61 -    abelian_group.axioms comm_monoid.axioms cring_axioms.intro prems)
    1.62 -
    1.63 -lemma (in cring) is_abelian_group:
    1.64 -  "abelian_group R"
    1.65 -  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
    1.66 +  proof (rule cring.intro)
    1.67 +    show "ring_axioms R"
    1.68 +    -- {* Right-distributivity follows from left-distributivity and
    1.69 +          commutativity. *}
    1.70 +    proof (rule ring_axioms.intro)
    1.71 +      fix x y z
    1.72 +      assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
    1.73 +      note [simp]= comm_monoid.axioms [OF comm_monoid]
    1.74 +        abelian_group.axioms [OF abelian_group]
    1.75 +        abelian_monoid.a_closed
    1.76 +        magma.m_closed
    1.77 +        
    1.78 +      from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
    1.79 +        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
    1.80 +      also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
    1.81 +      also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
    1.82 +        by (simp add: comm_semigroup.m_comm [OF comm_semigroup.intro])
    1.83 +      finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
    1.84 +    qed
    1.85 +  qed (auto intro: cring.intro
    1.86 +      abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
    1.87  
    1.88  lemma (in cring) is_comm_monoid:
    1.89    "comm_monoid R"
    1.90 @@ -338,22 +378,11 @@
    1.91    with G show ?thesis by (simp add: a_ac)
    1.92  qed
    1.93  
    1.94 -lemma (in cring) r_distr:
    1.95 -  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.96 -  ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
    1.97 -proof -
    1.98 -  assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
    1.99 -  then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
   1.100 -  also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
   1.101 -  also from R have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
   1.102 -  finally show ?thesis .
   1.103 -qed
   1.104 -
   1.105  text {* 
   1.106    The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
   1.107  *}
   1.108  
   1.109 -lemma (in cring) l_null [simp]:
   1.110 +lemma (in ring) l_null [simp]:
   1.111    "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
   1.112  proof -
   1.113    assume R: "x \<in> carrier R"
   1.114 @@ -364,16 +393,18 @@
   1.115    with R show ?thesis by (simp del: r_zero)
   1.116  qed
   1.117  
   1.118 -lemma (in cring) r_null [simp]:
   1.119 +lemma (in ring) r_null [simp]:
   1.120    "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
   1.121  proof -
   1.122    assume R: "x \<in> carrier R"
   1.123 -  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: m_ac)
   1.124 -  also from R have "... = \<zero>" by simp
   1.125 -  finally show ?thesis .
   1.126 +  then have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)"
   1.127 +    by (simp add: r_distr del: l_zero r_zero)
   1.128 +  also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp
   1.129 +  finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" .
   1.130 +  with R show ?thesis by (simp del: r_zero)
   1.131  qed
   1.132  
   1.133 -lemma (in cring) l_minus:
   1.134 +lemma (in ring) l_minus:
   1.135    "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
   1.136  proof -
   1.137    assume R: "x \<in> carrier R" "y \<in> carrier R"
   1.138 @@ -384,20 +415,27 @@
   1.139    with R show ?thesis by (simp add: a_assoc r_neg )
   1.140  qed
   1.141  
   1.142 -lemma (in cring) r_minus:
   1.143 +lemma (in ring) r_minus:
   1.144    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
   1.145  proof -
   1.146    assume R: "x \<in> carrier R" "y \<in> carrier R"
   1.147 -  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: m_ac)
   1.148 -  also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
   1.149 -  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: m_ac)
   1.150 -  finally show ?thesis .
   1.151 +  then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
   1.152 +  also from R have "... = \<zero>" by (simp add: l_neg r_null)
   1.153 +  finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" .
   1.154 +  with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
   1.155 +  with R show ?thesis by (simp add: a_assoc r_neg )
   1.156  qed
   1.157  
   1.158 -lemma (in cring) minus_eq:
   1.159 +lemma (in ring) minus_eq:
   1.160    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
   1.161    by (simp only: minus_def)
   1.162  
   1.163 +lemmas (in ring) ring_simprules =
   1.164 +  a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   1.165 +  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq
   1.166 +  r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   1.167 +  a_lcomm r_distr l_null r_null l_minus r_minus
   1.168 +
   1.169  lemmas (in cring) cring_simprules =
   1.170    a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   1.171    a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
   1.172 @@ -417,7 +455,7 @@
   1.173  text {* Two examples for use of method algebra *}
   1.174  
   1.175  lemma
   1.176 -  includes cring R + cring S
   1.177 +  includes ring R + cring S
   1.178    shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
   1.179    a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
   1.180    by algebra