842 @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} |
847 @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} |
843 by (fastsimp intro!: greatest_LowerI simp: Lower_def) |
848 by (fastsimp intro!: greatest_LowerI simp: Lower_def) |
844 then show "EX i. greatest ?L i (Lower ?L B)" .. |
849 then show "EX i. greatest ?L i (Lower ?L B)" .. |
845 qed |
850 qed |
846 |
851 |
847 subsubsection {* Lattice of subgroups of a group *} |
852 text {* An other example, that of the lattice of subgroups of a group, |
848 |
853 can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} |
849 theorem (in group) subgroups_partial_order: |
|
850 "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" |
|
851 by (rule partial_order.intro) simp_all |
|
852 |
|
853 lemma (in group) subgroup_self: |
|
854 "subgroup (carrier G) G" |
|
855 by (rule subgroupI) auto |
|
856 |
|
857 lemma (in group) subgroup_imp_group: |
|
858 "subgroup H G ==> group (G(| carrier := H |))" |
|
859 using subgroup.groupI [OF _ group.intro] . |
|
860 |
|
861 lemma (in group) is_monoid [intro, simp]: |
|
862 "monoid G" |
|
863 by (rule monoid.intro) |
|
864 |
|
865 lemma (in group) subgroup_inv_equality: |
|
866 "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x" |
|
867 apply (rule_tac inv_equality [THEN sym]) |
|
868 apply (rule group.l_inv [OF subgroup_imp_group, simplified]) |
|
869 apply assumption+ |
|
870 apply (rule subsetD [OF subgroup.subset]) |
|
871 apply assumption+ |
|
872 apply (rule subsetD [OF subgroup.subset]) |
|
873 apply assumption |
|
874 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified]) |
|
875 apply assumption+ |
|
876 done |
|
877 |
|
878 theorem (in group) subgroups_Inter: |
|
879 assumes subgr: "(!!H. H \<in> A ==> subgroup H G)" |
|
880 and not_empty: "A ~= {}" |
|
881 shows "subgroup (\<Inter>A) G" |
|
882 proof (rule subgroupI) |
|
883 from subgr [THEN subgroup.subset] and not_empty |
|
884 show "\<Inter>A \<subseteq> carrier G" by blast |
|
885 next |
|
886 from subgr [THEN subgroup.one_closed] |
|
887 show "\<Inter>A ~= {}" by blast |
|
888 next |
|
889 fix x assume "x \<in> \<Inter>A" |
|
890 with subgr [THEN subgroup.m_inv_closed] |
|
891 show "inv x \<in> \<Inter>A" by blast |
|
892 next |
|
893 fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A" |
|
894 with subgr [THEN subgroup.m_closed] |
|
895 show "x \<otimes> y \<in> \<Inter>A" by blast |
|
896 qed |
|
897 |
|
898 theorem (in group) subgroups_complete_lattice: |
|
899 "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" |
|
900 (is "complete_lattice ?L") |
|
901 proof (rule partial_order.complete_lattice_criterion1) |
|
902 show "partial_order ?L" by (rule subgroups_partial_order) |
|
903 next |
|
904 have "greatest ?L (carrier G) (carrier ?L)" |
|
905 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) |
|
906 then show "EX G. greatest ?L G (carrier ?L)" .. |
|
907 next |
|
908 fix A |
|
909 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |
|
910 then have Int_subgroup: "subgroup (\<Inter>A) G" |
|
911 by (fastsimp intro: subgroups_Inter) |
|
912 have "greatest ?L (\<Inter>A) (Lower ?L A)" |
|
913 (is "greatest ?L ?Int _") |
|
914 proof (rule greatest_LowerI) |
|
915 fix H |
|
916 assume H: "H \<in> A" |
|
917 with L have subgroupH: "subgroup H G" by auto |
|
918 from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms) |
|
919 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |
|
920 by (rule subgroup_imp_group) |
|
921 from groupH have monoidH: "monoid ?H" |
|
922 by (rule group.is_monoid) |
|
923 from H have Int_subset: "?Int \<subseteq> H" by fastsimp |
|
924 then show "le ?L ?Int H" by simp |
|
925 next |
|
926 fix H |
|
927 assume H: "H \<in> Lower ?L A" |
|
928 with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest) |
|
929 next |
|
930 show "A \<subseteq> carrier ?L" by (rule L) |
|
931 next |
|
932 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |
|
933 qed |
|
934 then show "EX I. greatest ?L I (Lower ?L A)" .. |
|
935 qed |
|
936 |
854 |
937 end |
855 end |