6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. |
6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. |
7 *) |
7 *) |
8 |
8 |
9 header {* Groups *} |
9 header {* Groups *} |
10 |
10 |
11 theory Group = FuncSet: |
11 theory Group = FuncSet + Lattice: |
12 |
12 |
13 section {* From Magmas to Groups *} |
13 section {* From Magmas to Groups *} |
14 |
14 |
15 text {* |
15 text {* |
16 Definitions follow \cite{Jacobson:1985}; with the exception of |
16 Definitions follow \cite{Jacobson:1985}; with the exception of |
17 \emph{magma} which, following Bourbaki, is a set together with a |
17 \emph{magma} which, following Bourbaki, is a set together with a |
18 binary, closed operation. |
18 binary, closed operation. |
19 *} |
19 *} |
20 |
20 |
21 subsection {* Definitions *} |
21 subsection {* Definitions *} |
22 |
|
23 (* Object with a carrier set. *) |
|
24 |
|
25 record 'a partial_object = |
|
26 carrier :: "'a set" |
|
27 |
22 |
28 record 'a semigroup = "'a partial_object" + |
23 record 'a semigroup = "'a partial_object" + |
29 mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70) |
24 mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70) |
30 |
25 |
31 record 'a monoid = "'a semigroup" + |
26 record 'a monoid = "'a semigroup" + |
373 assumes subset [intro, simp]: "H \<subseteq> carrier G" |
368 assumes subset [intro, simp]: "H \<subseteq> carrier G" |
374 and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H" |
369 and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H" |
375 |
370 |
376 declare (in submagma) magma.intro [intro] semigroup.intro [intro] |
371 declare (in submagma) magma.intro [intro] semigroup.intro [intro] |
377 semigroup_axioms.intro [intro] |
372 semigroup_axioms.intro [intro] |
378 (* |
|
379 alternative definition of submagma |
|
380 |
|
381 locale submagma = var H + struct G + |
|
382 assumes subset [intro, simp]: "carrier H \<subseteq> carrier G" |
|
383 and m_equal [simp]: "mult H = mult G" |
|
384 and m_closed [intro, simp]: |
|
385 "[| x \<in> carrier H; y \<in> carrier H |] ==> x \<otimes> y \<in> carrier H" |
|
386 *) |
|
387 |
373 |
388 lemma submagma_imp_subset: |
374 lemma submagma_imp_subset: |
389 "submagma H G ==> H \<subseteq> carrier G" |
375 "submagma H G ==> H \<subseteq> carrier G" |
390 by (rule submagma.subset) |
376 by (rule submagma.subset) |
391 |
377 |
725 |
711 |
726 lemma (in comm_group) inv_mult: |
712 lemma (in comm_group) inv_mult: |
727 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y" |
713 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y" |
728 by (simp add: m_ac inv_mult_group) |
714 by (simp add: m_ac inv_mult_group) |
729 |
715 |
|
716 subsection {* Lattice of subgroups of a group *} |
|
717 |
|
718 text_raw {* \label{sec:subgroup-lattice} *} |
|
719 |
|
720 theorem (in group) subgroups_partial_order: |
|
721 "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" |
|
722 by (rule partial_order.intro) simp_all |
|
723 |
|
724 lemma (in group) subgroup_self: |
|
725 "subgroup (carrier G) G" |
|
726 by (rule subgroupI) auto |
|
727 |
|
728 lemma (in group) subgroup_imp_group: |
|
729 "subgroup H G ==> group (G(| carrier := H |))" |
|
730 using subgroup.groupI [OF _ group.intro] . |
|
731 |
|
732 lemma (in group) is_monoid [intro, simp]: |
|
733 "monoid G" |
|
734 by (rule monoid.intro) |
|
735 |
|
736 lemma (in group) subgroup_inv_equality: |
|
737 "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x" |
|
738 apply (rule_tac inv_equality [THEN sym]) |
|
739 apply (rule group.l_inv [OF subgroup_imp_group, simplified]) |
|
740 apply assumption+ |
|
741 apply (rule subsetD [OF subgroup.subset]) |
|
742 apply assumption+ |
|
743 apply (rule subsetD [OF subgroup.subset]) |
|
744 apply assumption |
|
745 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified]) |
|
746 apply assumption+ |
|
747 done |
|
748 |
|
749 theorem (in group) subgroups_Inter: |
|
750 assumes subgr: "(!!H. H \<in> A ==> subgroup H G)" |
|
751 and not_empty: "A ~= {}" |
|
752 shows "subgroup (\<Inter>A) G" |
|
753 proof (rule subgroupI) |
|
754 from subgr [THEN subgroup.subset] and not_empty |
|
755 show "\<Inter>A \<subseteq> carrier G" by blast |
|
756 next |
|
757 from subgr [THEN subgroup.one_closed] |
|
758 show "\<Inter>A ~= {}" by blast |
|
759 next |
|
760 fix x assume "x \<in> \<Inter>A" |
|
761 with subgr [THEN subgroup.m_inv_closed] |
|
762 show "inv x \<in> \<Inter>A" by blast |
|
763 next |
|
764 fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A" |
|
765 with subgr [THEN subgroup.m_closed] |
|
766 show "x \<otimes> y \<in> \<Inter>A" by blast |
|
767 qed |
|
768 |
|
769 theorem (in group) subgroups_complete_lattice: |
|
770 "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" |
|
771 (is "complete_lattice ?L") |
|
772 proof (rule partial_order.complete_lattice_criterion1) |
|
773 show "partial_order ?L" by (rule subgroups_partial_order) |
|
774 next |
|
775 have "greatest ?L (carrier G) (carrier ?L)" |
|
776 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) |
|
777 then show "EX G. greatest ?L G (carrier ?L)" .. |
|
778 next |
|
779 fix A |
|
780 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |
|
781 then have Int_subgroup: "subgroup (\<Inter>A) G" |
|
782 by (fastsimp intro: subgroups_Inter) |
|
783 have "greatest ?L (\<Inter>A) (Lower ?L A)" |
|
784 (is "greatest ?L ?Int _") |
|
785 proof (rule greatest_LowerI) |
|
786 fix H |
|
787 assume H: "H \<in> A" |
|
788 with L have subgroupH: "subgroup H G" by auto |
|
789 from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms) |
|
790 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |
|
791 by (rule subgroup_imp_group) |
|
792 from groupH have monoidH: "monoid ?H" |
|
793 by (rule group.is_monoid) |
|
794 from H have Int_subset: "?Int \<subseteq> H" by fastsimp |
|
795 then show "le ?L ?Int H" by simp |
|
796 next |
|
797 fix H |
|
798 assume H: "H \<in> Lower ?L A" |
|
799 with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest) |
|
800 next |
|
801 show "A \<subseteq> carrier ?L" by (rule L) |
|
802 next |
|
803 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |
|
804 qed |
|
805 then show "EX I. greatest ?L I (Lower ?L A)" .. |
|
806 qed |
|
807 |
730 end |
808 end |