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
```