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>
 src/HOL/Algebra/Complete_Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/Divisibility.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions
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.6  theory Complete_Lattice
1.7 -imports Lattice
1.8 +imports Lattice Group
1.9  begin
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.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.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.6  theory Divisibility
2.7 -  imports "HOL-Library.Permutation" Coset Group
2.8 +  imports "HOL-Library.Permutation" Coset Group Lattice
2.9  begin
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.6  theory Group
3.7 -imports Complete_Lattice "HOL-Library.FuncSet"
3.8 +imports Order "HOL-Library.FuncSet"
3.9  begin
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.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