author | haftmann |

Thu Aug 24 17:41:49 2017 +0200 (2017-08-24) | |

changeset 66501 | 5a42eddc11c1 |

parent 66500 | ba94aeb02fbc |

child 66502 | 5df7a346f07b |

child 66506 | c1d8ab323d85 |

swapping of theory dependency yields less pervasive syntax requiring popular symbols \<mu>, \<nu>

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

2.1 --- a/src/HOL/Algebra/Divisibility.thy Thu Aug 24 17:24:12 2017 +0200 2.2 +++ b/src/HOL/Algebra/Divisibility.thy Thu Aug 24 17:41:49 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 2.8 + imports "HOL-Library.Permutation" Coset Group Lattice 2.9 begin 2.10 2.11 section \<open>Factorial Monoids\<close>

3.1 --- a/src/HOL/Algebra/Group.thy Thu Aug 24 17:24:12 2017 +0200 3.2 +++ b/src/HOL/Algebra/Group.thy Thu Aug 24 17:41:49 2017 +0200 3.3 @@ -5,7 +5,7 @@ 3.4 *) 3.5 3.6 theory Group 3.7 -imports Complete_Lattice "HOL-Library.FuncSet" 3.8 +imports Order "HOL-Library.FuncSet" 3.9 begin 3.10 3.11 section \<open>Monoids and Groups\<close> 3.12 @@ -817,42 +817,4 @@ 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