src/HOL/Algebra/Group.thy
changeset 13813 722593f2f068
child 13817 7e031a968443
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Feb 10 09:45:22 2003 +0100
     1.3 @@ -0,0 +1,372 @@
     1.4 +(*
     1.5 +  Title:  HOL/Algebra/Group.thy
     1.6 +  Id:     $Id$
     1.7 +  Author: Clemens Ballarin, started 4 February 2003
     1.8 +
     1.9 +Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
    1.10 +*)
    1.11 +
    1.12 +header {* Algebraic Structures up to Abelian Groups *}
    1.13 +
    1.14 +theory Group = FuncSet:
    1.15 +
    1.16 +text {*
    1.17 +  Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    1.18 +  the exception of \emph{magma} which, following Bourbaki, is a set
    1.19 +  together with a binary, closed operation.
    1.20 +*}
    1.21 +
    1.22 +section {* From Magmas to Groups *}
    1.23 +
    1.24 +subsection {* Definitions *}
    1.25 +
    1.26 +record 'a magma =
    1.27 +  carrier :: "'a set"
    1.28 +  mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    1.29 +
    1.30 +record 'a group = "'a magma" +
    1.31 +  one :: 'a ("\<one>\<index>")
    1.32 +  m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
    1.33 +
    1.34 +locale magma = struct G +
    1.35 +  assumes m_closed [intro, simp]:
    1.36 +    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    1.37 +
    1.38 +locale semigroup = magma +
    1.39 +  assumes m_assoc:
    1.40 +    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.41 +     (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    1.42 +
    1.43 +locale group = semigroup +
    1.44 +  assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    1.45 +    and inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
    1.46 +    and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    1.47 +    and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
    1.48 +
    1.49 +subsection {* Cancellation Laws and Basic Properties *}
    1.50 +
    1.51 +lemma (in group) l_cancel [simp]:
    1.52 +  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.53 +   (x \<otimes> y = x \<otimes> z) = (y = z)"
    1.54 +proof
    1.55 +  assume eq: "x \<otimes> y = x \<otimes> z"
    1.56 +    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
    1.57 +  then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc)
    1.58 +  with G show "y = z" by (simp add: l_inv)
    1.59 +next
    1.60 +  assume eq: "y = z"
    1.61 +    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
    1.62 +  then show "x \<otimes> y = x \<otimes> z" by simp
    1.63 +qed
    1.64 +
    1.65 +lemma (in group) r_one [simp]:  
    1.66 +  "x \<in> carrier G ==> x \<otimes> \<one> = x"
    1.67 +proof -
    1.68 +  assume x: "x \<in> carrier G"
    1.69 +  then have "inv x \<otimes> (x \<otimes> \<one>) = inv x \<otimes> x"
    1.70 +    by (simp add: m_assoc [symmetric] l_inv)
    1.71 +  with x show ?thesis by simp 
    1.72 +qed
    1.73 +
    1.74 +lemma (in group) r_inv:
    1.75 +  "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
    1.76 +proof -
    1.77 +  assume x: "x \<in> carrier G"
    1.78 +  then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
    1.79 +    by (simp add: m_assoc [symmetric] l_inv)
    1.80 +  with x show ?thesis by (simp del: r_one)
    1.81 +qed
    1.82 +
    1.83 +lemma (in group) r_cancel [simp]:
    1.84 +  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.85 +   (y \<otimes> x = z \<otimes> x) = (y = z)"
    1.86 +proof
    1.87 +  assume eq: "y \<otimes> x = z \<otimes> x"
    1.88 +    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
    1.89 +  then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
    1.90 +    by (simp add: m_assoc [symmetric])
    1.91 +  with G show "y = z" by (simp add: r_inv)
    1.92 +next
    1.93 +  assume eq: "y = z"
    1.94 +    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
    1.95 +  then show "y \<otimes> x = z \<otimes> x" by simp
    1.96 +qed
    1.97 +
    1.98 +lemma (in group) inv_inv [simp]:
    1.99 +  "x \<in> carrier G ==> inv (inv x) = x"
   1.100 +proof -
   1.101 +  assume x: "x \<in> carrier G"
   1.102 +  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by (simp add: l_inv r_inv)
   1.103 +  with x show ?thesis by simp
   1.104 +qed
   1.105 +
   1.106 +lemma (in group) inv_mult:
   1.107 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
   1.108 +proof -
   1.109 +  assume G: "x \<in> carrier G" "y \<in> carrier G"
   1.110 +  then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
   1.111 +    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
   1.112 +  with G show ?thesis by simp
   1.113 +qed
   1.114 +
   1.115 +subsection {* Substructures *}
   1.116 +
   1.117 +locale submagma = var H + struct G +
   1.118 +  assumes subset [intro, simp]: "H \<subseteq> carrier G"
   1.119 +    and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   1.120 +
   1.121 +declare (in submagma) magma.intro [intro] semigroup.intro [intro]
   1.122 +
   1.123 +(*
   1.124 +alternative definition of submagma
   1.125 +
   1.126 +locale submagma = var H + struct G +
   1.127 +  assumes subset [intro, simp]: "carrier H \<subseteq> carrier G"
   1.128 +    and m_equal [simp]: "mult H = mult G"
   1.129 +    and m_closed [intro, simp]:
   1.130 +      "[| x \<in> carrier H; y \<in> carrier H |] ==> x \<otimes> y \<in> carrier H"
   1.131 +*)
   1.132 +
   1.133 +lemma submagma_imp_subset:
   1.134 +  "submagma H G ==> H \<subseteq> carrier G"
   1.135 +  by (rule submagma.subset)
   1.136 +
   1.137 +lemma (in submagma) subsetD [dest, simp]:
   1.138 +  "x \<in> H ==> x \<in> carrier G"
   1.139 +  using subset by blast
   1.140 +
   1.141 +lemma (in submagma) magmaI [intro]:
   1.142 +  includes magma G
   1.143 +  shows "magma (G(| carrier := H |))"
   1.144 +  by rule simp
   1.145 +
   1.146 +lemma (in submagma) semigroup_axiomsI [intro]:
   1.147 +  includes semigroup G
   1.148 +  shows "semigroup_axioms (G(| carrier := H |))"
   1.149 +    by rule (simp add: m_assoc)
   1.150 +
   1.151 +lemma (in submagma) semigroupI [intro]:
   1.152 +  includes semigroup G
   1.153 +  shows "semigroup (G(| carrier := H |))"
   1.154 +  using prems by fast
   1.155 +
   1.156 +locale subgroup = submagma H G +
   1.157 +  assumes one_closed [intro, simp]: "\<one> \<in> H"
   1.158 +    and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
   1.159 +
   1.160 +declare (in subgroup) group.intro [intro]
   1.161 +
   1.162 +lemma (in subgroup) group_axiomsI [intro]:
   1.163 +  includes group G
   1.164 +  shows "group_axioms (G(| carrier := H |))"
   1.165 +  by rule (simp_all add: l_inv)
   1.166 +
   1.167 +lemma (in subgroup) groupI [intro]:
   1.168 +  includes group G
   1.169 +  shows "group (G(| carrier := H |))"
   1.170 +  using prems by fast
   1.171 +
   1.172 +text {*
   1.173 +  Since @{term H} is nonempty, it contains some element @{term x}.  Since
   1.174 +  it is closed under inverse, it contains @{text "inv x"}.  Since
   1.175 +  it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
   1.176 +*}
   1.177 +
   1.178 +lemma (in group) one_in_subset:
   1.179 +  "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
   1.180 +   ==> \<one> \<in> H"
   1.181 +by (force simp add: l_inv)
   1.182 +
   1.183 +text {* A characterization of subgroups: closed, non-empty subset. *}
   1.184 +
   1.185 +lemma (in group) subgroupI:
   1.186 +  assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
   1.187 +    and inv: "!!a. a \<in> H ==> inv a \<in> H"
   1.188 +    and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
   1.189 +  shows "subgroup H G"
   1.190 +proof
   1.191 +  from subset and mult show "submagma H G" ..
   1.192 +next
   1.193 +  have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
   1.194 +  with inv show "subgroup_axioms H G"
   1.195 +    by (intro subgroup_axioms.intro) simp_all
   1.196 +qed
   1.197 +
   1.198 +text {*
   1.199 +  Repeat facts of submagmas for subgroups.  Necessary???
   1.200 +*}
   1.201 +
   1.202 +lemma (in subgroup) subset:
   1.203 +  "H \<subseteq> carrier G"
   1.204 +  ..
   1.205 +
   1.206 +lemma (in subgroup) m_closed:
   1.207 +  "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   1.208 +  ..
   1.209 +
   1.210 +declare magma.m_closed [simp]
   1.211 +
   1.212 +declare group.one_closed [iff] group.inv_closed [simp]
   1.213 +  group.l_one [simp] group.r_one [simp] group.inv_inv [simp]
   1.214 +
   1.215 +lemma subgroup_nonempty:
   1.216 +  "~ subgroup {} G"
   1.217 +  by (blast dest: subgroup.one_closed)
   1.218 +
   1.219 +lemma (in subgroup) finite_imp_card_positive:
   1.220 +  "finite (carrier G) ==> 0 < card H"
   1.221 +proof (rule classical)
   1.222 +  have sub: "subgroup H G" using prems ..
   1.223 +  assume fin: "finite (carrier G)"
   1.224 +    and zero: "~ 0 < card H"
   1.225 +  then have "finite H" by (blast intro: finite_subset dest: subset)
   1.226 +  with zero sub have "subgroup {} G" by simp
   1.227 +  with subgroup_nonempty show ?thesis by contradiction
   1.228 +qed
   1.229 +
   1.230 +subsection {* Direct Products *}
   1.231 +
   1.232 +constdefs
   1.233 +  DirProdMagma ::
   1.234 +    "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a \<times> 'b) magma"
   1.235 +    (infixr "\<times>\<^sub>m" 80)
   1.236 +  "G \<times>\<^sub>m H == (| carrier = carrier G \<times> carrier H,
   1.237 +    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
   1.238 +
   1.239 +  DirProdGroup ::
   1.240 +    "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
   1.241 +    (infixr "\<times>\<^sub>g" 80)
   1.242 +  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
   1.243 +    mult = mult (G \<times>\<^sub>m H),
   1.244 +    one = (one G, one H),
   1.245 +    m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
   1.246 +
   1.247 +lemma DirProdMagma_magma:
   1.248 +  includes magma G + magma H
   1.249 +  shows "magma (G \<times>\<^sub>m H)"
   1.250 +  by rule (auto simp add: DirProdMagma_def)
   1.251 +
   1.252 +lemma DirProdMagma_semigroup_axioms:
   1.253 +  includes semigroup G + semigroup H
   1.254 +  shows "semigroup_axioms (G \<times>\<^sub>m H)"
   1.255 +  by rule (auto simp add: DirProdMagma_def G.m_assoc H.m_assoc)
   1.256 +
   1.257 +lemma DirProdMagma_semigroup:
   1.258 +  includes semigroup G + semigroup H
   1.259 +  shows "semigroup (G \<times>\<^sub>m H)"
   1.260 +  using prems
   1.261 +  by (fast intro: semigroup.intro
   1.262 +    DirProdMagma_magma DirProdMagma_semigroup_axioms)
   1.263 +
   1.264 +lemma DirProdGroup_magma:
   1.265 +  includes magma G + magma H
   1.266 +  shows "magma (G \<times>\<^sub>g H)"
   1.267 +  by rule (auto simp add: DirProdGroup_def DirProdMagma_def)
   1.268 +
   1.269 +lemma DirProdGroup_semigroup_axioms:
   1.270 +  includes semigroup G + semigroup H
   1.271 +  shows "semigroup_axioms (G \<times>\<^sub>g H)"
   1.272 +  by rule
   1.273 +    (auto simp add: DirProdGroup_def DirProdMagma_def G.m_assoc H.m_assoc)
   1.274 +
   1.275 +lemma DirProdGroup_semigroup:
   1.276 +  includes semigroup G + semigroup H
   1.277 +  shows "semigroup (G \<times>\<^sub>g H)"
   1.278 +  using prems
   1.279 +  by (fast intro: semigroup.intro
   1.280 +    DirProdGroup_magma DirProdGroup_semigroup_axioms)
   1.281 +
   1.282 +(* ... and further lemmas for group ... *)
   1.283 +
   1.284 +lemma
   1.285 +  includes group G + group H
   1.286 +  shows "group (G \<times>\<^sub>g H)"
   1.287 +by rule
   1.288 +  (auto intro: magma.intro semigroup_axioms.intro group_axioms.intro
   1.289 +    simp add: DirProdGroup_def DirProdMagma_def
   1.290 +      G.m_assoc H.m_assoc G.l_inv H.l_inv)
   1.291 +
   1.292 +subsection {* Homomorphisms *}
   1.293 +
   1.294 +constdefs
   1.295 +  hom :: "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a => 'b)set"
   1.296 +  "hom G H ==
   1.297 +    {h. h \<in> carrier G -> carrier H &
   1.298 +      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
   1.299 +
   1.300 +lemma (in semigroup) hom:
   1.301 +  includes semigroup G
   1.302 +  shows "semigroup (| carrier = hom G G, mult = op o |)"
   1.303 +proof
   1.304 +  show "magma (| carrier = hom G G, mult = op o |)"
   1.305 +    by rule (simp add: Pi_def hom_def)
   1.306 +next
   1.307 +  show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
   1.308 +    by rule (simp add: o_assoc)
   1.309 +qed
   1.310 +
   1.311 +lemma hom_mult:
   1.312 +  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |] 
   1.313 +   ==> h (mult G x y) = mult H (h x) (h y)"
   1.314 +  by (simp add: hom_def) 
   1.315 +
   1.316 +lemma hom_closed:
   1.317 +  "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
   1.318 +  by (auto simp add: hom_def funcset_mem)
   1.319 +
   1.320 +locale group_hom = group G + group H + var h +
   1.321 +  assumes homh: "h \<in> hom G H"
   1.322 +  notes hom_mult [simp] = hom_mult [OF homh]
   1.323 +    and hom_closed [simp] = hom_closed [OF homh]
   1.324 +
   1.325 +lemma (in group_hom) one_closed [simp]:
   1.326 +  "h \<one> \<in> carrier H"
   1.327 +  by simp
   1.328 +
   1.329 +lemma (in group_hom) hom_one [simp]:
   1.330 +  "h \<one> = \<one>\<^sub>2"
   1.331 +proof -
   1.332 +  have "h \<one> \<otimes>\<^sub>2 \<one>\<^sub>2 = h \<one> \<otimes>\<^sub>2 h \<one>"
   1.333 +    by (simp add: hom_mult [symmetric] del: hom_mult)
   1.334 +  then show ?thesis by (simp del: r_one)
   1.335 +qed
   1.336 +
   1.337 +lemma (in group_hom) inv_closed [simp]:
   1.338 +  "x \<in> carrier G ==> h (inv x) \<in> carrier H"
   1.339 +  by simp
   1.340 +
   1.341 +lemma (in group_hom) hom_inv [simp]:
   1.342 +  "x \<in> carrier G ==> h (inv x) = inv\<^sub>2 (h x)"
   1.343 +proof -
   1.344 +  assume x: "x \<in> carrier G"
   1.345 +  then have "h x \<otimes>\<^sub>2 h (inv x) = \<one>\<^sub>2"
   1.346 +    by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
   1.347 +  also from x have "... = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)"
   1.348 +    by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   1.349 +  finally have "h x \<otimes>\<^sub>2 h (inv x) = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" .
   1.350 +  with x show ?thesis by simp
   1.351 +qed
   1.352 +
   1.353 +section {* Abelian Structures *}
   1.354 +
   1.355 +subsection {* Definition *}
   1.356 +
   1.357 +locale abelian_semigroup = semigroup +
   1.358 +  assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   1.359 +
   1.360 +lemma (in abelian_semigroup) m_lcomm:
   1.361 +  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.362 +   x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   1.363 +proof -
   1.364 +  assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.365 +  from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)
   1.366 +  also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)
   1.367 +  also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)
   1.368 +  finally show ?thesis .
   1.369 +qed
   1.370 +
   1.371 +lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
   1.372 +
   1.373 +locale abelian_group = abelian_semigroup + group
   1.374 +
   1.375 +end