src/HOL/Algebra/Module.thy
 author ballarin Thu Jul 31 09:49:21 2008 +0200 (2008-07-31) changeset 27714 27b4d7c01f8b parent 20318 0e0ea63fe768 child 28823 dcbef866c9e2 permissions -rw-r--r--
Tuned (for the sake of a meaningless log entry).
 wenzelm@14706 ` 1` ```(* Title: HOL/Algebra/Module.thy ``` ballarin@13936 ` 2` ``` ID: \$Id\$ ``` ballarin@13936 ` 3` ``` Author: Clemens Ballarin, started 15 April 2003 ``` ballarin@13936 ` 4` ``` Copyright: Clemens Ballarin ``` ballarin@13936 ` 5` ```*) ``` ballarin@13936 ` 6` ballarin@20318 ` 7` ```theory Module imports Ring begin ``` ballarin@20318 ` 8` ballarin@13936 ` 9` ballarin@20318 ` 10` ```section {* Modules over an Abelian Group *} ``` ballarin@20318 ` 11` ballarin@20318 ` 12` ```subsection {* Definitions *} ``` ballarin@13936 ` 13` ballarin@13936 ` 14` ```record ('a, 'b) module = "'b ring" + ``` ballarin@13936 ` 15` ``` smult :: "['a, 'b] => 'b" (infixl "\\" 70) ``` ballarin@13936 ` 16` ballarin@13936 ` 17` ```locale module = cring R + abelian_group M + ``` ballarin@13936 ` 18` ``` assumes smult_closed [simp, intro]: ``` ballarin@15095 ` 19` ``` "[| a \ carrier R; x \ carrier M |] ==> a \\<^bsub>M\<^esub> x \ carrier M" ``` ballarin@13936 ` 20` ``` and smult_l_distr: ``` ballarin@13936 ` 21` ``` "[| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@15095 ` 22` ``` (a \ b) \\<^bsub>M\<^esub> x = a \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> b \\<^bsub>M\<^esub> x" ``` ballarin@13936 ` 23` ``` and smult_r_distr: ``` ballarin@13936 ` 24` ``` "[| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@15095 ` 25` ``` a \\<^bsub>M\<^esub> (x \\<^bsub>M\<^esub> y) = a \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> y" ``` ballarin@13936 ` 26` ``` and smult_assoc1: ``` ballarin@13936 ` 27` ``` "[| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@15095 ` 28` ``` (a \ b) \\<^bsub>M\<^esub> x = a \\<^bsub>M\<^esub> (b \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 29` ``` and smult_one [simp]: ``` ballarin@15095 ` 30` ``` "x \ carrier M ==> \ \\<^bsub>M\<^esub> x = x" ``` ballarin@13936 ` 31` ballarin@13936 ` 32` ```locale algebra = module R M + cring M + ``` ballarin@13936 ` 33` ``` assumes smult_assoc2: ``` ballarin@13936 ` 34` ``` "[| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@15095 ` 35` ``` (a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> y = a \\<^bsub>M\<^esub> (x \\<^bsub>M\<^esub> y)" ``` ballarin@13936 ` 36` ballarin@13936 ` 37` ```lemma moduleI: ``` ballarin@19783 ` 38` ``` fixes R (structure) and M (structure) ``` ballarin@13936 ` 39` ``` assumes cring: "cring R" ``` ballarin@13936 ` 40` ``` and abelian_group: "abelian_group M" ``` ballarin@13936 ` 41` ``` and smult_closed: ``` ballarin@15095 ` 42` ``` "!!a x. [| a \ carrier R; x \ carrier M |] ==> a \\<^bsub>M\<^esub> x \ carrier M" ``` ballarin@13936 ` 43` ``` and smult_l_distr: ``` ballarin@13936 ` 44` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@15095 ` 45` ``` (a \ b) \\<^bsub>M\<^esub> x = (a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> (b \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 46` ``` and smult_r_distr: ``` ballarin@13936 ` 47` ``` "!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@15095 ` 48` ``` a \\<^bsub>M\<^esub> (x \\<^bsub>M\<^esub> y) = (a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> y)" ``` ballarin@13936 ` 49` ``` and smult_assoc1: ``` ballarin@13936 ` 50` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@15095 ` 51` ``` (a \ b) \\<^bsub>M\<^esub> x = a \\<^bsub>M\<^esub> (b \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 52` ``` and smult_one: ``` ballarin@15095 ` 53` ``` "!!x. x \ carrier M ==> \ \\<^bsub>M\<^esub> x = x" ``` ballarin@13936 ` 54` ``` shows "module R M" ``` ballarin@13936 ` 55` ``` by (auto intro: module.intro cring.axioms abelian_group.axioms ``` ballarin@27714 ` 56` ``` module_axioms.intro assms) ``` ballarin@13936 ` 57` ballarin@13936 ` 58` ```lemma algebraI: ``` ballarin@19783 ` 59` ``` fixes R (structure) and M (structure) ``` ballarin@13936 ` 60` ``` assumes R_cring: "cring R" ``` ballarin@13936 ` 61` ``` and M_cring: "cring M" ``` ballarin@13936 ` 62` ``` and smult_closed: ``` ballarin@15095 ` 63` ``` "!!a x. [| a \ carrier R; x \ carrier M |] ==> a \\<^bsub>M\<^esub> x \ carrier M" ``` ballarin@13936 ` 64` ``` and smult_l_distr: ``` ballarin@13936 ` 65` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@15095 ` 66` ``` (a \ b) \\<^bsub>M\<^esub> x = (a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> (b \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 67` ``` and smult_r_distr: ``` ballarin@13936 ` 68` ``` "!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@15095 ` 69` ``` a \\<^bsub>M\<^esub> (x \\<^bsub>M\<^esub> y) = (a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> y)" ``` ballarin@13936 ` 70` ``` and smult_assoc1: ``` ballarin@13936 ` 71` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@15095 ` 72` ``` (a \ b) \\<^bsub>M\<^esub> x = a \\<^bsub>M\<^esub> (b \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 73` ``` and smult_one: ``` ballarin@15095 ` 74` ``` "!!x. x \ carrier M ==> (one R) \\<^bsub>M\<^esub> x = x" ``` ballarin@13936 ` 75` ``` and smult_assoc2: ``` ballarin@13936 ` 76` ``` "!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@15095 ` 77` ``` (a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> y = a \\<^bsub>M\<^esub> (x \\<^bsub>M\<^esub> y)" ``` ballarin@13936 ` 78` ``` shows "algebra R M" ``` ballarin@19984 ` 79` ```apply intro_locales ``` ballarin@27714 ` 80` ```apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+ ``` ballarin@19931 ` 81` ```apply (rule module_axioms.intro) ``` ballarin@19931 ` 82` ``` apply (simp add: smult_closed) ``` ballarin@19931 ` 83` ``` apply (simp add: smult_l_distr) ``` ballarin@19931 ` 84` ``` apply (simp add: smult_r_distr) ``` ballarin@19931 ` 85` ``` apply (simp add: smult_assoc1) ``` ballarin@19931 ` 86` ``` apply (simp add: smult_one) ``` ballarin@27714 ` 87` ```apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+ ``` ballarin@19931 ` 88` ```apply (rule algebra_axioms.intro) ``` ballarin@19931 ` 89` ``` apply (simp add: smult_assoc2) ``` ballarin@19931 ` 90` ```done ``` ballarin@13936 ` 91` ballarin@13936 ` 92` ```lemma (in algebra) R_cring: ``` ballarin@13936 ` 93` ``` "cring R" ``` ballarin@19984 ` 94` ``` by unfold_locales ``` ballarin@13936 ` 95` ballarin@13936 ` 96` ```lemma (in algebra) M_cring: ``` ballarin@13936 ` 97` ``` "cring M" ``` ballarin@19984 ` 98` ``` by unfold_locales ``` ballarin@13936 ` 99` ballarin@13936 ` 100` ```lemma (in algebra) module: ``` ballarin@13936 ` 101` ``` "module R M" ``` ballarin@13936 ` 102` ``` by (auto intro: moduleI R_cring is_abelian_group ``` ballarin@13936 ` 103` ``` smult_l_distr smult_r_distr smult_assoc1) ``` ballarin@13936 ` 104` wenzelm@14651 ` 105` ballarin@13936 ` 106` ```subsection {* Basic Properties of Algebras *} ``` ballarin@13936 ` 107` ballarin@13936 ` 108` ```lemma (in algebra) smult_l_null [simp]: ``` ballarin@15095 ` 109` ``` "x \ carrier M ==> \ \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub>" ``` ballarin@13936 ` 110` ```proof - ``` ballarin@13936 ` 111` ``` assume M: "x \ carrier M" ``` ballarin@20168 ` 112` ``` note facts = M smult_closed [OF R.zero_closed] ``` ballarin@15095 ` 113` ``` from facts have "\ \\<^bsub>M\<^esub> x = (\ \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \ \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (\ \\<^bsub>M\<^esub> x)" by algebra ``` ballarin@15095 ` 114` ``` also from M have "... = (\ \ \) \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (\ \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 115` ``` by (simp add: smult_l_distr del: R.l_zero R.r_zero) ``` ballarin@20168 ` 116` ``` also from facts have "... = \\<^bsub>M\<^esub>" apply algebra apply algebra done ``` ballarin@13936 ` 117` ``` finally show ?thesis . ``` ballarin@13936 ` 118` ```qed ``` ballarin@13936 ` 119` ballarin@13936 ` 120` ```lemma (in algebra) smult_r_null [simp]: ``` ballarin@15095 ` 121` ``` "a \ carrier R ==> a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> = \\<^bsub>M\<^esub>"; ``` ballarin@13936 ` 122` ```proof - ``` ballarin@13936 ` 123` ``` assume R: "a \ carrier R" ``` ballarin@13936 ` 124` ``` note facts = R smult_closed ``` ballarin@15095 ` 125` ``` from facts have "a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> = (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>)" ``` ballarin@13936 ` 126` ``` by algebra ``` ballarin@15095 ` 127` ``` also from R have "... = a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub> \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>)" ``` ballarin@13936 ` 128` ``` by (simp add: smult_r_distr del: M.l_zero M.r_zero) ``` ballarin@15095 ` 129` ``` also from facts have "... = \\<^bsub>M\<^esub>" by algebra ``` ballarin@13936 ` 130` ``` finally show ?thesis . ``` ballarin@13936 ` 131` ```qed ``` ballarin@13936 ` 132` ballarin@13936 ` 133` ```lemma (in algebra) smult_l_minus: ``` ballarin@15095 ` 134` ``` "[| a \ carrier R; x \ carrier M |] ==> (\a) \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 135` ```proof - ``` ballarin@13936 ` 136` ``` assume RM: "a \ carrier R" "x \ carrier M" ``` ballarin@20168 ` 137` ``` from RM have a_smult: "a \\<^bsub>M\<^esub> x \ carrier M" by simp ``` ballarin@20168 ` 138` ``` from RM have ma_smult: "\a \\<^bsub>M\<^esub> x \ carrier M" by simp ``` ballarin@20168 ` 139` ``` note facts = RM a_smult ma_smult ``` ballarin@15095 ` 140` ``` from facts have "(\a) \\<^bsub>M\<^esub> x = (\a \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` ballarin@15095 ` 141` ``` by algebra ``` ballarin@15095 ` 142` ``` also from RM have "... = (\a \ a) \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 143` ``` by (simp add: smult_l_distr) ``` ballarin@20168 ` 144` ``` also from facts smult_l_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` ballarin@20168 ` 145` ``` apply algebra apply algebra done ``` ballarin@13936 ` 146` ``` finally show ?thesis . ``` ballarin@13936 ` 147` ```qed ``` ballarin@13936 ` 148` ballarin@13936 ` 149` ```lemma (in algebra) smult_r_minus: ``` ballarin@15095 ` 150` ``` "[| a \ carrier R; x \ carrier M |] ==> a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>x) = \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 151` ```proof - ``` ballarin@13936 ` 152` ``` assume RM: "a \ carrier R" "x \ carrier M" ``` ballarin@13936 ` 153` ``` note facts = RM smult_closed ``` ballarin@15095 ` 154` ``` from facts have "a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>x) = (a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>x \\<^bsub>M\<^esub> a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 155` ``` by algebra ``` ballarin@15095 ` 156` ``` also from RM have "... = a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>x \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 157` ``` by (simp add: smult_r_distr) ``` ballarin@15095 ` 158` ``` also from facts smult_r_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" by algebra ``` ballarin@13936 ` 159` ``` finally show ?thesis . ``` ballarin@13936 ` 160` ```qed ``` ballarin@13936 ` 161` ballarin@13936 ` 162` ```end ```