New theory GroupTheory/Module.thy of modules
authorpaulson
Fri Sep 27 10:33:47 2002 +0200 (2002-09-27)
changeset 13589b6d1a29dc978
parent 13588 07b66a557487
child 13590 d8e98ef3ad13
New theory GroupTheory/Module.thy of modules
src/HOL/GroupTheory/Module.thy
src/HOL/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/GroupTheory/Module.thy	Fri Sep 27 10:33:47 2002 +0200
     1.3 @@ -0,0 +1,62 @@
     1.4 +(*  Title:      HOL/GroupTheory/Module
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson
     1.7 +
     1.8 +*)
     1.9 +
    1.10 +header{*Modules*}
    1.11 +
    1.12 +theory Module = Ring:
    1.13 +
    1.14 +text{*The record includes all the group components (carrier, sum, gminus,
    1.15 +zero), adding the scalar product.*}
    1.16 +record ('a,'b) module  = "'a group" + 
    1.17 +  sprod :: "'b \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "\<star>\<index>" 70) 
    1.18 +
    1.19 +text{*The locale assumes all the properties of a ring and an Abelian group,
    1.20 +adding laws relating them.*}
    1.21 +locale module = ring R + abelian_group M +
    1.22 +  assumes sprod_funcset: "sprod M \<in> carrier R \<rightarrow> carrier M \<rightarrow> carrier M"
    1.23 +      and sprod_assoc:   
    1.24 +            "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|] 
    1.25 +             ==> (r \<cdot>\<^sub>1 s) \<star>\<^sub>2 a = r \<star>\<^sub>2 (s \<star>\<^sub>2 a)"
    1.26 +      and sprod_distrib_left:
    1.27 +            "[|r \<in> carrier R; a \<in> carrier M; b \<in> carrier M|] 
    1.28 +             ==> r \<star>\<^sub>2 (a \<oplus>\<^sub>2 b) = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (r \<star>\<^sub>2 b)"
    1.29 +      and sprod_distrib_right:
    1.30 +            "[|r \<in> carrier R; s \<in> carrier R; a \<in> carrier M|] 
    1.31 +             ==> (r \<oplus>\<^sub>1 s) \<star>\<^sub>2 a = (r \<star>\<^sub>2 a) \<oplus>\<^sub>2 (s \<star>\<^sub>2 a)"
    1.32 +
    1.33 +lemma module_iff:
    1.34 +     "module R M = (ring R & abelian_group M & module_axioms R M)"
    1.35 +by (simp add: module_def ring_def abelian_group_def) 
    1.36 +
    1.37 +text{*The sum and product in @{text R} are @{text "r \<oplus>\<^sub>1 s"} and @{text
    1.38 +"r \<cdot>\<^sub>1 s"}, respectively.  The sum in @{text M} is @{text "a \<oplus>\<^sub>2 b"}.*}
    1.39 +
    1.40 +
    1.41 +text{*We have to write the ring product as @{text "\<cdot>\<^sub>2"}. But if we
    1.42 +refer to the scalar product as @{text "\<cdot>\<^sub>1"} then syntactic ambiguities
    1.43 +arise.  This presumably happens because the subscript merely determines which
    1.44 +structure argument to insert, which happens after parsing.  Better to use a
    1.45 +different symbol such as @{text "\<star>"}*}
    1.46 +
    1.47 +subsection {*Trivial Example: Every Ring is an R-Module Over Itself *}
    1.48 +
    1.49 +constdefs
    1.50 + triv_mod :: "('a,'b) ring_scheme => ('a,'a) module"
    1.51 +  "triv_mod R == (|carrier = carrier R,
    1.52 +                 sum = sum R,
    1.53 +                 gminus = gminus R,
    1.54 +                 zero = zero R, 
    1.55 +                 sprod = prod R|)"
    1.56 +
    1.57 +theorem module_triv_mod: "ring R ==> module R (triv_mod R)"
    1.58 +apply (simp add: triv_mod_def module_iff module_axioms_def
    1.59 +                 ring_def ring_axioms_def abelian_group_def
    1.60 +                 distrib_l_def distrib_r_def semigroup_def group_axioms_def)
    1.61 +apply (simp add: abelian_group_axioms_def)
    1.62 +  --{*Combining the two simplifications causes looping!*}
    1.63 +done
    1.64 +
    1.65 +end
     2.1 --- a/src/HOL/IsaMakefile	Thu Sep 26 15:21:38 2002 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Sep 27 10:33:47 2002 +0200
     2.3 @@ -281,7 +281,7 @@
     2.4    GroupTheory/Coset.thy \
     2.5    GroupTheory/Exponent.thy \
     2.6    GroupTheory/Group.thy \
     2.7 -  GroupTheory/Ring.thy \
     2.8 +  GroupTheory/Module.thy GroupTheory/Ring.thy \
     2.9    GroupTheory/Sylow.thy \
    2.10    GroupTheory/ROOT.ML \
    2.11    GroupTheory/document/root.tex