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

author | haftmann |

Thu, 24 Aug 2017 17:41:49 +0200 | |

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>

--- a/src/HOL/Algebra/Complete_Lattice.thy Thu Aug 24 17:24:12 2017 +0200 +++ b/src/HOL/Algebra/Complete_Lattice.thy Thu Aug 24 17:41:49 2017 +0200 @@ -7,7 +7,7 @@ *) theory Complete_Lattice -imports Lattice +imports Lattice Group begin section \<open>Complete Lattices\<close> @@ -1192,8 +1192,43 @@ then show "EX i. greatest ?L i (Lower ?L B)" .. 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> +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 subsection \<open>Limit preserving functions\<close>

--- a/src/HOL/Algebra/Divisibility.thy Thu Aug 24 17:24:12 2017 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Thu Aug 24 17:41:49 2017 +0200 @@ -6,7 +6,7 @@ section \<open>Divisibility in monoids and rings\<close> theory Divisibility - imports "HOL-Library.Permutation" Coset Group + imports "HOL-Library.Permutation" Coset Group Lattice begin section \<open>Factorial Monoids\<close>

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