683 subsection {* The Lattice of Subgroups of a Group *} 
683 subsection {* The Lattice of Subgroups of a Group *} 
684 
684 
685 text_raw {* \label{sec:subgrouplattice} *} 
685 text_raw {* \label{sec:subgrouplattice} *} 
686 
686 
687 theorem (in group) subgroups_partial_order: 
687 theorem (in group) subgroups_partial_order: 
688 "partial_order ( carrier = {H. subgroup H G}, le = op \<subseteq> )" 
688 "partial_order {H. subgroup H G} (op \<subseteq>)" 
689 by (rule partial_order.intro) simp_all 
689 by (rule partial_order.intro) simp_all 
690 
690 
691 lemma (in group) subgroup_self: 
691 lemma (in group) subgroup_self: 
692 "subgroup (carrier G) G" 
692 "subgroup (carrier G) G" 
693 by (rule subgroupI) auto 
693 by (rule subgroupI) auto 
728 with subgr [THEN subgroup.m_closed] 
728 with subgr [THEN subgroup.m_closed] 
729 show "x \<otimes> y \<in> \<Inter>A" by blast 
729 show "x \<otimes> y \<in> \<Inter>A" by blast 
730 qed 
730 qed 
731 
731 
732 theorem (in group) subgroups_complete_lattice: 
732 theorem (in group) subgroups_complete_lattice: 
733 "complete_lattice ( carrier = {H. subgroup H G}, le = op \<subseteq> )" 
733 "complete_lattice {H. subgroup H G} (op \<subseteq>)" 
734 (is "complete_lattice ?L") 
734 (is "complete_lattice ?car ?le") 
735 proof (rule partial_order.complete_lattice_criterion1) 
735 proof (rule partial_order.complete_lattice_criterion1) 
736 show "partial_order ?L" by (rule subgroups_partial_order) 
736 show "partial_order ?car ?le" by (rule subgroups_partial_order) 
737 next 
737 next 
738 have "greatest ?L (carrier G) (carrier ?L)" 
738 have "order_syntax.greatest ?car ?le (carrier G) ?car" 
739 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) 
739 by (unfold order_syntax.greatest_def) 
740 then show "\<exists>G. greatest ?L G (carrier ?L)" .. 
740 (simp add: subgroup.subset subgroup_self) 

741 then show "\<exists>G. order_syntax.greatest ?car ?le G ?car" .. 
741 next 
742 next 
742 fix A 
743 fix A 
743 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" 
744 assume L: "A \<subseteq> ?car" and non_empty: "A ~= {}" 
744 then have Int_subgroup: "subgroup (\<Inter>A) G" 
745 then have Int_subgroup: "subgroup (\<Inter>A) G" 
745 by (fastsimp intro: subgroups_Inter) 
746 by (fastsimp intro: subgroups_Inter) 
746 have "greatest ?L (\<Inter>A) (Lower ?L A)" 
747 have "order_syntax.greatest ?car ?le (\<Inter>A) (order_syntax.Lower ?car ?le A)" 
747 (is "greatest ?L ?Int _") 
748 (is "order_syntax.greatest _ _ ?Int _") 
748 proof (rule greatest_LowerI) 
749 proof (rule order_syntax.greatest_LowerI) 
749 fix H 
750 fix H 
750 assume H: "H \<in> A" 
751 assume H: "H \<in> A" 
751 with L have subgroupH: "subgroup H G" by auto 
752 with L have subgroupH: "subgroup H G" by auto 
752 from subgroupH have groupH: "group (G ( carrier := H ))" (is "group ?H") 
753 from subgroupH have groupH: "group (G ( carrier := H ))" (is "group ?H") 
753 by (rule subgroup_imp_group) 
754 by (rule subgroup_imp_group) 
754 from groupH have monoidH: "monoid ?H" 
755 from groupH have monoidH: "monoid ?H" 
755 by (rule group.is_monoid) 
756 by (rule group.is_monoid) 
756 from H have Int_subset: "?Int \<subseteq> H" by fastsimp 
757 from H have Int_subset: "?Int \<subseteq> H" by fastsimp 
757 then show "le ?L ?Int H" by simp 
758 then show "?le ?Int H" by simp 
758 next 
759 next 
759 fix H 
760 fix H 
760 assume H: "H \<in> Lower ?L A" 
761 assume H: "H \<in> order_syntax.Lower ?car ?le A" 
761 with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest) 
762 with L Int_subgroup show "?le H ?Int" 

763 by (fastsimp simp: order_syntax.Lower_def intro: Inter_greatest) 
762 next 
764 next 
763 show "A \<subseteq> carrier ?L" by (rule L) 
765 show "A \<subseteq> ?car" by (rule L) 
764 next 
766 next 
765 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) 
767 show "?Int \<in> ?car" by simp (rule Int_subgroup) 
766 qed 
768 qed 
767 then show "\<exists>I. greatest ?L I (Lower ?L A)" .. 
769 then show "\<exists>I. order_syntax.greatest ?car ?le I (order_syntax.Lower ?car ?le A)" .. 
768 qed 
770 qed 
769 
771 
770 end 
772 end 