src/HOL/Algebra/Module.thy
 author ballarin Wed Apr 30 10:01:35 2003 +0200 (2003-04-30) changeset 13936 d3671b878828 child 13940 c67798653056 permissions -rw-r--r--
 ballarin@13936 ` 1` ```(* Title: HOL/Algebra/Module ``` 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@13936 ` 7` ```theory Module = CRing: ``` ballarin@13936 ` 8` ballarin@13936 ` 9` ```section {* Modules over an Abelian Group *} ``` ballarin@13936 ` 10` ballarin@13936 ` 11` ```record ('a, 'b) module = "'b ring" + ``` ballarin@13936 ` 12` ``` smult :: "['a, 'b] => 'b" (infixl "\\" 70) ``` ballarin@13936 ` 13` ballarin@13936 ` 14` ```locale module = cring R + abelian_group M + ``` ballarin@13936 ` 15` ``` assumes smult_closed [simp, intro]: ``` ballarin@13936 ` 16` ``` "[| a \ carrier R; x \ carrier M |] ==> a \\<^sub>2 x \ carrier M" ``` ballarin@13936 ` 17` ``` and smult_l_distr: ``` ballarin@13936 ` 18` ``` "[| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@13936 ` 19` ``` (a \ b) \\<^sub>2 x = a \\<^sub>2 x \\<^sub>2 b \\<^sub>2 x" ``` ballarin@13936 ` 20` ``` and smult_r_distr: ``` ballarin@13936 ` 21` ``` "[| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@13936 ` 22` ``` a \\<^sub>2 (x \\<^sub>2 y) = a \\<^sub>2 x \\<^sub>2 a \\<^sub>2 y" ``` ballarin@13936 ` 23` ``` and smult_assoc1: ``` ballarin@13936 ` 24` ``` "[| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@13936 ` 25` ``` (a \ b) \\<^sub>2 x = a \\<^sub>2 (b \\<^sub>2 x)" ``` ballarin@13936 ` 26` ``` and smult_one [simp]: ``` ballarin@13936 ` 27` ``` "x \ carrier M ==> \ \\<^sub>2 x = x" ``` ballarin@13936 ` 28` ballarin@13936 ` 29` ```locale algebra = module R M + cring M + ``` ballarin@13936 ` 30` ``` assumes smult_assoc2: ``` ballarin@13936 ` 31` ``` "[| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@13936 ` 32` ``` (a \\<^sub>2 x) \\<^sub>2 y = a \\<^sub>2 (x \\<^sub>2 y)" ``` ballarin@13936 ` 33` ballarin@13936 ` 34` ```lemma moduleI: ``` ballarin@13936 ` 35` ``` assumes cring: "cring R" ``` ballarin@13936 ` 36` ``` and abelian_group: "abelian_group M" ``` ballarin@13936 ` 37` ``` and smult_closed: ``` ballarin@13936 ` 38` ``` "!!a x. [| a \ carrier R; x \ carrier M |] ==> smult M a x \ carrier M" ``` ballarin@13936 ` 39` ``` and smult_l_distr: ``` ballarin@13936 ` 40` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@13936 ` 41` ``` smult M (add R a b) x = add M (smult M a x) (smult M b x)" ``` ballarin@13936 ` 42` ``` and smult_r_distr: ``` ballarin@13936 ` 43` ``` "!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@13936 ` 44` ``` smult M a (add M x y) = add M (smult M a x) (smult M a y)" ``` ballarin@13936 ` 45` ``` and smult_assoc1: ``` ballarin@13936 ` 46` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@13936 ` 47` ``` smult M (mult R a b) x = smult M a (smult M b x)" ``` ballarin@13936 ` 48` ``` and smult_one: ``` ballarin@13936 ` 49` ``` "!!x. x \ carrier M ==> smult M (one R) x = x" ``` ballarin@13936 ` 50` ``` shows "module R M" ``` ballarin@13936 ` 51` ``` by (auto intro: module.intro cring.axioms abelian_group.axioms ``` ballarin@13936 ` 52` ``` module_axioms.intro prems) ``` ballarin@13936 ` 53` ballarin@13936 ` 54` ```lemma algebraI: ``` ballarin@13936 ` 55` ``` assumes R_cring: "cring R" ``` ballarin@13936 ` 56` ``` and M_cring: "cring M" ``` ballarin@13936 ` 57` ``` and smult_closed: ``` ballarin@13936 ` 58` ``` "!!a x. [| a \ carrier R; x \ carrier M |] ==> smult M a x \ carrier M" ``` ballarin@13936 ` 59` ``` and smult_l_distr: ``` ballarin@13936 ` 60` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@13936 ` 61` ``` smult M (add R a b) x = add M (smult M a x) (smult M b x)" ``` ballarin@13936 ` 62` ``` and smult_r_distr: ``` ballarin@13936 ` 63` ``` "!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@13936 ` 64` ``` smult M a (add M x y) = add M (smult M a x) (smult M a y)" ``` ballarin@13936 ` 65` ``` and smult_assoc1: ``` ballarin@13936 ` 66` ``` "!!a b x. [| a \ carrier R; b \ carrier R; x \ carrier M |] ==> ``` ballarin@13936 ` 67` ``` smult M (mult R a b) x = smult M a (smult M b x)" ``` ballarin@13936 ` 68` ``` and smult_one: ``` ballarin@13936 ` 69` ``` "!!x. x \ carrier M ==> smult M (one R) x = x" ``` ballarin@13936 ` 70` ``` and smult_assoc2: ``` ballarin@13936 ` 71` ``` "!!a x y. [| a \ carrier R; x \ carrier M; y \ carrier M |] ==> ``` ballarin@13936 ` 72` ``` mult M (smult M a x) y = smult M a (mult M x y)" ``` ballarin@13936 ` 73` ``` shows "algebra R M" ``` ballarin@13936 ` 74` ``` by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms ``` ballarin@13936 ` 75` ``` module_axioms.intro prems) ``` ballarin@13936 ` 76` ballarin@13936 ` 77` ```lemma (in algebra) R_cring: ``` ballarin@13936 ` 78` ``` "cring R" ``` ballarin@13936 ` 79` ``` by (rule cring.intro) assumption+ ``` ballarin@13936 ` 80` ballarin@13936 ` 81` ```lemma (in algebra) M_cring: ``` ballarin@13936 ` 82` ``` "cring M" ``` ballarin@13936 ` 83` ``` by (rule cring.intro) assumption+ ``` ballarin@13936 ` 84` ballarin@13936 ` 85` ```lemma (in algebra) module: ``` ballarin@13936 ` 86` ``` "module R M" ``` ballarin@13936 ` 87` ``` by (auto intro: moduleI R_cring is_abelian_group ``` ballarin@13936 ` 88` ``` smult_l_distr smult_r_distr smult_assoc1) ``` ballarin@13936 ` 89` ballarin@13936 ` 90` ```subsection {* Basic Properties of Algebras *} ``` ballarin@13936 ` 91` ballarin@13936 ` 92` ```lemma (in algebra) smult_l_null [simp]: ``` ballarin@13936 ` 93` ``` "x \ carrier M ==> \ \\<^sub>2 x = \\<^sub>2" ``` ballarin@13936 ` 94` ```proof - ``` ballarin@13936 ` 95` ``` assume M: "x \ carrier M" ``` ballarin@13936 ` 96` ``` note facts = M smult_closed ``` ballarin@13936 ` 97` ``` from facts have "\ \\<^sub>2 x = (\ \\<^sub>2 x \\<^sub>2 \ \\<^sub>2 x) \\<^sub>2 \\<^sub>2 (\ \\<^sub>2 x)" by algebra ``` ballarin@13936 ` 98` ``` also from M have "... = (\ \ \) \\<^sub>2 x \\<^sub>2 \\<^sub>2 (\ \\<^sub>2 x)" ``` ballarin@13936 ` 99` ``` by (simp add: smult_l_distr del: R.l_zero R.r_zero) ``` ballarin@13936 ` 100` ``` also from facts have "... = \\<^sub>2" by algebra ``` ballarin@13936 ` 101` ``` finally show ?thesis . ``` ballarin@13936 ` 102` ```qed ``` ballarin@13936 ` 103` ballarin@13936 ` 104` ```lemma (in algebra) smult_r_null [simp]: ``` ballarin@13936 ` 105` ``` "a \ carrier R ==> a \\<^sub>2 \\<^sub>2 = \\<^sub>2"; ``` ballarin@13936 ` 106` ```proof - ``` ballarin@13936 ` 107` ``` assume R: "a \ carrier R" ``` ballarin@13936 ` 108` ``` note facts = R smult_closed ``` ballarin@13936 ` 109` ``` from facts have "a \\<^sub>2 \\<^sub>2 = (a \\<^sub>2 \\<^sub>2 \\<^sub>2 a \\<^sub>2 \\<^sub>2) \\<^sub>2 \\<^sub>2 (a \\<^sub>2 \\<^sub>2)" ``` ballarin@13936 ` 110` ``` by algebra ``` ballarin@13936 ` 111` ``` also from R have "... = a \\<^sub>2 (\\<^sub>2 \\<^sub>2 \\<^sub>2) \\<^sub>2 \\<^sub>2 (a \\<^sub>2 \\<^sub>2)" ``` ballarin@13936 ` 112` ``` by (simp add: smult_r_distr del: M.l_zero M.r_zero) ``` ballarin@13936 ` 113` ``` also from facts have "... = \\<^sub>2" by algebra ``` ballarin@13936 ` 114` ``` finally show ?thesis . ``` ballarin@13936 ` 115` ```qed ``` ballarin@13936 ` 116` ballarin@13936 ` 117` ```lemma (in algebra) smult_l_minus: ``` ballarin@13936 ` 118` ``` "[| a \ carrier R; x \ carrier M |] ==> (\a) \\<^sub>2 x = \\<^sub>2 (a \\<^sub>2 x)" ``` ballarin@13936 ` 119` ```proof - ``` ballarin@13936 ` 120` ``` assume RM: "a \ carrier R" "x \ carrier M" ``` ballarin@13936 ` 121` ``` note facts = RM smult_closed ``` ballarin@13936 ` 122` ``` from facts have "(\a) \\<^sub>2 x = (\a \\<^sub>2 x \\<^sub>2 a \\<^sub>2 x) \\<^sub>2 \\<^sub>2(a \\<^sub>2 x)" by algebra ``` ballarin@13936 ` 123` ``` also from RM have "... = (\a \ a) \\<^sub>2 x \\<^sub>2 \\<^sub>2(a \\<^sub>2 x)" ``` ballarin@13936 ` 124` ``` by (simp add: smult_l_distr) ``` ballarin@13936 ` 125` ``` also from facts smult_l_null have "... = \\<^sub>2(a \\<^sub>2 x)" by algebra ``` ballarin@13936 ` 126` ``` finally show ?thesis . ``` ballarin@13936 ` 127` ```qed ``` ballarin@13936 ` 128` ballarin@13936 ` 129` ```lemma (in algebra) smult_r_minus: ``` ballarin@13936 ` 130` ``` "[| a \ carrier R; x \ carrier M |] ==> a \\<^sub>2 (\\<^sub>2x) = \\<^sub>2 (a \\<^sub>2 x)" ``` ballarin@13936 ` 131` ```proof - ``` ballarin@13936 ` 132` ``` assume RM: "a \ carrier R" "x \ carrier M" ``` ballarin@13936 ` 133` ``` note facts = RM smult_closed ``` ballarin@13936 ` 134` ``` from facts have "a \\<^sub>2 (\\<^sub>2x) = (a \\<^sub>2 \\<^sub>2x \\<^sub>2 a \\<^sub>2 x) \\<^sub>2 \\<^sub>2(a \\<^sub>2 x)" ``` ballarin@13936 ` 135` ``` by algebra ``` ballarin@13936 ` 136` ``` also from RM have "... = a \\<^sub>2 (\\<^sub>2x \\<^sub>2 x) \\<^sub>2 \\<^sub>2(a \\<^sub>2 x)" ``` ballarin@13936 ` 137` ``` by (simp add: smult_r_distr) ``` ballarin@13936 ` 138` ``` also from facts smult_r_null have "... = \\<^sub>2(a \\<^sub>2 x)" by algebra ``` ballarin@13936 ` 139` ``` finally show ?thesis . ``` ballarin@13936 ` 140` ```qed ``` ballarin@13936 ` 141` ballarin@13936 ` 142` ```subsection {* Every Abelian Group is a \$\mathbb{Z}\$-module *} ``` ballarin@13936 ` 143` ballarin@13936 ` 144` ```text {* Not finished. *} ``` ballarin@13936 ` 145` ballarin@13936 ` 146` ```constdefs ``` ballarin@13936 ` 147` ``` INTEG :: "int ring" ``` ballarin@13936 ` 148` ``` "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)" ``` ballarin@13936 ` 149` ballarin@13936 ` 150` ```(* ``` ballarin@13936 ` 151` ``` INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module" ``` ballarin@13936 ` 152` ``` "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R, ``` ballarin@13936 ` 153` ``` zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)" ``` ballarin@13936 ` 154` ```*) ``` ballarin@13936 ` 155` ballarin@13936 ` 156` ```lemma cring_INTEG: ``` ballarin@13936 ` 157` ``` "cring INTEG" ``` ballarin@13936 ` 158` ``` by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI ``` ballarin@13936 ` 159` ``` zadd_zminus_inverse2 zadd_zmult_distrib) ``` ballarin@13936 ` 160` ballarin@13936 ` 161` ```end ```