summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | ballarin |

Thu, 31 Aug 2017 21:48:01 +0200 | |

changeset 66579 | 2db3fe23fdaf |

parent 66578 | 6a034c6c423f |

child 66580 | e5b1d4d55bf6 |

Revert 5a42eddc11c1.

--- a/src/HOL/Algebra/Complete_Lattice.thy Thu Aug 31 20:19:55 2017 +0200 +++ b/src/HOL/Algebra/Complete_Lattice.thy Thu Aug 31 21:48:01 2017 +0200 @@ -7,7 +7,7 @@ *) theory Complete_Lattice -imports Lattice Group +imports Lattice begin section \<open>Complete Lattices\<close> @@ -1192,43 +1192,8 @@ then show "EX i. greatest ?L i (Lower ?L B)" .. qed -theorem (in group) subgroups_complete_lattice: - "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>" - (is "complete_lattice ?L") -proof (rule partial_order.complete_lattice_criterion1) - show "partial_order ?L" by (rule subgroups_partial_order) -next - have "greatest ?L (carrier G) (carrier ?L)" - by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) - then show "\<exists>G. greatest ?L G (carrier ?L)" .. -next - fix A - assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" - then have Int_subgroup: "subgroup (\<Inter>A) G" - by (fastforce intro: subgroups_Inter) - have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _") - proof (rule greatest_LowerI) - fix H - assume H: "H \<in> A" - with L have subgroupH: "subgroup H G" by auto - from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H") - by (rule subgroup_imp_group) - from groupH have monoidH: "monoid ?H" - by (rule group.is_monoid) - from H have Int_subset: "?Int \<subseteq> H" by fastforce - then show "le ?L ?Int H" by simp - next - fix H - assume H: "H \<in> Lower ?L A" - with L Int_subgroup show "le ?L H ?Int" - by (fastforce simp: Lower_def intro: Inter_greatest) - next - show "A \<subseteq> carrier ?L" by (rule L) - next - show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) - qed - then show "\<exists>I. greatest ?L I (Lower ?L A)" .. -qed +text \<open>Another example, that of the lattice of subgroups of a group, + can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close> subsection \<open>Limit preserving functions\<close>

--- a/src/HOL/Algebra/Divisibility.thy Thu Aug 31 20:19:55 2017 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Thu Aug 31 21:48:01 2017 +0200 @@ -6,7 +6,7 @@ section \<open>Divisibility in monoids and rings\<close> theory Divisibility - imports "HOL-Library.Permutation" Coset Group Lattice + imports "HOL-Library.Permutation" Coset Group begin section \<open>Factorial Monoids\<close>

--- a/src/HOL/Algebra/Group.thy Thu Aug 31 20:19:55 2017 +0200 +++ b/src/HOL/Algebra/Group.thy Thu Aug 31 21:48:01 2017 +0200 @@ -5,7 +5,7 @@ *) theory Group -imports Order "HOL-Library.FuncSet" +imports Complete_Lattice "HOL-Library.FuncSet" begin section \<open>Monoids and Groups\<close> @@ -817,4 +817,42 @@ show "x \<otimes> y \<in> \<Inter>A" by blast qed +theorem (in group) subgroups_complete_lattice: + "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>" + (is "complete_lattice ?L") +proof (rule partial_order.complete_lattice_criterion1) + show "partial_order ?L" by (rule subgroups_partial_order) +next + have "greatest ?L (carrier G) (carrier ?L)" + by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) + then show "\<exists>G. greatest ?L G (carrier ?L)" .. +next + fix A + assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" + then have Int_subgroup: "subgroup (\<Inter>A) G" + by (fastforce intro: subgroups_Inter) + have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _") + proof (rule greatest_LowerI) + fix H + assume H: "H \<in> A" + with L have subgroupH: "subgroup H G" by auto + from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H") + by (rule subgroup_imp_group) + from groupH have monoidH: "monoid ?H" + by (rule group.is_monoid) + from H have Int_subset: "?Int \<subseteq> H" by fastforce + then show "le ?L ?Int H" by simp + next + fix H + assume H: "H \<in> Lower ?L A" + with L Int_subgroup show "le ?L H ?Int" + by (fastforce simp: Lower_def intro: Inter_greatest) + next + show "A \<subseteq> carrier ?L" by (rule L) + next + show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) + qed + then show "\<exists>I. greatest ?L I (Lower ?L A)" .. +qed + end