author | ballarin |

Thu Aug 31 21:48:01 2017 +0200 (2017-08-31) | |

changeset 66579 | 2db3fe23fdaf |

parent 66578 | 6a034c6c423f |

child 66580 | e5b1d4d55bf6 |

Revert 5a42eddc11c1.

1.1 --- a/src/HOL/Algebra/Complete_Lattice.thy Thu Aug 31 20:19:55 2017 +0200 1.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy Thu Aug 31 21:48:01 2017 +0200 1.3 @@ -7,7 +7,7 @@ 1.4 *) 1.5 1.6 theory Complete_Lattice 1.7 -imports Lattice Group 1.8 +imports Lattice 1.9 begin 1.10 1.11 section \<open>Complete Lattices\<close> 1.12 @@ -1192,43 +1192,8 @@ 1.13 then show "EX i. greatest ?L i (Lower ?L B)" .. 1.14 qed 1.15 1.16 -theorem (in group) subgroups_complete_lattice: 1.17 - "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>" 1.18 - (is "complete_lattice ?L") 1.19 -proof (rule partial_order.complete_lattice_criterion1) 1.20 - show "partial_order ?L" by (rule subgroups_partial_order) 1.21 -next 1.22 - have "greatest ?L (carrier G) (carrier ?L)" 1.23 - by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) 1.24 - then show "\<exists>G. greatest ?L G (carrier ?L)" .. 1.25 -next 1.26 - fix A 1.27 - assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" 1.28 - then have Int_subgroup: "subgroup (\<Inter>A) G" 1.29 - by (fastforce intro: subgroups_Inter) 1.30 - have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _") 1.31 - proof (rule greatest_LowerI) 1.32 - fix H 1.33 - assume H: "H \<in> A" 1.34 - with L have subgroupH: "subgroup H G" by auto 1.35 - from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H") 1.36 - by (rule subgroup_imp_group) 1.37 - from groupH have monoidH: "monoid ?H" 1.38 - by (rule group.is_monoid) 1.39 - from H have Int_subset: "?Int \<subseteq> H" by fastforce 1.40 - then show "le ?L ?Int H" by simp 1.41 - next 1.42 - fix H 1.43 - assume H: "H \<in> Lower ?L A" 1.44 - with L Int_subgroup show "le ?L H ?Int" 1.45 - by (fastforce simp: Lower_def intro: Inter_greatest) 1.46 - next 1.47 - show "A \<subseteq> carrier ?L" by (rule L) 1.48 - next 1.49 - show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) 1.50 - qed 1.51 - then show "\<exists>I. greatest ?L I (Lower ?L A)" .. 1.52 -qed 1.53 +text \<open>Another example, that of the lattice of subgroups of a group, 1.54 + can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close> 1.55 1.56 1.57 subsection \<open>Limit preserving functions\<close>

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

3.1 --- a/src/HOL/Algebra/Group.thy Thu Aug 31 20:19:55 2017 +0200 3.2 +++ b/src/HOL/Algebra/Group.thy Thu Aug 31 21:48:01 2017 +0200 3.3 @@ -5,7 +5,7 @@ 3.4 *) 3.5 3.6 theory Group 3.7 -imports Order "HOL-Library.FuncSet" 3.8 +imports Complete_Lattice "HOL-Library.FuncSet" 3.9 begin 3.10 3.11 section \<open>Monoids and Groups\<close> 3.12 @@ -817,4 +817,42 @@ 3.13 show "x \<otimes> y \<in> \<Inter>A" by blast 3.14 qed 3.15 3.16 +theorem (in group) subgroups_complete_lattice: 3.17 + "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>" 3.18 + (is "complete_lattice ?L") 3.19 +proof (rule partial_order.complete_lattice_criterion1) 3.20 + show "partial_order ?L" by (rule subgroups_partial_order) 3.21 +next 3.22 + have "greatest ?L (carrier G) (carrier ?L)" 3.23 + by (unfold greatest_def) (simp add: subgroup.subset subgroup_self) 3.24 + then show "\<exists>G. greatest ?L G (carrier ?L)" .. 3.25 +next 3.26 + fix A 3.27 + assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" 3.28 + then have Int_subgroup: "subgroup (\<Inter>A) G" 3.29 + by (fastforce intro: subgroups_Inter) 3.30 + have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _") 3.31 + proof (rule greatest_LowerI) 3.32 + fix H 3.33 + assume H: "H \<in> A" 3.34 + with L have subgroupH: "subgroup H G" by auto 3.35 + from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H") 3.36 + by (rule subgroup_imp_group) 3.37 + from groupH have monoidH: "monoid ?H" 3.38 + by (rule group.is_monoid) 3.39 + from H have Int_subset: "?Int \<subseteq> H" by fastforce 3.40 + then show "le ?L ?Int H" by simp 3.41 + next 3.42 + fix H 3.43 + assume H: "H \<in> Lower ?L A" 3.44 + with L Int_subgroup show "le ?L H ?Int" 3.45 + by (fastforce simp: Lower_def intro: Inter_greatest) 3.46 + next 3.47 + show "A \<subseteq> carrier ?L" by (rule L) 3.48 + next 3.49 + show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) 3.50 + qed 3.51 + then show "\<exists>I. greatest ?L I (Lower ?L A)" .. 3.52 +qed 3.53 + 3.54 end