src/HOL/Algebra/Ring.thy

     and "\<And>x. x \<in> carrier R \<Longrightarrow> \<exists>y \<in> carrier R. y \<oplus> x = \<zero>"
   using abelian_group.a_comm_group assms comm_groupE by fastforce+
 
 lemma (in abelian_monoid) a_monoid:
   "monoid (add_monoid G)"
-by (rule comm_monoid.axioms, rule a_comm_monoid) 
+by (rule comm_monoid.axioms, rule a_comm_monoid)
 
 lemma (in abelian_group) a_group:
   "group (add_monoid G)"
   by (simp add: group_def a_monoid)
     (simp add: comm_group.axioms group.axioms a_comm_group)

   by (rule a_monoid) (auto simp add: add_pow_def)
 
 context abelian_monoid
 begin
 
-lemmas a_closed = add.m_closed 
+lemmas a_closed = add.m_closed
 lemmas zero_closed = add.one_closed
 lemmas a_assoc = add.m_assoc
 lemmas l_zero = add.l_one
 lemmas r_zero = add.r_one
 lemmas minus_unique = add.inv_unique

 lemmas finsum_addf = add.finprod_multf
 lemmas finsum_cong' = add.finprod_cong'
 lemmas finsum_0 = add.finprod_0
 lemmas finsum_Suc = add.finprod_Suc
 lemmas finsum_Suc2 = add.finprod_Suc2
-lemmas finsum_add = add.finprod_mult
 lemmas finsum_infinite = add.finprod_infinite
 
 lemmas finsum_cong = add.finprod_cong
 text \<open>Usually, if this rule causes a failed congruence proof error,
    the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown.

        and "finprod (add_monoid G) = finsum G"
        and "pow     (add_monoid G) = (\<lambda>a k. add_pow G k a)"
   by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def add_pow_def)
 
 lemmas (in abelian_group) minus_add = add.inv_mult
- 
+
 text \<open>Derive an \<open>abelian_group\<close> from a \<open>comm_group\<close>\<close>
 
 lemma comm_group_abelian_groupI:
   fixes G (structure)
   assumes cg: "comm_group (add_monoid G)"

     fix x y z
     assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
     note [simp] = comm_monoid.axioms [OF comm_monoid]
       abelian_group.axioms [OF abelian_group]
       abelian_monoid.a_closed
-        
+
     from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
       by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
     also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
     also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
       by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])

 
 lemma (in abelian_group) r_neg1:
   "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> (x \<oplus> y) = y"
 proof -
   assume G: "x \<in> carrier G" "y \<in> carrier G"
-  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 
+  then have "(\<ominus> x \<oplus> x) \<oplus> y = y"
     by (simp only: l_neg l_zero)
   with G show ?thesis by (simp add: a_ac)
 qed
 
 lemma (in abelian_group) r_neg2:

 
 lemmas (in semiring) semiring_simprules
   [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
   a_closed zero_closed  m_closed one_closed
   a_assoc l_zero  a_comm m_assoc l_one l_distr r_zero
-  a_lcomm r_distr l_null r_null 
+  a_lcomm r_distr l_null r_null
 
 lemmas (in ring) ring_simprules
   [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq

 
 lemma add_pow_int_ge: "(k :: int) \<ge> 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = [ nat k ] \<cdot>\<^bsub>R\<^esub> a"
   by (simp add: add_pow_def int_pow_def nat_pow_def)
 
 lemma add_pow_int_lt: "(k :: int) < 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = \<ominus>\<^bsub>R\<^esub> ([ nat (- k) ] \<cdot>\<^bsub>R\<^esub> a)"
-  by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def) 
+  by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def)
 
 corollary (in semiring) add_pow_ldistr:
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "([(k :: nat)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"
 proof -

   also have " ... = (\<Oplus> i \<in> {..< k}. (a \<otimes> b))"
     using finsum_rdistr[of "{..<k}" a "\<lambda>x. b"] assms by simp
   also have " ... = [k] \<cdot> (a \<otimes> b)"
     using add.finprod_const[of "a \<otimes> b" "{..<k}"] assms by simp
   finally show ?thesis .
-qed 
+qed
 
 (* For integers, we need the uniqueness of the additive inverse *)
 lemma (in ring) add_pow_ldistr_int:
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "([(k :: int)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)"

   case True thus ?thesis
     using add_pow_int_ge[of k R] add_pow_ldistr[OF assms] by auto
 next
   case False thus ?thesis
     using add_pow_int_lt[of k R a] add_pow_int_lt[of k R "a \<otimes> b"]
-          add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto 
+          add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto
 qed
 
 lemma (in ring) add_pow_rdistr_int:
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "a \<otimes> ([(k :: int)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)"

   case True thus ?thesis
     using add_pow_int_ge[of k R] add_pow_rdistr[OF assms] by auto
 next
   case False thus ?thesis
     using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a \<otimes> b"]
-          add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto 
+          add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto
 qed
 
 
 subsection \<open>Integral Domains\<close>
 

   shows "(a \<otimes> b = a \<otimes> c) = (b = c)"
 proof
   assume eq: "a \<otimes> b = a \<otimes> c"
   with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
   with R have "a = \<zero> \<or> (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
-  with prem and R have "b \<ominus> c = \<zero>" by auto 
+  with prem and R have "b \<ominus> c = \<zero>" by auto
   with R have "b = b \<ominus> (b \<ominus> c)" by algebra
   also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
   finally show "b = c" .
 next
   assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp