author ballarin Mon Feb 10 09:45:22 2003 +0100 (2003-02-10) changeset 13813 722593f2f068 parent 13812 91713a1915ee child 13814 5402c2eaf393
New development of algebra: Groups.
     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