3 |
3 |
4 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. |
4 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. |
5 *) |
5 *) |
6 |
6 |
7 theory Group |
7 theory Group |
8 imports Order "HOL-Library.FuncSet" |
8 imports Complete_Lattice "HOL-Library.FuncSet" |
9 begin |
9 begin |
10 |
10 |
11 section \<open>Monoids and Groups\<close> |
11 section \<open>Monoids and Groups\<close> |
12 |
12 |
13 subsection \<open>Definitions\<close> |
13 subsection \<open>Definitions\<close> |
815 fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A" |
815 fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A" |
816 with subgr [THEN subgroup.m_closed] |
816 with subgr [THEN subgroup.m_closed] |
817 show "x \<otimes> y \<in> \<Inter>A" by blast |
817 show "x \<otimes> y \<in> \<Inter>A" by blast |
818 qed |
818 qed |
819 |
819 |
|
820 theorem (in group) subgroups_complete_lattice: |
|
821 "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>" |
|
822 (is "complete_lattice ?L") |
|
823 proof (rule partial_order.complete_lattice_criterion1) |
|
824 show "partial_order ?L" by (rule subgroups_partial_order) |
|
825 next |
|
826 have "greatest ?L (carrier G) (carrier ?L)" |
|
827 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) |
|
828 then show "\<exists>G. greatest ?L G (carrier ?L)" .. |
|
829 next |
|
830 fix A |
|
831 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |
|
832 then have Int_subgroup: "subgroup (\<Inter>A) G" |
|
833 by (fastforce intro: subgroups_Inter) |
|
834 have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _") |
|
835 proof (rule greatest_LowerI) |
|
836 fix H |
|
837 assume H: "H \<in> A" |
|
838 with L have subgroupH: "subgroup H G" by auto |
|
839 from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H") |
|
840 by (rule subgroup_imp_group) |
|
841 from groupH have monoidH: "monoid ?H" |
|
842 by (rule group.is_monoid) |
|
843 from H have Int_subset: "?Int \<subseteq> H" by fastforce |
|
844 then show "le ?L ?Int H" by simp |
|
845 next |
|
846 fix H |
|
847 assume H: "H \<in> Lower ?L A" |
|
848 with L Int_subgroup show "le ?L H ?Int" |
|
849 by (fastforce simp: Lower_def intro: Inter_greatest) |
|
850 next |
|
851 show "A \<subseteq> carrier ?L" by (rule L) |
|
852 next |
|
853 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |
|
854 qed |
|
855 then show "\<exists>I. greatest ?L I (Lower ?L A)" .. |
|
856 qed |
|
857 |
820 end |
858 end |