--- a/src/HOL/Algebra/Module.thy Wed Jul 04 22:44:24 2018 +0200
+++ b/src/HOL/Algebra/Module.thy Thu Jul 05 18:27:24 2018 +0100
@@ -167,4 +167,85 @@
by (simp add: Pi_def smult_r_distr)
qed
+
+
+subsection \<open>Submodules\<close>
+
+locale submodule = subgroup H "add_monoid M" for H and R :: "('a, 'b) ring_scheme" and M (structure)
++ assumes smult_closed [simp, intro]:
+ "\<lbrakk>a \<in> carrier R; x \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> x \<in> H"
+
+
+lemma (in module) submoduleI :
+ assumes subset: "H \<subseteq> carrier M"
+ and zero: "\<zero>\<^bsub>M\<^esub> \<in> H"
+ and a_inv: "!!a. a \<in> H \<Longrightarrow> \<ominus>\<^bsub>M\<^esub> a \<in> H"
+ and add : "\<And> a b. \<lbrakk>a \<in> H ; b \<in> H\<rbrakk> \<Longrightarrow> a \<oplus>\<^bsub>M\<^esub> b \<in> H"
+ and smult_closed : "\<And> a x. \<lbrakk>a \<in> carrier R; x \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> x \<in> H"
+ shows "submodule H R M"
+ apply (intro submodule.intro subgroup.intro)
+ using assms unfolding submodule_axioms_def
+ by (simp_all add : a_inv_def)
+
+
+lemma (in module) submoduleE :
+ assumes "submodule H R M"
+ shows "H \<subseteq> carrier M"
+ and "H \<noteq> {}"
+ and "\<And>a. a \<in> H \<Longrightarrow> \<ominus>\<^bsub>M\<^esub> a \<in> H"
+ and "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> H\<rbrakk> \<Longrightarrow> a \<odot>\<^bsub>M\<^esub> b \<in> H"
+ and "\<And> a b. \<lbrakk>a \<in> H ; b \<in> H\<rbrakk> \<Longrightarrow> a \<oplus>\<^bsub>M\<^esub> b \<in> H"
+ and "\<And> x. x \<in> H \<Longrightarrow> (a_inv M x) \<in> H"
+ using group.subgroupE[of "add_monoid M" H, OF _ submodule.axioms(1)[OF assms]] a_comm_group
+ submodule.smult_closed[OF assms]
+ unfolding comm_group_def a_inv_def
+ by auto
+
+
+lemma (in module) carrier_is_submodule :
+"submodule (carrier M) R M"
+ apply (intro submoduleI)
+ using a_comm_group group.inv_closed unfolding comm_group_def a_inv_def group_def monoid_def
+ by auto
+
+lemma (in submodule) submodule_is_module :
+ assumes "module R M"
+ shows "module R (M\<lparr>carrier := H\<rparr>)"
+proof (auto intro! : moduleI abelian_group.intro)
+ show "cring (R)" using assms unfolding module_def by auto
+ show "abelian_monoid (M\<lparr>carrier := H\<rparr>)"
+ using comm_monoid.submonoid_is_comm_monoid[OF _ subgroup_is_submonoid] assms
+ unfolding abelian_monoid_def module_def abelian_group_def
+ by auto
+ thus "abelian_group_axioms (M\<lparr>carrier := H\<rparr>)"
+ using subgroup_is_group assms
+ unfolding abelian_group_axioms_def comm_group_def abelian_monoid_def module_def abelian_group_def
+ by auto
+ show "\<And>z. z \<in> H \<Longrightarrow> \<one>\<^bsub>R\<^esub> \<odot> z = z"
+ using subgroup_imp_subset[OF subgroup_axioms] module.smult_one[OF assms]
+ by auto
+ fix a b x y assume a : "a \<in> carrier R" and b : "b \<in> carrier R" and x : "x \<in> H" and y : "y \<in> H"
+ show "(a \<oplus>\<^bsub>R\<^esub> b) \<odot> x = a \<odot> x \<oplus> b \<odot> x"
+ using a b x module.smult_l_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+ by auto
+ show "a \<odot> (x \<oplus> y) = a \<odot> x \<oplus> a \<odot> y"
+ using a x y module.smult_r_distr[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+ by auto
+ show "a \<otimes>\<^bsub>R\<^esub> b \<odot> x = a \<odot> (b \<odot> x)"
+ using a b x module.smult_assoc1[OF assms] subgroup_imp_subset[OF subgroup_axioms]
+ by auto
+qed
+
+
+lemma (in module) module_incl_imp_submodule :
+ assumes "H \<subseteq> carrier M"
+ and "module R (M\<lparr>carrier := H\<rparr>)"
+ shows "submodule H R M"
+ apply (intro submodule.intro)
+ using add.group_incl_imp_subgroup[OF assms(1)] assms module.axioms(2)[OF assms(2)]
+ module.smult_closed[OF assms(2)]
+ unfolding abelian_group_def abelian_group_axioms_def comm_group_def submodule_axioms_def
+ by simp_all
+
+
end