# HG changeset patch
# User ballarin
# Date 1504208881 -7200
# Node ID 2db3fe23fdaff76cfafc7d59d9a1c1eb03936f16
# Parent  6a034c6c423fa2553d57d413d8f069eee2a0e8fe
Revert 5a42eddc11c1.

diff -r 6a034c6c423f -r 2db3fe23fdaf src/HOL/Algebra/Complete_Lattice.thy
--- 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>
diff -r 6a034c6c423f -r 2db3fe23fdaf src/HOL/Algebra/Divisibility.thy
--- 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>
diff -r 6a034c6c423f -r 2db3fe23fdaf src/HOL/Algebra/Group.thy
--- 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