src/HOL/Algebra/Module.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 61565 352c73a689da child 68552 391e89e03eef permissions -rw-r--r--
More on Algebra by Paulo and Martin
 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` wenzelm@35849 ` 6` ```theory Module ``` wenzelm@35849 ` 7` ```imports Ring ``` wenzelm@35849 ` 8` ```begin ``` ballarin@13936 ` 9` wenzelm@61382 ` 10` ```section \Modules over an Abelian Group\ ``` ballarin@20318 ` 11` wenzelm@61382 ` 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@61565 ` 17` ```locale module = R?: cring + M?: abelian_group M for M (structure) + ``` 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@29237 ` 32` ```locale algebra = module + 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" ``` lp15@68551 ` 79` ``` apply intro_locales ``` lp15@68551 ` 80` ``` apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+ ``` lp15@68551 ` 81` ``` apply (rule module_axioms.intro) ``` lp15@68551 ` 82` ``` apply (simp add: smult_closed) ``` lp15@68551 ` 83` ``` apply (simp add: smult_l_distr) ``` lp15@68551 ` 84` ``` apply (simp add: smult_r_distr) ``` lp15@68551 ` 85` ``` apply (simp add: smult_assoc1) ``` lp15@68551 ` 86` ``` apply (simp add: smult_one) ``` lp15@68551 ` 87` ``` apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+ ``` lp15@68551 ` 88` ``` apply (rule algebra_axioms.intro) ``` lp15@68551 ` 89` ``` apply (simp add: smult_assoc2) ``` lp15@68551 ` 90` ``` done ``` ballarin@13936 ` 91` lp15@68551 ` 92` ```lemma (in algebra) R_cring: "cring R" .. ``` ballarin@13936 ` 93` lp15@68551 ` 94` ```lemma (in algebra) M_cring: "cring M" .. ``` ballarin@13936 ` 95` lp15@68551 ` 96` ```lemma (in algebra) module: "module R M" ``` lp15@68551 ` 97` ``` by (auto intro: moduleI R_cring is_abelian_group smult_l_distr smult_r_distr smult_assoc1) ``` ballarin@13936 ` 98` wenzelm@14651 ` 99` lp15@68551 ` 100` ```subsection \Basic Properties of Modules\ ``` ballarin@13936 ` 101` lp15@68551 ` 102` ```lemma (in module) smult_l_null [simp]: ``` lp15@68551 ` 103` ``` "x \ carrier M ==> \ \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub>" ``` lp15@68551 ` 104` ```proof- ``` lp15@68551 ` 105` ``` assume M : "x \ carrier M" ``` ballarin@20168 ` 106` ``` note facts = M smult_closed [OF R.zero_closed] ``` lp15@68551 ` 107` ``` from facts have "\ \\<^bsub>M\<^esub> x = (\ \ \) \\<^bsub>M\<^esub> x " ``` lp15@68551 ` 108` ``` using smult_l_distr by auto ``` lp15@68551 ` 109` ``` also have "... = \ \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \ \\<^bsub>M\<^esub> x" ``` lp15@68551 ` 110` ``` using smult_l_distr[of \ \ x] facts by auto ``` lp15@68551 ` 111` ``` finally show "\ \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub>" using facts ``` lp15@68551 ` 112` ``` by (metis M.add.r_cancel_one') ``` ballarin@13936 ` 113` ```qed ``` ballarin@13936 ` 114` lp15@68551 ` 115` ```lemma (in module) smult_r_null [simp]: ``` wenzelm@58860 ` 116` ``` "a \ carrier R ==> a \\<^bsub>M\<^esub> \\<^bsub>M\<^esub> = \\<^bsub>M\<^esub>" ``` ballarin@13936 ` 117` ```proof - ``` ballarin@13936 ` 118` ``` assume R: "a \ carrier R" ``` ballarin@13936 ` 119` ``` note facts = R smult_closed ``` ballarin@15095 ` 120` ``` 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>)" ``` lp15@68551 ` 121` ``` by (simp add: M.add.inv_solve_right) ``` ballarin@15095 ` 122` ``` 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 ` 123` ``` by (simp add: smult_r_distr del: M.l_zero M.r_zero) ``` lp15@68551 ` 124` ``` also from facts have "... = \\<^bsub>M\<^esub>" ``` lp15@68551 ` 125` ``` by (simp add: M.r_neg) ``` ballarin@13936 ` 126` ``` finally show ?thesis . ``` ballarin@13936 ` 127` ```qed ``` ballarin@13936 ` 128` lp15@68551 ` 129` ```lemma (in module) smult_l_minus: ``` lp15@68551 ` 130` ```"\ a \ carrier R; x \ carrier M \ \ (\a) \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> x)" ``` lp15@68551 ` 131` ```proof- ``` ballarin@13936 ` 132` ``` assume RM: "a \ carrier R" "x \ carrier M" ``` ballarin@20168 ` 133` ``` from RM have a_smult: "a \\<^bsub>M\<^esub> x \ carrier M" by simp ``` ballarin@20168 ` 134` ``` from RM have ma_smult: "\a \\<^bsub>M\<^esub> x \ carrier M" by simp ``` ballarin@20168 ` 135` ``` note facts = RM a_smult ma_smult ``` ballarin@15095 ` 136` ``` 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)" ``` lp15@68551 ` 137` ``` by (simp add: M.add.inv_solve_right) ``` ballarin@15095 ` 138` ``` also from RM have "... = (\a \ a) \\<^bsub>M\<^esub> x \\<^bsub>M\<^esub> \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 139` ``` by (simp add: smult_l_distr) ``` ballarin@20168 ` 140` ``` also from facts smult_l_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` lp15@68551 ` 141` ``` by (simp add: R.l_neg) ``` ballarin@13936 ` 142` ``` finally show ?thesis . ``` ballarin@13936 ` 143` ```qed ``` ballarin@13936 ` 144` lp15@68551 ` 145` ```lemma (in module) smult_r_minus: ``` ballarin@15095 ` 146` ``` "[| a \ carrier R; x \ carrier M |] ==> a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>x) = \\<^bsub>M\<^esub> (a \\<^bsub>M\<^esub> x)" ``` ballarin@13936 ` 147` ```proof - ``` ballarin@13936 ` 148` ``` assume RM: "a \ carrier R" "x \ carrier M" ``` ballarin@13936 ` 149` ``` note facts = RM smult_closed ``` ballarin@15095 ` 150` ``` 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)" ``` lp15@68551 ` 151` ``` by (simp add: M.add.inv_solve_right) ``` ballarin@15095 ` 152` ``` 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 ` 153` ``` by (simp add: smult_r_distr) ``` lp15@68551 ` 154` ``` also from facts smult_l_null have "... = \\<^bsub>M\<^esub>(a \\<^bsub>M\<^esub> x)" ``` lp15@68551 ` 155` ``` by (metis M.add.inv_closed M.add.inv_solve_right M.l_neg R.zero_closed r_null smult_assoc1) ``` ballarin@13936 ` 156` ``` finally show ?thesis . ``` ballarin@13936 ` 157` ```qed ``` ballarin@13936 ` 158` lp15@68551 ` 159` ```lemma (in module) finsum_smult_ldistr: ``` lp15@68551 ` 160` ``` "\ finite A; a \ carrier R; f: A \ carrier M \ \ ``` lp15@68551 ` 161` ``` a \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub> i \ A. (f i)) = (\\<^bsub>M\<^esub> i \ A. ( a \\<^bsub>M\<^esub> (f i)))" ``` lp15@68551 ` 162` ```proof (induct set: finite) ``` lp15@68551 ` 163` ``` case empty then show ?case ``` lp15@68551 ` 164` ``` by (metis M.finsum_empty M.zero_closed R.zero_closed r_null smult_assoc1 smult_l_null) ``` lp15@68551 ` 165` ```next ``` lp15@68551 ` 166` ``` case (insert x F) then show ?case ``` lp15@68551 ` 167` ``` by (simp add: Pi_def smult_r_distr) ``` lp15@68551 ` 168` ```qed ``` lp15@68551 ` 169` ballarin@13936 ` 170` ```end ```