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