769 "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" |
769 "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" |
770 (is "complete_lattice ?L") |
770 (is "complete_lattice ?L") |
771 proof (rule partial_order.complete_lattice_criterion1) |
771 proof (rule partial_order.complete_lattice_criterion1) |
772 show "partial_order ?L" by (rule subgroups_partial_order) |
772 show "partial_order ?L" by (rule subgroups_partial_order) |
773 next |
773 next |
774 show "\<exists>G. greatest ?L G (carrier ?L)" |
774 have "greatest ?L (carrier G) (carrier ?L)" |
775 proof |
775 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) |
776 show "greatest ?L (carrier G) (carrier ?L)" |
776 then show "\<exists>G. greatest ?L G (carrier ?L)" .. |
777 by (unfold greatest_def) |
|
778 (simp add: subgroup.subset subgroup_self) |
|
779 qed |
|
780 next |
777 next |
781 fix A |
778 fix A |
782 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |
779 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |
783 then have Int_subgroup: "subgroup (\<Inter>A) G" |
780 then have Int_subgroup: "subgroup (\<Inter>A) G" |
784 by (fastforce intro: subgroups_Inter) |
781 by (fastforce intro: subgroups_Inter) |
785 show "\<exists>I. greatest ?L I (Lower ?L A)" |
782 have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _") |
786 proof |
783 proof (rule greatest_LowerI) |
787 show "greatest ?L (\<Inter>A) (Lower ?L A)" |
784 fix H |
788 (is "greatest _ ?Int _") |
785 assume H: "H \<in> A" |
789 proof (rule greatest_LowerI) |
786 with L have subgroupH: "subgroup H G" by auto |
790 fix H |
787 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |
791 assume H: "H \<in> A" |
788 by (rule subgroup_imp_group) |
792 with L have subgroupH: "subgroup H G" by auto |
789 from groupH have monoidH: "monoid ?H" |
793 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |
790 by (rule group.is_monoid) |
794 by (rule subgroup_imp_group) |
791 from H have Int_subset: "?Int \<subseteq> H" by fastforce |
795 from groupH have monoidH: "monoid ?H" |
792 then show "le ?L ?Int H" by simp |
796 by (rule group.is_monoid) |
793 next |
797 from H have Int_subset: "?Int \<subseteq> H" by fastforce |
794 fix H |
798 then show "le ?L ?Int H" by simp |
795 assume H: "H \<in> Lower ?L A" |
799 next |
796 with L Int_subgroup show "le ?L H ?Int" |
800 fix H |
797 by (fastforce simp: Lower_def intro: Inter_greatest) |
801 assume H: "H \<in> Lower ?L A" |
798 next |
802 with L Int_subgroup show "le ?L H ?Int" |
799 show "A \<subseteq> carrier ?L" by (rule L) |
803 by (fastforce simp: Lower_def intro: Inter_greatest) |
800 next |
804 next |
801 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |
805 show "A \<subseteq> carrier ?L" by (rule L) |
|
806 next |
|
807 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |
|
808 qed |
|
809 qed |
802 qed |
|
803 then show "\<exists>I. greatest ?L I (Lower ?L A)" .. |
810 qed |
804 qed |
811 |
805 |
812 end |
806 end |