src/HOL/Algebra/Module.thy

       "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"
     and smult_assoc2:
       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
   shows "algebra R M"
-apply intro_locales
-apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
-apply (rule module_axioms.intro)
- apply (simp add: smult_closed)
- apply (simp add: smult_l_distr)
- apply (simp add: smult_r_distr)
- apply (simp add: smult_assoc1)
- apply (simp add: smult_one)
-apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
-apply (rule algebra_axioms.intro)
- apply (simp add: smult_assoc2)
-done
+  apply intro_locales
+             apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
+      apply (rule module_axioms.intro)
+          apply (simp add: smult_closed)
+         apply (simp add: smult_l_distr)
+        apply (simp add: smult_r_distr)
+       apply (simp add: smult_assoc1)
+      apply (simp add: smult_one)
+     apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
+  apply (rule algebra_axioms.intro)
+  apply (simp add: smult_assoc2)
+  done
 
-lemma (in algebra) R_cring:
-  "cring R"
-  ..
+lemma (in algebra) R_cring: "cring R" ..
 
-lemma (in algebra) M_cring:
-  "cring M"
-  ..
+lemma (in algebra) M_cring: "cring M" ..
 
-lemma (in algebra) module:
-  "module R M"
-  by (auto intro: moduleI R_cring is_abelian_group
-    smult_l_distr smult_r_distr smult_assoc1)
+lemma (in algebra) module: "module R M"
+  by (auto intro: moduleI R_cring is_abelian_group smult_l_distr smult_r_distr smult_assoc1)
 
 
-subsection \<open>Basic Properties of Algebras\<close>
+subsection \<open>Basic Properties of Modules\<close>
 
-lemma (in algebra) smult_l_null [simp]:
-  "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
-proof -
-  assume M: "x \<in> carrier M"
+lemma (in module) smult_l_null [simp]:
+ "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
+proof-
+  assume M : "x \<in> carrier M"
   note facts = M smult_closed [OF R.zero_closed]
-  from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)" by algebra
-  also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)"
-    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
-  also from facts have "... = \<zero>\<^bsub>M\<^esub>" apply algebra apply algebra done
-  finally show ?thesis .
+  from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x "
+    using smult_l_distr by auto
+  also have "... = \<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x"
+    using smult_l_distr[of \<zero> \<zero> x] facts by auto
+  finally show "\<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>" using facts
+    by (metis M.add.r_cancel_one')
 qed
 
-lemma (in algebra) smult_r_null [simp]:
+lemma (in module) smult_r_null [simp]:
   "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"
 proof -
   assume R: "a \<in> carrier R"
   note facts = R smult_closed
   from facts have "a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
-    by algebra
+    by (simp add: M.add.inv_solve_right)
   also from R have "... = a \<odot>\<^bsub>M\<^esub> (\<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
     by (simp add: smult_r_distr del: M.l_zero M.r_zero)
-  also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
+  also from facts have "... = \<zero>\<^bsub>M\<^esub>"
+    by (simp add: M.r_neg)
   finally show ?thesis .
 qed
 
-lemma (in algebra) smult_l_minus:
-  "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
-proof -
+lemma (in module) smult_l_minus:
+"\<lbrakk> a \<in> carrier R; x \<in> carrier M \<rbrakk> \<Longrightarrow> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
+proof-
   assume RM: "a \<in> carrier R" "x \<in> carrier M"
   from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
   from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
   note facts = RM a_smult ma_smult
   from facts have "(\<ominus>a) \<odot>\<^bsub>M\<^esub> x = (\<ominus>a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
-    by algebra
+    by (simp add: M.add.inv_solve_right)
   also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
     by (simp add: smult_l_distr)
   also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
-    apply algebra apply algebra done
+    by (simp add: R.l_neg)
   finally show ?thesis .
 qed
 
-lemma (in algebra) smult_r_minus:
+lemma (in module) smult_r_minus:
   "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
 proof -
   assume RM: "a \<in> carrier R" "x \<in> carrier M"
   note facts = RM smult_closed
   from facts have "a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = (a \<odot>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
-    by algebra
+    by (simp add: M.add.inv_solve_right)
   also from RM have "... = a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
     by (simp add: smult_r_distr)
-  also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
+  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
+    by (metis M.add.inv_closed M.add.inv_solve_right M.l_neg R.zero_closed r_null smult_assoc1)
   finally show ?thesis .
 qed
 
+lemma (in module) finsum_smult_ldistr:
+  "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier M \<rbrakk> \<Longrightarrow>
+     a \<odot>\<^bsub>M\<^esub> (\<Oplus>\<^bsub>M\<^esub> i \<in> A. (f i)) = (\<Oplus>\<^bsub>M\<^esub> i \<in> A. ( a \<odot>\<^bsub>M\<^esub> (f i)))"
+proof (induct set: finite)
+  case empty then show ?case
+    by (metis M.finsum_empty M.zero_closed R.zero_closed r_null smult_assoc1 smult_l_null)
+next
+  case (insert x F) then show ?case
+    by (simp add: Pi_def smult_r_distr)
+qed
+
 end